:: Isomorphisms of Direct Products of Finite Commutative Groups
:: by Hiroyuki Okazaki , Hiroshi Yamazaki and Yasunari Shidama
::
:: Received January 31, 2013
:: Copyright (c) 2013-2021 Association of Mizar Users

theorem Th1: :: GROUP_17:1

for A, B, A1, B1 being set st A misses B & A1 c= A & B1 c= B & A1 \/ B1 = A \/ B holds
( A1 = A & B1 = B )

proof end;

theorem Th2: :: GROUP_17:2

for H, K being non empty finite set holds card (product <*H,K*>) = (card H) * (card K)

proof end;

theorem Th3: :: GROUP_17:3

for ps, pt, f being bag of SetPrimes
for q being Nat st support ps misses support pt & f = ps + pt & q in support ps holds
ps . q = f . q

proof end;

theorem Th4: :: GROUP_17:4

for ps, pt, f being bag of SetPrimes
for q being Nat st support ps misses support pt & f = ps + pt & q in support pt holds
pt . q = f . q

proof end;

Lm1: for ps, pt, f being 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 end;

theorem Th5: :: GROUP_17:5

for h being non zero Nat
for q being Prime st not q,h are_coprime holds
q divides h

proof end;

theorem Th6: :: GROUP_17:6

for h, s being non zero Nat st ( for q being Prime st q in support (prime_factorization s) holds
not q,h are_coprime ) holds
support (prime_factorization s) c= support (prime_factorization h)

proof end;

theorem Th7: :: GROUP_17:7

for h, k, s, t being non zero Nat st h,k are_coprime & s * t = h * k & ( for q being Prime st q in support (prime_factorization s) holds
not q,h are_coprime ) & ( for q being Prime st q in support (prime_factorization t) holds
not q,k are_coprime ) holds
( s = h & t = k )

proof end;

Lm2: for G being non empty multMagma
for I being non empty finite set
for b being b₂ -defined the carrier of b₁ -valued total Function holds
( b * (canFS I) is FinSequence of G & dom (b * (canFS I)) = Seg (card I) )

proof end;

Lm3: for A, B being non empty finite set st A misses B holds
( (canFS A) ^ (canFS B) is one-to-one onto FinSequence of A \/ B & dom ((canFS A) ^ (canFS B)) = Seg (card (A \/ B)) )

proof end;

Lm4: for A, B being non empty finite set
for FA being b₁ -defined total Function
for FB being b₂ -defined total Function
for f, g being FinSequence
for FAB being b₁ \/ 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 end;

definition

let G be non empty multMagma ;
let I be finite set ;
let b be I -defined the carrier of G -valued total Function;

func Product b -> Element of G means :Def1: :: GROUP_17:def 1
ex f being FinSequence of G st
( it = Product f & f = b * (canFS I) );

existence
ex b₁ being Element of G ex f being FinSequence of G st
( b₁ = Product f & f = b * (canFS I) )

proof end;

uniqueness
for b₁, b₂ being Element of G st ex f being FinSequence of G st
( b₁ = Product f & f = b * (canFS I) ) & ex f being FinSequence of G st
( b₂ = Product f & f = b * (canFS I) ) holds
b₁ = b₂ ;

end;

:: deftheorem Def1 defines Product GROUP_17:def 1 :
for G being non empty multMagma
for I being finite set
for b being b₂ -defined the carrier of b₁ -valued total Function
for b₄ being Element of G holds
( b₄ = Product b iff ex f being FinSequence of G st
( b₄ = Product f & f = b * (canFS I) ) );

theorem Th8: :: GROUP_17:8

for G being commutative Group
for A, B being non empty finite set
for FA being b₂ -defined the carrier of b₁ -valued total Function
for FB being b₃ -defined the carrier of b₁ -valued total Function
for FAB being b₂ \/ b₃ -defined the carrier of b₁ -valued total Function st A misses B & FAB = FA +* FB holds
Product FAB = (Product FA) * (Product FB)

proof end;

theorem Th9: :: GROUP_17:9

for G being non empty multMagma
for q being set
for z being Element of G
for f being {b₂} -defined the carrier of b₁ -valued total Function st f = q .--> z holds
Product f = z

proof end;

theorem Th10: :: GROUP_17:10

for X, Y being non empty multMagma holds the carrier of (product <*X,Y*>) = product <* the carrier of X, the carrier of Y*>

proof end;

theorem Th11: :: GROUP_17:11

