:: Normal Subgroup of Product of Groups
:: by Hiroyuki Okazaki , Kenichi Arai and Yasunari Shidama
::
:: Received July 2, 2010
:: Copyright (c) 2010-2012 Association of Mizar Users


begin

registration
let I be non empty set ;
let F be Group-like multMagma-Family of I;
let i be Element of I;
clusterF . i ->  Group-like for multMagma ;
coherence
 for b1 being multMagma st b1 = F . i holds
b1 is Group-like by GROUP_7:def_6;
end;

registration
let I be non empty set ;
let F be associative multMagma-Family of I;
let i be Element of I;
clusterF . i ->  associative for multMagma ;
coherence
 for b1 being multMagma st b1 = F . i holds
b1 is associative by GROUP_7:def_7;
end;

registration
let I be non empty set ;
let F be commutative multMagma-Family of I;
let i be Element of I;
clusterF . i ->  commutative for multMagma ;
coherence
 for b1 being multMagma st b1 = F . i holds
b1 is commutative by GROUP_7:def_8;
end;

theorem Th1: :: GROUP_12:1
for I being non empty set
for F being Group-like associative multMagma-Family of I
for i being Element of I
for x being Function
for g being Element of (F . i) holds
( ( dom x = I &amp; x . i = g &amp; ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) ) iff x = (1_ (product F)) +* (i,g) )
proofend;

definition
let I be non empty set ;
let F be Group-like associative multMagma-Family of I;
let i be Element of I;
func ProjSet (F,i) ->  Subset of (product F) means :Def1: :: GROUP_12:def 1
 for x being set holds
( x in it iff ex g being Element of (F . i) st x = (1_ (product F)) +* (i,g) );
existence
 ex b1 being Subset of (product F) st
for x being set holds
( x in b1 iff ex g being Element of (F . i) st x = (1_ (product F)) +* (i,g) )
proofend;
uniqueness
 for b1, b2 being Subset of (product F) st ( for x being set holds
( x in b1 iff ex g being Element of (F . i) st x = (1_ (product F)) +* (i,g) ) ) &amp; ( for x being set holds
( x in b2 iff ex g being Element of (F . i) st x = (1_ (product F)) +* (i,g) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines ProjSet GROUP_12:def_1_:_
 for I being non empty set
for F being Group-like associative multMagma-Family of I
for i being Element of I
for b4 being Subset of (product F) holds
( b4 = ProjSet (F,i) iff for x being set holds
( x in b4 iff ex g being Element of (F . i) st x = (1_ (product F)) +* (i,g) ) );

registration
let I be non empty set ;
let F be Group-like associative multMagma-Family of I;
let i be Element of I;
cluster ProjSet (F,i) ->  non empty ;
coherence
 not ProjSet (F,i) is empty
proofend;
end;

theorem Th2: :: GROUP_12:2
for I being non empty set
for F being Group-like associative multMagma-Family of I
for i being Element of I
for x0 being set holds
( x0 in ProjSet (F,i) iff ex x being Function ex g being Element of (F . i) st
( x = x0 &amp; dom x = I &amp; x . i = g &amp; ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) ) )
proofend;

theorem Th3: :: GROUP_12:3
for I being non empty set
for F being Group-like associative multMagma-Family of I
for i being Element of I
for g1, g2 being Element of (product F)
for z1, z2 being Element of (F . i) st g1 = (1_ (product F)) +* (i,z1) &amp; g2 = (1_ (product F)) +* (i,z2) holds
g1 * g2 = (1_ (product F)) +* (i,(z1 * z2))
proofend;

theorem Th4: :: GROUP_12:4
for I being non empty set
for F being Group-like associative multMagma-Family of I
for i being Element of I
for g1 being Element of (product F)
for z1 being Element of (F . i) st g1 = (1_ (product F)) +* (i,z1) holds
g1 " = (1_ (product F)) +* (i,(z1 "))
proofend;

theorem Th5: :: GROUP_12:5
for I being non empty set
for F being Group-like associative multMagma-Family of I
for i being Element of I
for g1, g2 being Element of (product F) st g1 in ProjSet (F,i) &amp; g2 in ProjSet (F,i) holds
g1 * g2 in ProjSet (F,i)
proofend;

theorem Th6: :: GROUP_12:6
for I being non empty set
for F being Group-like associative multMagma-Family of I
for i being Element of I
for g being Element of (product F) st g in ProjSet (F,i) holds
g " in ProjSet (F,i)
proofend;

definition
let I be non empty set ;
let F be Group-like associative multMagma-Family of I;
let i be Element of I;
func ProjGroup (F,i) ->  strict Subgroup of product F means :Def2: :: GROUP_12:def 2
 the carrier of it = ProjSet (F,i);
existence
 ex b1 being strict Subgroup of product F st the carrier of b1 = ProjSet (F,i)
proofend;
uniqueness
 for b1, b2 being strict Subgroup of product F st the carrier of b1 = ProjSet (F,i) &amp; the carrier of b2 = ProjSet (F,i) holds
b1 = b2 by GROUP_2:59;
end;

:: deftheorem Def2 defines ProjGroup GROUP_12:def_2_:_
 for I being non empty set
for F being Group-like associative multMagma-Family of I
for i being Element of I
for b4 being strict Subgroup of product F holds
( b4 = ProjGroup (F,i) iff the carrier of b4 = ProjSet (F,i) );

