:: 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;
cluster F . 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;
cluster F . 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;
cluster F . 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 & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) ) iff x = (1_ (product F)) +* (i,g) )
proof end;

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) )
proof end;
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) ) ) & ( 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
proof end;
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
proof end;
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 & dom x = I & x . i = g & ( for j being Element of I st j <> i holds
x . j = 1_ (F . j) ) ) )
proof end;

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) & g2 = (1_ (product F)) +* (i,z2) holds
g1 * g2 = (1_ (product F)) +* (i,(z1 * z2))
proof end;

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 "))
proof end;

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) & g2 in ProjSet (F,i) holds
g1 * g2 in ProjSet (F,i)
proof end;

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)
proof end;

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)
proof end;
uniqueness
for b1, b2 being strict Subgroup of product F st the carrier of b1 = ProjSet (F,i) & 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 & ( for x being Element of (F . i) holds f . x = (1_ (product F)) +* (i,x) ) )
proof end;

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)
proof end;
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) ) & ( for x being Element of (F . i) holds b2 . x = (1_ (product F)) +* (i,x) ) holds
b1 = b2
proof end;
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
proof end;
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 ;
proof end;
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 & x in ProjGroup (F,i) & y in ProjGroup (F,j) holds
x * y = y * x
proof end;

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 & J <= n & GJ = F . J holds
for x being Element of (product F)
for s being FinSequence of (product F) st len s < J & ( for k being Element of Seg n st k in dom s holds
s . k in ProjGroup (F,k) ) & x = Product s holds
x . J = 1_ GJ
proof end;

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 & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s holds
for i being Nat st 1 <= i & i <= n holds
ex si being Element of (product F) st
( si = s . i & x . i = si . i )
proof end;

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 & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s & len t = n & ( for k being Element of Seg n holds t . k in ProjGroup (F,k) ) & x = Product t holds
s = t
proof end;

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 & ( for k being Element of Seg n holds s . k in ProjGroup (F,k) ) & x = Product s )
proof end;

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 ) & ( for x being Element of G ex s being FinSequence of G st
( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & x = Product s ) ) & ( for s, t being FinSequence of G st len s = n & ( for k being Element of Seg n holds s . k in F . k ) & len t = n & ( for k being Element of Seg n holds t . k in F . k ) & Product s = Product t holds
s = t ) holds
ex f being Homomorphism of (product F),G st
( f is bijective & ( for x being Element of (product F) ex s being FinSequence of G st
( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & s = x & f . x = Product s ) ) )
proof end;

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 & ( for x being Element of (product F) ex s being FinSequence of (product G) st
( len s = n & ( for k being Element of Seg n holds s . k in F . k ) & s = x & f . x = Product s ) ) )
proof end;