for G being Group
for A, B being normal Subgroup of G st the carrier of A /\ the carrier of B = {(1_ G)} holds
for a, b being Element of G st a in A & b in B holds
a * b = b * a

proof end;

theorem Th12: :: GROUP_17:12

for G being Group
for A, B being normal Subgroup of G st ( for x being Element of G ex a, b being 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 being Element of G st a in A & b in B holds
h . <*a,b*> = a * b ) )

proof end;

theorem Th13: :: GROUP_17:13

for G being finite commutative Group
for m being Nat
for A being Subset of G st A = { x where x is Element of G : x |^ m = 1_ G } holds
( A <> {} & ( for g1, g2 being Element of G st g1 in A & g2 in A holds
g1 * g2 in A ) & ( for g being Element of G st g in A holds
g " in A ) )

proof end;

theorem Th14: :: GROUP_17:14

for G being finite commutative Group
for m being Nat
for A being Subset of G st A = { x where x is Element of G : x |^ m = 1_ G } holds
ex H being finite strict Subgroup of G st
( the carrier of H = A & H is commutative & H is normal )

proof end;

Lm5: for G being finite Group
for q being Prime st q in support (prime_factorization (card G)) holds
ex a being Element of G st
( a <> 1_ G & ord a = q )

proof end;

theorem Th15: :: GROUP_17:15

for G being finite commutative Group
for m being Nat
for H being finite Subgroup of G st the carrier of H = { x where x is Element of G : x |^ m = 1_ G } holds
for q being Prime st q in support (prime_factorization (card H)) holds
not q,m are_coprime

proof end;

theorem Th16: :: GROUP_17:16

for G being finite commutative Group
for h, k being Nat st card G = h * k & h,k are_coprime holds
ex H, K being finite strict 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 being Element of G ex a, b being Element of G st
( a in H & b in K & x = a * b ) ) & the carrier of H /\ the carrier of K = {(1_ G)} )

proof end;

theorem Th17: :: GROUP_17:17

for H, K being finite Group holds card (product <*H,K*>) = (card H) * (card K)

proof end;

theorem Th18: :: GROUP_17:18

for G being finite commutative Group
for h, k being non zero Nat st card G = h * k & h,k are_coprime holds
ex H, K being finite strict 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 being Element of G st a in H & b in K holds
F . <*a,b*> = a * b ) ) )

proof end;

theorem Th19: :: GROUP_17:19

for G being Group
for q being set
for F being Group-like associative multMagma-Family of {q}
for 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 end;

theorem Th20: :: GROUP_17:20

for G being Group
for q being set
for F being Group-like associative multMagma-Family of {q}
for 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 end;

theorem Th21: :: GROUP_17:21

for q being set
for F being Group-like associative multMagma-Family of {q}
for G being Group st F = q .--> G holds
ex I being Homomorphism of G,(product F) st
( I is bijective & ( for x being Element of G holds I . x = q .--> x ) )

proof end;

theorem Th22: :: GROUP_17:22

for I0, I being non empty finite set
for F0 being Group-like associative multMagma-Family of I0
for F being Group-like associative multMagma-Family of I
for H, K being Group
for q being Element of I
for k being Element of K
for g being 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 end;

Lm6: for I being non empty set
for F being multMagma-Family of I
for x being set st x in the carrier of (product F) holds
x is b₁ -defined total Function

proof end;

Lm7: for I being non empty set
for F being multMagma-Family of I
for f being Function st f in the carrier of (product F) holds
for x being set st x in I holds
ex R being non empty multMagma st
( R = F . x & f . x in the carrier of R )

proof end;

theorem Th23: :: GROUP_17:23

for I0, I being non empty finite set
for F0 being Group-like associative multMagma-Family of I0
for F being Group-like associative multMagma-Family of I
for H, K being Group
for q being Element of I
for G0 being 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 being Function of (product <*H,K*>),(product F) st ( for h being Element of H
for k being Element of K ex g being Function st
( g = G0 . h & G . <*h,k*> = g +* (q .--> k) ) ) holds
G is Homomorphism of (product <*H,K*>),(product F)

proof end;

theorem Th24: :: GROUP_17:24

for I0, I being non empty finite set
for F0 being Group-like associative multMagma-Family of I0
for F being Group-like associative multMagma-Family of I
for H, K being Group
for q being Element of I
for G0 being 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 being Function of (product <*H,K*>),(product F) st ( for h being Element of H
for k being Element of K ex g being Function st
( g = G0 . h & G . <*h,k*> = g +* (q .--> k) ) ) holds
G is bijective