Lm1:  for I being non empty set
for F being Group-like associative multMagma-Family of I
for i being Element of I ex f being Homomorphism of (F . i),(ProjGroup (F,i)) st
( f is bijective &amp; ( for x being Element of (F . i) holds f . x = (1_ (product F)) +* (i,x) ) )
proofend;

definition
let I be non empty set ;
let F be Group-like associative multMagma-Family of I;
let i be Element of I;
func 1ProdHom (F,i) ->  Homomorphism of (F . i),(ProjGroup (F,i)) means :Def3: :: GROUP_12:def 3
 for x being Element of (F . i) holds it . x = (1_ (product F)) +* (i,x);
existence
 ex b1 being Homomorphism of (F . i),(ProjGroup (F,i)) st
for x being Element of (F . i) holds b1 . x = (1_ (product F)) +* (i,x)
proofend;
uniqueness
 for b1, b2 being Homomorphism of (F . i),(ProjGroup (F,i)) st ( for x being Element of (F . i) holds b1 . x = (1_ (product F)) +* (i,x) ) &amp; ( for x being Element of (F . i) holds b2 . x = (1_ (product F)) +* (i,x) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines 1ProdHom GROUP_12:def_3_:_
 for I being non empty set
for F being Group-like associative multMagma-Family of I
for i being Element of I
for b4 being Homomorphism of (F . i),(ProjGroup (F,i)) holds
( b4 = 1ProdHom (F,i) iff for x being Element of (F . i) holds b4 . x = (1_ (product F)) +* (i,x) );

registration
let I be non empty set ;
let F be Group-like associative multMagma-Family of I;
let i be Element of I;
cluster 1ProdHom (F,i) ->  bijective ;
coherence
 1ProdHom (F,i) is bijective
proofend;
end;

registration
let I be non empty set ;
let F be Group-like associative multMagma-Family of I;
let i be Element of I;
cluster ProjGroup (F,i) ->  strict normal ;
correctness
coherence
ProjGroup (F,i) is normal ;
proofend;
end;

theorem :: GROUP_12:7
for I being non empty set
for F being Group-like associative multMagma-Family of I
for i, j being Element of I
for x, y being Element of (product F) st i <> j &amp; x in ProjGroup (F,i) &amp; y in ProjGroup (F,j) holds
x * y = y * x
proofend;

theorem Th8: :: GROUP_12:8
for n being non empty Nat
for F being Group-like associative multMagma-Family of Seg n
for J being Nat
for GJ being Group st 1 <= J &amp; J <= n &amp; GJ = F . J holds
for x being Element of (product F)
for s being FinSequence of (product F) st len s < J &amp; ( for k being Element of Seg n st k in dom s holds
s . k in ProjGroup (F,k) ) &amp; x = Product s holds
x . J = 1_ GJ
proofend;

theorem Th9: :: GROUP_12:9
for n being non empty Nat
for F being Group-like associative multMagma-Family of Seg n
for x being Element of (product F)
for s being FinSequence of (product F) st len s = n &amp; ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) &amp; x = Product s holds
for i being Nat st 1 <= i &amp; i <= n holds
ex si being Element of (product F) st
( si = s . i &amp; x . i = si . i )
proofend;

theorem Th10: :: GROUP_12:10
for n being non empty Nat
for F being Group-like associative multMagma-Family of Seg n
for x being Element of (product F)
for s, t being FinSequence of (product F) st len s = n &amp; ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) &amp; x = Product s &amp; len t = n &amp; ( for k being Element of Seg n holds t . k in ProjGroup (F,k) ) &amp; x = Product t holds
s = t
proofend;

theorem Th11: :: GROUP_12:11
for n being non empty Nat
for F being Group-like associative multMagma-Family of Seg n
for x being Element of (product F) ex s being FinSequence of (product F) st
( len s = n &amp; ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) &amp; x = Product s )
proofend;

theorem Th12: :: GROUP_12:12
for n being non empty Nat
for G being commutative Group
for F being Group-like associative multMagma-Family of Seg n st ( for i being Element of Seg n holds F . i is Subgroup of G ) &amp; ( for x being Element of G ex s being FinSequence of G st
( len s = n &amp; ( for k being Element of Seg n holds s . k in F . k ) &amp; x = Product s ) ) &amp; ( for s, t being FinSequence of G st len s = n &amp; ( for k being Element of Seg n holds s . k in F . k ) &amp; len t = n &amp; ( for k being Element of Seg n holds t . k in F . k ) &amp; Product s = Product t holds
s = t ) holds
ex f being Homomorphism of (product F),G st
( f is bijective &amp; ( for x being Element of (product F) ex s being FinSequence of G st
( len s = n &amp; ( for k being Element of Seg n holds s . k in F . k ) &amp; s = x &amp; f . x = Product s ) ) )
proofend;

theorem :: GROUP_12:13
for n being non empty Nat
for G, F being Group-like associative commutative multMagma-Family of Seg n st ( for k being Element of Seg n holds F . k = ProjGroup (G,k) ) holds
ex f being Homomorphism of (product F),(product G) st
( f is bijective &amp; ( for x being Element of (product F) ex s being FinSequence of (product G) st
( len s = n &amp; ( for k being Element of Seg n holds s . k in F . k ) &amp; s = x &amp; f . x = Product s ) ) )
proofend;