defpred S1[ Nat] means for G being finite strict commutative Group st card (support (prime_factorization (card G))) = $1 & $1 <> 0 holds
ex I being non empty finite set ex F being Group-like associative commutative multMagma-Family of I ex HFG being Homomorphism of (product F),G st
( I = support (prime_factorization (card G)) & ( for p being Element of I holds
( F . p is strict Subgroup of G & card (F . p) = (prime_factorization (card G)) . p ) ) & ( for p, q being Element of I st p <> q holds
the carrier of (F . p) /\ the carrier of (F . q) = {(1_ G)} ) & HFG is bijective & ( for x being b2 -defined the carrier of b1 -valued total Function st ( for p being Element of I holds x . p in F . p ) holds
( x in product F & HFG . x = Product x ) ) );
A1:
S1[ 0 ]
;
A2:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A3:
S1[
n]
;
S1[n + 1]
thus
S1[
n + 1]
verumproof
let G be
finite strict commutative Group;
( card (support (prime_factorization (card G))) = n + 1 & n + 1 <> 0 implies ex I being non empty finite set ex F being Group-like associative commutative multMagma-Family of I ex HFG being Homomorphism of (product F),G st
( I = support (prime_factorization (card G)) & ( for p being Element of I holds
( F . p is strict Subgroup of G & card (F . p) = (prime_factorization (card G)) . p ) ) & ( for p, q being Element of I st p <> q holds
the carrier of (F . p) /\ the carrier of (F . q) = {(1_ G)} ) & HFG is bijective & ( for x being b1 -defined the carrier of G -valued total Function st ( for p being Element of I holds x . p in F . p ) holds
( x in product F & HFG . x = Product x ) ) ) )
assume A4:
(
card (support (prime_factorization (card G))) = n + 1 &
n + 1
<> 0 )
;
ex I being non empty finite set ex F being Group-like associative commutative multMagma-Family of I ex HFG being Homomorphism of (product F),G st
( I = support (prime_factorization (card G)) & ( for p being Element of I holds
( F . p is strict Subgroup of G & card (F . p) = (prime_factorization (card G)) . p ) ) & ( for p, q being Element of I st p <> q holds
the carrier of (F . p) /\ the carrier of (F . q) = {(1_ G)} ) & HFG is bijective & ( for x being b1 -defined the carrier of G -valued total Function st ( for p being Element of I holds x . p in F . p ) holds
( x in product F & HFG . x = Product x ) ) )
per cases
( n = 0 or n <> 0 )
;
suppose A5:
n = 0
;
ex I being non empty finite set ex F being Group-like associative commutative multMagma-Family of I ex HFG being Homomorphism of (product F),G st
( I = support (prime_factorization (card G)) & ( for p being Element of I holds
( F . p is strict Subgroup of G & card (F . p) = (prime_factorization (card G)) . p ) ) & ( for p, q being Element of I st p <> q holds
the carrier of (F . p) /\ the carrier of (F . q) = {(1_ G)} ) & HFG is bijective & ( for x being b1 -defined the carrier of G -valued total Function st ( for p being Element of I holds x . p in F . p ) holds
( x in product F & HFG . x = Product x ) ) )set f =
prime_factorization (card G);
A6:
support (prime_factorization (card G)) = support (pfexp (card G))
by NAT_3:def 9;
support (prime_factorization (card G)) <> {}
by A4;
then consider q being
object such that A7:
q in support (prime_factorization (card G))
by XBOOLE_0:def 1;
reconsider q =
q as
Prime by A6, A7, NAT_3:34;
card {q} = 1
by CARD_1:30;
then consider q0 being
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 (prime_factorization Gq) = Gq
by NAT_3:61;
q |-count (card G) <> 0
then A11:
support (pfexp Gq) = {q}
by NAT_3:42;
then
q in support (pfexp Gq)
by TARSKI:def 1;
then A12:
(prime_factorization Gq) . q = q |^ (q |-count Gq)
by NAT_3:def 9;
support (prime_factorization Gq) = {q}
by A11, NAT_3:def 9;
then A13:
support (prime_factorization Gq) = support (pfexp (card G))
by A9, NAT_3:def 9;
for
p being
Nat st
p in support (pfexp (card G)) holds
(prime_factorization Gq) . p = p |^ (p |-count (card G))
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;
for
y being
set st
y in rng (q .--> G) holds
y is non
empty multMagma
then reconsider F =
q .--> G as
multMagma-Family of
I by GROUP_7:def 1;
A16:
for
s,
t being
Element of
I st
s <> t holds
the
carrier of
(F . s) /\ the
carrier of
(F . t) = {(1_ G)}
A18:
for
x being
Element of
I holds
(
F . x is
strict Subgroup of
G &
card (F . x) = (prime_factorization (card G)) . x )
A22:
for
i being
Element of
I holds
F . i is
Group-like
;
A23:
for
i being
Element of
I holds
F . i is
associative
;
for
i being
Element of
I holds
F . i is
commutative
;
then reconsider F =
F as
Group-like associative commutative multMagma-Family of
I by A22, GROUP_7:def 6, A23, GROUP_7:def 7, GROUP_7:def 8;
take
I
;
ex F being Group-like associative commutative multMagma-Family of I ex HFG being Homomorphism of (product F),G st
( I = support (prime_factorization (card G)) & ( for p being Element of I holds
( F . p is strict Subgroup of G & card (F . p) = (prime_factorization (card G)) . p ) ) & ( for p, q being Element of I st p <> q holds
the carrier of (F . p) /\ the carrier of (F . q) = {(1_ G)} ) & HFG is bijective & ( for x being I -defined the carrier of G -valued total Function st ( for p being Element of I holds x . p in F . p ) holds
( x in product F & HFG . x = Product x ) ) )take
F
;
ex HFG being Homomorphism of (product F),G st
( I = support (prime_factorization (card G)) & ( for p being Element of I holds
( F . p is strict Subgroup of G & card (F . p) = (prime_factorization (card G)) . p ) ) & ( for p, q being Element of I st p <> q holds
the carrier of (F . p) /\ the carrier of (F . q) = {(1_ G)} ) & HFG is bijective & ( for x being I -defined the carrier of G -valued total Function st ( for p being Element of I holds x . p in F . p ) holds
( x in product F & HFG . x = Product x ) ) )consider HFG being
Homomorphism of
(product F),
G such that A24:
(
HFG is
bijective & ( for
x being
{q} -defined the
carrier of
G -valued total Function holds
HFG . x = Product x ) )
by Th26;
for
x being
I -defined the
carrier of
G -valued total Function st ( for
p being
Element of
I holds
x . p in F . p ) holds
(
x in product F &
HFG . x = Product x )
by A24, Th25;
hence
ex
HFG being
Homomorphism of
(product F),
G st
(
I = support (prime_factorization (card G)) & ( for
p being
Element of
I holds
(
F . p is
strict Subgroup of
G &
card (F . p) = (prime_factorization (card G)) . p ) ) & ( for
p,
q being
Element of
I st
p <> q holds
the
carrier of
(F . p) /\ the
carrier of
(F . q) = {(1_ G)} ) &
HFG is
bijective & ( for
x being
I -defined the
carrier of
G -valued total Function st ( for
p being
Element of
I holds
x . p in F . p ) holds
(
x in product F &
HFG . x = Product x ) ) )
by A9, A24, A16, A18;
verum end; suppose A25:
n <> 0
;
ex I being non empty finite set ex F being Group-like associative commutative multMagma-Family of I ex HFG being Homomorphism of (product F),G st
( I = support (prime_factorization (card G)) & ( for p being Element of I holds
( F . p is strict Subgroup of G & card (F . p) = (prime_factorization (card G)) . p ) ) & ( for p, q being Element of I st p <> q holds
the carrier of (F . p) /\ the carrier of (F . q) = {(1_ G)} ) & HFG is bijective & ( for x being b1 -defined the carrier of G -valued total Function st ( for p being Element of I holds x . p in F . p ) holds
( x in product F & HFG . x = Product x ) ) )set f =
prime_factorization (card G);
A26:
Product (prime_factorization (card G)) = card G
by NAT_3:61;
A27:
support (prime_factorization (card G)) = support (pfexp (card G))
by NAT_3:def 9;
support (prime_factorization (card G)) <> {}
by A4;
then consider q being
object such that A28:
q in support (prime_factorization (card G))
by XBOOLE_0:def 1;
reconsider q =
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 =
(prime_factorization (card G)) -' (prime_factorization Gq);
q |-count (card G) <> 0
then A29:
support (pfexp Gq) = {q}
by NAT_3:42;
then
q in support (pfexp Gq)
by TARSKI:def 1;
then A30:
(prime_factorization Gq) . q = q |^ (q |-count Gq)
by NAT_3:def 9;
A31:
(prime_factorization Gq) . q = q |^ (q |-count (card G))
by NAT_3:25, INT_2:def 4, A30;
A32:
support (prime_factorization Gq) = {q}
by A29, NAT_3:def 9;
A33:
for
x being
object holds
(
x in support ((prime_factorization (card G)) -' (prime_factorization Gq)) iff
x in (support (prime_factorization (card G))) \ {q} )
then A41:
support ((prime_factorization (card G)) -' (prime_factorization Gq)) = (support (prime_factorization (card G))) \ {q}
by TARSKI:2;
then A42:
support ((prime_factorization (card G)) -' (prime_factorization Gq)) misses support (prime_factorization Gq)
by A32, XBOOLE_1:79;
reconsider h =
(prime_factorization (card G)) -' (prime_factorization Gq) as
bag of
SetPrimes ;
A43:
for
x being
Prime st
x in support h holds
ex
n being
Nat st
(
0 < n &
h . x = x |^ n )
then A46:
h is
prime-factorization-like
by INT_7:def 1;
A47:
{q} c= support (prime_factorization (card G))
by A28, ZFMISC_1:31;
A48:
support h c= support (prime_factorization (card G))
by XBOOLE_1:36, A41;
A49:
(support h) \/ {q} = support (prime_factorization (card G))
by A28, ZFMISC_1:31, A41, XBOOLE_1:45;
for
x being
object st
x in SetPrimes holds
(prime_factorization (card G)) . x = (h . x) + ((prime_factorization Gq) . x)
then
h + (prime_factorization Gq) = prime_factorization (card G)
by PRE_POLY:33;
then A59:
Product (prime_factorization (card G)) = (Product h) * (Product (prime_factorization Gq))
by A32, XBOOLE_1:79, A41, NAT_3:19;
( not
Product h is
zero & not
Product (prime_factorization Gq) is
zero )
by A59, NAT_3:61;
then consider H,
K being
finite strict Subgroup of
G such that A60:
(
card H = Product h &
card K = Product (prime_factorization Gq) & 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 being
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 =
H,
K =
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 (prime_factorization (card G)))) - (card {q})
by A41, A28, EULER_1:4
.=
(n + 1) - 1
by A4, CARD_1:30
.=
n
;
then consider I0 being non
empty finite set ,
F0 being
Group-like associative commutative multMagma-Family of
I0,
HFG0 being
Homomorphism of
(product F0),
H such that A62:
(
I0 = support (prime_factorization (card H)) & ( for
p being
Element of
I0 holds
(
F0 . p is
strict Subgroup of
H &
card (F0 . p) = (prime_factorization (card H)) . p ) ) & ( for
p,
q being
Element of
I0 st
p <> q holds
the
carrier of
(F0 . p) /\ the
carrier of
(F0 . q) = {(1_ H)} ) &
HFG0 is
bijective & ( for
x being
I0 -defined the
carrier of
H -valued total Function st ( for
p being
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 =
I0 \/ {q} 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 (F0 +* (q .--> K)) =
(dom F0) \/ (dom (q .--> K))
by FUNCT_4:def 1
.=
I0 \/ (dom (q .--> K))
by PARTFUN1:def 2
.=
I0 \/ {q}
;
then reconsider F =
F0 +* (q .--> K) as
I -defined Function by RELAT_1:def 18;
reconsider F =
F as
ManySortedSet of
I by PARTFUN1:def 2, A67;
for
y being
set st
y in rng F holds
y is non
empty multMagma
then reconsider F =
F as
multMagma-Family of
I by GROUP_7:def 1;
A74:
for
x being
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;
( F . x is strict Subgroup of G & card (F . x) = (prime_factorization (card G)) . x )
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 (prime_factorization (card G))) \ {q}
by A33, TARSKI:2
;
per cases
( x in I0 or x in {q} )
by XBOOLE_0:def 3;
suppose A78:
x in I0
;
( F . x is strict Subgroup of G & card (F . x) = (prime_factorization (card G)) . x )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 (prime_factorization (card G)) & 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 = ((prime_factorization (card G)) . x0) -' ((prime_factorization Gq) . x0)
by PRE_POLY:def 6;
(prime_factorization Gq) . 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;
verum end; suppose A83:
x in {q}
;
( F . x is strict Subgroup of G & card (F . x) = (prime_factorization (card G)) . x )then A84:
F . x = (q .--> K) . x
by FUNCT_4:def 1, A76;
x in support (prime_factorization (card G))
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 (prime_factorization Gq)
by A60, A83, FUNCOP_1:7, A84
.=
Gq
by NAT_3:61
.=
(prime_factorization (card G)) . 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;
verum end; 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 =
F as
Group-like associative 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 being
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 (prime_factorization (card G))) \ {q}
by TARSKI:2, A33
.=
I \ {q}
by A62, A49, A46, INT_7:15, A63
;
A91:
not
q in I0
then consider FHK being
Homomorphism of
(product F),
(product <*H,K*>) such that A92:
(
FHK is
bijective & ( for
x0 being
Function for
k being
Element of
K for
h being
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 =
HFG as
Homomorphism of
(product F),
G ;
A94:
for
x being
I -defined the
carrier of
G -valued total Function st ( for
p being
Element of
I holds
x . p in F . p ) holds
(
x in product F &
HFG . x = Product x )
proof
let x be
I -defined the
carrier of
G -valued total Function;
( ( for p being Element of I holds x . p in F . p ) implies ( x in product F & HFG . x = Product x ) )
assume A95:
for
p being
Element of
I holds
x . p in F . p
;
( x in product F & HFG . x = Product x )
then
x in the
carrier of
(product F)
by Th29;
then consider x0 being
I0 -defined total Function,
k being
Element of
K such that A96:
(
x0 in product F0 &
x = x0 +* (q .--> k) & ( for
p being
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;
then reconsider x0 =
x0 as
I0 -defined the
carrier of
H -valued total 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
I0 -defined the
carrier of
G -valued total Function by RELAT_1:def 19;
A100:
Product x0 = Product xx0
by Th32;
thus
x in product F
by Th29, A95;
HFG . x = Product x
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
;
verum
end;
for
s,
t being
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 <> t implies the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)} )
assume A102:
s <> t
;
the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)}
dom F = I
by PARTFUN1:def 2;
then A103:
(
s in dom F &
t in dom F )
;
per cases
( ( s in I0 & t in I0 ) or not s in I0 or not t in I0 )
;
suppose
(
s in I0 &
t in I0 )
;
the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)}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 (prime_factorization (card G))) \ {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;
verum end; suppose A109:
( not
s in I0 or not
t in I0 )
;
the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)}thus
the
carrier of
(F . s) /\ the
carrier of
(F . t) = {(1_ G)}
verumproof
per cases
( not s in I0 or not t in I0 )
by A109;
suppose A110:
not
s in I0
;
the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)}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
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 (prime_factorization (card G))) \ {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;
verum end; suppose A118:
not
t in I0
;
the carrier of (F . s) /\ the carrier of (F . t) = {(1_ G)}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
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 (prime_factorization (card G))) \ {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;
verum end; end;
end; end; end;
end; hence
ex
I being non
empty finite set ex
F being
Group-like associative commutative multMagma-Family of
I ex
HFG being
Homomorphism of
(product F),
G st
(
I = support (prime_factorization (card G)) & ( for
p being
Element of
I holds
(
F . p is
strict Subgroup of
G &
card (F . p) = (prime_factorization (card G)) . p ) ) & ( for
p,
q being
Element of
I st
p <> q holds
the
carrier of
(F . p) /\ the
carrier of
(F . q) = {(1_ G)} ) &
HFG is
bijective & ( for
x being
b1 -defined the
carrier of
G -valued total Function st ( for
p being
Element of
I holds
x . p in F . p ) holds
(
x in product F &
HFG . x = Product x ) ) )
by A65, A74, A93, A89, A92, A94;
verum end; end;
end;
end;
A126:
for k being Nat holds S1[k]
from NAT_1:sch 2(A1, A2);
let G be finite strict commutative Group; ( card G > 1 implies ex I being non empty finite set ex F being Group-like associative commutative multMagma-Family of I ex HFG being Homomorphism of (product F),G st
( I = support (prime_factorization (card G)) & ( for p being Element of I holds
( F . p is strict Subgroup of G & card (F . p) = (prime_factorization (card G)) . p ) ) & ( for p, q being Element of I st p <> q holds
the carrier of (F . p) /\ the carrier of (F . q) = {(1_ G)} ) & HFG is bijective & ( for x being b1 -defined the carrier of G -valued total Function st ( for p being Element of I holds x . p in F . p ) holds
( x in product F & HFG . x = Product x ) ) ) )
assume A127:
card G > 1
; ex I being non empty finite set ex F being Group-like associative commutative multMagma-Family of I ex HFG being Homomorphism of (product F),G st
( I = support (prime_factorization (card G)) & ( for p being Element of I holds
( F . p is strict Subgroup of G & card (F . p) = (prime_factorization (card G)) . p ) ) & ( for p, q being Element of I st p <> q holds
the carrier of (F . p) /\ the carrier of (F . q) = {(1_ G)} ) & HFG is bijective & ( for x being b1 -defined the carrier of G -valued total Function st ( for p being Element of I holds x . p in F . p ) holds
( x in product F & HFG . x = Product x ) ) )
card (support (prime_factorization (card G))) <> 0
hence
ex I being non empty finite set ex F being Group-like associative commutative multMagma-Family of I ex HFG being Homomorphism of (product F),G st
( I = support (prime_factorization (card G)) & ( for p being Element of I holds
( F . p is strict Subgroup of G & card (F . p) = (prime_factorization (card G)) . p ) ) & ( for p, q being Element of I st p <> q holds
the carrier of (F . p) /\ the carrier of (F . q) = {(1_ G)} ) & HFG is bijective & ( for x being b1 -defined the carrier of G -valued total Function st ( for p being Element of I holds x . p in F . p ) holds
( x in product F & HFG . x = Product x ) ) )
by A126; verum