proof end;

theorem Th25: :: GROUP_17:25

for q being set
for F being multMagma-Family of {q}
for G being non empty multMagma st F = q .--> G holds
for y being {b₁} -defined the carrier of b₃ -valued total Function holds
( y in the carrier of (product F) & y . q in the carrier of G & y = q .--> (y . q) )

proof end;

theorem Th26: :: GROUP_17:26

for q being set
for F being Group-like associative multMagma-Family of {q}
for G being Group st F = q .--> G holds
ex HFG being Homomorphism of (product F),G st
( HFG is bijective & ( for x being {b₁} -defined the carrier of b₃ -valued total Function holds HFG . x = Product x ) )

proof end;

theorem Th27: :: GROUP_17:27

for I0, I being non empty finite set
for F0 being Group-like associative multMagma-Family of I0
for F being Group-like associative multMagma-Family of I
for H, K being Group
for q being Element of I
for G0 being Homomorphism of H,(product F0) st not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) & G0 is bijective holds
ex G being Homomorphism of (product <*H,K*>),(product F) st
( G is bijective & ( for h being Element of H
for k being Element of K ex g being Function st
( g = G0 . h & G . <*h,k*> = g +* (q .--> k) ) ) )

proof end;

theorem Th28: :: GROUP_17:28

for I0, I being non empty finite set
for F0 being Group-like associative multMagma-Family of I0
for F being Group-like associative multMagma-Family of I
for H, K being Group
for q being Element of I
for G0 being Homomorphism of (product F0),H st not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) & G0 is bijective holds
ex G being Homomorphism of (product F),(product <*H,K*>) st
( G is bijective & ( for x0 being Function
for k being Element of K
for h being Element of H st h = G0 . x0 & x0 in product F0 holds
G . (x0 +* (q .--> k)) = <*h,k*> ) )

proof end;

theorem Th29: :: GROUP_17:29

for I being non empty finite set
for F being Group-like associative multMagma-Family of I
for x being b₁ -defined total Function st ( for p being Element of I holds x . p in F . p ) holds
x in the carrier of (product F)

proof end;

theorem Th30: :: GROUP_17:30

for I0, I being non empty finite set
for F0 being Group-like associative multMagma-Family of I0
for F being Group-like associative multMagma-Family of I
for K being Group
for q being Element of I
for x being Element of (product F) st not q in I0 & I = I0 \/ {q} & F = F0 +* (q .--> K) holds
ex x0 being b₁ -defined total Function ex k being Element of K st
( x0 in product F0 & x = x0 +* (q .--> k) & ( for p being Element of I0 holds x0 . p in F0 . p ) )

proof end;

theorem Th31: :: GROUP_17:31

for G being Group
for H being Subgroup of G
for f being FinSequence of G
for g being FinSequence of H st f = g holds
Product f = Product g

proof end;

theorem Th32: :: GROUP_17:32

for I being non empty finite set
for G being Group
for H being Subgroup of G
for x being b₁ -defined the carrier of b₂ -valued total Function
for x0 being b₁ -defined the carrier of b₃ -valued total Function st x = x0 holds
Product x = Product x0

proof end;

theorem Th33: :: GROUP_17:33

for G being commutative Group
for I0, I being non empty finite set
for q being Element of I
for x being b₃ -defined the carrier of b₁ -valued total Function
for x0 being b₂ -defined the carrier of b₁ -valued total Function
for k being Element of G st not q in I0 & I = I0 \/ {q} & x = x0 +* (q .--> k) holds
Product x = (Product x0) * k

proof end;

theorem Th34: :: GROUP_17:34

for G being finite strict commutative Group st card G > 1 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 b₂ -defined the carrier of b₁ -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 end;

theorem :: GROUP_17:35

for G being finite strict commutative Group st card G > 1 holds
ex I being non empty finite set ex F being Group-like associative commutative multMagma-Family of I 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)} ) & ( for y being Element of G ex x being b₂ -defined the carrier of b₁ -valued total Function st
( ( for p being Element of I holds x . p in F . p ) & y = Product x ) ) & ( for x1, x2 being b₂ -defined the carrier of b₁ -valued total Function st ( for p being Element of I holds x1 . p in F . p ) & ( for p being Element of I holds x2 . p in F . p ) & Product x1 = Product x2 holds
x1 = x2 ) )

proof end;