:: by Hiroyuki Okazaki , Kenichi Arai and Yasunari Shidama

::

:: Received July 2, 2010

:: Copyright (c) 2010-2016 Association of Mizar Users

registration

let I be non empty set ;

let F be Group-like multMagma-Family of I;

let i be Element of I;

coherence

for b_{1} being multMagma st b_{1} = F . i holds

b_{1} is Group-like
by GROUP_7:def 6;

end;
let F be Group-like multMagma-Family of I;

let i be Element of I;

coherence

for b

b

registration

let I be non empty set ;

let F be associative multMagma-Family of I;

let i be Element of I;

coherence

for b_{1} being multMagma st b_{1} = F . i holds

b_{1} is associative
by GROUP_7:def 7;

end;
let F be associative multMagma-Family of I;

let i be Element of I;

coherence

for b

b

registration

let I be non empty set ;

let F be commutative multMagma-Family of I;

let i be Element of I;

coherence

for b_{1} being multMagma st b_{1} = F . i holds

b_{1} is commutative
by GROUP_7:def 8;

end;
let F be commutative multMagma-Family of I;

let i be Element of I;

coherence

for b

b

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

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;

ex b_{1} being Subset of (product F) st

for x being set holds

( x in b_{1} iff ex g being Element of (F . i) st x = (1_ (product F)) +* (i,g) )

for b_{1}, b_{2} being Subset of (product F) st ( for x being set holds

( x in b_{1} iff ex g being Element of (F . i) st x = (1_ (product F)) +* (i,g) ) ) & ( for x being set holds

( x in b_{2} iff ex g being Element of (F . i) st x = (1_ (product F)) +* (i,g) ) ) holds

b_{1} = b_{2}

end;
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 for x being set holds

( x in it iff ex g being Element of (F . i) st x = (1_ (product F)) +* (i,g) );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof 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 b_{4} being Subset of (product F) holds

( b_{4} = ProjSet (F,i) iff for x being set holds

( x in b_{4} iff ex g being Element of (F . i) st x = (1_ (product F)) +* (i,g) ) );

for I being non empty set

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

for i being Element of I

for b

( b

( x in b

registration

let I be non empty set ;

let F be Group-like associative multMagma-Family of I;

let i be Element of I;

coherence

not ProjSet (F,i) is empty

end;
let F be Group-like associative multMagma-Family of I;

let i be Element of I;

coherence

not ProjSet (F,i) is empty

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

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

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

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)

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)

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;

ex b_{1} being strict Subgroup of product F st the carrier of b_{1} = ProjSet (F,i)

for b_{1}, b_{2} being strict Subgroup of product F st the carrier of b_{1} = ProjSet (F,i) & the carrier of b_{2} = ProjSet (F,i) holds

b_{1} = b_{2}
by GROUP_2:59;

end;
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 the carrier of it = ProjSet (F,i);

ex b

proof end;

uniqueness for b

b

:: 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 b_{4} being strict Subgroup of product F holds

( b_{4} = ProjGroup (F,i) iff the carrier of b_{4} = ProjSet (F,i) );

for I being non empty set

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

for i being Element of I

for b

( b

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;

ex b_{1} being Homomorphism of (F . i),(ProjGroup (F,i)) st

for x being Element of (F . i) holds b_{1} . x = (1_ (product F)) +* (i,x)

for b_{1}, b_{2} being Homomorphism of (F . i),(ProjGroup (F,i)) st ( for x being Element of (F . i) holds b_{1} . x = (1_ (product F)) +* (i,x) ) & ( for x being Element of (F . i) holds b_{2} . x = (1_ (product F)) +* (i,x) ) holds

b_{1} = b_{2}

end;
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 for x being Element of (F . i) holds it . x = (1_ (product F)) +* (i,x);

ex b

for x being Element of (F . i) holds b

proof end;

uniqueness for b

b

proof 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 b_{4} being Homomorphism of (F . i),(ProjGroup (F,i)) holds

( b_{4} = 1ProdHom (F,i) iff for x being Element of (F . i) holds b_{4} . x = (1_ (product F)) +* (i,x) );

for I being non empty set

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

for i being Element of I

for b

( b

registration

let I be non empty set ;

let F be Group-like associative multMagma-Family of I;

let i be Element of I;

coherence

1ProdHom (F,i) is bijective

end;
let F be Group-like associative multMagma-Family of I;

let i be Element of I;

coherence

1ProdHom (F,i) is bijective

proof end;

registration

let I be non empty set ;

let F be Group-like associative multMagma-Family of I;

let i be Element of I;

correctness

coherence

ProjGroup (F,i) is normal ;

end;
let F be Group-like associative multMagma-Family of I;

let i be Element of I;

correctness

coherence

ProjGroup (F,i) is normal ;

proof 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

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

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

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

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

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

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

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;