:: Isomorphisms of Direct Products of Finite Commutative Groups
:: by Hiroyuki Okazaki , Hiroshi Yamazaki and Yasunari Shidama
::
:: Received January 31, 2013
:: Copyright (c) 2013 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, GROUP_2, FINSEQ_1, STRUCT_0;
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 LM17Z:
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 AS1: A misses B;
assume AS2: A1 c= A & B1 c= B;
assume AS3: A1 \/ B1 = A \/ B;
PP1:A c= A1
proof
let x be element;
assume P0: x in A; then
P1: x in A \/ B by XBOOLE_0:def 3;
not x in B1
proof
assume x in B1; then
x in A /\ B by P0,XBOOLE_0:def 4,AS2;
hence contradiction by AS1, XBOOLE_0:def 7;
end;
hence x in A1 by P1,XBOOLE_0:def 3,AS3;
end;
B c= B1
proof
let x be element;
assume P0: x in B; then
P1: x in A \/ B by XBOOLE_0:def 3;
not x in A1
proof
assume x in A1; then
x in A /\ B by P0,XBOOLE_0:def 4,AS2;
hence contradiction by AS1, XBOOLE_0:def 7;
end;
hence x in B1 by P1,XBOOLE_0:def 3,AS3;
end;
hence thesis by AS2,XBOOLE_0:def 10,PP1;
end;
theorem LM16:
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 element 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 LM17S:
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 AS: (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 AS,XBOOLE_0:def 4;
thus f.q =ps.q + pt.q by AS,PRE_POLY:def 5
.= ps.q + 0 by A2,PRE_POLY:def 7
.= ps.q;
end;
theorem LM17T:
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 AS: (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 AS,XBOOLE_0:def 4;
thus f.q =ps.q + pt.q by AS,PRE_POLY:def 5
.= 0 + pt.q by A2,PRE_POLY:def 7
.= pt.q;
end;
LM17C:
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 AS1: ps is prime-factorization-like;
assume AS2: pt is prime-factorization-like;
assume AS3: f = ps + pt;
assume AS4: (support ps) misses (support pt);
A1: support f = (support ps) \/ (support pt) by AS3,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 P1:x in support f;
per cases by P1,A1,XBOOLE_0:def 3;
suppose P11: x in support ps;
ps.x = f.x by AS3,AS4,P11,LM17S;
hence thesis by P11,AS1,INT_7:def 1;
end;
suppose P12: x in (support pt);
pt.x = f.x by AS3,AS4,P12,LM17T;
hence thesis by P12,AS2,INT_7:def 1;
end;
end;
hence thesis by INT_7:def 1;
end;
theorem LM17X:
for h be non zero Nat, q being Prime
st not q,h are_relative_prime holds
q divides h
proof
let h be non zero Nat, q be Prime;
set pq = prime_factorization q;
set ph = prime_factorization h;
A2: q=Product pq by NAT_3:61;
A3: h=Product ph by NAT_3:61;
assume not q,h are_relative_prime; then
(support pq) /\ (support ph) <> {} by XBOOLE_0:def 7,INT_7:12,A2,A3;
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 element such that
A41: x in {q} /\ (support pfexp h) by XBOOLE_0:def 1;
A4: x in {q} & x in (support pfexp h) by A41,XBOOLE_0:def 4;
x=q by A4,TARSKI:def 1;
hence q divides h by NAT_3:36,A4;
end;
theorem LM17Y:
for h,s be non zero Nat
st for q being Prime st q in support (prime_factorization s)
holds not q,h are_relative_prime holds
support (prime_factorization s) c= support (prime_factorization h)
proof
let h,s be non zero Nat;
assume AS1: for q being Prime st q in
support (prime_factorization s) holds not q,h are_relative_prime;
let x be element;
assume A1: x in support prime_factorization s; then
reconsider q=x as Prime by NEWTON:def 6;
q divides h by LM17X,A1,AS1; then
q in support (pfexp h) by ORDINAL1:def 13,NAT_3:37;
hence thesis by NAT_3:def 9;
end;
theorem LM18B:
for h,k,s,t be non zero Nat
st h,k are_relative_prime & s * t = h * k
& (for q being Prime st q in support prime_factorization s
holds not q,h are_relative_prime)
& (for q being Prime st q in support prime_factorization t
holds not q,k are_relative_prime)
holds
s = h & t = k
proof
let h,k,s,t be non zero Nat;
assume AS1: h,k are_relative_prime;
assume AS2: s * t = h * k;
assume AS3: for q being Prime st q in
support (prime_factorization s) holds not q,h are_relative_prime;
assume AS4:
for q being Prime st q in support prime_factorization t
holds not q,k are_relative_prime;
set ps=prime_factorization s;
set ph=prime_factorization h;
set pt=prime_factorization t;
set pk=prime_factorization k;
P1: support (ps) c= support (ph) by AS3,LM17Y;
P2: support (pt) c= support (pk) by AS4,LM17Y;
support pfexp h misses support pfexp k by NAT_3:44,AS1; then
support (ph) misses support pfexp k by NAT_3:def 9; then
P4:support (ph) misses support (pk) by NAT_3:def 9;
set f = ps + pt;
set g = ph + pk;
L1: f is prime-factorization-like by P4,P1,P2,XBOOLE_1:64,LM17C;
L2: g is prime-factorization-like by P4,LM17C;
L3: Product g = (Product ph)*(Product pk) by P4,NAT_3:19
.= h*(Product pk) by NAT_3:61
.= h*k by NAT_3:61;
N1: Product f = (Product ps)*(Product pt)
by P1,P2,XBOOLE_1:64,P4,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 N1,INT_7:15,L1,L2,L3,AS2
.= (support ph) \/ (support pk) by PRE_POLY:38;
then
Q12: support ps = support ph
& support pt = support pk by P1,P2,P4,LM17Z;
R1: support ps = support pfexp h by Q12,NAT_3:def 9;
R2: support pt = support pfexp k by Q12,NAT_3:def 9;
T4:for p being Nat st p in support pfexp h
holds ps.p = p |^ (p |-count h)
proof
let p be Nat;
assume AS6: p in support pfexp h; then
J0: p in support ph by NAT_3:def 9;
J1: p in support (ps) by AS6,Q12,NAT_3:def 9;
thus ps.p = f.p by LM17S,J1,P1,P2,XBOOLE_1:64,P4
.=ph.p by LM17S,J0,P4,INT_7:15,L1,L2,L3,AS2,N1
.= p |^ (p |-count h) by AS6,NAT_3:def 9;
end;
P5:for p being Nat st p in support pfexp k
holds pt.p = p |^ (p |-count k)
proof
let p be Nat;
assume AS6: p in support pfexp k; then
J0: p in support pk by NAT_3:def 9;
J1: p in support (pt) by Q12,AS6,NAT_3:def 9;
thus (pt).p = f.p by LM17T,J1,P1,P2,XBOOLE_1:64,P4
.=pk.p by LM17T,J0,P4,N1,INT_7:15,L1,L2,L3,AS2
.= p |^ (p |-count k) by AS6,NAT_3:def 9;
end;
thus s = Product (ps) by NAT_3:61
.=Product (ph) by T4,R1,NAT_3:def 9
.= h by NAT_3:61;
thus t = Product (pt) by NAT_3:61
.=Product (pk) by P5,R2,NAT_3:def 9
.= k by NAT_3:61;
end;
LM01: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;
LM02:
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 AS: A misses B;
P1: rng canFS(A) = A by FUNCT_2:def 3;
P2: rng canFS(B) = B by FUNCT_2:def 3; then
P4: rng(canFS(A)^ canFS(B)) = A \/ B by FINSEQ_1:31,P1; 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 AS,CARD_2:40;
hence thesis by P1,FINSEQ_3:91,AS,P2,P4,FUNCT_2:def 3;
end;
LM03B:
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 AS1: A misses B;
assume AS2: FAB = FA +* FB;
assume AS3: f =FA*canFS(A);
assume AS4: g = FB*canFS(B);
reconsider csAB = canFS(A)^ canFS(B) as one-to-one onto
FinSequence of (A \/ B) by LM02,AS1;
set fAB= FAB* (canFS(A) ^ canFS(B));
set cSA = canFS(A);
set cSB = canFS(B);
A1: A = dom FA & rng cSA = A by FUNCT_2:def 3,PARTFUN1:def 2; then
A2: dom f = dom (cSA) by AS3,RELAT_1:27; then
A3: dom f = Seg len cSA by FINSEQ_1:def 3;
B1: B = dom FB & rng cSB = B by FUNCT_2:def 3,PARTFUN1:def 2; then
dom g = dom (cSB) by AS4,RELAT_1:27; then
A6: dom g = Seg len cSB by FINSEQ_1:def 3;
R1: A \/ B = dom FAB by AS2,FUNCT_4:def 1,A1,B1;
rng csAB = A \/ B by FUNCT_2:def 3; then
P2: dom fAB = dom csAB by RELAT_1:27,R1; then
dom fAB = Seg len csAB by FINSEQ_1:def 3;
then reconsider fAB as FinSequence by FINSEQ_1:def 2;
Q1: dom fAB = Seg card(A \/ B) by P2,LM02,AS1
.=Seg (card(A) + card(B)) by AS1,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 A3,FINSEQ_1:def 3
.=Seg (len f + len g) by A6,FINSEQ_1:def 3;
Q2: for k be Nat st k in dom f holds fAB.k=f.k
proof
let k be Nat;
assume D2:k in dom f;
then k in dom csAB by A2,FINSEQ_1:26,TARSKI:def 3; then
D4: fAB.k=FAB.(csAB.k) by FUNCT_1:13;
D5: csAB.k = cSA.k by D2,A2,FINSEQ_1:def 7;
not csAB.k in dom FB
proof
assume X1: csAB.k in dom FB;
cSA.k in rng cSA by D2,A2,FUNCT_1:3;
then
csAB.k in A /\ B by D5,X1,XBOOLE_0:def 4;
hence contradiction by AS1,XBOOLE_0:def 7;
end; then
FAB.(csAB.k) = FA.(csAB.k) by AS2,FUNCT_4:11;
hence fAB.k = FA.(cSA.k) by D4,D2,A2,FINSEQ_1:def 7
.=f.k by AS3,D2,A2, 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 D1: k in dom g;
Y1: len cSA = len f by A3,FINSEQ_1:def 3;
D2: k in dom cSB by AS4,RELAT_1:27,B1,D1;
then (len f + k) in dom csAB by Y1,FINSEQ_1:28; then
D4: fAB.(len f + k)=FAB.(csAB.(len f + k)) by FUNCT_1:13;
csAB.(len f + k) = cSB.k by D2,Y1,FINSEQ_1:def 7;
hence fAB.(len f + k) = FB.(cSB.k)
by D4,D2,FUNCT_1:3,FUNCT_4:13,AS2,B1
.=g.k by AS4,D2,FUNCT_1:13;
end;
hence thesis by FINSEQ_1:def 7,Q1,Q2;
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 :Def5:
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 Th45:
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 AS1: A misses B;
assume AS2: FAB = FA +* FB;
consider fA being FinSequence of G such that
P1:Product (FA) = Product fA & fA = FA*canFS(A) by Def5;
consider fB being FinSequence of G such that
P2:Product (FB) = Product fB & fB = FB*canFS(B) by Def5;
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;
P3: cAB is one-to-one onto FinSequence of (A \/ B) &
dom (cAB) = SGAB by LM02,AS1;
reconsider cAB as one-to-one onto FinSequence of (A \/ B) by LM02,AS1;
rng (cAB) c= (A \/ B);
then
reconsider JcAB = (cAB) as Function of SGAB, (A \/ B) by FUNCT_2:2,P3;
P3A: 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,P3A;
reconsider IuAB = (uAB)" as Function of (A \/ B), SGAB by FINSEQ_1:95;
X1:rng uAB = (A \/ B) by FUNCT_2:def 3;
then
IuAB*KuAB = id SGAB & KuAB*IuAB = id (A \/ B) by FUNCT_2:29;
then
P6: 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 P6,FUNCT_2:27; then
reconsider p as Permutation of SGAB;
reconsider fAB as FinSequence of G by LM01;
P7: (canFS(A \/ B))*p = (KuAB * IuAB)*JcAB by RELAT_1:36
.= id (A \/ B) * JcAB by X1,FUNCT_2:29
.= canFS(A)^canFS(B) by FUNCT_2:17;
P8: SGAB = dom fAB by LM01;
P9: fA ^ fB = FAB*(canFS(A) ^ canFS(B)) by P1,P2,LM03B,AS1,AS2
.= fAB*p by RELAT_1:36,P7;
thus Product (FAB) = Product (fAB) by Def5
.= Product(fA ^ fB) by P8,P9,UPROOTS:16
.= Product (FA)*Product (FB) by P1,P2,GROUP_4:5;
end;
theorem Th49:
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 AS: 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;
P1: f* canFS({q}) is FinSequence of G
& dom (f*canFS({q})) = Seg card({q}) by LM01;
reconsider g= f* canFS({q}) as FinSequence of G by LM01;
X1: card {q} = 1 by CARD_1:30;
then dom (g) = Seg 1 by LM01;
then
P2: len g = 1 by FINSEQ_1:def 3;
P3:canFS({q}) = <*q*> by FINSEQ_1:94;
P4: q in {q} by TARSKI:def 1;
P5: 1 in dom g by P1,X1;
g.1 = f.((canFS({q})).1) by FUNCT_1:12,P5
.=f.q by P3,FINSEQ_1:40
.=z by AS,FUNCOP_1:7,P4; then
<*z*> = f* canFS({q}) by P2,FINSEQ_1:40;
hence Product f = Product zz by Def5
.= z by GROUP_4:9;
end;
begin :: Direct Product of Finite Commutative Groups
theorem LM01:
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;
A2: the carrier of product (<*X,Y*>) = product
Carrier (<*X,Y*>) by GROUP_7:def 2;
len <*CarrX,CarrY*> = 2 by FINSEQ_1:44; then
A4: dom <*CarrX,CarrY*> = {1,2} by FINSEQ_1:2,def 3;
A6: <*X,Y*>.1 = X & <*X,Y*>.2 = Y by FINSEQ_1:44;
for a be element 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 element;
assume
A7: a in dom (Carrier (<*X,Y*>));
per cases by A7,TARSKI:def 2;
suppose
A8: a = 1;
then ex R being 1-sorted st R = (<*X,Y*>).1
& (Carrier (<*X,Y*>)).1 = the carrier of R
by A7,PRALG_1:def 13;
hence thesis by FINSEQ_1:44,A6,A8;
end;
suppose
A9: a = 2;
then ex R being 1-sorted st R = (<*X,Y*>).2
& (Carrier (<*X,Y*>)).2 = the carrier of R by A7,PRALG_1:def 13;
hence thesis by FINSEQ_1:44,A6,A9;
end;
end;
hence thesis by PARTFUN1:def 2,A4,FUNCT_1:2,A2;
end;
theorem LM03:
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 AS1: (the carrier of A) /\ (the carrier of B) = {1_G};
let a,b be Element of G;
assume AS2: a in A & b in B;
P1: a*b*(b*a)" = a*b*(a"*b") by GROUP_1:17
.=(a*b*a") * b" by GROUP_1:def 3;
P2: b" in B by AS2,GROUP_2:51;
a*b in a*B by GROUP_2:27,AS2;
then a*b in B*a by GROUP_3:117;
then consider s be Element of G
such that P20: a*b = s*a & s in the carrier of B by GROUP_2:28;
a*b*a" in B by GROUP_3:1,P20;
then
P4: a*b*(b*a)" in the carrier of B by STRUCT_0:def 5,P1,P2,GROUP_2:50;
Q1: 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 AS2,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 Q20: b*a" = t*b & t in the carrier of A by GROUP_2:28;
b*a"* b" in A by GROUP_3:1,Q20;
then a*b*(b*a)" in the carrier of A by STRUCT_0:def 5,Q1,AS2,GROUP_2:50;
then a*b*(b*a)" in (the carrier of A) /\ (the carrier of B)
by XBOOLE_0:def 4,P4;
then a*b*(b*a)" = 1_G by AS1,TARSKI:def 1;
then 1_G * (b*a) = a*b by GROUP_1:14;
hence thesis by GROUP_1:def 4;
end;
theorem Th18:
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 AS1: 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 AS2: (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;
A2: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
A3: 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 A3,A5;
end;
consider h be Function of product <*A,B*>, G such that
A5: for z be Element of product <*A,B*>
holds P[z,h.z] from FUNCT_2:sch 3(A2);
P5: 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 P50: a in A & b in B;
then
reconsider a1= a as Element of A;
reconsider b1= b as Element of B by P50;
consider x be Element of G, y be Element of G such that
A12: x in A & y in B
& <*a1,b1*> =<*x,y*> & h.(<*a1,b1*>)=x*y by A5;
A13: a1= (<*a1,b1*>).1 by FINSEQ_1:44
.= x by FINSEQ_1:44,A12;
b1= (<*a1,b1*>).2 by FINSEQ_1:44
.= y by FINSEQ_1:44,A12;
hence thesis by A12,A13;
end;
now let z1,z2 be element;
assume A7: 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 A8: x1 in A & y1 in B
& z1 =<*x1,y1*> & h.z1=x1*y1 by A5;
consider x2 be Element of G,
y2 be Element of G such that A9: x2 in A & y2 in B
& z2 =<*x2,y2*> & h.z2=x2*y2 by A5,A7;
x1 = x2*y2*y1" by GROUP_1:14,A9,A7,A8;
then
x1 = x2*(y2*y1") by GROUP_1:def 3;
then
X1: x2"*x1 = y2*y1" by GROUP_1:13;
x2" in A by A9,GROUP_2:51;
then
X2: x2"*x1 in the carrier of A by GROUP_2:50,A8,STRUCT_0:def 5;
y1" in B by A8,GROUP_2:51;
then y2*y1" in the carrier of B by A9,GROUP_2:50,STRUCT_0:def 5;
then
X4: x2"*x1 in (the carrier of A) /\ (the carrier of B)
by X1,X2,XBOOLE_0:def 4;
then x2"*x1 = 1_G by AS2,TARSKI:def 1;
then x1 = x2 * 1_G by GROUP_1:13;
then
X5:x1 = x2 by GROUP_1:def 4;
y2*y1" = 1_G by AS2,TARSKI:def 1,X1,X4;
then y2 = 1_G * y1 by GROUP_1:14;
hence z1=z2 by A8,A9,X5,GROUP_1:def 4;
end; then
A10:h is one-to-one by FUNCT_2:19;
now let w be element;
assume w in the carrier of G; then
reconsider g = w as Element of G;
consider a,b be Element of G such that
A11: a in A & b in B & g = a*b by AS1;
reconsider a1=a as Element of A by A11;
reconsider b1=b as Element of B by A11;
h.(<*a1,b1*>)=a*b by P5,A11;
hence w in rng h by A11,FUNCT_2:112;
end; then
the carrier of G c= rng h by TARSKI:def 3; then
P6: 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
A3: 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
B3: w = <*a,b*> by TOPALG_4:1;
reconsider a1 = a, b1 = b as Element of G by GROUP_2:41,STRUCT_0:def 5;
D2: y*b = y1*b1 by GROUP_2:43;
G1: z*w = <* x*a, y*b *> by A3,B3,GROUP_7:29
.= <* x1*a1, y1*b1 *> by GROUP_2:43,D2;
T1: x1 in A & a1 in A;
then
G2: x1*a1 in A by GROUP_2:50;
T2: y1 in B & b1 in B;
then
G3: y1*b1 in B by GROUP_2:50;
G4:
h.(z*w) = (x1*a1)*(y1*b1) by P5, G1,G2,G3
.= x1*(a1*(y1*b1)) by GROUP_1:def 3
.= x1*((a1*y1)*b1) by GROUP_1:def 3
.= x1*((y1*a1)*b1) by LM03,AS2,T1,T2
.= x1*(y1*(a1*b1)) by GROUP_1:def 3
.= (x1*y1)*(a1*b1) by GROUP_1:def 3;
h.z = x1*y1 by A3,P5,T1,T2;
hence h.(z*w) = h.z *h.w by G4,B3,P5,T1,T2;
end;
then h is Homomorphism of product <*A,B*>,G by GROUP_6:def 6;
hence thesis by P5,P6,A10;
end;
theorem LM12:
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 AS1: A ={x where x is Element of G: x|^m = 1_G};
(1_G) |^m = 1_G by GROUP_1:31;
then
X0:1_G in A by AS1;
X1: 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 AS2: g1 in A & g2 in A;
then
P1: ex x1 be Element of G st g1=x1 & x1|^m = 1_G by AS1;
P2: ex x2 be Element of G st g2=x2 & x2|^m = 1_G by AS1,AS2;
(g1 * g2) |^m = g1 |^m * g2 |^m by GROUP_1:38
.= 1_G by GROUP_1:def 4,P1,P2;
hence g1 * g2 in A by AS1;
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
P1: ex x be Element of G st g=x & x|^m = 1_G by AS1;
g" |^ m = (g |^ m)" by GROUP_1:37
.= 1_G by GROUP_1:8,P1;
hence g" in A by AS1;
end;
hence thesis by X0,X1;
end;
theorem LM13:
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 LM12; 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;
LM14A:
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
P1: ord g = q by GROUP_10:11,NAT_3:36;
P2: 1 < q by INT_2:def 4;
take g;
thus thesis by P1,P2,GROUP_1:42;
end;
theorem LM14:
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_relative_prime
proof
let G be finite commutative Group,
m be Nat,
H be finite Subgroup of G;
assume AS1: the carrier of H = {x where x is Element of G: x|^m = 1_G};
let q be Prime;
assume AS2: q in support prime_factorization card H;
assume AS3: q,m are_relative_prime;
consider a be Element of H such that
P1: a <> 1_H & ord a = q by AS2,LM14A;
a in {x where x is Element of G: x|^m = 1_G} by AS1; then
consider x be Element of G such that
P5A: x=a & x|^m = 1_G;
P5:a|^m =1_G by P5A,GROUP_4:2;
q gcd m = 1 by AS3,INT_2:def 3;
then
consider x,y be Integer such that
P3: 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,P3
.= ((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 P1, GROUP_1:41
.= ((1_H) |^ x) * ((1_H) |^y) by P5,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,P1;
end;
theorem LM15:
for G being finite commutative Group,
h,k be Nat
st card G = h*k & h,k are_relative_prime 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 AS:card G = h*k & h,k are_relative_prime;
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 element;
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 by TARSKI:def 3;
B c= the carrier of G
proof
let y be element;
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 by TARSKI:def 3;
consider H being strict finite Subgroup of G such that P1:
the carrier of H = A & H is commutative
& H is normal by LM13;
consider K being strict finite Subgroup of G
such that P2:
the carrier of K = B & K is commutative & K is normal by LM13;
(1_G) |^ h = 1_G by GROUP_1:31;
then
P3: 1_G in the carrier of H by P1;
(1_G) |^ k = 1_G by GROUP_1:31;
then
1_G in the carrier of K by P2;
then
1_G in (the carrier of H) /\ (the carrier of K)
by P3,XBOOLE_0:def 4;
then
P4: {1_G} c= (the carrier of H) /\ (the carrier of K)
by ZFMISC_1:31;
h gcd k = 1 by AS,INT_2:def 3;
then
consider a,b be Integer such that
P9: a*h + b*k = 1 by NAT_D:68;
(the carrier of H) /\ (the carrier of K) c= {1_G}
proof
let z be element;
assume P5: 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;
P6: w in A & w in B by P1,P2,P5,XBOOLE_0:def 4;
then
P7: ex x be Element of G st w=x & x|^h = 1_G;
P8: ex x be Element of G st w=x & x|^k = 1_G by P6;
w = w|^1 by GROUP_1:26
.= (w|^(a*h)) * (w|^(b*k)) by GROUP_1:33,P9
.= ((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,P8,P7
.= 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
P5: (the carrier of H) /\ (the carrier of K) c= {1_G} by TARSKI:def 3;
P6: 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;
P7: x = x|^1 by GROUP_1:26
.=(x|^(b*k)) * (x|^(a*h)) by GROUP_1:33,P9;
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 AS,GR_CY_1:9
.= 1_G by GROUP_1:31;
then
P8: s in H by P1;
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 AS,GR_CY_1:9
.= 1_G by GROUP_1:31;
then t in K by P2;
hence thesis by P7,P8;
end;
take H,K;
thus thesis by P1,P2,P5,P6,P4,XBOOLE_0:def 10;
end;
theorem LM17:
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 LM01;
hence thesis by LM16;
end;
theorem LM18:
for G being finite commutative Group,
h,k be non zero Nat
st card G = h*k & h,k are_relative_prime
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_relative_prime;
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 LM15;
take H,K;
consider F being Homomorphism of product <*H,K*>,G such that
X1: 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,Th18;
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 X1,FUNCT_2:def 1,FUNCT_2:def 3; then
card (product <*H,K*>) = card G by CARD_1:5,WELLORD2:def 4; then
X5: s * t = h * k by A1,LM17;
X8:for q being Prime st q in support (prime_factorization s)
holds not q,h are_relative_prime by A2,LM14;
for q being Prime st q in support (prime_factorization t)
holds not q,k are_relative_prime by A2,LM14;
hence thesis by A2,X1,X5,LM18B,X8,A1;
end;
begin :: Finite Direct Products of Finite Commutative Groups
theorem LM18Th40:
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 AS1:F = q .--> G;
assume AS2:for x being Element of G holds f . x = q .--> x;
A4: the carrier of product F = product (Carrier F) by GROUP_7:def 2;
now
let a, b be Element of G;
P1: (f . a) = q .--> a by AS2;
P2: (f . b) = q .--> b by AS2;
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
P3: fa*fb = gab & dom gab = dom (Carrier F) &
for y be element st y in dom (Carrier F)
holds gab.y in (Carrier F).y by CARD_3:def 5,A4;
P5: for z being element st z in dom gab holds gab . z = a*b
proof
let z be element;
assume P52P:z in dom gab;
P54: G = F.z by AS1,FUNCOP_1:7,P52P,P3;
P55: ga.z = a by FUNCOP_1:7,P52P,P3;
gb.z = b by FUNCOP_1:7,P52P,P3;
hence gab . z = a*b by P1,P2,P3,P52P,P54,P55,GROUP_7:1;
end;
gab = (dom gab) --> a*b by P5,FUNCOP_1:11
.= q .--> (a*b) by P3,PARTFUN1:def 2
.= f . (a * b) by AS2;
hence f . (a * b) = (f . a) * (f . b) by P3;
end;
hence thesis by GROUP_6:def 6;
end;
theorem LM18Th41:
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 AS0:F = q .--> G;
assume AS2: for x being Element of G holds f . x = q .--> x;
A2: 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 13,A2;
then
A5: (Carrier F) . q = the carrier of G by AS0,FUNCOP_1:7,A2;
A6: dom (Carrier F) = {q} by PARTFUN1:def 2;
for x1,x2 be element 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 element;
assume BS1: 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;
P2: f . x2 = q .--> x2 by AS2;
thus z1 = (q .--> x1) .q by FUNCOP_1:7,A2
.=(q .--> x2) .q by P2,AS2,BS1
.=z2 by FUNCOP_1:7,A2;
end; then
P1: f is one-to-one by FUNCT_2:19;
for y be element st y in the carrier of product F
ex x be element st x in the carrier of G & y = f.x
proof
let y be element;
assume y in the carrier of product F; then
consider g be Function such that
P2: y = g & dom g = dom (Carrier F)
& for z be element 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,P2,A2,A6;
P4: for z being element st z in dom g holds
g . z = x by TARSKI:def 1,P2;
take x;
thus x in the carrier of G;
thus y = (dom g) --> x by P4,FUNCOP_1:11,P2
.= q .--> x by P2,PARTFUN1:def 2
.= f . x by AS2;
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 P1;
end;
theorem LM18R1:
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 AS: F = q .--> G;
A2: 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 13,A2;
then
A5: (Carrier F) . q = the carrier of G by AS,FUNCOP_1:7,A2;
A6: dom (Carrier F) = {q} by PARTFUN1:def 2;
defpred P[set, set] means $2= (q .--> $1);
A7: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;
A8: dom w = {q} by FUNCOP_1:13;
now let i be element;
assume A9P:i in dom w; then
A9: i = q by TARSKI:def 1;
w.i = z by FUNCOP_1:7,A9P;
hence w.i in (Carrier F) . i by A5,A9;
end; then
w in product Carrier F by A6,A8,CARD_3:9;
hence ex w be Element of product F st P[z,w] by A4;
end;
consider I being Function of G, product F such that
A9: for x being Element of G holds P[x,I.x] from FUNCT_2:sch 3(A7);
reconsider I as Homomorphism of G, product F by LM18Th40,AS,A9;
I is bijective by LM18Th41,AS,A9;
hence thesis by A9;
end;
theorem LM18A12:
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 AS: g in the carrier of product F0 & not q in I0 & I = I0 \/ {q} &
F = F0 +* (q .--> K);
set HK = <*H,K*>;
D0: dom Carrier F0 = I0 by PARTFUN1:def 2;
D3: dom (q .--> k) = {q} by FUNCOP_1:13;
D4: dom (q .--> K) = {q} by FUNCOP_1:13;
DF0: dom F0 = I0 by PARTFUN1:def 2;
set w = g +* (q .--> k);
A800:g in product (Carrier F0) by AS,GROUP_7:def 2;
then A80:
ex g0 be Function st g = g0 & dom g0 = dom (Carrier F0) &
for y be element 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,A800
.= I by AS,FUNCOP_1:13;
then
A85A: dom w = dom (Carrier F) by PARTFUN1:def 2;
for x be element st x in dom (Carrier F)
holds w.x in (Carrier F).x
proof
let x be element;
assume F4: x in dom (Carrier F);
per cases by AS,XBOOLE_0:def 3,F4;
suppose D51: x in I0;
E1: not x in {q} by AS,D51,TARSKI:def 1;
then
D52: F.x = F0.x by AS,FUNCT_4:def 1,DF0,D4,F4;
consider R1 being 1-sorted such that
F52: R1 = F0.x & (Carrier F0).x = the carrier of R1
by PRALG_1:def 13,D51;
consider R2 being 1-sorted such that
F53: R2 = F.x
& (Carrier F).x = the carrier of R2 by PRALG_1:def 13,F4;
w.x = g.x by FUNCT_4:def 1,A80,D0,D3,F4,AS,E1;
hence w.x in (Carrier F).x by F52,F53,D52,D51,D0,A80;
end;
suppose D51: x in {q}; then
F.x = (q .--> K).x by AS,FUNCT_4:def 1,DF0,D4; then
D55: F.x = K by D51,FUNCOP_1:7;
D52: w.x = (q .--> k).x by A80,D0,D3,AS,FUNCT_4:def 1,D51
.= k by D51,FUNCOP_1:7;
ex R2 being 1-sorted st R2 = F.x
& (Carrier F).x = the carrier of R2 by PRALG_1:def 13,D51;
hence w.x in (Carrier F).x by D52,D55;
end;
end;
then w in product (Carrier F) by A85A,CARD_3:def 5;
hence thesis by GROUP_7:def 2;
end;
XLM18Th401:
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;
XLM18Th402:
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;
D1: 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
D2: f = g & dom g = dom (Carrier F) &
for y be element st y in dom (Carrier F)
holds g.y in (Carrier F).y by CARD_3:def 5,A1;
let x be set;
assume A2: x in I;
consider R being 1-sorted such that
A4: R = F . x & (Carrier F).x = the carrier of R by PRALG_1:def 13,A2;
x in dom F by A2,PARTFUN1:def 2;
then R in rng F by A4,FUNCT_1:3;
then R is non empty multMagma by GROUP_7:def 1;
hence thesis by A2,D2,D1,A4;
end;
theorem XLM18Th40:
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 AS0:
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 AS1:
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*>;
D1: 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
P1A: a = <*h1,k1*> by TOPALG_4:1;
consider h2 be Element of H,k2 be Element of K such that
P1B: b = <*h2,k2*> by TOPALG_4:1;
consider g1 be Function such that
P1C: g1=G0.h1 & G.(<*h1,k1*>) = g1 +* (q .--> k1) by AS1;
consider g2 be Function such that
P1D: g2=G0.h2 & G.(<*h2,k2*>) = g2 +* (q .--> k2) by AS1;
D3: dom (q .--> k1) = {q} by FUNCOP_1:13;
D4: dom (q .--> k2) = {q} by FUNCOP_1:13;
D34:dom (q .--> (k1*k2)) = {q} by FUNCOP_1:13;
D35:dom (q .--> K) = {q} by FUNCOP_1:13;
reconsider g1 as total I0 -defined Function by P1C,XLM18Th401;
reconsider g2 as total I0 -defined Function by P1D,XLM18Th401;
reconsider g12 = G0. (h1*h2)
as total I0 -defined Function by XLM18Th401;
P2AB:ex g12 be Function st
g12=G0.(h1*h2) & G.(<*h1*h2,k1*k2*>) = g12 +* (q .--> (k1*k2)) by AS1;
reconsider Ga=G.a, Gb=G.b as Element of (product F);
reconsider ga = g1 +* (q .--> k1)
as total I-defined Function by XLM18Th401,P1C;
reconsider gb = g2 +* (q .--> k2)
as total I-defined Function by XLM18Th401,P1D;
reconsider pab = Ga*Gb as total I -defined Function by XLM18Th401;
X1: dom pab = dom (Carrier F) by PARTFUN1:def 2,D1;
X3: g12 =(G0.h1)*(G0.h2) by AS0,GROUP_6:def 6;
reconsider gab = G.(a*b) as total I -defined Function by XLM18Th401;
X5: gab = g12 +* (q .--> (k1*k2)) by P1A,P1B,GROUP_7:29,P2AB;
ZLM3: 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 D51: i in I0;
HG1: dom g1 = I0 by PARTFUN1:def 2;
HG2: dom g2 = I0 by PARTFUN1:def 2;
HG12: dom g12 = I0 by PARTFUN1:def 2;
HGF: dom F0 = I0 by PARTFUN1:def 2;
G51: i in dom g1 \/ dom (q .--> k1) by HG1,D51,XBOOLE_0:def 3;
G52: i in dom g2 \/ dom (q .--> k2) by HG2,D51,XBOOLE_0:def 3;
G53: i in dom g12 \/ dom (q .--> (k1*k2))
by HG12,D51,XBOOLE_0:def 3;
G54: i in dom F0 \/ dom (q .--> K) by HGF,D51,XBOOLE_0:def 3;
Q2: not i in dom (q .--> k1) by AS0,D51,FUNCOP_1:75;
Q3:not i in dom (q .--> k2) by AS0,D51,FUNCOP_1:75;
Q4:not i in dom (q .--> (k1*k2)) by AS0,D51,FUNCOP_1:75;
not i in dom (q .--> K) by AS0,D51,FUNCOP_1:75;
hence thesis by G54,FUNCT_4:def 1,AS0,Q2,G51,G52,Q4,Q3,G53,X5;
end;
ZLM4: ga.q = k1 & gb.q = k2 & gab.q = k1*k2 & F.q = K
proof
D51: q in {q} by TARSKI:def 1;
H1:q in dom (q .--> k1) by TARSKI:def 1,D3;
H2:q in dom (q .--> k2) by TARSKI:def 1,D4;
H12:q in dom (q .--> (k1*k2)) by TARSKI:def 1,D34;
H13: q in dom (q .--> K) by TARSKI:def 1,D35;
G51: q in dom g1 \/ dom (q .--> k1) by D3,D51,XBOOLE_0:def 3;
G52: q in dom g2 \/ dom (q .--> k2) by D4,D51,XBOOLE_0:def 3;
G53: q in dom g12 \/ dom (q .--> (k1*k2))
by D34,D51,XBOOLE_0:def 3;
G54: q in dom F0 \/ dom (q .--> K) by D35,D51,XBOOLE_0:def 3;
Q2: ga.q = (q .--> k1).q by H1,G51,FUNCT_4:def 1
.= k1 by FUNCOP_1:7,D51;
Q3: gb.q = (q .--> k2).q by H2,G52,FUNCT_4:def 1
.= k2 by FUNCOP_1:7,D51;
Q4: gab.q = (q .--> (k1*k2)).q by H12,G53,X5,FUNCT_4:def 1
.= k1*k2 by FUNCOP_1:7,D51;
F.q = (q .--> K).q by H13,G54,AS0,FUNCT_4:def 1
.= K by FUNCOP_1:7,D51;
hence thesis by Q2,Q3,Q4;
end;
ZLM5: for x be set st x in I0 holds pab.x = gab.x
proof
let x be set;
assume A1: x in I0; then
A2: x in I by AS0,XBOOLE_0:def 3;
consider S be non empty multMagma such that
A3: S = F0.x & g1.x in the carrier of S by A1,XLM18Th402,P1C;
reconsider x0 = g1.x as Element of S by A3;
ex R be non empty multMagma st
R = F0.x & g2.x in the carrier of R by XLM18Th402,A1,P1D;
then
reconsider y0 = g2.x as Element of S by A3;
A7: S = F.x by A3,ZLM3,A1;
x0 = ga.x & y0=gb.x by ZLM3,A1;
hence pab.x=x0 * y0 by A2,A7,GROUP_7:1,P1C,P1A,P1D,P1B
.= g12.x by X3,P1C,P1D,GROUP_7:1,A1,A3
.= gab.x by ZLM3,A1;
end;
for x be element st x in dom gab holds gab.x = pab.x
proof
let x be element;
assume x in dom gab; then
per cases by XBOOLE_0:def 3,AS0;
suppose x in I0;
hence gab.x = pab.x by ZLM5;
end;
suppose x in {q}; then
x=q by TARSKI:def 1;
hence gab.x = pab.x by ZLM4,GROUP_7:1,P1C,P1A,P1D,P1B;
end;
end;
hence G . (a * b) = (G . a) * (G . b)
by X1,PARTFUN1:def 2,D1,FUNCT_1:2;
end;
hence thesis by GROUP_6:def 6;
end;
theorem XLM18Th41:
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 AS0:
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 AS2:
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*>;
D0: dom (Carrier F0) = I0 by PARTFUN1:def 2;
D1: dom (Carrier F) = I by PARTFUN1:def 2;
DF0: dom F0 = I0 by PARTFUN1:def 2;
A5: the carrier of product F = product Carrier F by GROUP_7:def 2;
D35: dom (q .--> K) = {q} by FUNCOP_1:13;
for x1,x2 be element 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 element;
assume BS1:
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 T1: x1 = <*h1,k1*> by TOPALG_4:1;
consider h2 be Element of H,k2 be Element of K
such that T2: x2 = <*h2,k2*> by TOPALG_4:1;
consider g1 be Function
such that T3: g1=G0.h1 & G.(<*h1,k1*>) = g1 +* (q .--> k1) by AS2;
consider g2 be Function
such that T4: g2=G0.h2 & G.(<*h2,k2*>) = g2 +* (q .--> k2) by AS2;
reconsider g1 as total I0-defined Function by XLM18Th401,T3;
reconsider g2 as total I0-defined Function by XLM18Th401,T4;
reconsider ga = g1 +* (q .--> k1)
as total I-defined Function by XLM18Th401,T3;
reconsider gb = g2 +* (q .--> k2)
as total I-defined Function by XLM18Th401,T4;
D3: dom (q .--> k1) = {q} by FUNCOP_1:13;
D4: dom (q .--> k2) = {q} by FUNCOP_1:13;
ZLM3: 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 D51: i in I0;
HG1: dom g1 = I0 by PARTFUN1:def 2;
HG2: dom g2 = I0 by PARTFUN1:def 2;
G51: i in dom g1 \/ dom (q .--> k1) by HG1,D51,XBOOLE_0:def 3;
G52: i in dom g2 \/ dom (q .--> k2) by HG2,D51,XBOOLE_0:def 3;
G54: i in dom F0 \/ dom (q .--> K) by DF0,D51,XBOOLE_0:def 3;
Q2: not i in dom (q .--> k1) by AS0,D51,FUNCOP_1:75;
Q3:not i in dom (q .--> k2) by AS0,D51,FUNCOP_1:75;
not i in dom (q .--> K) by AS0,D51,FUNCOP_1:75;
hence thesis by G54,AS0,Q2,G51,G52,FUNCT_4:def 1,Q3;
end;
YP1: dom g2 = I0 by PARTFUN1:def 2;
for x be element st x in dom g1 holds g1.x = g2.x
proof
let x be element;
assume P2: x in dom g1;
thus g1.x = ga.x by ZLM3,P2
.= g2.x by ZLM3,P2,T3,T4,T1,T2,BS1;
end;
then
YP5:G0.h1 = G0.h2 by T3,T4,FUNCT_1:2,PARTFUN1:def 2,YP1;
ga.q = k1 & gb.q = k2
proof
D51: q in {q} by TARSKI:def 1;
H1:q in dom (q .--> k1) by TARSKI:def 1,D3;
H2:q in dom (q .--> k2) by TARSKI:def 1,D4;
G51: q in dom g1 \/ dom (q .--> k1) by D3,D51,XBOOLE_0:def 3;
G52: q in dom g2 \/ dom (q .--> k2) by D4,D51,XBOOLE_0:def 3;
Q2: ga.q = (q .--> k1).q by H1,G51,FUNCT_4:def 1
.= k1 by FUNCOP_1:7,D51;
gb.q = (q .--> k2).q by H2,G52,FUNCT_4:def 1
.= k2 by FUNCOP_1:7,D51;
hence thesis by Q2;
end;
hence z1=z2 by T1,T2,YP5,AS0,FUNCT_2:19,T3,T4,BS1;
end;
then
P1: G is one-to-one by FUNCT_2:19;
for y be element st y in the carrier of product F
ex x be element st x in the carrier of product <*H,K*> & y = G.x
proof
let y be element;
assume BS1: y in the carrier of product F; then
reconsider y as total I-defined Function by XLM18Th401;
D51: q in {q} by TARSKI:def 1;
H13: q in dom (q .--> K) by TARSKI:def 1,D35;
G54: q in dom F0 \/ dom (q .--> K) by D35,D51,XBOOLE_0:def 3;
FQ: F.q = (q .--> K).q by H13,G54,AS0,FUNCT_4:def 1
.= K by FUNCOP_1:7,D51;
ex R be non empty multMagma st
R = F.q & y.q in the carrier of R by XLM18Th402,BS1; then
reconsider k=y.q as Element of K by FQ;
reconsider y0 = y|I0 as I0-defined Function;
A50: the carrier of product F0 = product (Carrier F0) by GROUP_7:def 2;
I = dom y by PARTFUN1:def 2; then
L0: dom y0 = I0 by RELAT_1:62,AS0,XBOOLE_1:7;
for i be element st i in dom Carrier F0
holds y0.i in (Carrier F0).i
proof
let i be element;
assume ASD51:i in dom Carrier F0; then
D51: i in I0;
G54: i in dom F0 \/ dom (q .--> K) by DF0,ASD51,XBOOLE_0:def 3;
AD2:not i in dom (q .--> K) by AS0,D51,FUNCOP_1:75;
AD7:I0 c= I by XBOOLE_1:7,AS0;
AD3: ex R being 1-sorted st
R = F0 . i & (Carrier F0) . i = the carrier of R
by ASD51,PRALG_1:def 13;
ex R being 1-sorted st
R = F . i & (Carrier F) . i = the carrier of R
by D51,AD7,PRALG_1:def 13; then
AD5: (Carrier F0) . i = (Carrier F) . i
by G54,FUNCT_4:def 1,AS0,AD2,AD3;
ex g be Function st y = g & dom g = dom Carrier F &
for i be element st i in dom Carrier F
holds g.i in (Carrier F).i by CARD_3:def 5,BS1,A5; then
y.i in (Carrier F).i by AD7,D1,D51;
hence y0.i in (Carrier F0).i by AD5,ASD51,FUNCT_1:49;
end; then
y0 in the carrier of (product F0) by L0,D0,CARD_3:def 5,A50; then
y0 in rng G0 by AS0,FUNCT_2:def 3; then
consider h be Element of H such that
F1: y0=G0.h by FUNCT_2:113;
X2: dom y = I by PARTFUN1:def 2; then
y|{q} = q .--> k by FUNCT_7:6; then
F2: y = y|I0 +* (q .--> k) by AS0,X2,FUNCT_4:70;
consider g be Function
such that F3: g=G0.h & G.(<*h,k*>) = g +* (q .--> k) by AS2;
thus thesis by F1,F2,F3;
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 P1;
end;
theorem LM18R0:
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 AS: F = q .--> G;
A2: 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 13,A2; then
A5: (Carrier F) . q = the carrier of G by A2,AS,FUNCOP_1:7;
A6: dom (Carrier F) = {q} by PARTFUN1:def 2;
let y be (the carrier of G)-valued total {q} -defined Function;
X1: 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;
X3: for x be element st x in dom y holds y.x = z by TARSKI:def 1;
now let i be element;
assume ASA9:i in dom y; then
A9: i = q by TARSKI:def 1;
y.i = z by TARSKI:def 1,ASA9;
hence y.i in (Carrier F) . i by A5,A9;
end;
hence thesis by X3,FUNCOP_1:11,A6,X1,CARD_3:9,A4;
end;
theorem LM18R:
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 AS: F = q .--> G;
consider I be Homomorphism of G, product F such that
P1: I is bijective &
for x being Element of G holds I . x = q .--> x by LM18R1,AS;
set HFG = I";
R1: rng I = the carrier of (product F) by P1,FUNCT_2:def 3; then
reconsider HFG as Function of product F, G by FUNCT_2:25,P1;
P3: HFG*I = id (the carrier of G)
& I*HFG = id (the carrier of (product F)) by P1,R1,FUNCT_2:29;
P5:HFG is onto by P3,FUNCT_2:23;
reconsider HFG as Homomorphism of product F,G by P1,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;
P6: y in the carrier of product F &
y.q in the carrier of G &
y= q .--> y.q by AS,LM18R0;
reconsider z=y.q as Element of G by AS,LM18R0;
X4: I . z = q .--> z by P1
.= y by AS,LM18R0;
thus HFG.y = z by FUNCT_2:26,P1,X4
.= Product y by Th49,P6;
end;
hence thesis by P5,P1;
end;
theorem LM18A1:
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 AS: not q in I0 & I = I0 \/ {q} &
F = F0 +* (q .--> K) & G0 is bijective;
set HK = <*H,K*>;
B5: 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);
A7: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 A8: z = <*h,k*> by TOPALG_4:1;
consider g be Function such that
A9: G0.h = g & dom g = dom (Carrier F0) &
for y be element st y in dom (Carrier F0)
holds g.y in (Carrier F0).y by CARD_3:def 5,B5;
set w = g +* (q .--> k);
w in the carrier of (product F) by AS,A9,LM18A12;
hence thesis by A8,A9;
end;
consider G being Function of product <*H,K*>, product F such that
A9: for x being Element of product <*H,K*>
holds P[x,G.x] from FUNCT_2:sch 3(A7);
A10: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
A100: z = <*h1,k1*> & g =G0.h1 & G.z = g +* (q .--> k1) by A9;
A102: h1 =(<*h1,k1*>).1 by FINSEQ_1:44
.= h by FINSEQ_1:44,A100;
k1 =(<*h1,k1*>).2 by FINSEQ_1:44
.= k by FINSEQ_1:44,A100;
hence thesis by A100,A102;
end;
then reconsider G as Homomorphism of product <*H,K*>,(product F)
by XLM18Th40,AS;
G is bijective by XLM18Th41,AS,A10;
hence thesis by A10;
end;
theorem LM18A:
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 AS: not q in I0 &
I = I0 \/ {q} & F = F0 +* (q .--> K) & G0 is bijective;
set L0=G0";
R1: rng G0 = the carrier of H by FUNCT_2:def 3,AS; then
reconsider L0 as Function of H, product F0 by FUNCT_2:25,AS;
P3: L0*G0 = id the carrier of product F0
& G0*L0 = id the carrier of H by AS,R1,FUNCT_2:29;
P5:L0 is onto by P3,FUNCT_2:23;
reconsider L0 as Homomorphism of H,product F0 by AS,GROUP_6:62;
consider L be Homomorphism of product <*H,K*>,(product F) such that
P6: 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 LM18A1,AS,P5;
set G=L";
GR1: rng L = the carrier of (product F) by FUNCT_2:def 3,P6;
then
reconsider G as Function of product F, product <*H,K*> by FUNCT_2:25,P6;
GP3: G * L = id (the carrier of product <*H,K*>)
& L * G = id (the carrier of (product F))
by P6,GR1,FUNCT_2:29;
GP5:G is onto by GP3,FUNCT_2:23;
reconsider G as Homomorphism of product F,(product <*H,K*>)
by P6,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 AS1: h = G0.x0 & x0 in (product F0);
consider g be Function such that
Q1: g=L0.h & L.(<*h,k*>) = g +* (q .--> k) by P6;
g = x0 by Q1,AS,AS1,FUNCT_2:26;
hence G.(x0 +* (q .--> k)) = <*h,k*> by P6,FUNCT_2:26,Q1;
end;
hence thesis by GP5,P6;
end;
theorem Th19A1:
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 AS: for p be Element of I holds x.p in F.p;
D1: dom (Carrier F) = I by PARTFUN1:def 2;
D3: the carrier of product F = product (Carrier F) by GROUP_7:def 2;
D4: dom x = I by PARTFUN1:def 2;
now let i be element;
assume A2:i in dom (Carrier F);
consider R being 1-sorted such that
A4:
R = F . i & (Carrier F) . i = the carrier of R by PRALG_1:def 13,A2;
reconsider i0=i as Element of I by A2;
x.i0 in the carrier of R by A4,STRUCT_0:def 5,AS;
hence x.i in (Carrier F) . i by A4;
end;
hence thesis by D3,D1,D4,CARD_3:def 5;
end;
theorem Th19A2:
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 AS0: not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K);
reconsider y=x as total I-defined Function by XLM18Th401;
D1: dom (Carrier F) = I by PARTFUN1:def 2;
A5: the carrier of product F = product (Carrier F) by GROUP_7:def 2;
DF0: dom F0 = I0 by PARTFUN1:def 2;
D35: dom (q .--> K) = {q} by FUNCOP_1:13;
D51: q in {q} by TARSKI:def 1;
H13: q in dom (q .--> K) by TARSKI:def 1,D35;
G54: q in dom F0 \/ dom (q .--> K) by D35,D51,XBOOLE_0:def 3;
FQ: F.q = (q .--> K).q by H13,G54,AS0,FUNCT_4:def 1
.= K by FUNCOP_1:7,D51;
ex R be non empty multMagma st
R = F.q & y.q in the carrier of R by XLM18Th402; then
reconsider k=y.q as Element of K by FQ;
reconsider y0 = y|I0 as I0-defined Function;
A50: the carrier of product F0 = product (Carrier F0) by GROUP_7:def 2;
I = dom y by PARTFUN1:def 2; then
L0: dom y0 = I0 by RELAT_1:62,AS0,XBOOLE_1:7; then
reconsider y0 as total I0-defined Function by PARTFUN1:def 2;
D0: dom (Carrier F0) = I0 by PARTFUN1:def 2;
L2: 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;
G54: i in dom F0 \/ dom (q .--> K) by DF0,XBOOLE_0:def 3;
i <> q by AS0; then
AD2:not i in dom (q .--> K) by FUNCOP_1:75;
AD7: i in I by TARSKI:def 3,XBOOLE_1:7,AS0;
consider R being 1-sorted such that
AD3: R = F0 . i & (Carrier F0) . i = the carrier of R by PRALG_1:def 13;
ex R being 1-sorted st
R = F . i & (Carrier F) . i = the carrier of R by AD7,PRALG_1:def 13;
then
AD5: (Carrier F0) . i = (Carrier F) . i
by AD2,G54,FUNCT_4:def 1,AS0,AD3;
ex g be Function st y = g & dom g = dom (Carrier F) &
for i be element st i in dom Carrier F
holds g.i in (Carrier F).i by CARD_3:def 5,A5;
then y.i in (Carrier F).i by AD7,D1;
hence thesis by AD3,FUNCT_1:49,AD5;
end;
for i be element st i in dom (Carrier F0)
holds y0.i in (Carrier F0).i by L2; then
RS1: y0 in the carrier of (product F0) by A50,L0,D0,CARD_3:def 5;
X2: dom y = I by PARTFUN1:def 2; then
y|{q} = q .--> k by FUNCT_7:6;
then y = y|I0 +* (q .--> k) by AS0,X2,FUNCT_4:70;
hence thesis by RS1,STRUCT_0:def 5,L2;
end;
theorem Th19A3A:
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;
P0:P[0]
proof
let f be FinSequence of G, g be FinSequence of H;
assume AS1:0 = len f & f=g; then
f = <*> the carrier of G; then
P2: Product f = 1_G by GROUP_4:8;
g = <*> the carrier of H by AS1;
then Product g = 1_H by GROUP_4:8;
hence thesis by P2,GROUP_2:44;
end;
PN: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume AS2: P[k];
let f be FinSequence of G,
g be FinSequence of H;
assume AS3:k+1 = len f & f=g;
X0:k+1 in Seg (k+1) by FINSEQ_1:4;
then k+1 in dom f by AS3,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 X0,AS3,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;
P3: f = f1^<* af *> by AS3,RFINSEQ:7;
P4: g = g1^<* ag *> by AS3,RFINSEQ:7;
P5: Product f = Product(f1) * af by GROUP_4:6,P3;
P6: Product g = Product(g1) * ag by GROUP_4:6,P4;
len f1 = k by FINSEQ_1:59,AS3,NAT_1:11;
then Product(f1) = Product(g1) by AS3,AS2;
hence thesis by P5,P6,GROUP_2:43,AS3;
end;
X2: for k be Nat holds P[k] from NAT_1:sch 2(P0,PN);
let f be FinSequence of G, g be FinSequence of H;
assume X3: f = g;
len f is Nat;
hence thesis by X3,X2;
end;
theorem Th19A3:
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 AS:x=x0;
consider f being FinSequence of G such that
P1: Product x = Product f & f = x*canFS(I) by Def5;
consider g being FinSequence of the carrier of H such that
P2: Product x0 = Product g & g = x0*canFS(I) by Def5;
thus thesis by P1,AS,P2,Th19A3A;
end;
theorem Th19A4:
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 AS: 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;
P1: I0 misses {q}
proof
assume I0 meets {q}; then
consider x be element such that
P2: x in I0 & x in {q} by XBOOLE_0:3;
thus contradiction by P2,AS,TARSKI:def 1;
end;
Product x = (Product x0) * (Product y) by P1,AS,Th45;
hence thesis by Th49;
end;
theorem Th19:
for G being 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 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 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 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;
P0:P[0];
P1: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume APN: P[n];
thus P[n+1]
proof
let G be finite commutative Group;
assume AS1:
card(support (prime_factorization card G)) = n+1 & n+1 <> 0;
per cases;
suppose X1:n = 0;
set f = prime_factorization card G;
P1: support (f) = support pfexp card(G) by NAT_3:def 9;
support (f) <> {} by AS1;
then
consider q be element such that
P3: q in support (f) by XBOOLE_0:def 1;
reconsider q as Prime by P1,P3,NAT_3:34;
card {q} = 1 by CARD_1:30;
then
consider q0 be element such that
X2: support prime_factorization card G = {q0} by CARD_1:29,X1,AS1;
X3: {q} = support (prime_factorization card G) by X2,TARSKI:def 1,P3;
reconsider Gq = q|^ (q |-count (card G)) as non zero Nat;
set g = prime_factorization Gq;
Q3: 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 P3,PRE_POLY:def 7;
end; then
Q31: support pfexp Gq = {q} by NAT_3:42; then
q in support pfexp Gq by TARSKI:def 1; then
Q31B:g.q = q |^ (q |-count Gq) by NAT_3:def 9;
support g = {q} by Q31,NAT_3:def 9; then
Y1: support g = support pfexp (card G) by X3,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,X3;
then p=q by TARSKI:def 1;
hence thesis by Q31B,NAT_3:25,INT_2:def 4;
end;
then
P8: Gq = Product (prime_factorization (card G))
by Y1,NAT_3:def 9,Q3
.= card G by NAT_3:61;
reconsider I = {q} as non empty finite set;
set F = q .--> G;
for y being set st y in rng F holds y is non empty multMagma
proof
let y be set;
assume y in rng F;
then consider x be element
such that D4: x in dom F & y=F.x by FUNCT_1:def 3;
thus y is non empty multMagma by FUNCOP_1:7,D4;
end; then
reconsider F as multMagma-Family of I by GROUP_7:def 1;
GG1: 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 GG11: s <> t;
s=q by TARSKI:def 1;
hence (the carrier of (F.s)) /\ (the carrier of (F.t))
={1_G} by GG11,TARSKI:def 1;
end;
XPF: for x be Element of I holds F.x is Subgroup of G &
card (F.x) = (prime_factorization card G).x
proof
let x be Element of I;
D55: (q .--> G).x = G by FUNCOP_1:7;
x in support f by TARSKI:def 1,P3; then
Q33: x in support pfexp (card G) by NAT_3:def 9;
Q34: x = q by TARSKI:def 1;
card(F.x) = card G by FUNCOP_1:7
.= f.x by Q34,Q33,NAT_3:def 9,P8;
hence thesis by D55,GROUP_2:54;
end;
AR1:for i being Element of I holds F . i is Group-like by XPF;
AR2:for i being Element of I holds F . i is associative by XPF;
for i being Element of I holds F . i is commutative by XPF;
then
reconsider F as associative Group-like commutative
multMagma-Family of I
by AR1,GROUP_7:def 6,AR2,GROUP_7:def 7,GROUP_7:def 8;
take I,F;
consider HFG be Homomorphism of product F,G such that
X4: HFG is bijective &
for x be (the carrier of G)-valued total {q} -defined Function
holds HFG.x =Product x by LM18R;
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 STRUCT_0:def 5,X4,LM18R0;
hence thesis by X3,X4,GG1,XPF;
end;
suppose NN: n <> 0;
set f = prime_factorization card G;
P0: Product f = card G by NAT_3:61;
P1: support (f) = support pfexp card(G) by NAT_3:def 9;
support (f) <> {} by AS1; then
consider q be element such that
P3: q in support (f) by XBOOLE_0:def 1;
reconsider q as Prime by P1,P3,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 P3,PRE_POLY:def 7;
end;
then
Q31: support pfexp Gq = {q} by NAT_3:42; then
q in support pfexp Gq by TARSKI:def 1; then
Q31D:g.q = q |^ (q |-count Gq) by NAT_3:def 9;
Q31B:g.q = q|^ (q |-count (card G)) by NAT_3:25,INT_2:def 4,Q31D;
Q31C: support g = {q} by Q31,NAT_3:def 9;
XQQ32: for x be element holds x in support h iff
x in (support f) \ {q}
proof
let x be element;
hereby assume Q320: x in support h; then
Q32: x in (support f) by PRE_POLY:39,TARSKI:def 3;
then
Q33: x in support pfexp (card G) by NAT_3:def 9;
not x in {q}
proof
assume x in {q};
then
Q34: 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 Q34,Q33,NAT_3:def 9
.=q |^ (q |-count (card G)) -' q |^ (q |-count (card G))
by NAT_3:25,INT_2:def 4,Q31D
.=q |^ (q |-count (card G)) - q |^ (q |-count (card G))
by XREAL_0:def 2
.= 0;
hence contradiction by Q320,PRE_POLY:def 7;
end;
hence x in (support f) \ {q} by XBOOLE_0:def 5,Q32;
end;
assume x in (support f) \ {q}; then
Q34: x in (support f) & not x in {q} by XBOOLE_0:def 5;
x in support pfexp (card G) by Q34,NAT_3:def 9; then
reconsider x0=x as Prime by NAT_3:34;
Q37:h.x0 = f.x0 -' g.x0 by PRE_POLY:def 6;
Q38: g.x0 = 0 by Q34,Q31C,PRE_POLY:def 7;
f.x0 <> 0 by Q34,PRE_POLY:def 7;
then h.x <> 0 by Q37,Q38,NAT_D:40;
hence x in (support h) by PRE_POLY:def 7;
end;
then
Q32: support h = (support f) \ {q} by TARSKI:2;
then
P5: support h misses support g by Q31C,XBOOLE_1:79;
reconsider h as bag of SetPrimes;
Q4: 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
Q34: x in (support f) & not x in {q} by XBOOLE_0:def 5,Q32;
Q37:h.x = f.x -' g.x by PRE_POLY:def 6;
g.x = 0 by Q34,Q31C,PRE_POLY:def 7;
then h.x = f.x by Q37,NAT_D:40;
hence thesis by Q34,INT_7:def 1;
end;
then
Q4X: h is prime-factorization-like by INT_7:def 1;
Q41: {q} c= support (f) by P3,ZFMISC_1:31;
Q42: support h c= support f by XBOOLE_1:36,Q32;
Q43: (support h) \/ {q} = support f
by P3,ZFMISC_1:31,Q32,XBOOLE_1:45;
for x being element st x in SetPrimes holds
f . x = (h . x) + (g . x)
proof
let x be element;
assume x in SetPrimes;
per cases;
suppose P41: not x in support f;
then
P42: not x in support h by Q42;
P43: not x in support g by Q31C,Q41,P41;
thus f . x = (0 qua Real) by PRE_POLY:def 7,P41
.= (h . x) + (0 qua Real) by PRE_POLY:def 7,P42
.= (h . x) + (g . x) by PRE_POLY:def 7,P43;
end;
suppose R44: x in support f;
Q33: x in support pfexp (card G) by R44,NAT_3:def 9;
thus f . x = (h . x) + (g . x)
proof
per cases by R44,Q43,XBOOLE_0:def 3;
suppose x in (support h); then
Q34:x in (support f) & not x in {q}
by Q32,XBOOLE_0:def 5;
x in support pfexp (card G) by Q34,NAT_3:def 9; then
reconsider x0=x as Prime by NAT_3:34;
Q37:h.x0 = f.x0 -' g.x0 by PRE_POLY:def 6;
g.x0 = 0 by Q34,Q31C,PRE_POLY:def 7;
hence thesis by Q37,NAT_D:40;
end;
suppose x in {q};
then
Q34: x = q by TARSKI:def 1;
R34:h.x =f.q -' g.q by Q34,PRE_POLY:def 6;
f.q = q |^ (q |-count (card G)) by Q34,Q33,NAT_3:def 9;
then
h.x = f.q - g.q by R34,XREAL_0:def 2,Q31B;
hence thesis by Q34;
end;
end;
end;
end;
then h + g = f by PRE_POLY:33;
then
P6: Product f = (Product h) * Product g
by Q31C,XBOOLE_1:79,Q32,NAT_3:19;
Product h is non zero & Product g is non zero by P6,NAT_3:61;
then
consider H,K being strict finite Subgroup of G such that
P8:
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 P0,P6,LM18,Q4X,P5,INT_7:12;
reconsider H, K as finite commutative Group;
P10: support prime_factorization card H = support h
by INT_7:16,INT_7:def 1,Q4,P8;
card(support prime_factorization card H)
= card (support h) by INT_7:16,INT_7:def 1,Q4,P8
.=card (support f) - card{q} by Q32,P3,EULER_1:4
.= n+1 -1 by AS1,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 P12:
I0 = support (prime_factorization card H)
& (for p be Element of I0 holds F0.p is 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 APN,NN;
set I = I0 \/ {q};
reconsider I as non empty finite set;
P2100:Product (prime_factorization card H)
= Product h by P8,NAT_3:61; then
P120: prime_factorization card H = h by Q4X,INT_7:15;
P14: I = support (prime_factorization card G)
by P12,Q43,Q4X,INT_7:15,P2100;
set F = F0 +* (q .--> K);
D2: dom (q .--> K) = {q} by FUNCOP_1:13;
D1: dom F = dom F0 \/ dom (q .--> K) by FUNCT_4:def 1
.= I0 \/ dom (q .--> K) by PARTFUN1:def 2
.= I0 \/ {q} by FUNCOP_1:13;
then
reconsider F as I -defined Function by RELAT_1:def 18;
reconsider F as ManySortedSet of I by PARTFUN1:def 2,D1;
for y being set st y in rng F holds y is non empty multMagma
proof
let y be set;
assume y in rng F; then
consider x be element
such that D4: x in dom F & y=F.x by FUNCT_1:def 3;
F5: x in dom F0 \/ dom (q .--> K) by D4,FUNCT_4:def 1;
D6: I0 = support h by INT_7:16,INT_7:def 1,Q4,P8,P12
.= (support f) \ {q} by TARSKI:2,XQQ32;
per cases by XBOOLE_0:def 3,D4;
suppose D51: x in I0; then
not x in dom (q .--> K) by D6,XBOOLE_0:def 5; then
D52: F.x = F0.x by FUNCT_4:def 1,F5;
x in dom F0 by D51,PARTFUN1:def 2; then
F0.x in rng F0 by FUNCT_1:3;
hence y is non empty multMagma by D52,D4,GROUP_7:def 1;
end;
suppose D52: x in {q}; then
F.x = (q .--> K).x by FUNCT_4:def 1,F5,D2;
hence y is non empty multMagma by D4,D52,FUNCOP_1:7;
end;
end; then
reconsider F as multMagma-Family of I by GROUP_7:def 1;
XPF: for x be Element of I holds F.x is Subgroup of G &
card (F.x) = (prime_factorization card G).x
proof
let x be Element of I;
D4: x in dom F by D1;
F5: x in dom F0 \/ dom (q .--> K) by D4,FUNCT_4:def 1;
D6: I0 = support h by INT_7:16,INT_7:def 1,Q4,P8,P12
.= (support f) \ {q} by XQQ32,TARSKI:2;
per cases by XBOOLE_0:def 3;
suppose D51: x in I0;
then
not x in dom (q .--> K) by D6,XBOOLE_0:def 5; then
D52: F.x = F0.x by FUNCT_4:def 1,F5;
reconsider p = x as Element of I0 by D51;
D53: F0.p is Subgroup of H &
card (F0.p) = (prime_factorization card H).p by P12;
Q34:x in (support f) & not x in {q}
by Q32,XBOOLE_0:def 5,P10,P12,D51;
x in support pfexp card G by Q34,NAT_3:def 9; then
reconsider x0=x as Prime by NAT_3:34;
Q37:h.x0 = f.x0 -' g.x0 by PRE_POLY:def 6;
g.x0 = 0 by Q34,Q31C,PRE_POLY:def 7;
hence F.x is Subgroup of G &
card (F.x) = (prime_factorization card G).x
by D52,D53,GROUP_2:56,P120,Q37,NAT_D:40;
end;
suppose D52: x in {q}; then
D55:F.x = (q .--> K).x by FUNCT_4:def 1,F5,D2;
x in support f by D52,Q41; then
Q33: x in support pfexp (card G) by NAT_3:def 9;
Q34: x = q by TARSKI:def 1,D52;
card(F.x) = (Product g) by P8,D52,FUNCOP_1:7,D55
.= Gq by NAT_3:61
.= f.x by Q34,Q33,NAT_3:def 9;
hence F.x is Subgroup of G &
card (F.x) = (prime_factorization card G).x
by D55,D52,FUNCOP_1:7;
end;
end;
AR1:for i being Element of I holds F . i is Group-like by XPF;
AR2:for i being Element of I holds F . i is associative by XPF;
for i being Element of I holds F . i is commutative by XPF;
then
reconsider F as associative Group-like commutative
multMagma-Family of I by AR1,GROUP_7:def 6,
AR2,GROUP_7:def 7,GROUP_7:def 8;
consider FHKG being Homomorphism of product <*H,K*>,G such that
XX1: FHKG is bijective
& for a,b be Element of G
st a in H & b in K holds FHKG.(<*a,b*>) = a*b by P8;
D6: I0 = support h by INT_7:16,INT_7:def 1,Q4,P8,P12
.= (support f) \ {q} by TARSKI:2,XQQ32
.= I \ {q} by P12,Q43,Q4X,INT_7:15,P2100;
NU1: not q in I0
proof
assume q in I0; then
q in I & not q in {q} by D6,XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1;
end; then
consider FHK be Homomorphism of (product F), product <*H,K*>
such that
D7: 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 LM18A,P12,P3,P14;
reconsider HFG = FHKG*FHK as Function of (product F), G;
XX2: HFG is onto by FUNCT_2:27,XX1,D7;
reconsider HFG as Homomorphism of (product F), G;
DX2: 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 U1: for p be Element of I holds x.p in F.p; then
x in the carrier of product F by Th19A1; then
consider x0 be total I0 -defined Function,
k be Element of K such that
U3: x0 in product F0 & x = x0 +* (q .-->k) &
for p be Element of I0 holds
x0.p in F0.p by Th19A2,NU1,P3,P14;
reconsider h = HFG0.x0 as Element of H by FUNCT_2:5,U3;
reconsider hh=h,kk=k as Element of G by GROUP_2:42;
now let y be element;
assume y in rng x0; then
consider z be element such that
DX11: z in dom x0 & y=x0.z by FUNCT_1:def 3;
reconsider z as Element of I0 by DX11;
DX13: x0.z in F0.z by U3;
F0.z is Subgroup of H by P12;
hence y in the carrier of H
by DX11,STRUCT_0:def 5,DX13,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;
U5: HFG0.x0 =Product x0 by P12,U3;
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;
U50: Product x0 = Product xx0 by Th19A3;
thus x in product F by Th19A1,U1;
U6: hh in H & kk in K;
thus HFG.x = FHKG.(FHK.x) by FUNCT_2:15,Th19A1,U1
.= FHKG.(<* hh, kk *>) by D7,U3
.= hh*kk by XX1,U6
.= Product x by U5,U50,Th19A4,NU1,P3,P14,U3;
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 AA1: s <> t;
dom F = I by PARTFUN1:def 2; then
D4: 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;
F5: s in dom F0 \/ dom (q .--> K) by D4,FUNCT_4:def 1;
K5: t in dom F0 \/ dom (q .--> K) by D4,FUNCT_4:def 1;
D6: I0 = support h by INT_7:16,INT_7:def 1,Q4,P8,P12
.= (support f) \ {q} by TARSKI:2,XQQ32;
then
not ss in dom (q .--> K) by XBOOLE_0:def 5;
then
D52: F.ss = F0.ss by FUNCT_4:def 1,F5;
not tt in dom (q .--> K) by D6,XBOOLE_0:def 5;
then
K52: F.tt = F0.tt by FUNCT_4:def 1,K5;
(the carrier of (F0.ss))
/\ (the carrier of (F0.tt)) ={1_H} by P12,AA1;
hence (the carrier of (F.s))
/\ (the carrier of (F.t)) ={1_G} by D52,K52,GROUP_2:44;
end;
suppose AA3:not (s in I0 & t in I0);
thus (the carrier of (F.s)) /\ (the carrier of (F.t)) ={1_G}
proof
per cases by AA3;
suppose AA31: not s in I0;
F5: s in dom F0 \/ dom (q .--> K)
by D4,FUNCT_4:def 1;
D52: s in {q} by AA31,D6,XBOOLE_0:def 5; then
F.s = (q .--> K).s by FUNCT_4:def 1,F5,D2; then
D55: F.s = K by D52,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,D6;
then t=q by TARSKI:def 1;
hence contradiction by AA1,TARSKI:def 1,D52;
end;
then
reconsider tt =t as Element of I0;
K5: tt in dom F0 \/ dom (q .--> K)
by D4,FUNCT_4:def 1;
I0 = support h by INT_7:16,INT_7:def 1,Q4,P8,P12
.= (support f) \ {q} by TARSKI:2,XQQ32;
then
not tt in dom (q .--> K) by XBOOLE_0:def 5;
then
K52: F.tt = F0.tt by FUNCT_4:def 1,K5;
reconsider S1=F0.tt as Subgroup of H by P12;
K55: (the carrier of K) /\ (the carrier of S1)
c= {1_G} by P8,XBOOLE_1:26,GROUP_2:def 5;
K56: 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,K56; 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 D55,K52,K55,XBOOLE_0:def 10;
end;
suppose AA32: not t in I0;
F5: t in dom F0 \/ dom (q .--> K) by D4,FUNCT_4:def 1;
D52: t in {q} by AA32,D6,XBOOLE_0:def 5; then
F.t = (q .--> K).t by FUNCT_4:def 1,F5,D2; then
D55: F.t = K by D52,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,D6; then
s=q by TARSKI:def 1;
hence contradiction by AA1,TARSKI:def 1,D52;
end;
then
reconsider ss = s as Element of I0;
K5: ss in dom F0 \/ dom (q .--> K)
by D4,FUNCT_4:def 1;
I0 = support h by INT_7:16,INT_7:def 1,Q4,P8,P12
.= (support f) \ {q} by XQQ32,TARSKI:2;
then
not ss in dom (q .--> K) by XBOOLE_0:def 5; then
K52: F.ss = F0.ss by FUNCT_4:def 1,K5;
reconsider S1=F0.ss as Subgroup of H by P12;
K55: (the carrier of K) /\ (the carrier of S1)
c= {1_G} by P8,XBOOLE_1:26,GROUP_2:def 5;
K56: 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,K56; 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 D55,K52,K55,XBOOLE_0:def 10;
end;
end;
end;
end;
hence thesis by P14,XPF,XX2,XX1,D7,DX2;
end;
end;
end;
P2: for k be Nat holds P[k] from NAT_1:sch 2(P0,P1);
let G be finite commutative Group;
assume P3: 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 P3,NAT_3:57;
end;
hence thesis by P2;
end;
theorem
for G being 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 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 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
P1:
I = support (prime_factorization card G)
& (for p be Element of I holds F.p is 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 Th19;
P4: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 P1,FUNCT_2:def 3;
then
consider x be element such that
P2: x in the carrier of product F & y = HFG.x by FUNCT_2:11;
reconsider x as total I-defined Function by P2,XLM18Th401;
P3: 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
P4: R = F.p & x.p in the carrier of R by XLM18Th402,P2;
thus x.p in (F.p) by P4;
end;
rng x c= the carrier of G
proof
let y be element;
assume y in rng x; then
consider i be element such that
D2: i in dom x & y=x.i by FUNCT_1:def 3;
reconsider i as Element of I by D2;
consider R be non empty multMagma such that
P4: R = F.i & x.i in the carrier of R by P2,XLM18Th402;
F.i is Subgroup of G by P1; then
the carrier of (F.i) c= the carrier of G by GROUP_2:def 5;
hence y in the carrier of G by D2,P4;
end;
then
reconsider x as (the carrier of G)-valued
total I -defined Function by RELAT_1:def 19,TARSKI:def 3;
take x;
thus thesis by P1,P2,P3;
end;
now let x1,x2 be (the carrier of G)-valued total I -defined Function;
assume AS2:
(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 AS2,P1; then
P4: HFG.x1 = HFG.x2 by AS2,P1;
x1 in the carrier of product F &
x2 in the carrier of product F by AS2,P1,STRUCT_0:def 5;
hence x1=x2 by P4,P1,FUNCT_2:19;
end;
hence thesis by P1,P4;
end;