:: 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 )

( A1 = A & B1 = B )

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

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

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 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)

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 )

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

( 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

for FB being b

for f, g being FinSequence

for FAB being b

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;

ex b_{1} being Element of G ex f being FinSequence of G st

( b_{1} = Product f & f = b * (canFS I) )

for b_{1}, b_{2} being Element of G st ex f being FinSequence of G st

( b_{1} = Product f & f = b * (canFS I) ) & ex f being FinSequence of G st

( b_{2} = Product f & f = b * (canFS I) ) holds

b_{1} = b_{2}
;

end;
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 f being FinSequence of G st

( it = Product f & f = b * (canFS I) );

ex b

( b

proof end;

uniqueness for b

( b

( b

b

:: deftheorem Def1 defines Product GROUP_17:def 1 :

for G being non empty multMagma

for I being finite set

for b being b_{2} -defined the carrier of b_{1} -valued total Function

for b_{4} being Element of G holds

( b_{4} = Product b iff ex f being FinSequence of G st

( b_{4} = Product f & f = b * (canFS I) ) );

for G being non empty multMagma

for I being finite set

for b being b

for b

( b

( b

theorem Th8: :: GROUP_17:8

for G being commutative Group

for A, B being non empty finite set

for FA being b_{2} -defined the carrier of b_{1} -valued total Function

for FB being b_{3} -defined the carrier of b_{1} -valued total Function

for FAB being b_{2} \/ b_{3} -defined the carrier of b_{1} -valued total Function st A misses B & FAB = FA +* FB holds

Product FAB = (Product FA) * (Product FB)

for A, B being non empty finite set

for FA being b

for FB being b

for FAB being b

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_{2}} -defined the carrier of b_{1} -valued total Function st f = q .--> z holds

Product f = z

for q being set

for z being Element of G

for f being {b

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

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 ) )

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 ) )

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 )

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

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)} )

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 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 ) ) )

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)

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

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 ) )

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)

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

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)

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

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_{1}} -defined the carrier of b_{3} -valued total Function holds

( y in the carrier of (product F) & y . q in the carrier of G & y = q .--> (y . q) )

for F being multMagma-Family of {q}

for G being non empty multMagma st F = q .--> G holds

for y being {b

( 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_{1}} -defined the carrier of b_{3} -valued total Function holds HFG . x = Product x ) )

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

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) ) ) )

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*> ) )

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_{1} -defined total Function st ( for p being Element of I holds x . p in F . p ) holds

x in the carrier of (product F)

for F being Group-like associative multMagma-Family of I

for x being b

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_{1} -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 ) )

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

( 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

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_{1} -defined the carrier of b_{2} -valued total Function

for x0 being b_{1} -defined the carrier of b_{3} -valued total Function st x = x0 holds

Product x = Product x0

for G being Group

for H being Subgroup of G

for x being b

for x0 being b

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_{3} -defined the carrier of b_{1} -valued total Function

for x0 being b_{2} -defined the carrier of b_{1} -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

for I0, I being non empty finite set

for q being Element of I

for x being b

for x0 being b

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_{2} -defined the carrier of b_{1} -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 ) ) )

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

( 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_{2} -defined the carrier of b_{1} -valued total Function st

( ( for p being Element of I holds x . p in F . p ) & y = Product x ) ) & ( for x1, x2 being b_{2} -defined the carrier of b_{1} -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 ) )

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

( ( for p being Element of I holds x . p in F . p ) & y = Product x ) ) & ( for x1, x2 being b

x1 = x2 ) )

proof end;