:: 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 b2 -defined the carrier of b1 -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 b1 -defined total Function
for FB being b2 -defined total Function
for f, g being FinSequence
for FAB being b1 \/ b2 -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 b1 being Element of G ex f being FinSequence of G st
( b1 = Product f & f = b * (canFS I) )
proof end;
uniqueness
for b1, b2 being Element of G st ex f being FinSequence of G st
( b1 = Product f & f = b * (canFS I) ) & ex f being FinSequence of G st
( b2 = Product f & f = b * (canFS I) ) holds
b1 = b2
;
end;

:: deftheorem Def1 defines Product GROUP_17:def 1 :
for G being non empty multMagma
for I being finite set
for b being b2 -defined the carrier of b1 -valued total Function
for b4 being Element of G holds
( b4 = Product b iff ex f being FinSequence of G st
( b4 = 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 b2 -defined the carrier of b1 -valued total Function
for FB being b3 -defined the carrier of b1 -valued total Function
for FAB being b2 \/ b3 -defined the carrier of b1 -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 {b2} -defined the carrier of b1 -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 b1 -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 {b1} -defined the carrier of b3 -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 {b1} -defined the carrier of b3 -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 b1 -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 b1 -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 b1 -defined the carrier of b2 -valued total Function
for x0 being b1 -defined the carrier of b3 -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 b3 -defined the carrier of b1 -valued total Function
for x0 being b2 -defined the carrier of b1 -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 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 ) ) )
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 b2 -defined the carrier of b1 -valued total Function st
( ( for p being Element of I holds x . p in F . p ) & y = Product x ) ) & ( for x1, x2 being b2 -defined the carrier of b1 -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;