:: Isomorphisms of Direct Products of Finite Commutative Groups
:: by Hiroyuki Okazaki , Hiroshi Yamazaki and Yasunari Shidama
::
:: Received January 31, 2013
:: Copyright (c) 2013-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies FINSEQ_1, FUNCT_1, RELAT_1, RLVECT_2, CARD_3, TARSKI, BINOP_1,
GROUP_1, XXREAL_0, GROUP_2, CARD_1, FUNCT_4, GROUP_6, GROUP_7, FUNCOP_1,
ALGSTR_0, PARTFUN1, FUNCT_2, SUBSET_1, XBOOLE_0, STRUCT_0, NAT_1,
ORDINAL4, PRE_TOPC, ARYTM_1, ARYTM_3, FINSET_1, INT_2, ZFMISC_1, PBOOLE,
NEWTON, INT_1, NAT_3, REAL_1, PRE_POLY, XCMPLX_0, UPROOTS, INT_7;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
RELSET_1, PARTFUN1, FUNCT_2, DOMAIN_1, FUNCOP_1, FUNCT_4, FINSET_1,
CARD_1, PBOOLE, CARD_3, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1,
INT_1, INT_2, BINOP_1, FINSEQ_1, NEWTON, PRE_POLY, NAT_3, STRUCT_0,
ALGSTR_0, GROUP_1, GROUP_2, GROUP_3, GROUP_4, GROUP_6, PRALG_1, GROUP_7,
INT_7;
constructors BINOP_1, REALSET1, GROUP_6, MONOID_0, PRALG_1, GROUP_4, CARD_2,
GROUP_7, RELSET_1, WELLORD2, NAT_D, INT_7, RECDEF_1, NAT_3, FINSOP_1;
registrations XBOOLE_0, XREAL_0, STRUCT_0, GROUP_2, MONOID_0, FUNCT_2, CARD_1,
CARD_3, GROUP_7, GROUP_3, RELSET_1, FINSEQ_1, INT_1, AOFA_000, GR_CY_1,
FINSET_1, NAT_3, RELAT_1, FUNCT_1, MEMBERED, FUNCOP_1, NEWTON, VALUED_0,
PRE_POLY, PBOOLE, INT_7, GROUP_6, ORDINAL1;
requirements NUMERALS, SUBSET, ARITHM, BOOLE;
definitions TARSKI;
equalities GROUP_2, FINSEQ_1, STRUCT_0, FUNCOP_1;
expansions STRUCT_0;
theorems PRALG_1, FUNCT_1, CARD_3, FUNCT_2, XREAL_0, FUNCOP_1, TARSKI,
GROUP_1, GROUP_2, GROUP_3, EULER_1, FUNCT_4, FINSEQ_1, GROUP_4, GROUP_6,
ORDINAL1, FINSEQ_3, NAT_1, RFINSEQ, XBOOLE_0, RELAT_1, GROUP_7, FUNCT_7,
STRUCT_0, PRVECT_3, CARD_2, INT_7, XBOOLE_1, NEWTON, PRE_POLY, GROUP_10,
UPROOTS, PARTFUN1, NAT_3, INT_2, NAT_D, ZFMISC_1, GR_CY_1, CARD_1,
WELLORD2, TOPALG_4;
schemes NAT_1, FUNCT_2;
begin :: Preliminaries
theorem Th1:
for A,B,A1,B1 be set st A misses B
& A1 c= A & B1 c= B & A1 \/ B1 = A \/ B holds
A1 = A & B1 = B
proof
let A,B,A1,B1 be set;
assume A1: A misses B;
assume A2: A1 c= A & B1 c= B;
assume A3: A1 \/ B1 = A \/ B;
A4:A c= A1
proof
let x be object;
assume A5: x in A; then
A6: x in A \/ B by XBOOLE_0:def 3;
not x in B1
proof
assume x in B1; then
x in A /\ B by A5,XBOOLE_0:def 4,A2;
hence contradiction by A1, XBOOLE_0:def 7;
end;
hence x in A1 by A6,XBOOLE_0:def 3,A3;
end;
B c= B1
proof
let x be object;
assume A7: x in B; then
A8: x in A \/ B by XBOOLE_0:def 3;
not x in A1
proof
assume x in A1; then
x in A /\ B by A7,XBOOLE_0:def 4,A2;
hence contradiction by A1, XBOOLE_0:def 7;
end;
hence x in B1 by A8,XBOOLE_0:def 3,A3;
end;
hence thesis by A2,XBOOLE_0:def 10,A4;
end;
theorem Th2:
for H,K be non empty finite set holds
card product (<* H, K *>) = card(H)*card(K)
proof
let H,K be non empty finite set;
consider I be Function of [:H,K:], product <*H,K*> such that
A1: I is one-to-one onto
& for x,y be object st x in H & y in K
holds I.(x,y) = <*x,y*> by PRVECT_3:5;
A2: dom I = [:H,K:] by FUNCT_2:def 1;
rng I = product <*H,K*> by FUNCT_2:def 3,A1;
then card ([:H,K:]) = card(product <*H,K*>)
by CARD_1:5,A1,A2,WELLORD2:def 4;
hence thesis by CARD_2:46;
end;
theorem Th3:
for ps,pt,f be bag of SetPrimes,
q being Nat
st (support ps) misses (support pt) & f = ps + pt & q in (support ps) holds
ps.q = f.q
proof
let ps,pt,f be bag of SetPrimes, q be Nat;
assume A1: (support ps) misses (support pt)
& f = ps + pt & q in (support ps); then
(support ps) /\ (support pt) = {} by XBOOLE_0:def 7; then
A2: not q in (support pt) by A1,XBOOLE_0:def 4;
thus f.q =ps.q + pt.q by A1,PRE_POLY:def 5
.= ps.q + 0 by A2,PRE_POLY:def 7
.= ps.q;
end;
theorem Th4:
for ps,pt,f be bag of SetPrimes,
q being Nat
st (support ps) misses (support pt) & f = ps + pt & q in (support pt) holds
pt.q = f.q
proof
let ps,pt,f be bag of SetPrimes,
q be Nat;
assume A1: (support ps) misses (support pt)
& f = ps + pt & q in (support pt); then
(support ps) /\ (support pt) = {} by XBOOLE_0:def 7; then
A2:not q in (support ps) by A1,XBOOLE_0:def 4;
thus f.q =ps.q + pt.q by A1,PRE_POLY:def 5
.= 0 + pt.q by A2,PRE_POLY:def 7
.= pt.q;
end;
Lm1:
for ps,pt,f be bag of SetPrimes
st ps is prime-factorization-like & pt is prime-factorization-like &
f = ps + pt & (support ps) misses (support pt)
holds f is prime-factorization-like
proof
let ps,pt,f be bag of SetPrimes;
assume A1: ps is prime-factorization-like;
assume A2: pt is prime-factorization-like;
assume A3: f = ps + pt;
assume A4: (support ps) misses (support pt);
A5: support f = (support ps) \/ (support pt) by A3,PRE_POLY:38;
for x being Prime st x in
support f ex n be Nat st 0 < n & f.x = x |^n
proof
let x be Prime;
assume A6:x in support f;
per cases by A6,A5,XBOOLE_0:def 3;
suppose A7: x in support ps;
ps.x = f.x by A3,A4,A7,Th3;
hence thesis by A7,A1,INT_7:def 1;
end;
suppose A8: x in (support pt);
pt.x = f.x by A3,A4,A8,Th4;
hence thesis by A8,A2,INT_7:def 1;
end;
end;
hence thesis by INT_7:def 1;
end;
theorem Th5:
for h be non zero Nat, q being Prime
st not q,h are_coprime holds
q divides h
proof
let h be non zero Nat, q be Prime;
set pq = prime_factorization q;
set ph = prime_factorization h;
A1: q=Product pq by NAT_3:61;
A2: h=Product ph by NAT_3:61;
assume not q,h are_coprime; then
(support pq) /\ (support ph) <> {} by XBOOLE_0:def 7,INT_7:12,A1,A2;
then (support pfexp q) /\ (support ph) <> {} by NAT_3:def 9;
then (support pfexp q) /\ (support pfexp h) <> {} by NAT_3:def 9;
then {q} /\ (support pfexp h) <> {} by NAT_3:43;
then consider x be object such that
A3: x in {q} /\ (support pfexp h) by XBOOLE_0:def 1;
A4: x in {q} & x in (support pfexp h) by A3,XBOOLE_0:def 4;
x=q by A4,TARSKI:def 1;
hence q divides h by NAT_3:36,A4;
end;
theorem Th6:
for h,s be non zero Nat
st for q being Prime st q in support (prime_factorization s)
holds not q,h are_coprime holds
support (prime_factorization s) c= support (prime_factorization h)
proof
let h,s be non zero Nat;
assume A1: for q being Prime st q in
support (prime_factorization s) holds not q,h are_coprime;
let x be object;
assume A2: x in support prime_factorization s; then
reconsider q=x as Prime by NEWTON:def 6;
q divides h by Th5,A2,A1; then
q in support (pfexp h) by ORDINAL1:def 13,NAT_3:37;
hence thesis by NAT_3:def 9;
end;
theorem Th7:
for h,k,s,t be non zero Nat
st h,k are_coprime & s * t = h * k
& (for q being Prime st q in support prime_factorization s
holds not q,h are_coprime)
& (for q being Prime st q in support prime_factorization t
holds not q,k are_coprime)
holds
s = h & t = k
proof
let h,k,s,t be non zero Nat;
assume A1: h,k are_coprime;
assume A2: s * t = h * k;
assume A3: for q being Prime st q in
support (prime_factorization s) holds not q,h are_coprime;
assume A4:
for q being Prime st q in support prime_factorization t
holds not q,k are_coprime;
set ps=prime_factorization s;
set ph=prime_factorization h;
set pt=prime_factorization t;
set pk=prime_factorization k;
A5: support (ps) c= support (ph) by A3,Th6;
A6: support (pt) c= support (pk) by A4,Th6;
support pfexp h misses support pfexp k by NAT_3:44,A1; then
support (ph) misses support pfexp k by NAT_3:def 9; then
A7:support (ph) misses support (pk) by NAT_3:def 9;
set f = ps + pt;
set g = ph + pk;
A8: f is prime-factorization-like by A7,A5,A6,XBOOLE_1:64,Lm1;
A9: g is prime-factorization-like by A7,Lm1;
A10: Product g = (Product ph)*(Product pk) by A7,NAT_3:19
.= h*(Product pk) by NAT_3:61
.= h*k by NAT_3:61;
A11: Product f = (Product ps)*(Product pt)
by A5,A6,XBOOLE_1:64,A7,NAT_3:19
.= s*(Product pt) by NAT_3:61
.= s*t by NAT_3:61;
(support ps) \/ (support pt) = support (f) by PRE_POLY:38
.=support (g) by A11,INT_7:15,A8,A9,A10,A2
.= (support ph) \/ (support pk) by PRE_POLY:38;
then
A12: support ps = support ph
& support pt = support pk by A5,A6,A7,Th1;
A13: support ps = support pfexp h by A12,NAT_3:def 9;
A14: support pt = support pfexp k by A12,NAT_3:def 9;
A15:for p being Nat st p in support pfexp h
holds ps.p = p |^ (p |-count h)
proof
let p be Nat;
assume A16: p in support pfexp h; then
A17: p in support ph by NAT_3:def 9;
A18: p in support (ps) by A16,A12,NAT_3:def 9;
thus ps.p = f.p by Th3,A18,A5,A6,XBOOLE_1:64,A7
.=ph.p by Th3,A17,A7,INT_7:15,A8,A9,A10,A2,A11
.= p |^ (p |-count h) by A16,NAT_3:def 9;
end;
A19:for p being Nat st p in support pfexp k
holds pt.p = p |^ (p |-count k)
proof
let p be Nat;
assume A20: p in support pfexp k; then
A21: p in support pk by NAT_3:def 9;
A22: p in support (pt) by A12,A20,NAT_3:def 9;
thus (pt).p = f.p by Th4,A22,A5,A6,XBOOLE_1:64,A7
.=pk.p by Th4,A21,A7,A11,INT_7:15,A8,A9,A10,A2
.= p |^ (p |-count k) by A20,NAT_3:def 9;
end;
thus s = Product (ps) by NAT_3:61
.=Product (ph) by A15,A13,NAT_3:def 9
.= h by NAT_3:61;
thus t = Product (pt) by NAT_3:61
.=Product (pk) by A19,A14,NAT_3:def 9
.= k by NAT_3:61;
end;
Lm2:for G be non empty multMagma,
I be non empty finite set,
b be (the carrier of G)-valued total I -defined Function holds
b*canFS(I) is FinSequence of G & dom (b*canFS(I)) = Seg card(I)
proof
let G be non empty multMagma,
I be non empty finite set,
b be (the carrier of G)-valued total I -defined Function;
set cS = canFS(I);
set f = b*cS;
A1: rng f c= the carrier of G;
I = dom b & rng cS = I by FUNCT_2:def 3,PARTFUN1:def 2;
then A2: dom f = dom cS by RELAT_1:27;
then dom f = Seg len cS by FINSEQ_1:def 3;
then f is FinSequence by FINSEQ_1:def 2;
then reconsider f as FinSequence of G by A1,FINSEQ_1:def 4;
len canFS I = card I by FINSEQ_1:93;
then dom f = Seg card(I) by A2,FINSEQ_1:def 3;
hence thesis;
end;
Lm3:
for A,B being non empty finite set st A misses B holds
canFS(A)^ canFS(B) is one-to-one onto FinSequence of (A \/ B) &
dom (canFS(A)^ canFS(B)) = Seg (card(A \/ B))
proof
let A,B be non empty finite set;
assume A1: A misses B;
A2: rng canFS(A) = A by FUNCT_2:def 3;
A3: rng canFS(B) = B by FUNCT_2:def 3; then
A4: rng(canFS(A)^ canFS(B)) = A \/ B by FINSEQ_1:31,A2; then
reconsider f = canFS(A)^ canFS(B) as FinSequence of (A \/ B)
by FINSEQ_1:def 4;
dom f = Seg (len canFS(A) + len canFS(B)) by FINSEQ_1:def 7
.= Seg (card(A) + len canFS(B)) by FINSEQ_1:93
.= Seg (card(A) + card(B)) by FINSEQ_1:93
.= Seg (card(A \/ B)) by A1,CARD_2:40;
hence thesis by A2,FINSEQ_3:91,A1,A3,A4,FUNCT_2:def 3;
end;
Lm4:
for A,B being non empty finite set,
FA be total A -defined Function,
FB be total B -defined Function,
f,g be FinSequence,
FAB be (A \/ B) -defined Function
st A misses B & FAB = FA +* FB & f =FA*canFS(A) & g =FB*canFS(B) holds
f ^ g = FAB* (canFS(A) ^ canFS(B))
proof
let A,B be non empty finite set,
FA be total A -defined Function,
FB be total B -defined Function,
f,g be FinSequence,
FAB be (A \/ B) -defined Function;
assume A1: A misses B;
assume A2: FAB = FA +* FB;
assume A3: f =FA*canFS(A);
assume A4: g = FB*canFS(B);
reconsider csAB = canFS(A)^ canFS(B) as one-to-one onto
FinSequence of (A \/ B) by Lm3,A1;
set fAB= FAB* (canFS(A) ^ canFS(B));
set cSA = canFS(A);
set cSB = canFS(B);
A5: A = dom FA & rng cSA = A by FUNCT_2:def 3,PARTFUN1:def 2; then
A6: dom f = dom (cSA) by A3,RELAT_1:27; then
A7: dom f = Seg len cSA by FINSEQ_1:def 3;
A8: B = dom FB & rng cSB = B by FUNCT_2:def 3,PARTFUN1:def 2; then
dom g = dom (cSB) by A4,RELAT_1:27; then
A9: dom g = Seg len cSB by FINSEQ_1:def 3;
A10: A \/ B = dom FAB by A2,FUNCT_4:def 1,A5,A8;
rng csAB = A \/ B by FUNCT_2:def 3; then
A11: dom fAB = dom csAB by RELAT_1:27,A10; then
dom fAB = Seg len csAB by FINSEQ_1:def 3;
then reconsider fAB as FinSequence by FINSEQ_1:def 2;
A12: dom fAB = Seg card(A \/ B) by A11,Lm3,A1
.=Seg (card(A) + card(B)) by A1,CARD_2:40
.=Seg (len cSA + card(B)) by FINSEQ_1:93
.=Seg (len cSA + len cSB) by FINSEQ_1:93
.=Seg (len f + len cSB) by A7,FINSEQ_1:def 3
.=Seg (len f + len g) by A9,FINSEQ_1:def 3;
A13: for k be Nat st k in dom f holds fAB.k=f.k
proof
let k be Nat;
assume A14:k in dom f;
then k in dom csAB by A6,FINSEQ_1:26,TARSKI:def 3; then
A15: fAB.k=FAB.(csAB.k) by FUNCT_1:13;
A16: csAB.k = cSA.k by A14,A6,FINSEQ_1:def 7;
not csAB.k in dom FB
proof
assume A17: csAB.k in dom FB;
cSA.k in rng cSA by A14,A6,FUNCT_1:3;
then
csAB.k in A /\ B by A16,A17,XBOOLE_0:def 4;
hence contradiction by A1,XBOOLE_0:def 7;
end; then
FAB.(csAB.k) = FA.(csAB.k) by A2,FUNCT_4:11;
hence fAB.k = FA.(cSA.k) by A15,A14,A6,FINSEQ_1:def 7
.=f.k by A3,A14,A6, FUNCT_1:13;
end;
for k be Nat st k in dom g holds fAB.(len f + k) = g.k
proof
let k be Nat;
assume A18: k in dom g;
A19: len cSA = len f by A7,FINSEQ_1:def 3;
A20: k in dom cSB by A4,RELAT_1:27,A8,A18;
then (len f + k) in dom csAB by A19,FINSEQ_1:28; then
A21: fAB.(len f + k)=FAB.(csAB.(len f + k)) by FUNCT_1:13;
csAB.(len f + k) = cSB.k by A20,A19,FINSEQ_1:def 7;
hence fAB.(len f + k) = FB.(cSB.k)
by A21,A20,FUNCT_1:3,FUNCT_4:13,A2,A8
.=g.k by A4,A20,FUNCT_1:13;
end;
hence thesis by FINSEQ_1:def 7,A12,A13;
end;
definition
let G be non empty multMagma,
I be finite set,
b be (the carrier of G)-valued total I -defined Function;
func Product b -> Element of G means :Def1:
ex f being FinSequence of G st it = Product f & f = b*canFS(I);
existence
proof
set cS = canFS(I);
set f = b*cS;
A1: rng f c= the carrier of G;
I = dom b & rng cS = I by FUNCT_2:def 3,PARTFUN1:def 2; then
dom f = dom cS by RELAT_1:27;
then dom f = Seg len cS by FINSEQ_1:def 3;
then f is FinSequence by FINSEQ_1:def 2;
then reconsider f as FinSequence of G by A1,FINSEQ_1:def 4;
take Product f;
thus thesis;
end;
uniqueness;
end;
theorem Th8:
for G being commutative Group,
A,B being non empty finite set,
FA be (the carrier of G)-valued total A -defined Function,
FB be (the carrier of G)-valued total B -defined Function,
FAB be (the carrier of G)-valued total A \/ B -defined Function
st A misses B & FAB = FA +* FB holds
Product (FAB) = (Product FA) * (Product FB)
proof
let G be commutative Group,
A,B be non empty finite set,
FA be (the carrier of G)-valued total A -defined Function,
FB be (the carrier of G)-valued total B -defined Function,
FAB be (the carrier of G)-valued total A \/ B -defined Function;
assume A1: A misses B;
assume A2: FAB = FA +* FB;
consider fA being FinSequence of G such that
A3:Product (FA) = Product fA & fA = FA*canFS(A) by Def1;
consider fB being FinSequence of G such that
A4:Product (FB) = Product fB & fB = FB*canFS(B) by Def1;
set fAB = FAB*canFS(A \/ B);
set cAB = canFS(A)^canFS(B);
set uAB = canFS(A \/ B);
reconsider SGAB = Seg (card(A \/ B)) as non empty finite set;
A5: cAB is one-to-one onto FinSequence of (A \/ B) &
dom (cAB) = SGAB by Lm3,A1;
reconsider cAB as one-to-one onto FinSequence of (A \/ B) by Lm3,A1;
rng (cAB) c= (A \/ B);
then
reconsider JcAB = (cAB) as Function of SGAB, (A \/ B) by FUNCT_2:2,A5;
A6: dom uAB = Seg (len uAB) by FINSEQ_1:def 3
.=SGAB by FINSEQ_1:93;
rng (uAB) c= (A \/ B); then
reconsider KuAB = uAB as Function of SGAB, (A \/ B) by FUNCT_2:2,A6;
reconsider IuAB = (uAB)" as Function of (A \/ B), SGAB by FINSEQ_1:95;
A7:rng uAB = (A \/ B) by FUNCT_2:def 3;
then
IuAB*KuAB = id SGAB & KuAB*IuAB = id (A \/ B) by FUNCT_2:29;
then
A8: IuAB is one-to-one & IuAB is onto by FUNCT_2:23;
set p=IuAB*JcAB;
p is onto & p is one-to-one by A8,FUNCT_2:27; then
reconsider p as Permutation of SGAB;
reconsider fAB as FinSequence of G by Lm2;
A9: (canFS(A \/ B))*p = (KuAB * IuAB)*JcAB by RELAT_1:36
.= id (A \/ B) * JcAB by A7,FUNCT_2:29
.= canFS(A)^canFS(B) by FUNCT_2:17;
A10: SGAB = dom fAB by Lm2;
A11: fA ^ fB = FAB*(canFS(A) ^ canFS(B)) by A3,A4,Lm4,A1,A2
.= fAB*p by RELAT_1:36,A9;
thus Product (FAB) = Product (fAB) by Def1
.= Product(fA ^ fB) by A10,A11,UPROOTS:16
.= Product (FA)*Product (FB) by A3,A4,GROUP_4:5;
end;
theorem Th9:
for G being non empty multMagma,
q be set,
z be Element of G,
f be (the carrier of G)-valued total {q}-defined Function
st f = q .--> z
holds Product f = z
proof
let G be non empty multMagma,
q be set,
z be Element of G,
f be (the carrier of G)-valued total {q}-defined Function;
assume A1: f = q .--> z;
set zz = <*z*>;
rng zz = {z} by FINSEQ_1:38; then
reconsider zz as FinSequence of G by FINSEQ_1:def 4;
A2: f* canFS({q}) is FinSequence of G
& dom (f*canFS({q})) = Seg card({q}) by Lm2;
reconsider g= f* canFS({q}) as FinSequence of G by Lm2;
A3: card {q} = 1 by CARD_1:30;
then dom (g) = Seg 1 by Lm2;
then
A4: len g = 1 by FINSEQ_1:def 3;
A5:canFS({q}) = <*q*> by FINSEQ_1:94;
A6: q in {q} by TARSKI:def 1;
A7: 1 in dom g by A2,A3;
g.1 = f.((canFS({q})).1) by FUNCT_1:12,A7
.=f.q by A5
.=z by A1,FUNCOP_1:7,A6; then
<*z*> = f* canFS({q}) by A4,FINSEQ_1:40;
hence Product f = Product zz by Def1
.= z by GROUP_4:9;
end;
begin :: Direct Product of Finite Commutative Groups
theorem Th10:
for X,Y being non empty multMagma holds
the carrier of product <*X,Y*>
= product <* the carrier of X,the carrier of Y *>
proof
let X,Y be non empty multMagma;
set CarrX = the carrier of X;
set CarrY = the carrier of Y;
A1: the carrier of product (<*X,Y*>) = product
Carrier (<*X,Y*>) by GROUP_7:def 2;
len <*CarrX,CarrY*> = 2 by FINSEQ_1:44; then
A2: dom <*CarrX,CarrY*> = {1,2} by FINSEQ_1:2,def 3;
for a be object st a in dom (Carrier (<*X,Y*>))
holds (Carrier (<*X,Y*>)).a =
(<* the carrier of X,the carrier of Y *>).a
proof
let a be object;
assume
A4: a in dom (Carrier (<*X,Y*>));
per cases by A4,TARSKI:def 2;
suppose
A5: a = 1;
then ex R being 1-sorted st R = (<*X,Y*>).1
& (Carrier (<*X,Y*>)).1 = the carrier of R
by A4,PRALG_1:def 15;
hence thesis by A5;
end;
suppose
A6: a = 2;
then ex R being 1-sorted st R = (<*X,Y*>).2
& (Carrier (<*X,Y*>)).2 = the carrier of R by A4,PRALG_1:def 15;
hence thesis by A6;
end;
end;
hence thesis by PARTFUN1:def 2,A2,FUNCT_1:2,A1;
end;
theorem Th11:
for G being Group, A,B being normal Subgroup of G st
(the carrier of A) /\ (the carrier of B) = {1_G} holds
for a,b be Element of G st a in A & b in B holds a*b = b*a
proof
let G be Group, A,B be normal Subgroup of G;
assume A1: (the carrier of A) /\ (the carrier of B) = {1_G};
let a,b be Element of G;
assume A2: a in A & b in B;
A3: a*b*(b*a)" = a*b*(a"*b") by GROUP_1:17
.=(a*b*a") * b" by GROUP_1:def 3;
A4: b" in B by A2,GROUP_2:51;
a*b in a*B by GROUP_2:27,A2;
then a*b in B*a by GROUP_3:117;
then consider s be Element of G
such that A5: a*b = s*a & s in the carrier of B by GROUP_2:28;
a*b*a" in B by GROUP_3:1,A5;
then
A6: a*b*(b*a)" in the carrier of B by STRUCT_0:def 5,A3,A4,GROUP_2:50;
A7: a*b*(b*a)" = a*b*(a"*b") by GROUP_1:17
.=a*(b*(a"* b")) by GROUP_1:def 3
.=a*(b*a"* b") by GROUP_1:def 3;
a" in A by A2,GROUP_2:51;
then
b*a" in b*A by GROUP_2:27;
then b*a" in A*b by GROUP_3:117;
then consider t be Element of G
such that A8: b*a" = t*b & t in the carrier of A by GROUP_2:28;
b*a"* b" in A by GROUP_3:1,A8;
then a*b*(b*a)" in the carrier of A by STRUCT_0:def 5,A7,A2,GROUP_2:50;
then a*b*(b*a)" in (the carrier of A) /\ (the carrier of B)
by XBOOLE_0:def 4,A6;
then a*b*(b*a)" = 1_G by A1,TARSKI:def 1;
then 1_G * (b*a) = a*b by GROUP_1:14;
hence thesis by GROUP_1:def 4;
end;
theorem Th12:
for G being Group, A,B being normal Subgroup of G st
(for x be Element of G holds
ex a,b be Element of G st a in A & b in B & x = a*b)
& (the carrier of A) /\ (the carrier of B) = {1_G} holds
ex h being Homomorphism of product <*A,B*>,G st h is bijective
& for a,b be Element of G st a in A & b in B
holds h.(<*a,b*>) = a*b
proof
let G be Group, A,B be normal Subgroup of G;
assume A1: for x be Element of G holds
ex a,b be Element of G st a in A & b in B & x = a*b;
assume A2: (the carrier of A) /\ (the carrier of B) = {1_G};
defpred P[set,set] means ex x be Element of G, y be Element of G
st x in A & y in B & $1 =<*x,y*> & $2=x*y;
A3:for z be Element of product <*A,B*>
ex w be Element of G st P[z,w]
proof
let z be Element of product <*A,B*>;
consider x be Element of A, y be Element of B such that
A4: z = <*x,y*> by TOPALG_4:1;
reconsider x1 = x, y1 = y as Element of G by GROUP_2:41,STRUCT_0:def 5;
A5: x1*y1 is Element of G;
x1 in A & y1 in B;
hence thesis by A4,A5;
end;
consider h be Function of product <*A,B*>, G such that
A6: for z be Element of product <*A,B*>
holds P[z,h.z] from FUNCT_2:sch 3(A3);
A7: for a,b be Element of G
st a in A & b in B holds h. <*a,b*> = a*b
proof
let a,b be Element of G;
assume A8: a in A & b in B;
then
reconsider a1= a as Element of A;
reconsider b1= b as Element of B by A8;
consider x be Element of G, y be Element of G such that
A9: x in A & y in B
& <*a1,b1*> =<*x,y*> & h.(<*a1,b1*>)=x*y by A6;
A10: a1= (<*a1,b1*>).1
.= x by FINSEQ_1:44,A9;
b1= (<*a1,b1*>).2
.= y by FINSEQ_1:44,A9;
hence thesis by A9,A10;
end;
now let z1,z2 be object;
assume A11: z1 in the carrier of product <*A,B*>
& z2 in the carrier of product <*A,B*>
& h.z1=h.z2; then
consider x1 be Element of G,
y1 be Element of G such that A12: x1 in A & y1 in B
& z1 =<*x1,y1*> & h.z1=x1*y1 by A6;
consider x2 be Element of G,
y2 be Element of G such that A13: x2 in A & y2 in B
& z2 =<*x2,y2*> & h.z2=x2*y2 by A6,A11;
x1 = x2*y2*y1" by GROUP_1:14,A13,A11,A12;
then
x1 = x2*(y2*y1") by GROUP_1:def 3;
then
A14: x2"*x1 = y2*y1" by GROUP_1:13;
x2" in A by A13,GROUP_2:51;
then
A15: x2"*x1 in the carrier of A by GROUP_2:50,A12,STRUCT_0:def 5;
y1" in B by A12,GROUP_2:51;
then y2*y1" in the carrier of B by A13,GROUP_2:50,STRUCT_0:def 5;
then
A16: x2"*x1 in (the carrier of A) /\ (the carrier of B)
by A14,A15,XBOOLE_0:def 4;
then x2"*x1 = 1_G by A2,TARSKI:def 1;
then x1 = x2 * 1_G by GROUP_1:13;
then
A17:x1 = x2 by GROUP_1:def 4;
y2*y1" = 1_G by A2,TARSKI:def 1,A14,A16;
then y2 = 1_G * y1 by GROUP_1:14;
hence z1=z2 by A12,A13,A17,GROUP_1:def 4;
end; then
A18:h is one-to-one by FUNCT_2:19;
now let w be object;
assume w in the carrier of G; then
reconsider g = w as Element of G;
consider a,b be Element of G such that
A19: a in A & b in B & g = a*b by A1;
reconsider a1=a as Element of A by A19;
reconsider b1=b as Element of B by A19;
h.(<*a1,b1*>)=a*b by A7,A19;
hence w in rng h by A19,FUNCT_2:112;
end; then
the carrier of G c= rng h by TARSKI:def 3; then
A20: h is onto by FUNCT_2:def 3,XBOOLE_0:def 10;
for z, w being Element of product <*A,B*>
holds h . (z * w) = (h . z) * (h . w)
proof
let z,w be Element of product <*A,B*>;
consider x be Element of A, y be Element of B such that
A21: z = <*x,y*> by TOPALG_4:1;
reconsider x1 = x, y1 = y as Element of G by GROUP_2:41,STRUCT_0:def 5;
consider a be Element of A, b be Element of B such that
A22: w = <*a,b*> by TOPALG_4:1;
reconsider a1 = a, b1 = b as Element of G by GROUP_2:41,STRUCT_0:def 5;
A23: y*b = y1*b1 by GROUP_2:43;
A24: z*w = <* x*a, y*b *> by A21,A22,GROUP_7:29
.= <* x1*a1, y1*b1 *> by GROUP_2:43,A23;
A25: x1 in A & a1 in A;
then
A26: x1*a1 in A by GROUP_2:50;
A27: y1 in B & b1 in B;
then
A28: y1*b1 in B by GROUP_2:50;
A29:
h.(z*w) = (x1*a1)*(y1*b1) by A7, A24,A26,A28
.= x1*(a1*(y1*b1)) by GROUP_1:def 3
.= x1*((a1*y1)*b1) by GROUP_1:def 3
.= x1*((y1*a1)*b1) by Th11,A2,A25,A27
.= x1*(y1*(a1*b1)) by GROUP_1:def 3
.= (x1*y1)*(a1*b1) by GROUP_1:def 3;
h.z = x1*y1 by A21,A7,A25,A27;
hence h.(z*w) = h.z *h.w by A29,A22,A7,A25,A27;
end;
then h is Homomorphism of product <*A,B*>,G by GROUP_6:def 6;
hence thesis by A7,A20,A18;
end;
theorem Th13:
for G being finite commutative Group,
m be Nat,
A be Subset of G
st A ={x where x is Element of G: x|^m = 1_G}
holds
A <> {}
&
(for g1,g2 be Element of G
st g1 in A & g2 in A holds g1 * g2 in A) &
for g be Element of G st g in A holds g" in A
proof
let G be finite commutative Group,
m be Nat,
A be Subset of G;
assume A1: A ={x where x is Element of G: x|^m = 1_G};
(1_G) |^m = 1_G by GROUP_1:31;
then
A2:1_G in A by A1;
A3: for g1,g2 be Element of G
st g1 in A & g2 in A holds g1 * g2 in A
proof
let g1,g2 be Element of G;
assume A4: g1 in A & g2 in A;
then
A5: ex x1 be Element of G st g1=x1 & x1|^m = 1_G by A1;
A6: ex x2 be Element of G st g2=x2 & x2|^m = 1_G by A1,A4;
(g1 * g2) |^m = g1 |^m * g2 |^m by GROUP_1:38
.= 1_G by GROUP_1:def 4,A5,A6;
hence g1 * g2 in A by A1;
end;
for g be Element of G st g in A holds g" in A
proof
let g be Element of G;
assume g in A;
then
A7: ex x be Element of G st g=x & x|^m = 1_G by A1;
g" |^ m = (g |^ m)" by GROUP_1:37
.= 1_G by GROUP_1:8,A7;
hence g" in A by A1;
end;
hence thesis by A2,A3;
end;
theorem Th14:
for G being finite commutative Group,
m be Nat,
A be Subset of G
st A ={x where x is Element of G: x|^m = 1_G} holds
ex H being strict finite Subgroup of G
st the carrier of H = A & H is commutative normal
proof
let G be finite commutative Group,
m be Nat,
A be Subset of G;
assume A ={x where x is Element of G: x|^m = 1_G};
then
A <> {} & (for g1,g2 be Element of G
st g1 in A & g2 in A holds g1 * g2 in A) &
for g be Element of G st g in A holds g" in A by Th13; then
consider H being strict Subgroup of G such that
A1: the carrier of H = A by GROUP_2:52;
H is normal by GROUP_3:116;
hence thesis by A1;
end;
Lm5:
for G being finite Group,
q being Prime st q in support (prime_factorization card G)
ex a be Element of G st a <> 1_G & ord a = q
proof
let G be finite Group,
q be Prime;
assume q in support (prime_factorization card G);
then
q in support (pfexp card G) by NAT_3:def 9;
then
consider g being Element of G such that
A1: ord g = q by GROUP_10:11,NAT_3:36;
A2: 1 < q by INT_2:def 4;
take g;
thus thesis by A1,A2,GROUP_1:42;
end;
theorem Th15:
for G being finite commutative Group,
m be Nat,
H being finite Subgroup of G
st the carrier of H = {x where x is Element of G: x|^m = 1_G} holds
for q being Prime st q in support prime_factorization card H
holds not q,m are_coprime
proof
let G be finite commutative Group,
m be Nat,
H be finite Subgroup of G;
assume A1: the carrier of H = {x where x is Element of G: x|^m = 1_G};
let q be Prime;
assume A2: q in support prime_factorization card H;
assume A3: q,m are_coprime;
consider a be Element of H such that
A4: a <> 1_H & ord a = q by A2,Lm5;
a in {x where x is Element of G: x|^m = 1_G} by A1; then
consider x be Element of G such that
A5: x=a & x|^m = 1_G;
A6:a|^m =1_G by A5,GROUP_4:2;
q gcd m = 1 by A3,INT_2:def 3;
then
consider x,y be Integer such that
A7: x*q + y*m = 1 by NAT_D:68;
a = a|^1 by GROUP_1:26
.=(a|^(q*x)) * (a|^(m*y)) by GROUP_1:33,A7
.= ((a|^q) |^x) *(a|^(m*y)) by GROUP_1:35
.= ((a|^q) |^x) * ((a|^m) |^y) by GROUP_1:35
.= ((1_H) |^ x) * ((a|^m) |^y) by A4, GROUP_1:41
.= ((1_H) |^ x) * ((1_H) |^y) by A6,GROUP_2:44
.= 1_H * ((1_H) |^y) by GROUP_1:31
.= 1_H * 1_H by GROUP_1:31
.= 1_H by GROUP_1:def 4
.= 1_G by GROUP_2:44;
hence contradiction by GROUP_2:44,A4;
end;
theorem Th16:
for G being finite commutative Group,
h,k be Nat
st card G = h*k & h,k are_coprime holds
ex H,K being strict finite Subgroup of G st
the carrier of H = {x where x is Element of G: x|^h = 1_G} &
the carrier of K = {x where x is Element of G: x|^k = 1_G} &
H is normal & K is normal
&
(for x be Element of G holds
ex a,b be Element of G st a in H & b in K & x = a*b)
&
(the carrier of H) /\ (the carrier of K) = {1_G}
proof
let G be finite commutative Group,
h,k be Nat;
assume A1:card G = h*k & h,k are_coprime;
set A = {x where x is Element of G: x|^h = 1_G};
set B = {x where x is Element of G: x|^k = 1_G};
A c= the carrier of G
proof
let y be object;
assume y in A; then
ex x be Element of G st y=x & x|^h = 1_G;
hence y in the carrier of G;
end; then
reconsider A as Subset of G;
B c= the carrier of G
proof
let y be object;
assume y in B; then
ex x be Element of G st y=x & x|^k = 1_G;
hence y in the carrier of G;
end; then
reconsider B as Subset of G;
consider H being strict finite Subgroup of G such that A2:
the carrier of H = A & H is commutative
& H is normal by Th14;
consider K being strict finite Subgroup of G
such that A3:
the carrier of K = B & K is commutative & K is normal by Th14;
(1_G) |^ h = 1_G by GROUP_1:31;
then
A4: 1_G in the carrier of H by A2;
(1_G) |^ k = 1_G by GROUP_1:31;
then
1_G in the carrier of K by A3;
then
1_G in (the carrier of H) /\ (the carrier of K)
by A4,XBOOLE_0:def 4;
then
A5: {1_G} c= (the carrier of H) /\ (the carrier of K)
by ZFMISC_1:31;
h gcd k = 1 by A1,INT_2:def 3;
then
consider a,b be Integer such that
A6: a*h + b*k = 1 by NAT_D:68;
(the carrier of H) /\ (the carrier of K) c= {1_G}
proof
let z be object;
assume A7: z in (the carrier of H) /\ (the carrier of K);
then
z in the carrier of H by XBOOLE_0:def 4;
then
z in G by STRUCT_0:def 5,GROUP_2:40;
then
reconsider w=z as Element of G;
A8: w in A & w in B by A2,A3,A7,XBOOLE_0:def 4;
then
A9: ex x be Element of G st w=x & x|^h = 1_G;
A10: ex x be Element of G st w=x & x|^k = 1_G by A8;
w = w|^1 by GROUP_1:26
.= (w|^(a*h)) * (w|^(b*k)) by GROUP_1:33,A6
.= ((w|^h) |^a) *(w|^(b*k)) by GROUP_1:35
.= ((w|^h) |^a) * ((w|^k) |^b) by GROUP_1:35
.= 1_G * ((1_G) |^b) by GROUP_1:31,A10,A9
.= 1_G * 1_G by GROUP_1:31
.= 1_G by GROUP_1:def 4;
hence z in {1_G} by TARSKI:def 1;
end;
then
A11: (the carrier of H) /\ (the carrier of K) c= {1_G};
A12: for x be Element of G holds
ex s,t be Element of G
st s in H & t in K & x = s*t
proof
let x be Element of G;
A13: x = x|^1 by GROUP_1:26
.=(x|^(b*k)) * (x|^(a*h)) by GROUP_1:33,A6;
set t = x|^(a*h);
set s = x|^(b*k);
s |^h = x|^(b*k*h) by GROUP_1:35
.= x|^((k*h)*b)
.=(x|^(k*h)) |^ b by GROUP_1:35
.= (1_G) |^ b by A1,GR_CY_1:9
.= 1_G by GROUP_1:31;
then
A14: s in H by A2;
t |^k = x|^(a*h*k) by GROUP_1:35
.= x|^((h*k)*a)
.=(x|^(h*k)) |^ a by GROUP_1:35
.= (1_G) |^ a by A1,GR_CY_1:9
.= 1_G by GROUP_1:31;
then t in K by A3;
hence thesis by A13,A14;
end;
take H,K;
thus thesis by A2,A3,A11,A12,A5,XBOOLE_0:def 10;
end;
theorem Th17:
for H,K be finite Group holds
card product (<* H, K *>) = card(H)*card(K)
proof
let H,K be finite Group;
card (product (<* the carrier of H,the carrier of K *>))
= card(the carrier of product (<* H, K *>)) by Th10;
hence thesis by Th2;
end;
theorem Th18:
for G being finite commutative Group,
h,k be non zero Nat
st card G = h*k & h,k are_coprime
ex H,K being strict finite Subgroup of G st
card H = h & card K = k &
(the carrier of H) /\ (the carrier of K) = {1_G} &
ex F being Homomorphism of product <*H,K*>,G
st F is bijective
& for a,b be Element of G st a in H & b in K
holds F.(<*a,b*>) = a*b
proof
let G be finite commutative Group,
h,k be non zero Nat;
assume A1: card G = h*k & h,k are_coprime;
then
consider H,K being strict finite Subgroup of G such that
A2:
the carrier of H = {x where x is Element of G: x|^h = 1_G} &
the carrier of K = {x where x is Element of G: x|^k = 1_G} &
H is normal & K is normal &
(for x be Element of G holds
ex a,b be Element of G st a in H & b in K & x = a*b) &
(the carrier of H) /\ (the carrier of K) = {1_G} by Th16;
take H,K;
consider F being Homomorphism of product <*H,K*>,G such that
A3: F is bijective & for a,b be Element of G st a in H & b in K
holds F.(<*a,b*>) = a*b by A2,Th12;
set s = card H;
set t = card K;
F is one-to-one & dom F = the carrier of product <*H,K*>
& rng F = the carrier of G by A3,FUNCT_2:def 1,FUNCT_2:def 3; then
card (product <*H,K*>) = card G by CARD_1:5,WELLORD2:def 4; then
A4: s * t = h * k by A1,Th17;
A5:for q being Prime st q in support (prime_factorization s)
holds not q,h are_coprime by A2,Th15;
for q being Prime st q in support (prime_factorization t)
holds not q,k are_coprime by A2,Th15;
hence thesis by A2,A3,A4,Th7,A5,A1;
end;
begin :: Finite Direct Products of Finite Commutative Groups
theorem Th19:
for G be Group,
q be set,
F be associative Group-like multMagma-Family of {q},
f being Function of G,product F st F = q .--> G &
for x being Element of G holds f . x = q .--> x holds
f is Homomorphism of G,(product F)
proof
let G be Group,
q be set,
F be associative Group-like multMagma-Family of {q},
f be Function of G, product F;
assume A1:F = q .--> G;
assume A2:for x being Element of G holds f . x = q .--> x;
A3: the carrier of product F = product (Carrier F) by GROUP_7:def 2;
now
let a, b be Element of G;
A4: (f . a) = q .--> a by A2;
A5: (f . b) = q .--> b by A2;
reconsider fa=f.a, fb=f.b as Element of product F;
set ga = q .--> a;
set gb = q .--> b;
consider gab be Function such that
A6: fa*fb = gab & dom gab = dom (Carrier F) &
for y be object st y in dom (Carrier F)
holds gab.y in (Carrier F).y by CARD_3:def 5,A3;
A7: for z being object st z in dom gab holds gab . z = a*b
proof
let z be object;
assume A8:z in dom gab;
A9: G = F.z by A1,FUNCOP_1:7,A8,A6;
A10: ga.z = a by FUNCOP_1:7,A8,A6;
gb.z = b by FUNCOP_1:7,A8,A6;
hence gab . z = a*b by A4,A5,A6,A8,A9,A10,GROUP_7:1;
end;
gab = (dom gab) --> a*b by A7,FUNCOP_1:11
.= q .--> (a*b) by A6,PARTFUN1:def 2
.= f . (a * b) by A2;
hence f . (a * b) = (f . a) * (f . b) by A6;
end;
hence thesis by GROUP_6:def 6;
end;
theorem Th20:
for G be Group,
q be set,
F be associative Group-like multMagma-Family of {q},
f being Function of G,product F st F = q .--> G &
for x being Element of G holds f . x = q .--> x holds
f is bijective
proof
let G be Group,
q be set,
F be associative Group-like multMagma-Family of {q},
f be Function of G,product F;
assume A1:F = q .--> G;
assume A2: for x being Element of G holds f . x = q .--> x;
A3: q in {q} by TARSKI:def 1;
A4: the carrier of product F = product (Carrier F) by GROUP_7:def 2;
ex R being 1-sorted st
R = F . q & (Carrier F) . q = the carrier of R by PRALG_1:def 15,A3;
then
A5: (Carrier F) . q = the carrier of G by A1,FUNCOP_1:7,A3;
A6: dom (Carrier F) = {q} by PARTFUN1:def 2;
for x1,x2 be object st x1 in the carrier of G
& x2 in the carrier of G & f.x1 = f.x2 holds x1 = x2
proof
let z1,z2 be object;
assume A7: z1 in the carrier of G
& z2 in the carrier of G & f.z1 = f.z2;
then
reconsider x1=z1,x2=z2 as Element of G;
A8: f . x2 = q .--> x2 by A2;
thus z1 = (q .--> x1) .q by FUNCOP_1:7,A3
.=(q .--> x2) .q by A8,A2,A7
.=z2 by FUNCOP_1:7,A3;
end; then
A9: f is one-to-one by FUNCT_2:19;
for y be object st y in the carrier of product F
ex x be object st x in the carrier of G & y = f.x
proof
let y be object;
assume y in the carrier of product F; then
consider g be Function such that
A10: y = g & dom g = dom (Carrier F)
& for z be object st z in dom (Carrier F)
holds g.z in (Carrier F).z by CARD_3:def 5,A4;
reconsider x = g.q as Element of G by A5,A10,A3,A6;
A11: for z being object st z in dom g holds
g . z = x by TARSKI:def 1,A10;
take x;
thus x in the carrier of G;
thus y = (dom g) --> x by A11,FUNCOP_1:11,A10
.= q .--> x by A10,PARTFUN1:def 2
.= f . x by A2;
end;
then rng f = the carrier of product F by FUNCT_2:10;
then f is onto by FUNCT_2:def 3;
hence thesis by A9;
end;
theorem Th21:
for q be set,
F be associative Group-like multMagma-Family of {q},
G be Group st F = q .--> G holds
ex I be Homomorphism of G,product F st
I is bijective &
for x being Element of G holds I . x = q .--> x
proof
let q be set,
F be associative Group-like multMagma-Family of {q},
G be Group;
assume A1: F = q .--> G;
A2: q in {q} by TARSKI:def 1;
A3: the carrier of product F = product (Carrier F) by GROUP_7:def 2;
ex R being 1-sorted st
R = F . q & (Carrier F) . q = the carrier of R by PRALG_1:def 15,A2;
then
A4: (Carrier F) . q = the carrier of G by A1,FUNCOP_1:7,A2;
A5: dom (Carrier F) = {q} by PARTFUN1:def 2;
defpred P[set, set] means $2= (q .--> $1);
A6:for z be Element of G ex w be Element of product F st P[z,w]
proof
let z be Element of G;
set w = q .--> z;
now let i be object;
assume A8:i in dom w; then
A9: i = q by TARSKI:def 1;
w.i = z by FUNCOP_1:7,A8;
hence w.i in (Carrier F) . i by A4,A9;
end; then
w in product Carrier F by A5,CARD_3:9;
hence ex w be Element of product F st P[z,w] by A3;
end;
consider I being Function of G, product F such that
A10: for x being Element of G holds P[x,I.x] from FUNCT_2:sch 3(A6);
reconsider I as Homomorphism of G, product F by Th19,A1,A10;
I is bijective by Th20,A1,A10;
hence thesis by A10;
end;
theorem Th22:
for I0,I be non empty finite set,
F0 be associative Group-like multMagma-Family of I0,
F be associative Group-like multMagma-Family of I,
H,K be Group,
q be Element of I,
k be Element of K,
g be Function st
g in the carrier of product F0 &
not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) holds
g +* (q .--> k) in the carrier of product F
proof
let I0,I be non empty finite set,
F0 be associative Group-like multMagma-Family of I0,
F be associative Group-like multMagma-Family of I,
H,K be Group,
q be Element of I,
k be Element of K,
g be Function;
assume A1: g in the carrier of product F0 & not q in I0 & I = I0 \/ {q} &
F = F0 +* (q .--> K);
set HK = <*H,K*>;
A2: dom Carrier F0 = I0 by PARTFUN1:def 2;
A3: dom (q .--> k) = {q};
A4: dom (q .--> K) = {q};
A5: dom F0 = I0 by PARTFUN1:def 2;
set w = g +* (q .--> k);
A6:g in product (Carrier F0) by A1,GROUP_7:def 2;
then A7:
ex g0 be Function st g = g0 & dom g0 = dom (Carrier F0) &
for y be object st y in dom (Carrier F0) holds g0.y in (Carrier F0).y
by CARD_3:def 5;
dom w = (dom g) \/ (dom (q .--> k)) by FUNCT_4:def 1
.= I0 \/ (dom (q .--> k)) by PARTFUN1:def 2,A6
.= I by A1;
then
A8: dom w = dom (Carrier F) by PARTFUN1:def 2;
for x be object st x in dom (Carrier F)
holds w.x in (Carrier F).x
proof
let x be object;
assume A9: x in dom (Carrier F);
per cases by A1,XBOOLE_0:def 3,A9;
suppose A10: x in I0;
A11: not x in {q} by A1,A10,TARSKI:def 1;
then
A12: F.x = F0.x by A1,FUNCT_4:def 1,A5,A4,A9;
consider R1 being 1-sorted such that
A13: R1 = F0.x & (Carrier F0).x = the carrier of R1
by PRALG_1:def 15,A10;
consider R2 being 1-sorted such that
A14: R2 = F.x
& (Carrier F).x = the carrier of R2 by PRALG_1:def 15,A9;
w.x = g.x by FUNCT_4:def 1,A7,A2,A3,A9,A1,A11;
hence w.x in (Carrier F).x by A13,A14,A12,A10,A2,A7;
end;
suppose A15: x in {q}; then
F.x = (q .--> K).x by A1,FUNCT_4:def 1,A5,A4; then
A16: F.x = K by A15,FUNCOP_1:7;
A17: w.x = (q .--> k).x by A7,A2,A3,A1,FUNCT_4:def 1,A15
.= k by A15,FUNCOP_1:7;
ex R2 being 1-sorted st R2 = F.x
& (Carrier F).x = the carrier of R2 by PRALG_1:def 15,A15;
hence w.x in (Carrier F).x by A17,A16;
end;
end;
then w in product (Carrier F) by A8,CARD_3:def 5;
hence thesis by GROUP_7:def 2;
end;
Lm6:
for I be non empty set,
F be multMagma-Family of I,
x be set
st x in the carrier of product F
holds x is total I-defined Function
proof
let I be non empty set,
F be multMagma-Family of I,
x be set;
assume A1: x in the carrier of product F;
the carrier of product F = product (Carrier F) by GROUP_7:def 2;
hence thesis by A1;
end;
Lm7:
for I be non empty set,
F be multMagma-Family of I,
f be Function
st f in the carrier of product F
for x be set st x in I holds
ex R be non empty multMagma st
R = F.x & f.x in the carrier of R
proof
let I be non empty set,
F be multMagma-Family of I,
f be Function;
assume A1: f in the carrier of product F;
A2: dom (Carrier F) = I by PARTFUN1:def 2;
the carrier of product F = product Carrier F by GROUP_7:def 2;
then consider g be Function such that
A3: f = g & dom g = dom (Carrier F) &
for y be object st y in dom (Carrier F)
holds g.y in (Carrier F).y by CARD_3:def 5,A1;
let x be set;
assume A4: x in I;
consider R being 1-sorted such that
A5: R = F . x & (Carrier F).x = the carrier of R by PRALG_1:def 15,A4;
x in dom F by A4,PARTFUN1:def 2;
then R in rng F by A5,FUNCT_1:3;
then R is non empty multMagma by GROUP_7:def 1;
hence thesis by A4,A3,A2,A5;
end;
theorem Th23:
for I0,I be non empty finite set,
F0 be associative Group-like multMagma-Family of I0,
F be associative Group-like multMagma-Family of I,
H,K be Group,
q be Element of I,
G0 be Function of H,product F0 st
G0 is Homomorphism of H,product F0
& G0 is bijective & not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) holds
for G be Function of product <*H,K*>,(product F) st
for h be Element of H,k be Element of K
holds ex g be Function
st g=G0.h & G.(<*h,k*>) = g +* (q .--> k) holds
G is Homomorphism of product <*H,K*>,product F
proof
let I0,I be non empty finite set,
F0 be associative Group-like multMagma-Family of I0,
F be associative Group-like multMagma-Family of I,
H,K be Group,
q be Element of I,
G0 be Function of H,(product F0);
assume A1:
G0 is Homomorphism of H,(product F0)
& G0 is bijective
& not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K);
let G be Function of product <*H,K*>,(product F);
assume A2:
for h be Element of H,k be Element of K
holds ex g be Function
st g=G0.h & G.(<*h,k*>) = g +* (q .--> k);
set HK = <*H,K*>;
A3: dom (Carrier F) = I by PARTFUN1:def 2;
now
let a, b be Element of product <*H,K*>;
consider h1 be Element of H,k1 be Element of K such that
A4: a = <*h1,k1*> by TOPALG_4:1;
consider h2 be Element of H,k2 be Element of K such that
A5: b = <*h2,k2*> by TOPALG_4:1;
consider g1 be Function such that
A6: g1=G0.h1 & G.(<*h1,k1*>) = g1 +* (q .--> k1) by A2;
consider g2 be Function such that
A7: g2=G0.h2 & G.(<*h2,k2*>) = g2 +* (q .--> k2) by A2;
reconsider g1 as total I0 -defined Function by A6,Lm6;
reconsider g2 as total I0 -defined Function by A7,Lm6;
reconsider g12 = G0. (h1*h2)
as total I0 -defined Function by Lm6;
A12:ex g12 be Function st
g12=G0.(h1*h2) & G.(<*h1*h2,k1*k2*>) = g12 +* (q .--> (k1*k2)) by A2;
reconsider Ga=G.a, Gb=G.b as Element of (product F);
reconsider ga = g1 +* (q .--> k1)
as total I-defined Function by Lm6,A6;
reconsider gb = g2 +* (q .--> k2)
as total I-defined Function by Lm6,A7;
reconsider pab = Ga*Gb as total I -defined Function by Lm6;
A13: dom pab = dom (Carrier F) by PARTFUN1:def 2,A3;
A14: g12 =(G0.h1)*(G0.h2) by A1,GROUP_6:def 6;
reconsider gab = G.(a*b) as total I -defined Function by Lm6;
A15: gab = g12 +* (q .--> (k1*k2)) by A4,A5,GROUP_7:29,A12;
A16: for i be set st i in I0 holds ga.i = g1.i & gb.i = g2.i
& gab.i = g12.i & F.i = F0.i
proof
let i be set;
assume A17: i in I0;
A18: dom g1 = I0 by PARTFUN1:def 2;
A19: dom g2 = I0 by PARTFUN1:def 2;
A20: dom g12 = I0 by PARTFUN1:def 2;
A21: dom F0 = I0 by PARTFUN1:def 2;
A22: i in dom g1 \/ dom (q .--> k1) by A18,A17,XBOOLE_0:def 3;
A23: i in dom g2 \/ dom (q .--> k2) by A19,A17,XBOOLE_0:def 3;
A24: i in dom g12 \/ dom (q .--> (k1*k2))
by A20,A17,XBOOLE_0:def 3;
A25: i in dom F0 \/ dom (q .--> K) by A21,A17,XBOOLE_0:def 3;
not i in dom (q .--> K) by A1,A17,FUNCOP_1:75;
hence thesis by A25,FUNCT_4:def 1,A1,A22,A23,A24,A15;
end;
A29: ga.q = k1 & gb.q = k2 & gab.q = k1*k2 & F.q = K
proof
A30: q in {q} by TARSKI:def 1;
A31:q in dom (q .--> k1) by TARSKI:def 1;
A32:q in dom (q .--> k2) by TARSKI:def 1;
A33:q in dom (q .--> (k1*k2)) by TARSKI:def 1;
A34: q in dom (q .--> K) by TARSKI:def 1;
A35: q in dom g1 \/ dom (q .--> k1) by A30,XBOOLE_0:def 3;
A36: q in dom g2 \/ dom (q .--> k2) by A30,XBOOLE_0:def 3;
A37: q in dom g12 \/ dom (q .--> (k1*k2))
by A30,XBOOLE_0:def 3;
A38: q in dom F0 \/ dom (q .--> K) by A30,XBOOLE_0:def 3;
A39: ga.q = (q .--> k1).q by A31,A35,FUNCT_4:def 1
.= k1 by FUNCOP_1:7,A30;
A40: gb.q = (q .--> k2).q by A32,A36,FUNCT_4:def 1
.= k2 by FUNCOP_1:7,A30;
A41: gab.q = (q .--> (k1*k2)).q by A33,A37,A15,FUNCT_4:def 1
.= k1*k2 by FUNCOP_1:7,A30;
F.q = (q .--> K).q by A34,A38,A1,FUNCT_4:def 1
.= K by FUNCOP_1:7,A30;
hence thesis by A39,A40,A41;
end;
A42: for x be set st x in I0 holds pab.x = gab.x
proof
let x be set;
assume A43: x in I0; then
A44: x in I by A1,XBOOLE_0:def 3;
consider S be non empty multMagma such that
A45: S = F0.x & g1.x in the carrier of S by A43,Lm7,A6;
reconsider x0 = g1.x as Element of S by A45;
ex R be non empty multMagma st
R = F0.x & g2.x in the carrier of R by Lm7,A43,A7;
then
reconsider y0 = g2.x as Element of S by A45;
A46: S = F.x by A45,A16,A43;
x0 = ga.x & y0=gb.x by A16,A43;
hence pab.x=x0 * y0 by A44,A46,GROUP_7:1,A6,A4,A7,A5
.= g12.x by A14,A6,A7,GROUP_7:1,A43,A45
.= gab.x by A16,A43;
end;
for x be object st x in dom gab holds gab.x = pab.x
proof
let x be object;
assume x in dom gab; then
per cases by XBOOLE_0:def 3,A1;
suppose x in I0;
hence gab.x = pab.x by A42;
end;
suppose x in {q}; then
x=q by TARSKI:def 1;
hence gab.x = pab.x by A29,GROUP_7:1,A6,A4,A7,A5;
end;
end;
hence G . (a * b) = (G . a) * (G . b)
by A13,PARTFUN1:def 2,A3,FUNCT_1:2;
end;
hence thesis by GROUP_6:def 6;
end;
theorem Th24:
for I0,I be non empty finite set,
F0 be associative Group-like multMagma-Family of I0,
F be associative Group-like multMagma-Family of I,
H,K be Group,
q be Element of I,
G0 be Function of H, product F0 st
G0 is Homomorphism of H, product F0
& G0 is bijective
& not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) holds
for G be Function of product <*H,K*>, product F st
for h be Element of H,k be Element of K
holds ex g be Function
st g=G0.h & G.(<*h,k*>) = g +* (q .--> k)
holds G is bijective
proof
let I0,I be non empty finite set,
F0 be associative Group-like multMagma-Family of I0,
F be associative Group-like multMagma-Family of I,
H,K be Group,
q be Element of I,
G0 be Function of H,product F0;
assume A1:
G0 is Homomorphism of H,(product F0)
& G0 is bijective & not q in I0 & I = I0 \/ {q}
& F = F0 +* (q .--> K);
let G be Function of product <*H,K*>,(product F);
assume A2:
for h be Element of H,k be Element of K
holds ex g be Function
st g=G0.h & G.(<*h,k*>) = g +* (q .--> k);
set HK = <*H,K*>;
A3: dom (Carrier F0) = I0 by PARTFUN1:def 2;
A4: dom (Carrier F) = I by PARTFUN1:def 2;
A5: dom F0 = I0 by PARTFUN1:def 2;
A6: the carrier of product F = product Carrier F by GROUP_7:def 2;
for x1,x2 be object st
x1 in the carrier of product <*H,K*>
& x2 in the carrier of product <*H,K*>
& G.x1 = G.x2 holds x1 = x2
proof
let z1,z2 be object;
assume A8:
z1 in the carrier of product <*H,K*>
& z2 in the carrier of product <*H,K*> & G.z1 = G.z2; then
reconsider x1=z1,x2=z2 as Element of product <*H,K*>;
consider h1 be Element of H,k1 be Element of K
such that A9: x1 = <*h1,k1*> by TOPALG_4:1;
consider h2 be Element of H,k2 be Element of K
such that A10: x2 = <*h2,k2*> by TOPALG_4:1;
consider g1 be Function
such that A11: g1=G0.h1 & G.(<*h1,k1*>) = g1 +* (q .--> k1) by A2;
consider g2 be Function
such that A12: g2=G0.h2 & G.(<*h2,k2*>) = g2 +* (q .--> k2) by A2;
reconsider g1 as total I0-defined Function by Lm6,A11;
reconsider g2 as total I0-defined Function by Lm6,A12;
reconsider ga = g1 +* (q .--> k1)
as total I-defined Function by Lm6,A11;
reconsider gb = g2 +* (q .--> k2)
as total I-defined Function by Lm6,A12;
A15: for i be set st i in I0 holds ga.i = g1.i & gb.i = g2.i
& F.i = F0.i
proof
let i be set;
assume A16: i in I0;
A17: dom g1 = I0 by PARTFUN1:def 2;
A18: dom g2 = I0 by PARTFUN1:def 2;
A19: i in dom g1 \/ dom (q .--> k1) by A17,A16,XBOOLE_0:def 3;
A20: i in dom g2 \/ dom (q .--> k2) by A18,A16,XBOOLE_0:def 3;
A21: i in dom F0 \/ dom (q .--> K) by A5,A16,XBOOLE_0:def 3;
not i in dom (q .--> K) by A1,A16,FUNCOP_1:75;
hence thesis by A21,A1,A19,A20,FUNCT_4:def 1;
end;
A24: dom g2 = I0 by PARTFUN1:def 2;
for x be object st x in dom g1 holds g1.x = g2.x
proof
let x be object;
assume A25: x in dom g1;
thus g1.x = ga.x by A15,A25
.= g2.x by A15,A25,A11,A12,A9,A10,A8;
end;
then
A26:G0.h1 = G0.h2 by A11,A12,FUNCT_1:2,PARTFUN1:def 2,A24;
ga.q = k1 & gb.q = k2
proof
A27: q in {q} by TARSKI:def 1;
A28:q in dom (q .--> k1) by TARSKI:def 1;
A29:q in dom (q .--> k2) by TARSKI:def 1;
A30: q in dom g1 \/ dom (q .--> k1) by A27,XBOOLE_0:def 3;
A31: q in dom g2 \/ dom (q .--> k2) by A27,XBOOLE_0:def 3;
A32: ga.q = (q .--> k1).q by A28,A30,FUNCT_4:def 1
.= k1 by FUNCOP_1:7,A27;
gb.q = (q .--> k2).q by A29,A31,FUNCT_4:def 1
.= k2 by FUNCOP_1:7,A27;
hence thesis by A32;
end;
hence z1=z2 by A9,A10,A26,A1,FUNCT_2:19,A11,A12,A8;
end;
then
A33: G is one-to-one by FUNCT_2:19;
for y be object st y in the carrier of product F
ex x be object st x in the carrier of product <*H,K*> & y = G.x
proof
let y be object;
assume A34: y in the carrier of product F; then
reconsider y as total I-defined Function by Lm6;
A35: q in {q} by TARSKI:def 1;
A36: q in dom (q .--> K) by TARSKI:def 1;
A37: q in dom F0 \/ dom (q .--> K) by A35,XBOOLE_0:def 3;
A38: F.q = (q .--> K).q by A36,A37,A1,FUNCT_4:def 1
.= K by FUNCOP_1:7,A35;
ex R be non empty multMagma st
R = F.q & y.q in the carrier of R by Lm7,A34; then
reconsider k=y.q as Element of K by A38;
reconsider y0 = y|I0 as I0-defined Function;
A39: the carrier of product F0 = product (Carrier F0) by GROUP_7:def 2;
I = dom y by PARTFUN1:def 2; then
A40: dom y0 = I0 by RELAT_1:62,A1,XBOOLE_1:7;
for i be object st i in dom Carrier F0
holds y0.i in (Carrier F0).i
proof
let i be object;
assume A41:i in dom Carrier F0; then
A42: i in I0;
A43: i in dom F0 \/ dom (q .--> K) by A5,A41,XBOOLE_0:def 3;
A44:not i in dom (q .--> K) by A1,A42,FUNCOP_1:75;
A45:I0 c= I by XBOOLE_1:7,A1;
A46: ex R being 1-sorted st
R = F0 . i & (Carrier F0) . i = the carrier of R
by A41,PRALG_1:def 15;
ex R being 1-sorted st
R = F . i & (Carrier F) . i = the carrier of R
by A42,A45,PRALG_1:def 15; then
A47: (Carrier F0) . i = (Carrier F) . i
by A43,FUNCT_4:def 1,A1,A44,A46;
ex g be Function st y = g & dom g = dom Carrier F &
for i be object st i in dom Carrier F
holds g.i in (Carrier F).i by CARD_3:def 5,A34,A6; then
y.i in (Carrier F).i by A45,A4,A42;
hence y0.i in (Carrier F0).i by A47,A41,FUNCT_1:49;
end; then
y0 in the carrier of (product F0) by A40,A3,CARD_3:def 5,A39; then
y0 in rng G0 by A1,FUNCT_2:def 3; then
consider h be Element of H such that
A48: y0=G0.h by FUNCT_2:113;
A49: dom y = I by PARTFUN1:def 2; then
y|{q} = q .--> k by FUNCT_7:6; then
A50: y = y|I0 +* (q .--> k) by A1,A49,FUNCT_4:70;
consider g be Function
such that A51: g=G0.h & G.(<*h,k*>) = g +* (q .--> k) by A2;
thus thesis by A48,A50,A51;
end; then
rng G = the carrier of (product F) by FUNCT_2:10; then
G is onto by FUNCT_2:def 3;
hence thesis by A33;
end;
theorem Th25:
for q be set,
F be multMagma-Family of {q},
G be non empty multMagma st
F = q .--> G holds
for y be (the carrier of G)-valued total {q} -defined Function holds
y in the carrier of product F & y.q in the carrier of G &
y= q .--> y.q
proof
let q be set,
F be multMagma-Family of {q},
G be non empty multMagma;
assume A1: F = q .--> G;
A2: q in {q} by TARSKI:def 1;
A3: the carrier of product F = product Carrier F by GROUP_7:def 2;
ex R being 1-sorted st
R = F . q & (Carrier F) . q = the carrier of R
by PRALG_1:def 15,A2; then
A4: (Carrier F) . q = the carrier of G by A2,A1,FUNCOP_1:7;
A5: dom (Carrier F) = {q} by PARTFUN1:def 2;
let y be (the carrier of G)-valued total {q} -defined Function;
A6: dom y = {q} by PARTFUN1:def 2; then
y.q in rng y by FUNCT_1:3,A2; then
reconsider z=y.q as Element of G;
A7: for x be object st x in dom y holds y.x = z by TARSKI:def 1;
now let i be object;
assume A8:i in dom y; then
A9: i = q by TARSKI:def 1;
y.i = z by TARSKI:def 1,A8;
hence y.i in (Carrier F) . i by A4,A9;
end;
hence thesis by A7,FUNCOP_1:11,A5,A6,CARD_3:9,A3;
end;
theorem Th26:
for q be set,
F be associative Group-like multMagma-Family of {q},
G be Group st F = q .--> G holds
ex HFG be Homomorphism of product F,G st
HFG is bijective &
for x be (the carrier of G)-valued total {q} -defined Function
holds HFG.x = Product x
proof
let q be set,
F be associative Group-like multMagma-Family of {q},
G be Group;
assume A1: F = q .--> G;
consider I be Homomorphism of G, product F such that
A2: I is bijective &
for x being Element of G holds I . x = q .--> x by Th21,A1;
set HFG = I";
A3: rng I = the carrier of (product F) by A2,FUNCT_2:def 3; then
reconsider HFG as Function of product F, G by FUNCT_2:25,A2;
A4: HFG*I = id (the carrier of G)
& I*HFG = id (the carrier of (product F)) by A2,A3,FUNCT_2:29;
A5:HFG is onto by A4,FUNCT_2:23;
reconsider HFG as Homomorphism of product F,G by A2,GROUP_6:62;
for y be (the carrier of G)-valued total {q} -defined Function
holds HFG.y =Product y
proof
let y be (the carrier of G)-valued total {q} -defined Function;
A6: y in the carrier of product F &
y.q in the carrier of G &
y= q .--> y.q by A1,Th25;
reconsider z=y.q as Element of G by A1,Th25;
A7: I . z = q .--> z by A2
.= y by A1,Th25;
thus HFG.y = z by FUNCT_2:26,A2,A7
.= Product y by Th9,A6;
end;
hence thesis by A5,A2;
end;
theorem Th27:
for I0,I be non empty finite set,
F0 be associative Group-like multMagma-Family of I0,
F be associative Group-like multMagma-Family of I,
H,K be Group,
q be Element of I,
G0 be Homomorphism of H,(product F0) st
not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) & G0 is bijective
ex G be Homomorphism of product <*H,K*>,(product F) st
G is bijective &
for h be Element of H,k be Element of K
ex g be Function st g=G0.h & G.(<*h,k*>) = g +* (q .--> k)
proof
let I0,I be non empty finite set,
F0 be associative Group-like multMagma-Family of I0,
F be associative Group-like multMagma-Family of I,
H,K be Group,
q be Element of I,
G0 be Homomorphism of H,(product F0);
assume A1: not q in I0 & I = I0 \/ {q} &
F = F0 +* (q .--> K) & G0 is bijective;
set HK = <*H,K*>;
A2: the carrier of product F0 = product Carrier F0 by GROUP_7:def 2;
defpred P[set, set] means
ex h be Element of H,k be Element of K,
g be Function st $1 = <*h,k*> & g =G0.h & $2 = g +* (q .--> k);
A3:for z be Element of product <*H,K*>
ex w be Element of the carrier of (product F) st P[z,w]
proof
let z be Element of product <*H,K*>;
consider h be Element of H,k be Element of K
such that A4: z = <*h,k*> by TOPALG_4:1;
consider g be Function such that
A5: G0.h = g & dom g = dom (Carrier F0) &
for y be object st y in dom (Carrier F0)
holds g.y in (Carrier F0).y by CARD_3:def 5,A2;
set w = g +* (q .--> k);
w in the carrier of (product F) by A1,A5,Th22;
hence thesis by A4,A5;
end;
consider G being Function of product <*H,K*>, product F such that
A6: for x being Element of product <*H,K*>
holds P[x,G.x] from FUNCT_2:sch 3(A3);
A7:for h be Element of H,k be Element of K
holds ex g be Function
st g=G0.h & G.(<*h,k*>) = g +* (q .--> k)
proof
let h be Element of H,k be Element of K;
reconsider z= <*h,k*> as Element of product <*H,K*>;
consider h1 be Element of H,k1 be Element of K,
g be Function such that
A8: z = <*h1,k1*> & g =G0.h1 & G.z = g +* (q .--> k1) by A6;
A9: h1 =(<*h1,k1*>).1
.= h by FINSEQ_1:44,A8;
k1 =(<*h1,k1*>).2
.= k by FINSEQ_1:44,A8;
hence thesis by A8,A9;
end;
then reconsider G as Homomorphism of product <*H,K*>,(product F)
by Th23,A1;
G is bijective by Th24,A1,A7;
hence thesis by A7;
end;
theorem Th28:
for I0,I be non empty finite set,
F0 be associative Group-like multMagma-Family of I0,
F be associative Group-like multMagma-Family of I,
H,K be Group,
q be Element of I,
G0 be Homomorphism of product F0, H st not q in I0 &
I = I0 \/ {q} & F = F0 +* (q .--> K) & G0 is bijective holds
ex G be Homomorphism of product F, product <*H,K*> st G is bijective &
for x0 be Function,
k be Element of K,
h be Element of H
st h = G0.x0 & x0 in product F0 holds
G.(x0 +* (q .-->k)) = <* h, k *>
proof
let I0,I be non empty finite set,
F0 be associative Group-like multMagma-Family of I0,
F be associative Group-like multMagma-Family of I,
H,K be Group,
q be Element of I,
G0 be Homomorphism of product F0,H;
assume A1: not q in I0 &
I = I0 \/ {q} & F = F0 +* (q .--> K) & G0 is bijective;
set L0=G0";
A2: rng G0 = the carrier of H by FUNCT_2:def 3,A1; then
reconsider L0 as Function of H, product F0 by FUNCT_2:25,A1;
A3: L0*G0 = id the carrier of product F0
& G0*L0 = id the carrier of H by A1,A2,FUNCT_2:29;
A4:L0 is onto by A3,FUNCT_2:23;
reconsider L0 as Homomorphism of H,product F0 by A1,GROUP_6:62;
consider L be Homomorphism of product <*H,K*>,(product F) such that
A5: L is bijective &
for h be Element of H,k be Element of K
holds ex g be Function
st g=L0.h & L.(<*h,k*>) = g +* (q .--> k) by Th27,A1,A4;
set G=L";
A6: rng L = the carrier of (product F) by FUNCT_2:def 3,A5;
then
reconsider G as Function of product F, product <*H,K*> by FUNCT_2:25,A5;
A7: G * L = id (the carrier of product <*H,K*>)
& L * G = id (the carrier of (product F))
by A5,A6,FUNCT_2:29;
A8:G is onto by A7,FUNCT_2:23;
reconsider G as Homomorphism of product F,(product <*H,K*>)
by A5,GROUP_6:62;
for x0 be Function, k be Element of K, h be Element of H
st h = G0.x0 & x0 in (product F0) holds
G.(x0 +* (q .-->k)) = <* h, k *>
proof
let x0 be Function,
k be Element of K,
h be Element of H;
assume A9: h = G0.x0 & x0 in (product F0);
consider g be Function such that
A10: g=L0.h & L.(<*h,k*>) = g +* (q .--> k) by A5;
g = x0 by A10,A1,A9,FUNCT_2:26;
hence G.(x0 +* (q .--> k)) = <*h,k*> by A5,FUNCT_2:26,A10;
end;
hence thesis by A8,A5;
end;
theorem Th29:
for I be non empty finite set,
F be associative Group-like multMagma-Family of I,
x be total I -defined Function
st for p be Element of I holds x.p in F.p
holds x in the carrier of product F
proof
let I be non empty finite set,
F be associative Group-like multMagma-Family of I,
x be total I -defined Function;
assume A1: for p be Element of I holds x.p in F.p;
A2: dom (Carrier F) = I by PARTFUN1:def 2;
A3: the carrier of product F = product (Carrier F) by GROUP_7:def 2;
A4: dom x = I by PARTFUN1:def 2;
now let i be object;
assume A5:i in dom (Carrier F);
consider R being 1-sorted such that
A6:
R = F . i & (Carrier F) . i = the carrier of R by PRALG_1:def 15,A5;
reconsider i0=i as Element of I by A5;
x.i0 in the carrier of R by A6,STRUCT_0:def 5,A1;
hence x.i in (Carrier F) . i by A6;
end;
hence thesis by A3,A2,A4,CARD_3:def 5;
end;
theorem Th30:
for I0,I be non empty finite set,
F0 be associative Group-like multMagma-Family of I0,
F be associative Group-like multMagma-Family of I,
K be Group,
q be Element of I,
x be Element of product F st
not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) holds
ex x0 be total I0 -defined Function,
k be Element of K st x0 in product F0
& x = x0 +* (q .--> k) & for p be Element of I0 holds x0.p in F0.p
proof
let I0,I be non empty finite set,
F0 be associative Group-like multMagma-Family of I0,
F be associative Group-like multMagma-Family of I,
K be Group,
q be Element of I,
x be Element of product F;
assume A1: not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K);
reconsider y=x as total I-defined Function by Lm6;
A2: dom (Carrier F) = I by PARTFUN1:def 2;
A3: the carrier of product F = product (Carrier F) by GROUP_7:def 2;
A4: dom F0 = I0 by PARTFUN1:def 2;
A6: q in {q} by TARSKI:def 1;
A7: q in dom (q .--> K) by TARSKI:def 1;
A8: q in dom F0 \/ dom (q .--> K) by A6,XBOOLE_0:def 3;
A9: F.q = (q .--> K).q by A7,A8,A1,FUNCT_4:def 1
.= K by FUNCOP_1:7,A6;
ex R be non empty multMagma st
R = F.q & y.q in the carrier of R by Lm7; then
reconsider k=y.q as Element of K by A9;
reconsider y0 = y|I0 as I0-defined Function;
A10: the carrier of product F0 = product (Carrier F0) by GROUP_7:def 2;
I = dom y by PARTFUN1:def 2; then
A11: dom y0 = I0 by RELAT_1:62,A1,XBOOLE_1:7; then
reconsider y0 as total I0-defined Function by PARTFUN1:def 2;
A12: dom (Carrier F0) = I0 by PARTFUN1:def 2;
A13: for i be Element of I0
holds y0.i in (Carrier F0).i & y0.i in F0.i
proof
let i be Element of I0;
A14: i in dom F0 \/ dom (q .--> K) by A4,XBOOLE_0:def 3;
i <> q by A1; then
A15:not i in dom (q .--> K) by FUNCOP_1:75;
A16: i in I by TARSKI:def 3,XBOOLE_1:7,A1;
consider R being 1-sorted such that
A17: R = F0 . i & (Carrier F0) . i = the carrier of R by PRALG_1:def 15;
ex R being 1-sorted st
R = F . i & (Carrier F) . i = the carrier of R by A16,PRALG_1:def 15;
then
A18: (Carrier F0) . i = (Carrier F) . i
by A15,A14,FUNCT_4:def 1,A1,A17;
ex g be Function st y = g & dom g = dom (Carrier F) &
for i be object st i in dom Carrier F
holds g.i in (Carrier F).i by CARD_3:def 5,A3;
then y.i in (Carrier F).i by A16,A2;
hence thesis by A17,FUNCT_1:49,A18;
end;
for i be object st i in dom (Carrier F0)
holds y0.i in (Carrier F0).i by A13; then
A19: y0 in the carrier of (product F0) by A10,A11,A12,CARD_3:def 5;
A20: dom y = I by PARTFUN1:def 2; then
y|{q} = q .--> k by FUNCT_7:6;
then y = y|I0 +* (q .--> k) by A1,A20,FUNCT_4:70;
hence thesis by A19,STRUCT_0:def 5,A13;
end;
theorem Th31:
for G be Group,
H be Subgroup of G,
f being FinSequence of G,
g being FinSequence of H
st f=g
holds Product f = Product g
proof
let G be Group, H be Subgroup of G;
defpred P[Nat] means
for f being FinSequence of G, g being FinSequence of H
st $1 = len f & f=g holds Product f = Product g;
A1:P[0]
proof
let f be FinSequence of G, g be FinSequence of H;
assume A2:0 = len f & f=g; then
f = <*> the carrier of G; then
A3: Product f = 1_G by GROUP_4:8;
g = <*> the carrier of H by A2;
then Product g = 1_H by GROUP_4:8;
hence thesis by A3,GROUP_2:44;
end;
A4: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A5: P[k];
let f be FinSequence of G,
g be FinSequence of H;
assume A6:k+1 = len f & f=g;
A7:k+1 in Seg (k+1) by FINSEQ_1:4;
then k+1 in dom f by A6,FINSEQ_1:def 3;
then f.(k+1) in rng f by FUNCT_1:3;
then reconsider af = f.(k+1) as Element of G;
k+1 in dom g by A7,A6,FINSEQ_1:def 3;
then g.(k+1) in rng g by FUNCT_1:3; then
reconsider ag = g.(k+1) as Element of H;
reconsider f1 = f|k as FinSequence of G;
reconsider g1 = g|k as FinSequence of H;
A8: f = f1^<* af *> by A6,RFINSEQ:7;
A9: g = g1^<* ag *> by A6,RFINSEQ:7;
A10: Product f = Product(f1) * af by GROUP_4:6,A8;
A11: Product g = Product(g1) * ag by GROUP_4:6,A9;
len f1 = k by FINSEQ_1:59,A6,NAT_1:11;
then Product(f1) = Product(g1) by A6,A5;
hence thesis by A10,A11,GROUP_2:43,A6;
end;
A12: for k be Nat holds P[k] from NAT_1:sch 2(A1,A4);
let f be FinSequence of G, g be FinSequence of H;
assume A13: f = g;
len f is Nat;
hence thesis by A13,A12;
end;
theorem Th32:
for I be non empty finite set,
G be Group,
H be Subgroup of G,
x be (the carrier of G)-valued total I -defined Function,
x0 be (the carrier of H)-valued total I -defined Function
st x=x0
holds Product x = Product x0
proof
let I be non empty finite set,
G be Group,
H be Subgroup of G,
x be (the carrier of G)-valued total I -defined Function,
x0 be (the carrier of H)-valued total I -defined Function;
assume A1:x=x0;
consider f being FinSequence of G such that
A2: Product x = Product f & f = x*canFS(I) by Def1;
consider g being FinSequence of the carrier of H such that
A3: Product x0 = Product g & g = x0*canFS(I) by Def1;
thus thesis by A2,A1,A3,Th31;
end;
theorem Th33:
for G being commutative Group,
I0,I be non empty finite set,
q be Element of I,
x be (the carrier of G)-valued total I -defined Function,
x0 be (the carrier of G)-valued total I0 -defined Function,
k be Element of G st
not q in I0 & I = I0 \/ {q} & x = x0 +* (q .--> k)
holds
Product x = (Product x0)*k
proof
let G be commutative Group,
I0,I be non empty finite set,
q be Element of I,
x be (the carrier of G)-valued total I -defined Function,
x0 be (the carrier of G)-valued total I0 -defined Function,
k be Element of G;
assume A1: not q in I0 & I = I0 \/ {q} & x = x0 +* (q .--> k);
reconsider y = (q .--> k) as (the carrier of G)-valued
total {q} -defined Function;
A2: I0 misses {q}
proof
assume I0 meets {q}; then
consider x be object such that
A3: x in I0 & x in {q} by XBOOLE_0:3;
thus contradiction by A3,A1,TARSKI:def 1;
end;
Product x = (Product x0) * (Product y) by A2,A1,Th8;
hence thesis by Th9;
end;
theorem Th34:
for G being strict finite commutative Group
st card G > 1 holds
ex I be non empty finite set,
F be associative Group-like commutative multMagma-Family of I,
HFG be Homomorphism of product F,G st
I = support (prime_factorization card G)
& (for p be Element of I holds F.p is strict Subgroup of G &
card (F.p) = (prime_factorization card G).p) &
(for p,q be Element of I st p <> q holds
(the carrier of (F.p)) /\ (the carrier of (F.q)) = {1_G}) &
HFG is bijective &
for x be (the carrier of G)-valued total I -defined Function
st for p be Element of I holds x.p in F.p
holds x in product F & HFG.x = Product x
proof
defpred P[Nat] means
for G being strict finite commutative Group st
card(support (prime_factorization card G)) = $1 & $1 <> 0 holds
ex I be non empty finite set,
F be associative Group-like commutative multMagma-Family of I,
HFG be Homomorphism of product F,G st
I = support (prime_factorization card G)
& (for p be Element of I holds F.p is strict Subgroup of G &
card (F.p) = (prime_factorization card G).p) &
(for p,q be Element of I st p <> q holds
(the carrier of (F.p)) /\ (the carrier of (F.q)) ={1_G}) &
HFG is bijective &
for x be (the carrier of G)-valued total I -defined Function
st for p be Element of I holds x.p in F.p
holds x in product F & HFG.x =Product x;
A1:P[0];
A2: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume A3: P[n];
thus P[n+1]
proof
let G be strict finite commutative Group;
assume A4:
card(support (prime_factorization card G)) = n+1 & n+1 <> 0;
per cases;
suppose A5:n = 0;
set f = prime_factorization card G;
A6: support (f) = support pfexp card(G) by NAT_3:def 9;
support (f) <> {} by A4;
then
consider q be object such that
A7: q in support (f) by XBOOLE_0:def 1;
reconsider q as Prime by A6,A7,NAT_3:34;
card {q} = 1 by CARD_1:30;
then
consider q0 be object such that
A8: support prime_factorization card G = {q0} by CARD_1:29,A5,A4;
A9: {q} = support (prime_factorization card G) by A8,TARSKI:def 1,A7;
reconsider Gq = q|^ (q |-count (card G)) as non zero Nat;
set g = prime_factorization Gq;
A10: Product g = Gq by NAT_3:61;
q |-count (card G) <> 0
proof
assume q |-count (card G) = 0; then
f. q = 0 by NAT_3:55;
hence contradiction by A7,PRE_POLY:def 7;
end; then
A11: support pfexp Gq = {q} by NAT_3:42; then
q in support pfexp Gq by TARSKI:def 1; then
A12:g.q = q |^ (q |-count Gq) by NAT_3:def 9;
support g = {q} by A11,NAT_3:def 9; then
A13: support g = support pfexp (card G) by A9,NAT_3:def 9;
for p being Nat st p in support pfexp (card G)
holds g.p = p |^ (p |-count (card G))
proof
let p be Nat;
assume p in support pfexp (card G);
then p in {q} by NAT_3:def 9,A9;
then p=q by TARSKI:def 1;
hence thesis by A12,NAT_3:25,INT_2:def 4;
end;
then
A14: Gq = Product (prime_factorization (card G))
by A13,NAT_3:def 9,A10
.= card G by NAT_3:61;
reconsider I = {q} as non empty finite set;
set F = q .--> G;
reconsider F as multMagma-Family of I;
A16: for s,t be Element of I st s <> t holds
(the carrier of (F.s)) /\ (the carrier of (F.t)) ={1_G}
proof
let s,t be Element of I;
s=q by TARSKI:def 1;
hence thesis by TARSKI:def 1;
end;
A18: for x be Element of I holds
F.x is strict Subgroup of G &
card (F.x) = (prime_factorization card G).x
proof
let x be Element of I;
x in support f by TARSKI:def 1,A7; then
A20: x in support pfexp (card G) by NAT_3:def 9;
A21: x = q by TARSKI:def 1;
card(F.x) = card G
.= f.x by A21,A20,NAT_3:def 9,A14;
hence thesis by GROUP_2:54;
end;
reconsider F as associative Group-like commutative
multMagma-Family of I;
take I,F;
consider HFG be Homomorphism of product F,G such that
A24: HFG is bijective &
for x be (the carrier of G)-valued total {q} -defined Function
holds HFG.x =Product x by Th26;
for x be (the carrier of G)-valued total I -defined Function
st for p be Element of I holds x.p in F.p holds
x in product F & HFG.x =Product x by A24,Th25;
hence thesis by A9,A24,A16,A18;
end;
suppose A25: n <> 0;
set f = prime_factorization card G;
A26: Product f = card G by NAT_3:61;
A27: support (f) = support pfexp card(G) by NAT_3:def 9;
support (f) <> {} by A4; then
consider q be object such that
A28: q in support (f) by XBOOLE_0:def 1;
reconsider q as Prime by A27,A28,NAT_3:34;
reconsider Gq = q|^ (q |-count (card G)) as non zero Nat;
set g = prime_factorization Gq;
set h = f -' g;
q |-count (card G) <> 0
proof
assume q |-count (card G) = 0; then
f. q = 0 by NAT_3:55;
hence contradiction by A28,PRE_POLY:def 7;
end;
then
A29: support pfexp Gq = {q} by NAT_3:42; then
q in support pfexp Gq by TARSKI:def 1; then
A30:g.q = q |^ (q |-count Gq) by NAT_3:def 9;
A31:g.q = q|^ (q |-count (card G)) by NAT_3:25,INT_2:def 4,A30;
A32: support g = {q} by A29,NAT_3:def 9;
A33: for x be object holds x in support h iff
x in (support f) \ {q}
proof
let x be object;
hereby assume A34: x in support h; then
A35: x in (support f) by PRE_POLY:39,TARSKI:def 3;
then
A36: x in support pfexp (card G) by NAT_3:def 9;
not x in {q}
proof
assume x in {q};
then
A37: x = q by TARSKI:def 1;
h.x = f.x -' g.x by PRE_POLY:def 6
.=q |^ (q |-count (card G)) -' g.q by A37,A36,NAT_3:def 9
.=q |^ (q |-count (card G)) -' q |^ (q |-count (card G))
by NAT_3:25,INT_2:def 4,A30
.=q |^ (q |-count (card G)) - q |^ (q |-count (card G))
by XREAL_0:def 2
.= 0;
hence contradiction by A34,PRE_POLY:def 7;
end;
hence x in (support f) \ {q} by XBOOLE_0:def 5,A35;
end;
assume x in (support f) \ {q}; then
A38: x in (support f) & not x in {q} by XBOOLE_0:def 5;
x in support pfexp (card G) by A38,NAT_3:def 9; then
reconsider x0=x as Prime by NAT_3:34;
A39:h.x0 = f.x0 -' g.x0 by PRE_POLY:def 6;
A40: g.x0 = 0 by A38,A32,PRE_POLY:def 7;
f.x0 <> 0 by A38,PRE_POLY:def 7;
then h.x <> 0 by A39,A40,NAT_D:40;
hence x in (support h) by PRE_POLY:def 7;
end;
then
A41: support h = (support f) \ {q} by TARSKI:2;
then
A42: support h misses support g by A32,XBOOLE_1:79;
reconsider h as bag of SetPrimes;
A43: for x being Prime st x in
support h ex n be Nat st 0 < n & h.x = x |^n
proof
let x be Prime;
assume x in support h; then
A44: x in (support f) & not x in {q} by XBOOLE_0:def 5,A41;
A45:h.x = f.x -' g.x by PRE_POLY:def 6;
g.x = 0 by A44,A32,PRE_POLY:def 7;
then h.x = f.x by A45,NAT_D:40;
hence thesis by A44,INT_7:def 1;
end;
then
A46: h is prime-factorization-like by INT_7:def 1;
A47: {q} c= support (f) by A28,ZFMISC_1:31;
A48: support h c= support f by XBOOLE_1:36,A41;
A49: (support h) \/ {q} = support f
by A28,ZFMISC_1:31,A41,XBOOLE_1:45;
for x being object st x in SetPrimes holds
f . x = (h . x) + (g . x)
proof
let x be object;
assume x in SetPrimes;
per cases;
suppose A50: not x in support f;
then
A51: not x in support h by A48;
A52: not x in support g by A32,A47,A50;
thus f . x = (0 qua Real) by PRE_POLY:def 7,A50
.= (h . x) + (0 qua Real) by PRE_POLY:def 7,A51
.= (h . x) + (g . x) by PRE_POLY:def 7,A52;
end;
suppose A53: x in support f;
A54: x in support pfexp (card G) by A53,NAT_3:def 9;
thus f . x = (h . x) + (g . x)
proof
per cases by A53,A49,XBOOLE_0:def 3;
suppose x in (support h); then
A55:x in (support f) & not x in {q}
by A41,XBOOLE_0:def 5;
x in support pfexp (card G) by A55,NAT_3:def 9; then
reconsider x0=x as Prime by NAT_3:34;
A56:h.x0 = f.x0 -' g.x0 by PRE_POLY:def 6;
g.x0 = 0 by A55,A32,PRE_POLY:def 7;
hence thesis by A56,NAT_D:40;
end;
suppose x in {q};
then
A57: x = q by TARSKI:def 1;
A58:h.x =f.q -' g.q by A57,PRE_POLY:def 6;
f.q = q |^ (q |-count (card G)) by A57,A54,NAT_3:def 9;
then
h.x = f.q - g.q by A58,XREAL_0:def 2,A31;
hence thesis by A57;
end;
end;
end;
end;
then h + g = f by PRE_POLY:33;
then
A59: Product f = (Product h) * Product g
by A32,XBOOLE_1:79,A41,NAT_3:19;
Product h is non zero & Product g is non zero by A59,NAT_3:61;
then consider H,K being
strict finite Subgroup of G such that
A60: card H = (Product h) & card K = (Product g) &
(the carrier of H) /\ (the carrier of K) = {1_G} &
ex F being Homomorphism of product <*H,K*>,G
st F is bijective
& for a,b be Element of G st a in H & b in K
holds F.(<*a,b*>) = a*b by A26,A59,Th18,A46,A42,INT_7:12;
reconsider H, K as finite commutative Group;
A61: support prime_factorization card H = support h
by INT_7:16,INT_7:def 1,A43,A60;
card(support prime_factorization card H)
= card (support h) by INT_7:16,INT_7:def 1,A43,A60
.=card (support f) - card{q} by A41,A28,EULER_1:4
.= n+1 -1 by A4,CARD_1:30
.= n; then
consider I0 be non empty finite set,
F0 be associative Group-like commutative multMagma-Family of I0,
HFG0 be Homomorphism of product F0,H such that A62:
I0 = support (prime_factorization card H)
& (for p be Element of I0 holds
F0.p is strict Subgroup of H &
card (F0.p) = (prime_factorization card H).p) &
(for p,q be Element of I0 st p <> q holds
(the carrier of (F0.p)) /\ (the carrier of (F0.q)) ={1_H}) &
HFG0 is bijective &
for x be (the carrier of H)-valued total I0 -defined Function
st for p be Element of I0 holds x.p in F0.p
holds x in product F0 & HFG0.x =Product x by A3,A25;
set I = I0 \/ {q};
reconsider I as non empty finite set;
A63:Product (prime_factorization card H)
= Product h by A60,NAT_3:61; then
A64: prime_factorization card H = h by A46,INT_7:15;
A65: I = support (prime_factorization card G)
by A62,A49,A46,INT_7:15,A63;
set F = F0 +* (q .--> K);
A67: dom F = dom F0 \/ dom (q .--> K) by FUNCT_4:def 1
.= I0 \/ dom (q .--> K) by PARTFUN1:def 2
.= I0 \/ {q};
then
reconsider F as I -defined Function by RELAT_1:def 18;
reconsider F as ManySortedSet of I by PARTFUN1:def 2,A67;
reconsider F as multMagma-Family of I;
A74: for x be Element of I holds
F.x is strict Subgroup of G &
card (F.x) = (prime_factorization card G).x
proof
let x be Element of I;
A75: x in dom F by A67;
A76: x in dom F0 \/ dom (q .--> K) by A75,FUNCT_4:def 1;
A77: I0 = support h by INT_7:16,INT_7:def 1,A43,A60,A62
.= (support f) \ {q} by A33,TARSKI:2;
per cases by XBOOLE_0:def 3;
suppose A78: x in I0;
then
not x in dom (q .--> K) by A77,XBOOLE_0:def 5; then
A79: F.x = F0.x by FUNCT_4:def 1,A76;
reconsider p = x as Element of I0 by A78;
A80: F0.p is strict Subgroup of H &
card (F0.p) = (prime_factorization card H).p by A62;
A81:x in (support f) & not x in {q}
by A41,XBOOLE_0:def 5,A61,A62,A78;
x in support pfexp card G by A81,NAT_3:def 9; then
reconsider x0=x as Prime by NAT_3:34;
A82:h.x0 = f.x0 -' g.x0 by PRE_POLY:def 6;
g.x0 = 0 by A81,A32,PRE_POLY:def 7;
hence F.x is strict Subgroup of G &
card (F.x) = (prime_factorization card G).x
by A79,A80,GROUP_2:56,A64,A82,NAT_D:40;
end;
suppose A83: x in {q}; then
A84:F.x = (q .--> K).x by FUNCT_4:def 1,A76;
x in support f by A83,A47; then
A85: x in support pfexp (card G) by NAT_3:def 9;
A86: x = q by TARSKI:def 1,A83;
card(F.x) = (Product g) by A60,A83,FUNCOP_1:7,A84
.= Gq by NAT_3:61
.= f.x by A86,A85,NAT_3:def 9;
hence F.x is strict Subgroup of G &
card (F.x) = (prime_factorization card G).x
by A84,A83,FUNCOP_1:7;
end;
end;
A87:for i being Element of I holds F . i is Group-like by A74;
A88:for i being Element of I holds F . i is associative by A74;
for i being Element of I holds F . i is commutative by A74; then
reconsider F as associative Group-like commutative
multMagma-Family of I by A87,GROUP_7:def 6,
A88,GROUP_7:def 7,GROUP_7:def 8;
consider FHKG being Homomorphism of product <*H,K*>,G such that
A89: FHKG is bijective
& for a,b be Element of G
st a in H & b in K holds FHKG.(<*a,b*>) = a*b by A60;
A90: I0 = support h by INT_7:16,INT_7:def 1,A43,A60,A62
.= (support f) \ {q} by TARSKI:2,A33
.= I \ {q} by A62,A49,A46,INT_7:15,A63;
A91: not q in I0
proof
assume q in I0; then
q in I & not q in {q} by A90,XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1;
end; then
consider FHK be Homomorphism of (product F), product <*H,K*>
such that
A92: FHK is bijective & for x0 be Function,
k be Element of K, h be Element of H
st h = HFG0.x0 & x0 in product F0 holds
FHK.(x0 +* (q .-->k)) = <* h, k *> by Th28,A62,A28,A65;
reconsider HFG = FHKG*FHK as Function of (product F), G;
A93: HFG is onto by FUNCT_2:27,A89,A92;
reconsider HFG as Homomorphism of (product F), G;
A94: for x be (the carrier of G)-valued total I -defined Function
st for p be Element of I holds x.p in F.p
holds x in product F & HFG.x =Product x
proof
let x be (the carrier of G)-valued total I -defined Function;
assume A95: for p be Element of I holds x.p in F.p; then
x in the carrier of product F by Th29; then
consider x0 be total I0 -defined Function,
k be Element of K such that
A96: x0 in product F0 & x = x0 +* (q .-->k) &
for p be Element of I0 holds
x0.p in F0.p by Th30,A91,A28,A65;
reconsider h = HFG0.x0 as Element of H by FUNCT_2:5,A96;
reconsider hh=h,kk=k as Element of G by GROUP_2:42;
now let y be object;
assume y in rng x0; then
consider z be object such that
A97: z in dom x0 & y=x0.z by FUNCT_1:def 3;
reconsider z as Element of I0 by A97;
A98: x0.z in F0.z by A96;
F0.z is strict Subgroup of H by A62;
hence y in the carrier of H
by A97,STRUCT_0:def 5,A98,GROUP_2:40;
end; then
reconsider x0 as
(the carrier of H)-valued total I0 -defined Function
by RELAT_1:def 19,TARSKI:def 3;
A99: HFG0.x0 =Product x0 by A62,A96;
the carrier of H c= the carrier of G by GROUP_2:def 5;
then
rng x0 c= the carrier of G by XBOOLE_1:1;
then
reconsider xx0=x0 as (the carrier of G)-valued
total I0 -defined Function by RELAT_1:def 19;
A100: Product x0 = Product xx0 by Th32;
thus x in product F by Th29,A95;
A101: hh in H & kk in K;
thus HFG.x = FHKG.(FHK.x) by FUNCT_2:15,Th29,A95
.= FHKG.(<* hh, kk *>) by A92,A96
.= hh*kk by A89,A101
.= Product x by A99,A100,Th33,A91,A28,A65,A96;
end;
for s,t be Element of I st s <> t holds
(the carrier of (F.s)) /\ (the carrier of (F.t)) ={1_G}
proof
let s,t be Element of I;
assume A102: s <> t;
dom F = I by PARTFUN1:def 2; then
A103: s in dom F & t in dom F;
per cases;
suppose s in I0 & t in I0; then
reconsider ss=s,tt =t as Element of I0;
A104: s in dom F0 \/ dom (q .--> K) by A103,FUNCT_4:def 1;
A105: t in dom F0 \/ dom (q .--> K) by A103,FUNCT_4:def 1;
A106: I0 = support h by INT_7:16,INT_7:def 1,A43,A60,A62
.= (support f) \ {q} by TARSKI:2,A33;
then
not ss in dom (q .--> K) by XBOOLE_0:def 5;
then
A107: F.ss = F0.ss by FUNCT_4:def 1,A104;
not tt in dom (q .--> K) by A106,XBOOLE_0:def 5;
then
A108: F.tt = F0.tt by FUNCT_4:def 1,A105;
(the carrier of (F0.ss))
/\ (the carrier of (F0.tt)) ={1_H} by A62,A102;
hence (the carrier of (F.s))
/\ (the carrier of (F.t)) ={1_G} by A107,A108,GROUP_2:44;
end;
suppose A109:not (s in I0 & t in I0);
thus (the carrier of (F.s)) /\ (the carrier of (F.t)) ={1_G}
proof
per cases by A109;
suppose A110: not s in I0;
A111: s in dom F0 \/ dom (q .--> K)
by A103,FUNCT_4:def 1;
A112: s in {q} by A110,A90,XBOOLE_0:def 5; then
F.s = (q .--> K).s by FUNCT_4:def 1,A111; then
A113: F.s = K by A112,FUNCOP_1:7;
t in I0
proof
assume not t in I0;
then not t in I or t in {q} by XBOOLE_0:def 5,A90;
then t=q by TARSKI:def 1;
hence contradiction by A102,TARSKI:def 1,A112;
end;
then
reconsider tt =t as Element of I0;
A114: tt in dom F0 \/ dom (q .--> K)
by A103,FUNCT_4:def 1;
I0 = support h by INT_7:16,INT_7:def 1,A43,A60,A62
.= (support f) \ {q} by TARSKI:2,A33;
then
not tt in dom (q .--> K) by XBOOLE_0:def 5;
then
A115: F.tt = F0.tt by FUNCT_4:def 1,A114;
reconsider S1=F0.tt as strict Subgroup of H by A62;
A116: (the carrier of K) /\ (the carrier of S1)
c= {1_G} by A60,XBOOLE_1:26,GROUP_2:def 5;
A117: 1_G in the carrier of K by GROUP_2:46,STRUCT_0:def 5;
1_H in the carrier of S1 by GROUP_2:46,STRUCT_0:def 5;
then
1_G in the carrier of S1 by GROUP_2:44; then
1_G in (the carrier of K) /\ (the carrier of S1)
by XBOOLE_0:def 4,A117; then
{1_G } c= (the carrier of K)
/\ (the carrier of S1) by ZFMISC_1:31;
hence (the carrier of (F.s))
/\ (the carrier of (F.t)) ={1_G}
by A113,A115,A116,XBOOLE_0:def 10;
end;
suppose A118: not t in I0;
A119: t in dom F0 \/ dom (q .--> K) by A103,FUNCT_4:def 1;
A120: t in {q} by A118,A90,XBOOLE_0:def 5; then
F.t = (q .--> K).t by FUNCT_4:def 1,A119; then
A121: F.t = K by A120,FUNCOP_1:7;
s in I0
proof
assume not s in I0; then
not s in I or s in {q} by XBOOLE_0:def 5,A90; then
s=q by TARSKI:def 1;
hence contradiction by A102,TARSKI:def 1,A120;
end;
then
reconsider ss = s as Element of I0;
A122: ss in dom F0 \/ dom (q .--> K)
by A103,FUNCT_4:def 1;
I0 = support h by INT_7:16,INT_7:def 1,A43,A60,A62
.= (support f) \ {q} by A33,TARSKI:2;
then
not ss in dom (q .--> K) by XBOOLE_0:def 5; then
A123: F.ss = F0.ss by FUNCT_4:def 1,A122;
reconsider S1=F0.ss as strict Subgroup of H by A62;
A124: (the carrier of K) /\ (the carrier of S1)
c= {1_G} by A60,XBOOLE_1:26,GROUP_2:def 5;
A125: 1_G in the carrier of K by GROUP_2:46,STRUCT_0:def 5;
1_H in the carrier of S1 by GROUP_2:46,STRUCT_0:def 5;
then
1_G in the carrier of S1 by GROUP_2:44;
then
1_G in (the carrier of K) /\ (the carrier of S1)
by XBOOLE_0:def 4,A125; then
{1_G } c= (the carrier of K)
/\ (the carrier of S1) by ZFMISC_1:31;
hence
(the carrier of (F.s)) /\ (the carrier of (F.t)) ={1_G}
by A121,A123,A124,XBOOLE_0:def 10;
end;
end;
end;
end;
hence thesis by A65,A74,A93,A89,A92,A94;
end;
end;
end;
A126: for k be Nat holds P[k] from NAT_1:sch 2(A1,A2);
let G be strict finite commutative Group;
assume A127: card G > 1;
card(support (prime_factorization card G)) <> 0
proof
assume card(support (prime_factorization card G)) = 0;
then support prime_factorization card G = {};
hence contradiction by A127,NAT_3:57;
end;
hence thesis by A126;
end;
theorem
for G being strict finite commutative Group st card G > 1 holds
ex I be non empty finite set,
F be associative Group-like commutative multMagma-Family of I st
I = support (prime_factorization card G)
& (for p be Element of I holds F.p is strict Subgroup of G &
card (F.p) = (prime_factorization card G).p) &
(for p,q be Element of I st p <> q holds
(the carrier of (F.p)) /\ (the carrier of (F.q)) = {1_G})
&
(for y be Element of G
ex x be (the carrier of G)-valued total I -defined Function
st (for p be Element of I holds x.p in F.p) & y = Product x)
&
for x1,x2 be (the carrier of G)-valued total I -defined Function st
(for p be Element of I holds x1.p in F.p) &
(for p be Element of I holds x2.p in F.p) &
Product x1 = Product x2 holds x1=x2
proof
let G be strict finite commutative Group;
assume card G > 1; then
consider I be non empty finite set,
F be associative Group-like commutative multMagma-Family of I,
HFG be Homomorphism of product F,G such that
A1:
I = support (prime_factorization card G)
& (for p be Element of I holds F.p is strict Subgroup of G &
card (F.p) = (prime_factorization card G).p) &
(for p,q be Element of I st p <> q holds
(the carrier of (F.p)) /\ (the carrier of (F.q)) ={1_G}) &
HFG is bijective &
for x be (the carrier of G)-valued total I -defined Function
st for p be Element of I holds x.p in F.p
holds x in product F & HFG.x =Product x by Th34;
A2:for y be Element of G
holds ex x be (the carrier of G)-valued total I -defined Function
st (for p be Element of I holds x.p in F.p)
& y = Product x
proof
let y be Element of G;
y in the carrier of G;
then y in rng HFG by A1,FUNCT_2:def 3;
then
consider x be object such that
A3: x in the carrier of product F & y = HFG.x by FUNCT_2:11;
reconsider x as total I-defined Function by A3,Lm6;
A4: for p be Element of I holds x.p in F.p
proof
let p be Element of I;
consider R be non empty multMagma such that
A5: R = F.p & x.p in the carrier of R by Lm7,A3;
thus x.p in (F.p) by A5;
end;
rng x c= the carrier of G
proof
let y be object;
assume y in rng x; then
consider i be object such that
A6: i in dom x & y=x.i by FUNCT_1:def 3;
reconsider i as Element of I by A6;
consider R be non empty multMagma such that
A7: R = F.i & x.i in the carrier of R by A3,Lm7;
F.i is strict Subgroup of G by A1; then
the carrier of (F.i) c= the carrier of G by GROUP_2:def 5;
hence y in the carrier of G by A6,A7;
end;
then
reconsider x as (the carrier of G)-valued
total I -defined Function by RELAT_1:def 19;
take x;
thus thesis by A1,A3,A4;
end;
now let x1,x2 be (the carrier of G)-valued total I -defined Function;
assume A8:
(for p be Element of I holds x1.p in F.p) &
(for p be Element of I holds x2.p in F.p) &
Product x1 = Product x2;
x1 in product F & HFG.x1 =Product x1 by A8,A1; then
A9: HFG.x1 = HFG.x2 by A8,A1;
x1 in the carrier of product F &
x2 in the carrier of product F by A8,A1,STRUCT_0:def 5;
hence x1=x2 by A9,A1,FUNCT_2:19;
end;
hence thesis by A1,A2;
end;