:: GROUP_7 semantic presentation
begin
definition
let R be Relation;
attrR is multMagma-yielding means :Def1: :: GROUP_7:def 1
for y being set st y in rng R holds
y is non empty multMagma ;
end;
:: deftheorem Def1 defines multMagma-yielding GROUP_7:def_1_:_
for R being Relation holds
( R is multMagma-yielding iff for y being set st y in rng R holds
y is non empty multMagma );
registration
cluster Relation-like Function-like multMagma-yielding -> 1-sorted-yielding for set ;
coherence
for b1 being Function st b1 is multMagma-yielding holds
b1 is 1-sorted-yielding
proof
let f be Function; ::_thesis: ( f is multMagma-yielding implies f is 1-sorted-yielding )
assume A1: f is multMagma-yielding ; ::_thesis: f is 1-sorted-yielding
let x be set ; :: according to PRALG_1:def_11 ::_thesis: ( not x in dom f or f . x is 1-sorted )
assume x in dom f ; ::_thesis: f . x is 1-sorted
then f . x in rng f by FUNCT_1:def_3;
hence f . x is 1-sorted by A1, Def1; ::_thesis: verum
end;
end;
registration
let I be set ;
cluster Relation-like I -defined Function-like total multMagma-yielding for set ;
existence
ex b1 being ManySortedSet of I st b1 is multMagma-yielding
proof
set H = the non empty multMagma ;
set f = I --> the non empty multMagma ;
take I --> the non empty multMagma ; ::_thesis: I --> the non empty multMagma is multMagma-yielding
let a be set ; :: according to GROUP_7:def_1 ::_thesis: ( a in rng (I --> the non empty multMagma ) implies a is non empty multMagma )
assume a in rng (I --> the non empty multMagma ) ; ::_thesis: a is non empty multMagma
then ex x being set st
( x in dom (I --> the non empty multMagma ) & a = (I --> the non empty multMagma ) . x ) by FUNCT_1:def_3;
hence a is non empty multMagma by FUNCOP_1:7; ::_thesis: verum
end;
end;
registration
cluster Relation-like Function-like multMagma-yielding for set ;
existence
ex b1 being Function st b1 is multMagma-yielding
proof
set I = the set ;
set f = the multMagma-yielding ManySortedSet of the set ;
take the multMagma-yielding ManySortedSet of the set ; ::_thesis: the multMagma-yielding ManySortedSet of the set is multMagma-yielding
thus the multMagma-yielding ManySortedSet of the set is multMagma-yielding ; ::_thesis: verum
end;
end;
definition
let I be set ;
mode multMagma-Family of I is multMagma-yielding ManySortedSet of I;
end;
definition
let I be non empty set ;
let F be multMagma-Family of I;
let i be Element of I;
:: original: .
redefine funcF . i -> non empty multMagma ;
coherence
F . i is non empty multMagma
proof
dom F = I by PARTFUN1:def_2;
then F . i in rng F by FUNCT_1:def_3;
hence F . i is non empty multMagma by Def1; ::_thesis: verum
end;
end;
registration
let I be set ;
let F be multMagma-Family of I;
cluster Carrier F -> V2() ;
coherence
Carrier F is non-empty
proof
let i be set ; :: according to PBOOLE:def_13 ::_thesis: ( not i in I or not (Carrier F) . i is empty )
assume A1: i in I ; ::_thesis: not (Carrier F) . i is empty
dom F = I by PARTFUN1:def_2;
then F . i in rng F by A1, FUNCT_1:def_3;
then A2: F . i is non empty multMagma by Def1;
ex R being 1-sorted st
( R = F . i & (Carrier F) . i = the carrier of R ) by A1, PRALG_1:def_13;
hence not (Carrier F) . i is empty by A2; ::_thesis: verum
end;
end;
Lm1: now__::_thesis:_for_I_being_non_empty_set_
for_i_being_Element_of_I
for_F_being_multMagma-yielding_ManySortedSet_of_I
for_f_being_Element_of_product_(Carrier_F)_holds_f_._i_in_the_carrier_of_(F_._i)
let I be non empty set ; ::_thesis: for i being Element of I
for F being multMagma-yielding ManySortedSet of I
for f being Element of product (Carrier F) holds f . i in the carrier of (F . i)
let i be Element of I; ::_thesis: for F being multMagma-yielding ManySortedSet of I
for f being Element of product (Carrier F) holds f . i in the carrier of (F . i)
let F be multMagma-yielding ManySortedSet of I; ::_thesis: for f being Element of product (Carrier F) holds f . i in the carrier of (F . i)
let f be Element of product (Carrier F); ::_thesis: f . i in the carrier of (F . i)
A1: dom (Carrier F) = I by PARTFUN1:def_2;
ex R being 1-sorted st
( R = F . i & (Carrier F) . i = the carrier of R ) by PRALG_1:def_13;
hence f . i in the carrier of (F . i) by A1, CARD_3:9; ::_thesis: verum
end;
definition
let I be set ;
let F be multMagma-Family of I;
func product F -> strict multMagma means :Def2: :: GROUP_7:def 2
( the carrier of it = product (Carrier F) & ( for f, g being Element of product (Carrier F)
for i being set st i in I holds
ex Fi being non empty multMagma ex h being Function st
( Fi = F . i & h = the multF of it . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) ) );
existence
ex b1 being strict multMagma st
( the carrier of b1 = product (Carrier F) & ( for f, g being Element of product (Carrier F)
for i being set st i in I holds
ex Fi being non empty multMagma ex h being Function st
( Fi = F . i & h = the multF of b1 . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) ) )
proof
set A = product (Carrier F);
defpred S1[ Element of product (Carrier F), Element of product (Carrier F), set ] means for i being set st i in I holds
ex Fi being non empty multMagma ex h being Function st
( Fi = F . i & h = $3 & h . i = the multF of Fi . (($1 . i),($2 . i)) );
A1: dom (Carrier F) = I by PARTFUN1:def_2;
A2: for x, y being Element of product (Carrier F) ex z being Element of product (Carrier F) st S1[x,y,z]
proof
let x, y be Element of product (Carrier F); ::_thesis: ex z being Element of product (Carrier F) st S1[x,y,z]
defpred S2[ set , set ] means ex Fi being non empty multMagma st
( Fi = F . $1 & $2 = the multF of Fi . ((x . $1),(y . $1)) );
A3: for i being set st i in I holds
ex w being set st
( w in union (rng (Carrier F)) & S2[i,w] )
proof
let i be set ; ::_thesis: ( i in I implies ex w being set st
( w in union (rng (Carrier F)) & S2[i,w] ) )
assume A4: i in I ; ::_thesis: ex w being set st
( w in union (rng (Carrier F)) & S2[i,w] )
then reconsider I1 = I as non empty set ;
reconsider i1 = i as Element of I1 by A4;
reconsider F1 = F as multMagma-Family of I1 ;
take w = the multF of (F1 . i1) . ((x . i1),(y . i1)); ::_thesis: ( w in union (rng (Carrier F)) & S2[i,w] )
A5: (Carrier F) . i1 in rng (Carrier F) by A1, FUNCT_1:def_3;
A6: ex R being 1-sorted st
( R = F . i1 & (Carrier F1) . i1 = the carrier of R ) by PRALG_1:def_13;
then A7: y . i1 in the carrier of (F1 . i1) by A1, CARD_3:9;
x . i1 in the carrier of (F1 . i1) by A1, A6, CARD_3:9;
then the multF of (F1 . i1) . ((x . i1),(y . i1)) in the carrier of (F1 . i1) by A7, BINOP_1:17;
hence w in union (rng (Carrier F)) by A6, A5, TARSKI:def_4; ::_thesis: S2[i,w]
thus S2[i,w] ; ::_thesis: verum
end;
consider z being Function such that
A8: ( dom z = I & rng z c= union (rng (Carrier F)) & ( for x being set st x in I holds
S2[x,z . x] ) ) from FUNCT_1:sch_5(A3);
A9: for i being set st i in dom (Carrier F) holds
z . i in (Carrier F) . i
proof
let i be set ; ::_thesis: ( i in dom (Carrier F) implies z . i in (Carrier F) . i )
assume A10: i in dom (Carrier F) ; ::_thesis: z . i in (Carrier F) . i
then reconsider I1 = I as non empty set ;
A11: ex Fi being non empty multMagma st
( Fi = F . i & z . i = the multF of Fi . ((x . i),(y . i)) ) by A8, A10;
reconsider i1 = i as Element of I1 by A10;
reconsider F1 = F as multMagma-Family of I1 ;
A12: ex R being 1-sorted st
( R = F . i & (Carrier F) . i = the carrier of R ) by A10, PRALG_1:def_13;
then A13: y . i1 in the carrier of (F1 . i1) by A1, CARD_3:9;
x . i1 in the carrier of (F1 . i1) by A1, A12, CARD_3:9;
hence z . i in (Carrier F) . i by A11, A12, A13, BINOP_1:17; ::_thesis: verum
end;
dom z = dom (Carrier F) by A8, PARTFUN1:def_2;
then reconsider z = z as Element of product (Carrier F) by A9, CARD_3:9;
take z ; ::_thesis: S1[x,y,z]
let i be set ; ::_thesis: ( i in I implies ex Fi being non empty multMagma ex h being Function st
( Fi = F . i & h = z & h . i = the multF of Fi . ((x . i),(y . i)) ) )
assume i in I ; ::_thesis: ex Fi being non empty multMagma ex h being Function st
( Fi = F . i & h = z & h . i = the multF of Fi . ((x . i),(y . i)) )
then consider Fi being non empty multMagma such that
A14: Fi = F . i and
A15: z . i = the multF of Fi . ((x . i),(y . i)) by A8;
take Fi ; ::_thesis: ex h being Function st
( Fi = F . i & h = z & h . i = the multF of Fi . ((x . i),(y . i)) )
take z ; ::_thesis: ( Fi = F . i & z = z & z . i = the multF of Fi . ((x . i),(y . i)) )
thus ( Fi = F . i & z = z & z . i = the multF of Fi . ((x . i),(y . i)) ) by A14, A15; ::_thesis: verum
end;
consider B being BinOp of (product (Carrier F)) such that
A16: for a, b being Element of product (Carrier F) holds S1[a,b,B . (a,b)] from BINOP_1:sch_3(A2);
take multMagma(# (product (Carrier F)),B #) ; ::_thesis: ( the carrier of multMagma(# (product (Carrier F)),B #) = product (Carrier F) & ( for f, g being Element of product (Carrier F)
for i being set st i in I holds
ex Fi being non empty multMagma ex h being Function st
( Fi = F . i & h = the multF of multMagma(# (product (Carrier F)),B #) . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) ) )
thus the carrier of multMagma(# (product (Carrier F)),B #) = product (Carrier F) ; ::_thesis: for f, g being Element of product (Carrier F)
for i being set st i in I holds
ex Fi being non empty multMagma ex h being Function st
( Fi = F . i & h = the multF of multMagma(# (product (Carrier F)),B #) . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) )
let f, g be Element of product (Carrier F); ::_thesis: for i being set st i in I holds
ex Fi being non empty multMagma ex h being Function st
( Fi = F . i & h = the multF of multMagma(# (product (Carrier F)),B #) . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) )
let i be set ; ::_thesis: ( i in I implies ex Fi being non empty multMagma ex h being Function st
( Fi = F . i & h = the multF of multMagma(# (product (Carrier F)),B #) . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) )
assume i in I ; ::_thesis: ex Fi being non empty multMagma ex h being Function st
( Fi = F . i & h = the multF of multMagma(# (product (Carrier F)),B #) . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) )
hence ex Fi being non empty multMagma ex h being Function st
( Fi = F . i & h = the multF of multMagma(# (product (Carrier F)),B #) . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) by A16; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict multMagma st the carrier of b1 = product (Carrier F) & ( for f, g being Element of product (Carrier F)
for i being set st i in I holds
ex Fi being non empty multMagma ex h being Function st
( Fi = F . i & h = the multF of b1 . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) ) & the carrier of b2 = product (Carrier F) & ( for f, g being Element of product (Carrier F)
for i being set st i in I holds
ex Fi being non empty multMagma ex h being Function st
( Fi = F . i & h = the multF of b2 . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) ) holds
b1 = b2
proof
let A, B be strict multMagma ; ::_thesis: ( the carrier of A = product (Carrier F) & ( for f, g being Element of product (Carrier F)
for i being set st i in I holds
ex Fi being non empty multMagma ex h being Function st
( Fi = F . i & h = the multF of A . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) ) & the carrier of B = product (Carrier F) & ( for f, g being Element of product (Carrier F)
for i being set st i in I holds
ex Fi being non empty multMagma ex h being Function st
( Fi = F . i & h = the multF of B . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) ) implies A = B )
assume that
A17: the carrier of A = product (Carrier F) and
A18: for f, g being Element of product (Carrier F)
for i being set st i in I holds
ex Fi being non empty multMagma ex h being Function st
( Fi = F . i & h = the multF of A . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) and
A19: the carrier of B = product (Carrier F) and
A20: for f, g being Element of product (Carrier F)
for i being set st i in I holds
ex Fi being non empty multMagma ex h being Function st
( Fi = F . i & h = the multF of B . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) ; ::_thesis: A = B
for x, y being set st x in the carrier of A & y in the carrier of A holds
the multF of A . (x,y) = the multF of B . (x,y)
proof
set P = product (Carrier F);
let x, y be set ; ::_thesis: ( x in the carrier of A & y in the carrier of A implies the multF of A . (x,y) = the multF of B . (x,y) )
assume that
A21: x in the carrier of A and
A22: y in the carrier of A ; ::_thesis: the multF of A . (x,y) = the multF of B . (x,y)
reconsider x1 = x, y1 = y as Element of product (Carrier F) by A17, A21, A22;
[x1,y1] in [: the carrier of A, the carrier of A:] by A21, A22, ZFMISC_1:87;
then reconsider f = the multF of A . [x1,y1] as Element of product (Carrier F) by A17, FUNCT_2:5;
[x1,y1] in [: the carrier of B, the carrier of B:] by A19, ZFMISC_1:87;
then reconsider g = the multF of B . [x1,y1] as Element of product (Carrier F) by A19, FUNCT_2:5;
A23: dom (Carrier F) = I by PARTFUN1:def_2;
then A24: dom g = I by CARD_3:9;
A25: for i being set st i in I holds
f . i = g . i
proof
let i be set ; ::_thesis: ( i in I implies f . i = g . i )
assume A26: i in I ; ::_thesis: f . i = g . i
then A27: ex Gi being non empty multMagma ex h2 being Function st
( Gi = F . i & h2 = the multF of B . (x1,y1) & h2 . i = the multF of Gi . ((x1 . i),(y1 . i)) ) by A20;
ex Fi being non empty multMagma ex h1 being Function st
( Fi = F . i & h1 = the multF of A . (x1,y1) & h1 . i = the multF of Fi . ((x1 . i),(y1 . i)) ) by A18, A26;
hence f . i = g . i by A27; ::_thesis: verum
end;
dom f = I by A23, CARD_3:9;
hence the multF of A . (x,y) = the multF of B . (x,y) by A24, A25, FUNCT_1:2; ::_thesis: verum
end;
hence A = B by A17, A19, BINOP_1:1; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines product GROUP_7:def_2_:_
for I being set
for F being multMagma-Family of I
for b3 being strict multMagma holds
( b3 = product F iff ( the carrier of b3 = product (Carrier F) & ( for f, g being Element of product (Carrier F)
for i being set st i in I holds
ex Fi being non empty multMagma ex h being Function st
( Fi = F . i & h = the multF of b3 . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) ) ) );
registration
let I be set ;
let F be multMagma-Family of I;
cluster product F -> non empty strict constituted-Functions ;
coherence
( not product F is empty & product F is constituted-Functions )
proof
A1: the carrier of (product F) = product (Carrier F) by Def2;
hence not the carrier of (product F) is empty ; :: according to STRUCT_0:def_1 ::_thesis: product F is constituted-Functions
thus product F is constituted-Functions by A1, MONOID_0:80; ::_thesis: verum
end;
end;
theorem Th4: :: GROUP_7:1
for I, i being set
for f, g, h being Function
for F being multMagma-Family of I
for G being non empty multMagma
for p, q being Element of (product F)
for x, y being Element of G st i in I & G = F . i & f = p & g = q & h = p * q & f . i = x & g . i = y holds
x * y = h . i
proof
let I, i be set ; ::_thesis: for f, g, h being Function
for F being multMagma-Family of I
for G being non empty multMagma
for p, q being Element of (product F)
for x, y being Element of G st i in I & G = F . i & f = p & g = q & h = p * q & f . i = x & g . i = y holds
x * y = h . i
let f, g, h be Function; ::_thesis: for F being multMagma-Family of I
for G being non empty multMagma
for p, q being Element of (product F)
for x, y being Element of G st i in I & G = F . i & f = p & g = q & h = p * q & f . i = x & g . i = y holds
x * y = h . i
let F be multMagma-Family of I; ::_thesis: for G being non empty multMagma
for p, q being Element of (product F)
for x, y being Element of G st i in I & G = F . i & f = p & g = q & h = p * q & f . i = x & g . i = y holds
x * y = h . i
let G be non empty multMagma ; ::_thesis: for p, q being Element of (product F)
for x, y being Element of G st i in I & G = F . i & f = p & g = q & h = p * q & f . i = x & g . i = y holds
x * y = h . i
let p, q be Element of (product F); ::_thesis: for x, y being Element of G st i in I & G = F . i & f = p & g = q & h = p * q & f . i = x & g . i = y holds
x * y = h . i
let x, y be Element of G; ::_thesis: ( i in I & G = F . i & f = p & g = q & h = p * q & f . i = x & g . i = y implies x * y = h . i )
assume that
A1: i in I and
A2: G = F . i and
A3: f = p and
A4: g = q and
A5: h = p * q and
A6: f . i = x and
A7: g . i = y ; ::_thesis: x * y = h . i
set GP = product F;
q in the carrier of (product F) ;
then A8: g in product (Carrier F) by A4, Def2;
p in the carrier of (product F) ;
then f in product (Carrier F) by A3, Def2;
then ex Fi being non empty multMagma ex m being Function st
( Fi = F . i & m = the multF of (product F) . (f,g) & m . i = the multF of Fi . ((f . i),(g . i)) ) by A1, A8, Def2;
hence x * y = h . i by A2, A3, A4, A5, A6, A7; ::_thesis: verum
end;
definition
let I be set ;
let F be multMagma-Family of I;
attrF is Group-like means :Def3: :: GROUP_7:def 3
for i being set st i in I holds
ex Fi being non empty Group-like multMagma st Fi = F . i;
attrF is associative means :Def4: :: GROUP_7:def 4
for i being set st i in I holds
ex Fi being non empty associative multMagma st Fi = F . i;
attrF is commutative means :Def5: :: GROUP_7:def 5
for i being set st i in I holds
ex Fi being non empty commutative multMagma st Fi = F . i;
end;
:: deftheorem Def3 defines Group-like GROUP_7:def_3_:_
for I being set
for F being multMagma-Family of I holds
( F is Group-like iff for i being set st i in I holds
ex Fi being non empty Group-like multMagma st Fi = F . i );
:: deftheorem Def4 defines associative GROUP_7:def_4_:_
for I being set
for F being multMagma-Family of I holds
( F is associative iff for i being set st i in I holds
ex Fi being non empty associative multMagma st Fi = F . i );
:: deftheorem Def5 defines commutative GROUP_7:def_5_:_
for I being set
for F being multMagma-Family of I holds
( F is commutative iff for i being set st i in I holds
ex Fi being non empty commutative multMagma st Fi = F . i );
definition
let I be non empty set ;
let F be multMagma-Family of I;
redefine attr F is Group-like means :Def6: :: GROUP_7:def 6
for i being Element of I holds F . i is Group-like ;
compatibility
( F is Group-like iff for i being Element of I holds F . i is Group-like )
proof
hereby ::_thesis: ( ( for i being Element of I holds F . i is Group-like ) implies F is Group-like )
assume A1: F is Group-like ; ::_thesis: for i being Element of I holds F . i is Group-like
let i be Element of I; ::_thesis: F . i is Group-like
ex Fi being non empty Group-like multMagma st Fi = F . i by A1, Def3;
hence F . i is Group-like ; ::_thesis: verum
end;
assume A2: for i being Element of I holds F . i is Group-like ; ::_thesis: F is Group-like
let i be set ; :: according to GROUP_7:def_3 ::_thesis: ( i in I implies ex Fi being non empty Group-like multMagma st Fi = F . i )
assume i in I ; ::_thesis: ex Fi being non empty Group-like multMagma st Fi = F . i
then reconsider i1 = i as Element of I ;
reconsider F1 = F . i1 as non empty Group-like multMagma by A2;
take F1 ; ::_thesis: F1 = F . i
thus F1 = F . i ; ::_thesis: verum
end;
redefine attr F is associative means :Def7: :: GROUP_7:def 7
for i being Element of I holds F . i is associative ;
compatibility
( F is associative iff for i being Element of I holds F . i is associative )
proof
hereby ::_thesis: ( ( for i being Element of I holds F . i is associative ) implies F is associative )
assume A3: F is associative ; ::_thesis: for i being Element of I holds F . i is associative
let i be Element of I; ::_thesis: F . i is associative
ex Fi being non empty associative multMagma st Fi = F . i by A3, Def4;
hence F . i is associative ; ::_thesis: verum
end;
assume A4: for i being Element of I holds F . i is associative ; ::_thesis: F is associative
let i be set ; :: according to GROUP_7:def_4 ::_thesis: ( i in I implies ex Fi being non empty associative multMagma st Fi = F . i )
assume i in I ; ::_thesis: ex Fi being non empty associative multMagma st Fi = F . i
then reconsider i1 = i as Element of I ;
reconsider Fi = F . i1 as non empty associative multMagma by A4;
take Fi ; ::_thesis: Fi = F . i
thus Fi = F . i ; ::_thesis: verum
end;
redefine attr F is commutative means :: GROUP_7:def 8
for i being Element of I holds F . i is commutative ;
compatibility
( F is commutative iff for i being Element of I holds F . i is commutative )
proof
hereby ::_thesis: ( ( for i being Element of I holds F . i is commutative ) implies F is commutative )
assume A5: F is commutative ; ::_thesis: for i being Element of I holds F . i is commutative
let i be Element of I; ::_thesis: F . i is commutative
ex Fi being non empty commutative multMagma st Fi = F . i by A5, Def5;
hence F . i is commutative ; ::_thesis: verum
end;
assume A6: for i being Element of I holds F . i is commutative ; ::_thesis: F is commutative
let i be set ; :: according to GROUP_7:def_5 ::_thesis: ( i in I implies ex Fi being non empty commutative multMagma st Fi = F . i )
assume i in I ; ::_thesis: ex Fi being non empty commutative multMagma st Fi = F . i
then reconsider i1 = i as Element of I ;
reconsider Fi = F . i1 as non empty commutative multMagma by A6;
take Fi ; ::_thesis: Fi = F . i
thus Fi = F . i ; ::_thesis: verum
end;
end;
:: deftheorem Def6 defines Group-like GROUP_7:def_6_:_
for I being non empty set
for F being multMagma-Family of I holds
( F is Group-like iff for i being Element of I holds F . i is Group-like );
:: deftheorem Def7 defines associative GROUP_7:def_7_:_
for I being non empty set
for F being multMagma-Family of I holds
( F is associative iff for i being Element of I holds F . i is associative );
:: deftheorem defines commutative GROUP_7:def_8_:_
for I being non empty set
for F being multMagma-Family of I holds
( F is commutative iff for i being Element of I holds F . i is commutative );
registration
let I be set ;
cluster Relation-like I -defined Function-like total 1-sorted-yielding multMagma-yielding Group-like associative commutative for set ;
existence
ex b1 being multMagma-Family of I st
( b1 is Group-like & b1 is associative & b1 is commutative )
proof
set H = the commutative Group;
set f = I --> the commutative Group;
I --> the commutative Group is multMagma-yielding
proof
let i be set ; :: according to GROUP_7:def_1 ::_thesis: ( i in rng (I --> the commutative Group) implies i is non empty multMagma )
assume i in rng (I --> the commutative Group) ; ::_thesis: i is non empty multMagma
then ex x being set st
( x in dom (I --> the commutative Group) & i = (I --> the commutative Group) . x ) by FUNCT_1:def_3;
hence i is non empty multMagma by FUNCOP_1:7; ::_thesis: verum
end;
then reconsider f = I --> the commutative Group as multMagma-Family of I ;
take f ; ::_thesis: ( f is Group-like & f is associative & f is commutative )
hereby :: according to GROUP_7:def_3 ::_thesis: ( f is associative & f is commutative )
let i be set ; ::_thesis: ( i in I implies ex Fi being non empty Group-like multMagma st Fi = f . i )
assume A1: i in I ; ::_thesis: ex Fi being non empty Group-like multMagma st Fi = f . i
then reconsider I1 = I as non empty set ;
reconsider i1 = i as Element of I1 by A1;
reconsider F1 = f as multMagma-Family of I1 ;
reconsider Fi = F1 . i1 as non empty Group-like multMagma by FUNCOP_1:7;
take Fi = Fi; ::_thesis: Fi = f . i
thus Fi = f . i ; ::_thesis: verum
end;
hereby :: according to GROUP_7:def_4 ::_thesis: f is commutative
let i be set ; ::_thesis: ( i in I implies ex Fi being non empty associative multMagma st Fi = f . i )
assume A2: i in I ; ::_thesis: ex Fi being non empty associative multMagma st Fi = f . i
then reconsider I1 = I as non empty set ;
reconsider i1 = i as Element of I1 by A2;
reconsider F1 = f as multMagma-Family of I1 ;
reconsider Fi = F1 . i1 as non empty associative multMagma by FUNCOP_1:7;
take Fi = Fi; ::_thesis: Fi = f . i
thus Fi = f . i ; ::_thesis: verum
end;
let i be set ; :: according to GROUP_7:def_5 ::_thesis: ( i in I implies ex Fi being non empty commutative multMagma st Fi = f . i )
assume A3: i in I ; ::_thesis: ex Fi being non empty commutative multMagma st Fi = f . i
then reconsider I1 = I as non empty set ;
reconsider i1 = i as Element of I1 by A3;
reconsider F1 = f as multMagma-Family of I1 ;
reconsider Fi = F1 . i1 as non empty commutative multMagma by FUNCOP_1:7;
take Fi ; ::_thesis: Fi = f . i
thus Fi = f . i ; ::_thesis: verum
end;
end;
registration
let I be set ;
let F be Group-like multMagma-Family of I;
cluster product F -> strict Group-like ;
coherence
product F is Group-like
proof
defpred S1[ set , set ] means ex Fi being non empty multMagma ex e being Element of Fi st
( Fi = F . I & F = e & ( for h being Element of Fi holds
( h * e = h & e * h = h & ex g being Element of Fi st
( h * g = e & g * h = e ) ) ) );
set G = product F;
A1: dom (Carrier F) = I by PARTFUN1:def_2;
A2: for i being set st i in I holds
ex y being set st
( y in union (rng (Carrier F)) & S1[i,y] )
proof
let i be set ; ::_thesis: ( i in I implies ex y being set st
( y in union (rng (Carrier F)) & S1[i,y] ) )
assume A3: i in I ; ::_thesis: ex y being set st
( y in union (rng (Carrier F)) & S1[i,y] )
then reconsider I1 = I as non empty set ;
reconsider i1 = i as Element of I1 by A3;
reconsider F1 = F as Group-like multMagma-Family of I1 ;
A4: ex R being 1-sorted st
( R = F . i1 & (Carrier F1) . i1 = the carrier of R ) by PRALG_1:def_13;
F1 . i1 is Group-like by Def6;
then consider e being Element of (F1 . i1) such that
A5: for h being Element of (F1 . i1) holds
( h * e = h & e * h = h & ex g being Element of (F1 . i1) st
( h * g = e & g * h = e ) ) by GROUP_1:def_2;
take e ; ::_thesis: ( e in union (rng (Carrier F)) & S1[i,e] )
(Carrier F) . i1 in rng (Carrier F) by A1, FUNCT_1:def_3;
hence e in union (rng (Carrier F)) by A4, TARSKI:def_4; ::_thesis: S1[i,e]
take F1 . i1 ; ::_thesis: ex e being Element of (F1 . i1) st
( F1 . i1 = F . i & e = e & ( for h being Element of (F1 . i1) holds
( h * e = h & e * h = h & ex g being Element of (F1 . i1) st
( h * g = e & g * h = e ) ) ) )
take e ; ::_thesis: ( F1 . i1 = F . i & e = e & ( for h being Element of (F1 . i1) holds
( h * e = h & e * h = h & ex g being Element of (F1 . i1) st
( h * g = e & g * h = e ) ) ) )
thus ( F1 . i1 = F . i & e = e ) ; ::_thesis: for h being Element of (F1 . i1) holds
( h * e = h & e * h = h & ex g being Element of (F1 . i1) st
( h * g = e & g * h = e ) )
let h be Element of (F1 . i1); ::_thesis: ( h * e = h & e * h = h & ex g being Element of (F1 . i1) st
( h * g = e & g * h = e ) )
thus ( h * e = h & e * h = h & ex g being Element of (F1 . i1) st
( h * g = e & g * h = e ) ) by A5; ::_thesis: verum
end;
consider ee being Function such that
A6: dom ee = I and
rng ee c= union (rng (Carrier F)) and
A7: for x being set st x in I holds
S1[x,ee . x] from FUNCT_1:sch_5(A2);
now__::_thesis:_for_i_being_set_st_i_in_dom_ee_holds_
ee_._i_in_(Carrier_F)_._i
let i be set ; ::_thesis: ( i in dom ee implies ee . i in (Carrier F) . i )
assume A8: i in dom ee ; ::_thesis: ee . i in (Carrier F) . i
then A9: ex R being 1-sorted st
( R = F . i & (Carrier F) . i = the carrier of R ) by A6, PRALG_1:def_13;
ex Fi being non empty multMagma ex e being Element of Fi st
( Fi = F . i & ee . i = e & ( for h being Element of Fi holds
( h * e = h & e * h = h & ex g being Element of Fi st
( h * g = e & g * h = e ) ) ) ) by A6, A7, A8;
hence ee . i in (Carrier F) . i by A9; ::_thesis: verum
end;
then A10: ee in product (Carrier F) by A1, A6, CARD_3:9;
then reconsider e1 = ee as Element of (product F) by Def2;
take e1 ; :: according to GROUP_1:def_2 ::_thesis: for b1 being Element of the carrier of (product F) holds
( b1 * e1 = b1 & e1 * b1 = b1 & ex b2 being Element of the carrier of (product F) st
( b1 * b2 = e1 & b2 * b1 = e1 ) )
let h be Element of (product F); ::_thesis: ( h * e1 = h & e1 * h = h & ex b1 being Element of the carrier of (product F) st
( h * b1 = e1 & b1 * h = e1 ) )
reconsider h1 = h as Element of product (Carrier F) by Def2;
reconsider he = the multF of (product F) . (h,e1), eh = the multF of (product F) . (e1,h) as Element of product (Carrier F) by Def2;
A11: dom h1 = I by A1, CARD_3:9;
A12: now__::_thesis:_for_i_being_set_st_i_in_I_holds_
he_._i_=_h1_._i
let i be set ; ::_thesis: ( i in I implies he . i = h1 . i )
assume A13: i in I ; ::_thesis: he . i = h1 . i
then consider Fi being non empty multMagma , e2 being Element of Fi such that
A14: Fi = F . i and
A15: ee . i = e2 and
A16: for h being Element of Fi holds
( h * e2 = h & e2 * h = h & ex g being Element of Fi st
( h * g = e2 & g * h = e2 ) ) by A7;
reconsider h2 = h1 . i as Element of Fi by A13, A14, Lm1;
A17: ex Gi being non empty multMagma ex f being Function st
( Gi = F . i & f = the multF of (product F) . (h1,e1) & f . i = the multF of Gi . ((h1 . i),(ee . i)) ) by A10, A13, Def2;
h2 * e2 = h2 by A16;
hence he . i = h1 . i by A17, A14, A15; ::_thesis: verum
end;
dom he = I by A1, CARD_3:9;
hence h * e1 = h by A11, A12, FUNCT_1:2; ::_thesis: ( e1 * h = h & ex b1 being Element of the carrier of (product F) st
( h * b1 = e1 & b1 * h = e1 ) )
A18: now__::_thesis:_for_i_being_set_st_i_in_I_holds_
eh_._i_=_h1_._i
let i be set ; ::_thesis: ( i in I implies eh . i = h1 . i )
assume A19: i in I ; ::_thesis: eh . i = h1 . i
then consider Fi being non empty multMagma , e2 being Element of Fi such that
A20: Fi = F . i and
A21: ee . i = e2 and
A22: for h being Element of Fi holds
( h * e2 = h & e2 * h = h & ex g being Element of Fi st
( h * g = e2 & g * h = e2 ) ) by A7;
reconsider h2 = h1 . i as Element of Fi by A19, A20, Lm1;
A23: ex Gi being non empty multMagma ex f being Function st
( Gi = F . i & f = the multF of (product F) . (e1,h1) & f . i = the multF of Gi . ((ee . i),(h1 . i)) ) by A10, A19, Def2;
e2 * h2 = h2 by A22;
hence eh . i = h1 . i by A23, A20, A21; ::_thesis: verum
end;
defpred S2[ set , set ] means ex Fi being non empty multMagma ex hi being Element of Fi st
( Fi = F . I & hi = h1 . I & ex g being Element of Fi st
( hi * g = ee . I & g * hi = ee . I & F = g ) );
A24: for i being set st i in I holds
ex y being set st
( y in union (rng (Carrier F)) & S2[i,y] )
proof
let i be set ; ::_thesis: ( i in I implies ex y being set st
( y in union (rng (Carrier F)) & S2[i,y] ) )
assume A25: i in I ; ::_thesis: ex y being set st
( y in union (rng (Carrier F)) & S2[i,y] )
then consider Fi being non empty multMagma , e being Element of Fi such that
A26: Fi = F . i and
A27: ee . i = e and
A28: for h being Element of Fi holds
( h * e = h & e * h = h & ex g being Element of Fi st
( h * g = e & g * h = e ) ) by A7;
A29: ex R being 1-sorted st
( R = F . i & (Carrier F) . i = the carrier of R ) by A25, PRALG_1:def_13;
reconsider hi = h1 . i as Element of Fi by A25, A26, Lm1;
consider g being Element of Fi such that
A30: hi * g = e and
A31: g * hi = e by A28;
take g ; ::_thesis: ( g in union (rng (Carrier F)) & S2[i,g] )
(Carrier F) . i in rng (Carrier F) by A1, A25, FUNCT_1:def_3;
hence g in union (rng (Carrier F)) by A26, A29, TARSKI:def_4; ::_thesis: S2[i,g]
take Fi ; ::_thesis: ex hi being Element of Fi st
( Fi = F . i & hi = h1 . i & ex g being Element of Fi st
( hi * g = ee . i & g * hi = ee . i & g = g ) )
take hi ; ::_thesis: ( Fi = F . i & hi = h1 . i & ex g being Element of Fi st
( hi * g = ee . i & g * hi = ee . i & g = g ) )
thus ( Fi = F . i & hi = h1 . i ) by A26; ::_thesis: ex g being Element of Fi st
( hi * g = ee . i & g * hi = ee . i & g = g )
take g ; ::_thesis: ( hi * g = ee . i & g * hi = ee . i & g = g )
thus ( hi * g = ee . i & g * hi = ee . i & g = g ) by A27, A30, A31; ::_thesis: verum
end;
consider gg being Function such that
A32: dom gg = I and
rng gg c= union (rng (Carrier F)) and
A33: for x being set st x in I holds
S2[x,gg . x] from FUNCT_1:sch_5(A24);
now__::_thesis:_for_i_being_set_st_i_in_dom_gg_holds_
gg_._i_in_(Carrier_F)_._i
let i be set ; ::_thesis: ( i in dom gg implies gg . i in (Carrier F) . i )
assume A34: i in dom gg ; ::_thesis: gg . i in (Carrier F) . i
then A35: ex R being 1-sorted st
( R = F . i & (Carrier F) . i = the carrier of R ) by A32, PRALG_1:def_13;
ex Fi being non empty multMagma ex hi being Element of Fi st
( Fi = F . i & hi = h1 . i & ex g being Element of Fi st
( hi * g = ee . i & g * hi = ee . i & gg . i = g ) ) by A32, A33, A34;
hence gg . i in (Carrier F) . i by A35; ::_thesis: verum
end;
then A36: gg in product (Carrier F) by A1, A32, CARD_3:9;
then reconsider g1 = gg as Element of (product F) by Def2;
dom eh = I by A1, CARD_3:9;
hence e1 * h = h by A11, A18, FUNCT_1:2; ::_thesis: ex b1 being Element of the carrier of (product F) st
( h * b1 = e1 & b1 * h = e1 )
take g1 ; ::_thesis: ( h * g1 = e1 & g1 * h = e1 )
reconsider he = the multF of (product F) . (h,g1), eh = the multF of (product F) . (g1,h) as Element of product (Carrier F) by Def2;
A37: now__::_thesis:_for_i_being_set_st_i_in_I_holds_
he_._i_=_ee_._i
let i be set ; ::_thesis: ( i in I implies he . i = ee . i )
assume A38: i in I ; ::_thesis: he . i = ee . i
then A39: ex Fi being non empty multMagma ex hi being Element of Fi st
( Fi = F . i & hi = h1 . i & ex g being Element of Fi st
( hi * g = ee . i & g * hi = ee . i & gg . i = g ) ) by A33;
ex Gi being non empty multMagma ex h5 being Function st
( Gi = F . i & h5 = the multF of (product F) . (h1,gg) & h5 . i = the multF of Gi . ((h1 . i),(gg . i)) ) by A36, A38, Def2;
hence he . i = ee . i by A39; ::_thesis: verum
end;
A40: now__::_thesis:_for_i_being_set_st_i_in_I_holds_
eh_._i_=_ee_._i
let i be set ; ::_thesis: ( i in I implies eh . i = ee . i )
assume A41: i in I ; ::_thesis: eh . i = ee . i
then A42: ex Fi being non empty multMagma ex hi being Element of Fi st
( Fi = F . i & hi = h1 . i & ex g being Element of Fi st
( hi * g = ee . i & g * hi = ee . i & gg . i = g ) ) by A33;
ex Gi being non empty multMagma ex h5 being Function st
( Gi = F . i & h5 = the multF of (product F) . (gg,h1) & h5 . i = the multF of Gi . ((gg . i),(h1 . i)) ) by A36, A41, Def2;
hence eh . i = ee . i by A42; ::_thesis: verum
end;
dom he = I by A1, CARD_3:9;
hence h * g1 = e1 by A6, A37, FUNCT_1:2; ::_thesis: g1 * h = e1
dom eh = I by A1, CARD_3:9;
hence g1 * h = e1 by A6, A40, FUNCT_1:2; ::_thesis: verum
end;
end;
registration
let I be set ;
let F be associative multMagma-Family of I;
cluster product F -> strict associative ;
coherence
product F is associative
proof
set G = product F;
let x, y, z be Element of (product F); :: according to GROUP_1:def_3 ::_thesis: (x * y) * z = x * (y * z)
reconsider x1 = x, y1 = y, z1 = z as Element of product (Carrier F) by Def2;
set xy = the multF of (product F) . (x,y);
set yz = the multF of (product F) . (y,z);
set s = the multF of (product F) . (( the multF of (product F) . (x,y)),z);
set t = the multF of (product F) . (x,( the multF of (product F) . (y,z)));
reconsider xy = the multF of (product F) . (x,y), yz = the multF of (product F) . (y,z), s = the multF of (product F) . (( the multF of (product F) . (x,y)),z), t = the multF of (product F) . (x,( the multF of (product F) . (y,z))) as Element of product (Carrier F) by Def2;
A1: dom (Carrier F) = I by PARTFUN1:def_2;
then A2: dom t = I by CARD_3:9;
A3: now__::_thesis:_for_i_being_set_st_i_in_I_holds_
s_._i_=_t_._i
let i be set ; ::_thesis: ( i in I implies s . i = t . i )
assume A4: i in I ; ::_thesis: s . i = t . i
then consider XY being non empty multMagma , hxy being Function such that
A5: XY = F . i and
A6: hxy = the multF of (product F) . (x,y) and
A7: hxy . i = the multF of XY . ((x1 . i),(y1 . i)) by Def2;
A8: ex YZ being non empty multMagma ex hyz being Function st
( YZ = F . i & hyz = the multF of (product F) . (y,z) & hyz . i = the multF of YZ . ((y1 . i),(z1 . i)) ) by A4, Def2;
reconsider xi = x1 . i, yi = y1 . i as Element of XY by A4, A5, Lm1;
consider XYZ1 being non empty multMagma , hxyz1 being Function such that
A9: XYZ1 = F . i and
A10: hxyz1 = the multF of (product F) . (xy,z) and
A11: hxyz1 . i = the multF of XYZ1 . ((xy . i),(z1 . i)) by A4, Def2;
reconsider zi = z1 . i, xiyi = xi * yi as Element of XYZ1 by A4, A5, A9, Lm1;
reconsider xii = xi, yii = yi as Element of XYZ1 by A5, A9;
A12: XYZ1 is associative by A4, A9, Def7;
A13: ex XYZ2 being non empty multMagma ex hxyz2 being Function st
( XYZ2 = F . i & hxyz2 = the multF of (product F) . (x,yz) & hxyz2 . i = the multF of XYZ2 . ((x1 . i),(yz . i)) ) by A4, Def2;
thus s . i = xiyi * zi by A6, A7, A10, A11
.= xii * (yii * zi) by A5, A9, A12, GROUP_1:def_3
.= t . i by A8, A9, A13 ; ::_thesis: verum
end;
dom s = I by A1, CARD_3:9;
hence (x * y) * z = x * (y * z) by A2, A3, FUNCT_1:2; ::_thesis: verum
end;
end;
registration
let I be set ;
let F be commutative multMagma-Family of I;
cluster product F -> strict commutative ;
coherence
product F is commutative
proof
set G = product F;
let x, y be Element of (product F); :: according to GROUP_1:def_12 ::_thesis: x * y = y * x
reconsider x1 = x, y1 = y, xy = the multF of (product F) . (x,y), yx = the multF of (product F) . (y,x) as Element of product (Carrier F) by Def2;
A1: dom (Carrier F) = I by PARTFUN1:def_2;
then A2: dom yx = I by CARD_3:9;
A3: now__::_thesis:_for_i_being_set_st_i_in_I_holds_
xy_._i_=_yx_._i
let i be set ; ::_thesis: ( i in I implies xy . i = yx . i )
assume A4: i in I ; ::_thesis: xy . i = yx . i
then consider XY being non empty multMagma , hxy being Function such that
A5: XY = F . i and
A6: hxy = the multF of (product F) . (x,y) and
A7: hxy . i = the multF of XY . ((x1 . i),(y1 . i)) by Def2;
reconsider xi = x1 . i, yi = y1 . i as Element of XY by A4, A5, Lm1;
A8: ex YX being non empty multMagma ex hyx being Function st
( YX = F . i & hyx = the multF of (product F) . (y,x) & hyx . i = the multF of YX . ((y1 . i),(x1 . i)) ) by A4, Def2;
A9: ex Fi being non empty commutative multMagma st Fi = F . i by A4, Def5;
thus xy . i = xi * yi by A6, A7
.= yi * xi by A5, A9, GROUP_1:def_12
.= yx . i by A5, A8 ; ::_thesis: verum
end;
dom xy = I by A1, CARD_3:9;
hence x * y = y * x by A2, A3, FUNCT_1:2; ::_thesis: verum
end;
end;
theorem :: GROUP_7:2
for I, i being set
for F being multMagma-Family of I
for G being non empty multMagma st i in I & G = F . i & product F is Group-like holds
G is Group-like
proof
let I, i be set ; ::_thesis: for F being multMagma-Family of I
for G being non empty multMagma st i in I & G = F . i & product F is Group-like holds
G is Group-like
let F be multMagma-Family of I; ::_thesis: for G being non empty multMagma st i in I & G = F . i & product F is Group-like holds
G is Group-like
let G be non empty multMagma ; ::_thesis: ( i in I & G = F . i & product F is Group-like implies G is Group-like )
assume that
A1: i in I and
A2: G = F . i ; ::_thesis: ( not product F is Group-like or G is Group-like )
set GP = product F;
given e being Element of (product F) such that A3: for h being Element of (product F) holds
( h * e = h & e * h = h & ex g being Element of (product F) st
( h * g = e & g * h = e ) ) ; :: according to GROUP_1:def_2 ::_thesis: G is Group-like
reconsider f = e as Element of product (Carrier F) by Def2;
reconsider ei = f . i as Element of G by A1, A2, Lm1;
take ei ; :: according to GROUP_1:def_2 ::_thesis: for b1 being Element of the carrier of G holds
( b1 * ei = b1 & ei * b1 = b1 & ex b2 being Element of the carrier of G st
( b1 * b2 = ei & b2 * b1 = ei ) )
let h be Element of G; ::_thesis: ( h * ei = h & ei * h = h & ex b1 being Element of the carrier of G st
( h * b1 = ei & b1 * h = ei ) )
defpred S1[ set , set ] means ( ( $1 = i implies $2 = h ) & ( $1 <> i implies ex H being non empty multMagma ex a being Element of H st
( H = F . $1 & $2 = a ) ) );
A4: for j being set st j in I holds
ex k being set st S1[j,k]
proof
let j be set ; ::_thesis: ( j in I implies ex k being set st S1[j,k] )
assume A5: j in I ; ::_thesis: ex k being set st S1[j,k]
percases ( j = i or j <> i ) ;
suppose j = i ; ::_thesis: ex k being set st S1[j,k]
hence ex k being set st S1[j,k] ; ::_thesis: verum
end;
supposeA6: j <> i ; ::_thesis: ex k being set st S1[j,k]
j in dom F by A5, PARTFUN1:def_2;
then F . j in rng F by FUNCT_1:def_3;
then reconsider Fj = F . j as non empty multMagma by Def1;
set a = the Element of Fj;
take the Element of Fj ; ::_thesis: S1[j, the Element of Fj]
thus ( j = i implies the Element of Fj = h ) by A6; ::_thesis: ( j <> i implies ex H being non empty multMagma ex a being Element of H st
( H = F . j & the Element of Fj = a ) )
thus ( j <> i implies ex H being non empty multMagma ex a being Element of H st
( H = F . j & the Element of Fj = a ) ) ; ::_thesis: verum
end;
end;
end;
consider g being ManySortedSet of I such that
A7: for j being set st j in I holds
S1[j,g . j] from PBOOLE:sch_3(A4);
A8: dom g = I by PARTFUN1:def_2;
A9: now__::_thesis:_for_j_being_set_st_j_in_dom_g_holds_
g_._j_in_(Carrier_F)_._j
let j be set ; ::_thesis: ( j in dom g implies g . b1 in (Carrier F) . b1 )
assume A10: j in dom g ; ::_thesis: g . b1 in (Carrier F) . b1
then A11: ex R being 1-sorted st
( R = F . j & (Carrier F) . j = the carrier of R ) by PRALG_1:def_13;
percases ( i = j or j <> i ) ;
supposeA12: i = j ; ::_thesis: g . b1 in (Carrier F) . b1
then g . j = h by A7, A10;
hence g . j in (Carrier F) . j by A2, A11, A12; ::_thesis: verum
end;
suppose j <> i ; ::_thesis: g . b1 in (Carrier F) . b1
then ex H being non empty multMagma ex a being Element of H st
( H = F . j & g . j = a ) by A7, A10;
hence g . j in (Carrier F) . j by A11; ::_thesis: verum
end;
end;
end;
dom (Carrier F) = I by PARTFUN1:def_2;
then reconsider g = g as Element of product (Carrier F) by A8, A9, CARD_3:9;
A13: g . i = h by A1, A7;
reconsider g1 = g as Element of (product F) by Def2;
A14: e * g1 = g1 by A3;
g1 * e = g1 by A3;
hence ( h * ei = h & ei * h = h ) by A1, A2, A13, A14, Th4; ::_thesis: ex b1 being Element of the carrier of G st
( h * b1 = ei & b1 * h = ei )
consider gg being Element of (product F) such that
A15: g1 * gg = e and
A16: gg * g1 = e by A3;
reconsider r = gg as Element of product (Carrier F) by Def2;
reconsider r1 = r . i as Element of G by A1, A2, Lm1;
take r1 ; ::_thesis: ( h * r1 = ei & r1 * h = ei )
thus ( h * r1 = ei & r1 * h = ei ) by A1, A2, A13, A15, A16, Th4; ::_thesis: verum
end;
theorem :: GROUP_7:3
for I, i being set
for F being multMagma-Family of I
for G being non empty multMagma st i in I & G = F . i & product F is associative holds
G is associative
proof
let I, i be set ; ::_thesis: for F being multMagma-Family of I
for G being non empty multMagma st i in I & G = F . i & product F is associative holds
G is associative
let F be multMagma-Family of I; ::_thesis: for G being non empty multMagma st i in I & G = F . i & product F is associative holds
G is associative
let G be non empty multMagma ; ::_thesis: ( i in I & G = F . i & product F is associative implies G is associative )
assume that
A1: i in I and
A2: G = F . i and
A3: for x, y, z being Element of (product F) holds (x * y) * z = x * (y * z) ; :: according to GROUP_1:def_3 ::_thesis: G is associative
let x, y, z be Element of G; :: according to GROUP_1:def_3 ::_thesis: (x * y) * z = x * (y * z)
defpred S1[ set , set ] means ( ( $1 = i implies $2 = y ) & ( $1 <> i implies ex H being non empty multMagma ex a being Element of H st
( H = F . $1 & $2 = a ) ) );
A4: for j being set st j in I holds
ex k being set st S1[j,k]
proof
let j be set ; ::_thesis: ( j in I implies ex k being set st S1[j,k] )
assume A5: j in I ; ::_thesis: ex k being set st S1[j,k]
percases ( j = i or j <> i ) ;
suppose j = i ; ::_thesis: ex k being set st S1[j,k]
hence ex k being set st S1[j,k] ; ::_thesis: verum
end;
supposeA6: j <> i ; ::_thesis: ex k being set st S1[j,k]
j in dom F by A5, PARTFUN1:def_2;
then F . j in rng F by FUNCT_1:def_3;
then reconsider Fj = F . j as non empty multMagma by Def1;
set a = the Element of Fj;
take the Element of Fj ; ::_thesis: S1[j, the Element of Fj]
thus ( j = i implies the Element of Fj = y ) by A6; ::_thesis: ( j <> i implies ex H being non empty multMagma ex a being Element of H st
( H = F . j & the Element of Fj = a ) )
thus ( j <> i implies ex H being non empty multMagma ex a being Element of H st
( H = F . j & the Element of Fj = a ) ) ; ::_thesis: verum
end;
end;
end;
consider gy being ManySortedSet of I such that
A7: for j being set st j in I holds
S1[j,gy . j] from PBOOLE:sch_3(A4);
A8: dom gy = I by PARTFUN1:def_2;
A9: now__::_thesis:_for_j_being_set_st_j_in_dom_gy_holds_
gy_._j_in_(Carrier_F)_._j
let j be set ; ::_thesis: ( j in dom gy implies gy . b1 in (Carrier F) . b1 )
assume A10: j in dom gy ; ::_thesis: gy . b1 in (Carrier F) . b1
then A11: ex R being 1-sorted st
( R = F . j & (Carrier F) . j = the carrier of R ) by PRALG_1:def_13;
percases ( i = j or j <> i ) ;
supposeA12: i = j ; ::_thesis: gy . b1 in (Carrier F) . b1
then gy . j = y by A7, A10;
hence gy . j in (Carrier F) . j by A2, A11, A12; ::_thesis: verum
end;
suppose j <> i ; ::_thesis: gy . b1 in (Carrier F) . b1
then ex H being non empty multMagma ex a being Element of H st
( H = F . j & gy . j = a ) by A7, A10;
hence gy . j in (Carrier F) . j by A11; ::_thesis: verum
end;
end;
end;
defpred S2[ set , set ] means ( ( $1 = i implies $2 = z ) & ( $1 <> i implies ex H being non empty multMagma ex a being Element of H st
( H = F . $1 & $2 = a ) ) );
A13: for j being set st j in I holds
ex k being set st S2[j,k]
proof
let j be set ; ::_thesis: ( j in I implies ex k being set st S2[j,k] )
assume A14: j in I ; ::_thesis: ex k being set st S2[j,k]
percases ( j = i or j <> i ) ;
suppose j = i ; ::_thesis: ex k being set st S2[j,k]
hence ex k being set st S2[j,k] ; ::_thesis: verum
end;
supposeA15: j <> i ; ::_thesis: ex k being set st S2[j,k]
j in dom F by A14, PARTFUN1:def_2;
then F . j in rng F by FUNCT_1:def_3;
then reconsider Fj = F . j as non empty multMagma by Def1;
set a = the Element of Fj;
take the Element of Fj ; ::_thesis: S2[j, the Element of Fj]
thus ( j = i implies the Element of Fj = z ) by A15; ::_thesis: ( j <> i implies ex H being non empty multMagma ex a being Element of H st
( H = F . j & the Element of Fj = a ) )
thus ( j <> i implies ex H being non empty multMagma ex a being Element of H st
( H = F . j & the Element of Fj = a ) ) ; ::_thesis: verum
end;
end;
end;
consider gz being ManySortedSet of I such that
A16: for j being set st j in I holds
S2[j,gz . j] from PBOOLE:sch_3(A13);
set GP = product F;
defpred S3[ set , set ] means ( ( $1 = i implies $2 = x ) & ( $1 <> i implies ex H being non empty multMagma ex a being Element of H st
( H = F . $1 & $2 = a ) ) );
A17: for j being set st j in I holds
ex k being set st S3[j,k]
proof
let j be set ; ::_thesis: ( j in I implies ex k being set st S3[j,k] )
assume A18: j in I ; ::_thesis: ex k being set st S3[j,k]
percases ( j = i or j <> i ) ;
suppose j = i ; ::_thesis: ex k being set st S3[j,k]
hence ex k being set st S3[j,k] ; ::_thesis: verum
end;
supposeA19: j <> i ; ::_thesis: ex k being set st S3[j,k]
j in dom F by A18, PARTFUN1:def_2;
then F . j in rng F by FUNCT_1:def_3;
then reconsider Fj = F . j as non empty multMagma by Def1;
set a = the Element of Fj;
take the Element of Fj ; ::_thesis: S3[j, the Element of Fj]
thus ( j = i implies the Element of Fj = x ) by A19; ::_thesis: ( j <> i implies ex H being non empty multMagma ex a being Element of H st
( H = F . j & the Element of Fj = a ) )
thus ( j <> i implies ex H being non empty multMagma ex a being Element of H st
( H = F . j & the Element of Fj = a ) ) ; ::_thesis: verum
end;
end;
end;
consider gx being ManySortedSet of I such that
A20: for j being set st j in I holds
S3[j,gx . j] from PBOOLE:sch_3(A17);
A21: dom gx = I by PARTFUN1:def_2;
A22: now__::_thesis:_for_j_being_set_st_j_in_dom_gx_holds_
gx_._j_in_(Carrier_F)_._j
let j be set ; ::_thesis: ( j in dom gx implies gx . b1 in (Carrier F) . b1 )
assume A23: j in dom gx ; ::_thesis: gx . b1 in (Carrier F) . b1
then A24: ex R being 1-sorted st
( R = F . j & (Carrier F) . j = the carrier of R ) by PRALG_1:def_13;
percases ( i = j or j <> i ) ;
supposeA25: i = j ; ::_thesis: gx . b1 in (Carrier F) . b1
then gx . j = x by A20, A23;
hence gx . j in (Carrier F) . j by A2, A24, A25; ::_thesis: verum
end;
suppose j <> i ; ::_thesis: gx . b1 in (Carrier F) . b1
then ex H being non empty multMagma ex a being Element of H st
( H = F . j & gx . j = a ) by A20, A23;
hence gx . j in (Carrier F) . j by A24; ::_thesis: verum
end;
end;
end;
A26: dom gz = I by PARTFUN1:def_2;
A27: now__::_thesis:_for_j_being_set_st_j_in_dom_gz_holds_
gz_._j_in_(Carrier_F)_._j
let j be set ; ::_thesis: ( j in dom gz implies gz . b1 in (Carrier F) . b1 )
assume A28: j in dom gz ; ::_thesis: gz . b1 in (Carrier F) . b1
then A29: ex R being 1-sorted st
( R = F . j & (Carrier F) . j = the carrier of R ) by PRALG_1:def_13;
percases ( i = j or j <> i ) ;
supposeA30: i = j ; ::_thesis: gz . b1 in (Carrier F) . b1
then gz . j = z by A16, A28;
hence gz . j in (Carrier F) . j by A2, A29, A30; ::_thesis: verum
end;
suppose j <> i ; ::_thesis: gz . b1 in (Carrier F) . b1
then ex H being non empty multMagma ex a being Element of H st
( H = F . j & gz . j = a ) by A16, A28;
hence gz . j in (Carrier F) . j by A29; ::_thesis: verum
end;
end;
end;
A31: dom (Carrier F) = I by PARTFUN1:def_2;
then reconsider gx = gx as Element of product (Carrier F) by A21, A22, CARD_3:9;
reconsider gz = gz as Element of product (Carrier F) by A26, A31, A27, CARD_3:9;
reconsider gy = gy as Element of product (Carrier F) by A8, A31, A9, CARD_3:9;
reconsider x1 = gx, y1 = gy, z1 = gz as Element of (product F) by Def2;
reconsider xy = x1 * y1, xyz3 = (x1 * y1) * z1, yz = y1 * z1, xyz5 = x1 * (y1 * z1) as Element of product (Carrier F) by Def2;
reconsider xyi = xy . i, yzi = yz . i as Element of G by A1, A2, Lm1;
A32: (x1 * y1) * z1 = x1 * (y1 * z1) by A3;
A33: gx . i = x by A1, A20;
then A34: x * yzi = xyz5 . i by A1, A2, Th4;
A35: gz . i = z by A1, A16;
then A36: xyi * z = xyz3 . i by A1, A2, Th4;
A37: gy . i = y by A1, A7;
then xy . i = x * y by A1, A2, A33, Th4;
hence (x * y) * z = x * (y * z) by A1, A2, A32, A37, A35, A36, A34, Th4; ::_thesis: verum
end;
theorem :: GROUP_7:4
for I, i being set
for F being multMagma-Family of I
for G being non empty multMagma st i in I & G = F . i & product F is commutative holds
G is commutative
proof
let I, i be set ; ::_thesis: for F being multMagma-Family of I
for G being non empty multMagma st i in I & G = F . i & product F is commutative holds
G is commutative
let F be multMagma-Family of I; ::_thesis: for G being non empty multMagma st i in I & G = F . i & product F is commutative holds
G is commutative
let G be non empty multMagma ; ::_thesis: ( i in I & G = F . i & product F is commutative implies G is commutative )
assume that
A1: i in I and
A2: G = F . i and
A3: for x, y being Element of (product F) holds x * y = y * x ; :: according to GROUP_1:def_12 ::_thesis: G is commutative
let x, y be Element of G; :: according to GROUP_1:def_12 ::_thesis: x * y = y * x
defpred S1[ set , set ] means ( ( $1 = i implies $2 = y ) & ( $1 <> i implies ex H being non empty multMagma ex a being Element of H st
( H = F . $1 & $2 = a ) ) );
A4: for j being set st j in I holds
ex k being set st S1[j,k]
proof
let j be set ; ::_thesis: ( j in I implies ex k being set st S1[j,k] )
assume A5: j in I ; ::_thesis: ex k being set st S1[j,k]
percases ( j = i or j <> i ) ;
suppose j = i ; ::_thesis: ex k being set st S1[j,k]
hence ex k being set st S1[j,k] ; ::_thesis: verum
end;
supposeA6: j <> i ; ::_thesis: ex k being set st S1[j,k]
j in dom F by A5, PARTFUN1:def_2;
then F . j in rng F by FUNCT_1:def_3;
then reconsider Fj = F . j as non empty multMagma by Def1;
set a = the Element of Fj;
take the Element of Fj ; ::_thesis: S1[j, the Element of Fj]
thus ( j = i implies the Element of Fj = y ) by A6; ::_thesis: ( j <> i implies ex H being non empty multMagma ex a being Element of H st
( H = F . j & the Element of Fj = a ) )
thus ( j <> i implies ex H being non empty multMagma ex a being Element of H st
( H = F . j & the Element of Fj = a ) ) ; ::_thesis: verum
end;
end;
end;
consider gy being ManySortedSet of I such that
A7: for j being set st j in I holds
S1[j,gy . j] from PBOOLE:sch_3(A4);
set GP = product F;
defpred S2[ set , set ] means ( ( $1 = i implies $2 = x ) & ( $1 <> i implies ex H being non empty multMagma ex a being Element of H st
( H = F . $1 & $2 = a ) ) );
A8: for j being set st j in I holds
ex k being set st S2[j,k]
proof
let j be set ; ::_thesis: ( j in I implies ex k being set st S2[j,k] )
assume A9: j in I ; ::_thesis: ex k being set st S2[j,k]
percases ( j = i or j <> i ) ;
suppose j = i ; ::_thesis: ex k being set st S2[j,k]
hence ex k being set st S2[j,k] ; ::_thesis: verum
end;
supposeA10: j <> i ; ::_thesis: ex k being set st S2[j,k]
j in dom F by A9, PARTFUN1:def_2;
then F . j in rng F by FUNCT_1:def_3;
then reconsider Fj = F . j as non empty multMagma by Def1;
set a = the Element of Fj;
take the Element of Fj ; ::_thesis: S2[j, the Element of Fj]
thus ( j = i implies the Element of Fj = x ) by A10; ::_thesis: ( j <> i implies ex H being non empty multMagma ex a being Element of H st
( H = F . j & the Element of Fj = a ) )
thus ( j <> i implies ex H being non empty multMagma ex a being Element of H st
( H = F . j & the Element of Fj = a ) ) ; ::_thesis: verum
end;
end;
end;
consider gx being ManySortedSet of I such that
A11: for j being set st j in I holds
S2[j,gx . j] from PBOOLE:sch_3(A8);
A12: dom gy = I by PARTFUN1:def_2;
A13: now__::_thesis:_for_j_being_set_st_j_in_dom_gy_holds_
gy_._j_in_(Carrier_F)_._j
let j be set ; ::_thesis: ( j in dom gy implies gy . b1 in (Carrier F) . b1 )
assume A14: j in dom gy ; ::_thesis: gy . b1 in (Carrier F) . b1
then A15: ex R being 1-sorted st
( R = F . j & (Carrier F) . j = the carrier of R ) by PRALG_1:def_13;
percases ( i = j or j <> i ) ;
supposeA16: i = j ; ::_thesis: gy . b1 in (Carrier F) . b1
then gy . j = y by A7, A14;
hence gy . j in (Carrier F) . j by A2, A15, A16; ::_thesis: verum
end;
suppose j <> i ; ::_thesis: gy . b1 in (Carrier F) . b1
then ex H being non empty multMagma ex a being Element of H st
( H = F . j & gy . j = a ) by A7, A14;
hence gy . j in (Carrier F) . j by A15; ::_thesis: verum
end;
end;
end;
A17: dom (Carrier F) = I by PARTFUN1:def_2;
then reconsider gy = gy as Element of product (Carrier F) by A12, A13, CARD_3:9;
A18: gy . i = y by A1, A7;
A19: dom gx = I by PARTFUN1:def_2;
now__::_thesis:_for_j_being_set_st_j_in_dom_gx_holds_
gx_._j_in_(Carrier_F)_._j
let j be set ; ::_thesis: ( j in dom gx implies gx . b1 in (Carrier F) . b1 )
assume A20: j in dom gx ; ::_thesis: gx . b1 in (Carrier F) . b1
then A21: ex R being 1-sorted st
( R = F . j & (Carrier F) . j = the carrier of R ) by PRALG_1:def_13;
percases ( i = j or j <> i ) ;
supposeA22: i = j ; ::_thesis: gx . b1 in (Carrier F) . b1
then gx . j = x by A11, A20;
hence gx . j in (Carrier F) . j by A2, A21, A22; ::_thesis: verum
end;
suppose j <> i ; ::_thesis: gx . b1 in (Carrier F) . b1
then ex H being non empty multMagma ex a being Element of H st
( H = F . j & gx . j = a ) by A11, A20;
hence gx . j in (Carrier F) . j by A21; ::_thesis: verum
end;
end;
end;
then reconsider gx = gx as Element of product (Carrier F) by A19, A17, CARD_3:9;
reconsider x1 = gx, y1 = gy as Element of (product F) by Def2;
A23: x1 * y1 = y1 * x1 by A3;
reconsider xy = x1 * y1 as Element of product (Carrier F) by Def2;
A24: gx . i = x by A1, A11;
then xy . i = x * y by A1, A2, A18, Th4;
hence x * y = y * x by A1, A2, A23, A24, A18, Th4; ::_thesis: verum
end;
theorem Th8: :: GROUP_7:5
for I being set
for s being ManySortedSet of I
for F being Group-like multMagma-Family of I st ( for i being set st i in I holds
ex G being non empty Group-like multMagma st
( G = F . i & s . i = 1_ G ) ) holds
s = 1_ (product F)
proof
let I be set ; ::_thesis: for s being ManySortedSet of I
for F being Group-like multMagma-Family of I st ( for i being set st i in I holds
ex G being non empty Group-like multMagma st
( G = F . i & s . i = 1_ G ) ) holds
s = 1_ (product F)
let s be ManySortedSet of I; ::_thesis: for F being Group-like multMagma-Family of I st ( for i being set st i in I holds
ex G being non empty Group-like multMagma st
( G = F . i & s . i = 1_ G ) ) holds
s = 1_ (product F)
let F be Group-like multMagma-Family of I; ::_thesis: ( ( for i being set st i in I holds
ex G being non empty Group-like multMagma st
( G = F . i & s . i = 1_ G ) ) implies s = 1_ (product F) )
assume A1: for i being set st i in I holds
ex G being non empty Group-like multMagma st
( G = F . i & s . i = 1_ G ) ; ::_thesis: s = 1_ (product F)
set GP = product F;
A2: dom (Carrier F) = I by PARTFUN1:def_2;
A3: dom s = I by PARTFUN1:def_2;
now__::_thesis:_for_i_being_set_st_i_in_dom_s_holds_
s_._i_in_(Carrier_F)_._i
let i be set ; ::_thesis: ( i in dom s implies s . i in (Carrier F) . i )
assume A4: i in dom s ; ::_thesis: s . i in (Carrier F) . i
then A5: ex R being 1-sorted st
( R = F . i & (Carrier F) . i = the carrier of R ) by PRALG_1:def_13;
ex G being non empty Group-like multMagma st
( G = F . i & s . i = 1_ G ) by A1, A4;
hence s . i in (Carrier F) . i by A5; ::_thesis: verum
end;
then A6: s in product (Carrier F) by A3, A2, CARD_3:9;
then reconsider e = s as Element of (product F) by Def2;
now__::_thesis:_for_h_being_Element_of_(product_F)_holds_
(_h_*_e_=_h_&_e_*_h_=_h_)
let h be Element of (product F); ::_thesis: ( h * e = h & e * h = h )
reconsider h1 = h, he = h * e, eh = e * h as Element of product (Carrier F) by Def2;
A7: dom h1 = I by A2, CARD_3:9;
A8: now__::_thesis:_for_i_being_set_st_i_in_I_holds_
he_._i_=_h1_._i
let i be set ; ::_thesis: ( i in I implies he . i = h1 . i )
assume A9: i in I ; ::_thesis: he . i = h1 . i
then consider G being non empty Group-like multMagma such that
A10: G = F . i and
A11: s . i = 1_ G by A1;
reconsider b = h1 . i, c = s . i as Element of G by A9, A10, A11, Lm1;
A12: ex Fi being non empty multMagma ex m being Function st
( Fi = F . i & m = the multF of (product F) . (h,s) & m . i = the multF of Fi . ((h1 . i),(s . i)) ) by A6, A9, Def2;
b * c = b by A11, GROUP_1:def_4;
hence he . i = h1 . i by A12, A10; ::_thesis: verum
end;
dom he = I by A2, CARD_3:9;
hence h * e = h by A7, A8, FUNCT_1:2; ::_thesis: e * h = h
A13: now__::_thesis:_for_i_being_set_st_i_in_I_holds_
eh_._i_=_h1_._i
let i be set ; ::_thesis: ( i in I implies eh . i = h1 . i )
assume A14: i in I ; ::_thesis: eh . i = h1 . i
then consider G being non empty Group-like multMagma such that
A15: G = F . i and
A16: s . i = 1_ G by A1;
reconsider b = h1 . i, c = s . i as Element of G by A14, A15, A16, Lm1;
A17: ex Fi being non empty multMagma ex m being Function st
( Fi = F . i & m = the multF of (product F) . (s,h) & m . i = the multF of Fi . ((s . i),(h1 . i)) ) by A6, A14, Def2;
c * b = b by A16, GROUP_1:def_4;
hence eh . i = h1 . i by A17, A15; ::_thesis: verum
end;
dom eh = I by A2, CARD_3:9;
hence e * h = h by A7, A13, FUNCT_1:2; ::_thesis: verum
end;
hence s = 1_ (product F) by GROUP_1:4; ::_thesis: verum
end;
theorem Th9: :: GROUP_7:6
for I, i being set
for f being Function
for F being Group-like multMagma-Family of I
for G being non empty Group-like multMagma st i in I & G = F . i & f = 1_ (product F) holds
f . i = 1_ G
proof
let I, i be set ; ::_thesis: for f being Function
for F being Group-like multMagma-Family of I
for G being non empty Group-like multMagma st i in I & G = F . i & f = 1_ (product F) holds
f . i = 1_ G
let f be Function; ::_thesis: for F being Group-like multMagma-Family of I
for G being non empty Group-like multMagma st i in I & G = F . i & f = 1_ (product F) holds
f . i = 1_ G
let F be Group-like multMagma-Family of I; ::_thesis: for G being non empty Group-like multMagma st i in I & G = F . i & f = 1_ (product F) holds
f . i = 1_ G
let G be non empty Group-like multMagma ; ::_thesis: ( i in I & G = F . i & f = 1_ (product F) implies f . i = 1_ G )
assume that
A1: i in I and
A2: G = F . i and
A3: f = 1_ (product F) ; ::_thesis: f . i = 1_ G
set GP = product F;
f in the carrier of (product F) by A3;
then A4: f in product (Carrier F) by Def2;
then reconsider e = f . i as Element of G by A1, A2, Lm1;
now__::_thesis:_for_h_being_Element_of_G_holds_
(_h_*_e_=_h_&_e_*_h_=_h_)
let h be Element of G; ::_thesis: ( h * e = h & e * h = h )
defpred S1[ set , set ] means ( ( $1 = i implies $2 = h ) & ( $1 <> i implies ex H being non empty Group-like multMagma st
( H = F . $1 & $2 = 1_ H ) ) );
A5: for j being set st j in I holds
ex k being set st S1[j,k]
proof
let j be set ; ::_thesis: ( j in I implies ex k being set st S1[j,k] )
assume A6: j in I ; ::_thesis: ex k being set st S1[j,k]
percases ( j = i or j <> i ) ;
suppose j = i ; ::_thesis: ex k being set st S1[j,k]
hence ex k being set st S1[j,k] ; ::_thesis: verum
end;
supposeA7: j <> i ; ::_thesis: ex k being set st S1[j,k]
consider Fj being non empty Group-like multMagma such that
A8: Fj = F . j by A6, Def3;
take 1_ Fj ; ::_thesis: S1[j, 1_ Fj]
thus ( j = i implies 1_ Fj = h ) by A7; ::_thesis: ( j <> i implies ex H being non empty Group-like multMagma st
( H = F . j & 1_ Fj = 1_ H ) )
thus ( j <> i implies ex H being non empty Group-like multMagma st
( H = F . j & 1_ Fj = 1_ H ) ) by A8; ::_thesis: verum
end;
end;
end;
consider g being ManySortedSet of I such that
A9: for j being set st j in I holds
S1[j,g . j] from PBOOLE:sch_3(A5);
A10: dom g = I by PARTFUN1:def_2;
A11: now__::_thesis:_for_j_being_set_st_j_in_dom_g_holds_
g_._j_in_(Carrier_F)_._j
let j be set ; ::_thesis: ( j in dom g implies g . b1 in (Carrier F) . b1 )
assume A12: j in dom g ; ::_thesis: g . b1 in (Carrier F) . b1
then A13: ex R being 1-sorted st
( R = F . j & (Carrier F) . j = the carrier of R ) by PRALG_1:def_13;
percases ( i = j or j <> i ) ;
supposeA14: i = j ; ::_thesis: g . b1 in (Carrier F) . b1
then g . j = h by A9, A12;
hence g . j in (Carrier F) . j by A2, A13, A14; ::_thesis: verum
end;
suppose j <> i ; ::_thesis: g . b1 in (Carrier F) . b1
then ex H being non empty Group-like multMagma st
( H = F . j & g . j = 1_ H ) by A9, A12;
hence g . j in (Carrier F) . j by A13; ::_thesis: verum
end;
end;
end;
dom (Carrier F) = I by PARTFUN1:def_2;
then A15: g in product (Carrier F) by A10, A11, CARD_3:9;
then reconsider g1 = g as Element of (product F) by Def2;
A16: g1 * (1_ (product F)) = g1 by GROUP_1:def_4;
A17: g . i = h by A1, A9;
A18: g . i = h by A1, A9;
ex Fi being non empty multMagma ex m being Function st
( Fi = F . i & m = the multF of (product F) . (g,f) & m . i = the multF of Fi . ((g . i),(f . i)) ) by A1, A4, A15, Def2;
hence h * e = h by A2, A3, A16, A18; ::_thesis: e * h = h
A19: (1_ (product F)) * g1 = g1 by GROUP_1:def_4;
ex Fi being non empty multMagma ex m being Function st
( Fi = F . i & m = the multF of (product F) . (f,g) & m . i = the multF of Fi . ((f . i),(g . i)) ) by A1, A4, A15, Def2;
hence e * h = h by A2, A3, A19, A17; ::_thesis: verum
end;
hence f . i = 1_ G by GROUP_1:4; ::_thesis: verum
end;
theorem Th10: :: GROUP_7:7
for I being set
for g being Function
for s being ManySortedSet of I
for F being Group-like associative multMagma-Family of I
for x being Element of (product F) st x = g & ( for i being set st i in I holds
ex G being Group ex y being Element of G st
( G = F . i & s . i = y " & y = g . i ) ) holds
s = x "
proof
let I be set ; ::_thesis: for g being Function
for s being ManySortedSet of I
for F being Group-like associative multMagma-Family of I
for x being Element of (product F) st x = g & ( for i being set st i in I holds
ex G being Group ex y being Element of G st
( G = F . i & s . i = y " & y = g . i ) ) holds
s = x "
let g be Function; ::_thesis: for s being ManySortedSet of I
for F being Group-like associative multMagma-Family of I
for x being Element of (product F) st x = g & ( for i being set st i in I holds
ex G being Group ex y being Element of G st
( G = F . i & s . i = y " & y = g . i ) ) holds
s = x "
let s be ManySortedSet of I; ::_thesis: for F being Group-like associative multMagma-Family of I
for x being Element of (product F) st x = g & ( for i being set st i in I holds
ex G being Group ex y being Element of G st
( G = F . i & s . i = y " & y = g . i ) ) holds
s = x "
let F be Group-like associative multMagma-Family of I; ::_thesis: for x being Element of (product F) st x = g & ( for i being set st i in I holds
ex G being Group ex y being Element of G st
( G = F . i & s . i = y " & y = g . i ) ) holds
s = x "
let x be Element of (product F); ::_thesis: ( x = g & ( for i being set st i in I holds
ex G being Group ex y being Element of G st
( G = F . i & s . i = y " & y = g . i ) ) implies s = x " )
assume that
A1: x = g and
A2: for i being set st i in I holds
ex G being Group ex y being Element of G st
( G = F . i & s . i = y " & y = g . i ) ; ::_thesis: s = x "
set GP = product F;
A3: dom (Carrier F) = I by PARTFUN1:def_2;
A4: dom s = I by PARTFUN1:def_2;
now__::_thesis:_for_i_being_set_st_i_in_dom_s_holds_
s_._i_in_(Carrier_F)_._i
let i be set ; ::_thesis: ( i in dom s implies s . i in (Carrier F) . i )
assume A5: i in dom s ; ::_thesis: s . i in (Carrier F) . i
then A6: ex R being 1-sorted st
( R = F . i & (Carrier F) . i = the carrier of R ) by PRALG_1:def_13;
ex G being Group ex y being Element of G st
( G = F . i & s . i = y " & y = g . i ) by A2, A5;
hence s . i in (Carrier F) . i by A6; ::_thesis: verum
end;
then A7: s in product (Carrier F) by A3, A4, CARD_3:9;
then reconsider f1 = s as Element of (product F) by Def2;
reconsider II = 1_ (product F), xf = x * f1, fx = f1 * x, x1 = x as Element of product (Carrier F) by Def2;
A8: dom II = I by A3, CARD_3:9;
A9: now__::_thesis:_for_i_being_set_st_i_in_I_holds_
fx_._i_=_II_._i
let i be set ; ::_thesis: ( i in I implies fx . i = II . i )
assume A10: i in I ; ::_thesis: fx . i = II . i
then consider G being Group, y being Element of G such that
A11: G = F . i and
A12: s . i = y " and
A13: y = g . i by A2;
A14: ex Fi being non empty multMagma ex m being Function st
( Fi = F . i & m = the multF of (product F) . (s,x) & m . i = the multF of Fi . ((s . i),(x1 . i)) ) by A7, A10, Def2;
(y ") * y = 1_ G by GROUP_1:def_5;
hence fx . i = II . i by A1, A10, A14, A11, A12, A13, Th9; ::_thesis: verum
end;
dom fx = I by A3, CARD_3:9;
then A15: f1 * x = 1_ (product F) by A8, A9, FUNCT_1:2;
A16: now__::_thesis:_for_i_being_set_st_i_in_I_holds_
xf_._i_=_II_._i
let i be set ; ::_thesis: ( i in I implies xf . i = II . i )
assume A17: i in I ; ::_thesis: xf . i = II . i
then consider G being Group, y being Element of G such that
A18: G = F . i and
A19: s . i = y " and
A20: y = g . i by A2;
A21: ex Fi being non empty multMagma ex m being Function st
( Fi = F . i & m = the multF of (product F) . (x,s) & m . i = the multF of Fi . ((x1 . i),(s . i)) ) by A7, A17, Def2;
y * (y ") = 1_ G by GROUP_1:def_5;
hence xf . i = II . i by A1, A17, A21, A18, A19, A20, Th9; ::_thesis: verum
end;
dom xf = I by A3, CARD_3:9;
then x * f1 = 1_ (product F) by A8, A16, FUNCT_1:2;
hence s = x " by A15, GROUP_1:def_5; ::_thesis: verum
end;
theorem Th11: :: GROUP_7:8
for I, i being set
for f, g being Function
for F being Group-like associative multMagma-Family of I
for x being Element of (product F)
for G being Group
for y being Element of G st i in I & G = F . i & f = x & g = x " & f . i = y holds
g . i = y "
proof
let I, i be set ; ::_thesis: for f, g being Function
for F being Group-like associative multMagma-Family of I
for x being Element of (product F)
for G being Group
for y being Element of G st i in I & G = F . i & f = x & g = x " & f . i = y holds
g . i = y "
let f, g be Function; ::_thesis: for F being Group-like associative multMagma-Family of I
for x being Element of (product F)
for G being Group
for y being Element of G st i in I & G = F . i & f = x & g = x " & f . i = y holds
g . i = y "
let F be Group-like associative multMagma-Family of I; ::_thesis: for x being Element of (product F)
for G being Group
for y being Element of G st i in I & G = F . i & f = x & g = x " & f . i = y holds
g . i = y "
let x be Element of (product F); ::_thesis: for G being Group
for y being Element of G st i in I & G = F . i & f = x & g = x " & f . i = y holds
g . i = y "
let G be Group; ::_thesis: for y being Element of G st i in I & G = F . i & f = x & g = x " & f . i = y holds
g . i = y "
let y be Element of G; ::_thesis: ( i in I & G = F . i & f = x & g = x " & f . i = y implies g . i = y " )
assume that
A1: i in I and
A2: G = F . i and
A3: f = x and
A4: g = x " and
A5: f . i = y ; ::_thesis: g . i = y "
set GP = product F;
A6: the multF of (product F) . (g,f) = (x ") * x by A3, A4
.= 1_ (product F) by GROUP_1:def_5 ;
x " in the carrier of (product F) ;
then A7: g in product (Carrier F) by A4, Def2;
then reconsider gi = g . i as Element of G by A1, A2, Lm1;
x in the carrier of (product F) ;
then A8: f in product (Carrier F) by A3, Def2;
then ex Fi being non empty multMagma ex h being Function st
( Fi = F . i & h = the multF of (product F) . (g,f) & h . i = the multF of Fi . ((g . i),(f . i)) ) by A1, A7, Def2;
then A9: gi * y = 1_ G by A1, A2, A5, A6, Th9;
A10: the multF of (product F) . (f,g) = x * (x ") by A3, A4
.= 1_ (product F) by GROUP_1:def_5 ;
ex Fi being non empty multMagma ex h being Function st
( Fi = F . i & h = the multF of (product F) . (f,g) & h . i = the multF of Fi . ((f . i),(g . i)) ) by A1, A8, A7, Def2;
then y * gi = 1_ G by A1, A2, A5, A10, Th9;
hence g . i = y " by A9, GROUP_1:def_5; ::_thesis: verum
end;
definition
let I be set ;
let F be Group-like associative multMagma-Family of I;
func sum F -> strict Subgroup of product F means :Def9: :: GROUP_7:def 9
for x being set holds
( x in the carrier of it iff ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st
( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) );
existence
ex b1 being strict Subgroup of product F st
for x being set holds
( x in the carrier of b1 iff ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st
( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) )
proof
set GP = product F;
set CF = Carrier F;
A1: dom (Carrier F) = I by PARTFUN1:def_2;
reconsider g = 1_ (product F) as Element of product (Carrier F) by Def2;
A2: dom g = dom (Carrier F) by CARD_3:9;
defpred S1[ set ] means ex J being finite Subset of I ex f being ManySortedSet of J st
( $1 = g +* f & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) );
consider A being set such that
A3: for x being set holds
( x in A iff ( x in product (Carrier F) & S1[x] ) ) from XBOOLE_0:sch_1();
A4: A c= the carrier of (product F)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A or a in the carrier of (product F) )
assume a in A ; ::_thesis: a in the carrier of (product F)
then a in product (Carrier F) by A3;
hence a in the carrier of (product F) by Def2; ::_thesis: verum
end;
A5: S1[g]
proof
set J = {} I;
dom {} = {} I ;
then reconsider f = {} as ManySortedSet of {} I by PARTFUN1:def_2, RELAT_1:def_18;
take {} I ; ::_thesis: ex f being ManySortedSet of {} I st
( g = g +* f & ( for j being set st j in {} I holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) )
take f ; ::_thesis: ( g = g +* f & ( for j being set st j in {} I holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) )
thus g = g +* {}
.= g +* f ; ::_thesis: for j being set st j in {} I holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G )
thus for j being set st j in {} I holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ; ::_thesis: verum
end;
then reconsider A = A as non empty set by A3;
set b = the multF of (product F) || A;
A6: for p being Element of product (Carrier F) holds dom p = I by PARTFUN1:def_2;
( dom ( the multF of (product F) || A) = [:A,A:] & rng ( the multF of (product F) || A) c= A )
proof
dom the multF of (product F) = [: the carrier of (product F), the carrier of (product F):] by FUNCT_2:def_1;
hence A7: dom ( the multF of (product F) || A) = [:A,A:] by A4, RELAT_1:62, ZFMISC_1:96; ::_thesis: rng ( the multF of (product F) || A) c= A
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ( the multF of (product F) || A) or y in A )
assume y in rng ( the multF of (product F) || A) ; ::_thesis: y in A
then consider x being set such that
A8: x in dom ( the multF of (product F) || A) and
A9: ( the multF of (product F) || A) . x = y by FUNCT_1:def_3;
consider x1, x2 being set such that
A10: x1 in A and
A11: x2 in A and
A12: x = [x1,x2] by A7, A8, ZFMISC_1:def_2;
consider J1 being finite Subset of I, f1 being ManySortedSet of J1 such that
A13: x1 = g +* f1 and
A14: for j being set st j in J1 holds
ex G being non empty Group-like multMagma st
( G = F . j & f1 . j in the carrier of G & f1 . j <> 1_ G ) by A3, A10;
consider J2 being finite Subset of I, f2 being ManySortedSet of J2 such that
A15: x2 = g +* f2 and
A16: for j being set st j in J2 holds
ex G being non empty Group-like multMagma st
( G = F . j & f2 . j in the carrier of G & f2 . j <> 1_ G ) by A3, A11;
reconsider x1 = x1, x2 = x2 as Function by A13, A15;
A17: dom f1 = J1 by PARTFUN1:def_2;
A18: now__::_thesis:_for_i_being_set_st_i_in_I_holds_
x1_._i_in_(Carrier_F)_._i
let i be set ; ::_thesis: ( i in I implies x1 . b1 in (Carrier F) . b1 )
assume A19: i in I ; ::_thesis: x1 . b1 in (Carrier F) . b1
then A20: ex R being 1-sorted st
( R = F . i & (Carrier F) . i = the carrier of R ) by PRALG_1:def_13;
percases ( i in J1 or not i in J1 ) ;
supposeA21: i in J1 ; ::_thesis: x1 . b1 in (Carrier F) . b1
then ex G being non empty Group-like multMagma st
( G = F . i & f1 . i in the carrier of G & f1 . i <> 1_ G ) by A14;
hence x1 . i in (Carrier F) . i by A13, A17, A20, A21, FUNCT_4:13; ::_thesis: verum
end;
supposeA22: not i in J1 ; ::_thesis: x1 . b1 in (Carrier F) . b1
consider G being non empty Group-like multMagma such that
A23: G = F . i by A19, Def3;
x1 . i = g . i by A13, A17, A22, FUNCT_4:11
.= 1_ G by A19, A23, Th9 ;
hence x1 . i in (Carrier F) . i by A20, A23; ::_thesis: verum
end;
end;
end;
A24: dom f2 = J2 by PARTFUN1:def_2;
A25: now__::_thesis:_for_i_being_set_st_i_in_I_holds_
x2_._i_in_(Carrier_F)_._i
let i be set ; ::_thesis: ( i in I implies x2 . b1 in (Carrier F) . b1 )
assume A26: i in I ; ::_thesis: x2 . b1 in (Carrier F) . b1
then A27: ex R being 1-sorted st
( R = F . i & (Carrier F) . i = the carrier of R ) by PRALG_1:def_13;
percases ( i in J2 or not i in J2 ) ;
supposeA28: i in J2 ; ::_thesis: x2 . b1 in (Carrier F) . b1
then ex G being non empty Group-like multMagma st
( G = F . i & f2 . i in the carrier of G & f2 . i <> 1_ G ) by A16;
hence x2 . i in (Carrier F) . i by A15, A24, A27, A28, FUNCT_4:13; ::_thesis: verum
end;
supposeA29: not i in J2 ; ::_thesis: x2 . b1 in (Carrier F) . b1
consider G being non empty Group-like multMagma such that
A30: G = F . i by A26, Def3;
x2 . i = g . i by A15, A24, A29, FUNCT_4:11
.= 1_ G by A26, A30, Th9 ;
hence x2 . i in (Carrier F) . i by A27, A30; ::_thesis: verum
end;
end;
end;
A31: dom x1 = (dom g) \/ (dom f1) by A13, FUNCT_4:def_1
.= I by A2, A1, A17, XBOOLE_1:12 ;
dom x2 = (dom g) \/ (dom f2) by A15, FUNCT_4:def_1
.= I by A2, A1, A24, XBOOLE_1:12 ;
then reconsider x2 = x2 as Element of product (Carrier F) by A1, A25, CARD_3:9;
reconsider x1 = x1 as Element of product (Carrier F) by A1, A31, A18, CARD_3:9;
reconsider X1 = x1, X2 = x2 as Element of (product F) by Def2;
A32: [x1,x2] in [:A,A:] by A10, A11, ZFMISC_1:87;
then A33: y = X1 * X2 by A9, A12, FUNCT_1:49;
then reconsider y1 = y as Element of product (Carrier F) by Def2;
defpred S2[ set ] means ex G being non empty Group-like multMagma ex k1, k2 being Element of G st
( G = F . $1 & k1 = x1 . $1 & k2 = x2 . $1 & k1 * k2 = 1_ G & f1 . $1 <> 1_ G & f2 . $1 <> 1_ G );
consider K being set such that
A34: for k being set holds
( k in K iff ( k in I & S2[k] ) ) from XBOOLE_0:sch_1();
A35: S1[y]
proof
defpred S3[ set , set ] means ex G being non empty Group-like multMagma ex k1, k2 being Element of G st
( G = F . $1 & k1 = x1 . $1 & k2 = x2 . $1 & $2 = k1 * k2 );
reconsider J = (J1 \/ J2) \ K as finite Subset of I ;
take J ; ::_thesis: ex f being ManySortedSet of J st
( y = g +* f & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) )
A36: dom y1 = I by A6;
A37: for j being set st j in J holds
ex t being set st S3[j,t]
proof
let j be set ; ::_thesis: ( j in J implies ex t being set st S3[j,t] )
assume A38: j in J ; ::_thesis: ex t being set st S3[j,t]
then consider G being non empty Group-like multMagma such that
A39: G = F . j by Def3;
reconsider k1 = x1 . j, k2 = x2 . j as Element of G by A38, A39, Lm1;
take k1 * k2 ; ::_thesis: S3[j,k1 * k2]
thus S3[j,k1 * k2] by A39; ::_thesis: verum
end;
consider f being ManySortedSet of J such that
A40: for j being set st j in J holds
S3[j,f . j] from PBOOLE:sch_3(A37);
take f ; ::_thesis: ( y = g +* f & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) )
set gf = g +* f;
A41: dom f = J by PARTFUN1:def_2;
A42: now__::_thesis:_for_i_being_set_st_i_in_I_holds_
y1_._i_=_(g_+*_f)_._i
let i be set ; ::_thesis: ( i in I implies y1 . b1 = (g +* f) . b1 )
assume A43: i in I ; ::_thesis: y1 . b1 = (g +* f) . b1
then consider Fi being non empty multMagma , h being Function such that
A44: Fi = F . i and
A45: h = the multF of (product F) . (x1,x2) and
A46: h . i = the multF of Fi . ((x1 . i),(x2 . i)) by Def2;
consider FF being non empty Group-like multMagma such that
A47: FF = F . i by A43, Def3;
reconsider Fi = Fi as non empty Group-like multMagma by A44, A47;
reconsider x1i = x1 . i, x2i = x2 . i as Element of Fi by A43, A44, Lm1;
A48: y1 . i = x1i * x2i by A9, A12, A32, A45, A46, FUNCT_1:49;
percases ( i in J or not i in J ) ;
supposeA49: i in J ; ::_thesis: y1 . b1 = (g +* f) . b1
then ex GG being non empty Group-like multMagma ex k1a, k2a being Element of GG st
( GG = F . i & k1a = x1 . i & k2a = x2 . i & f . i = k1a * k2a ) by A40;
hence y1 . i = (g +* f) . i by A33, A41, A44, A45, A46, A49, FUNCT_4:13; ::_thesis: verum
end;
supposeA50: not i in J ; ::_thesis: y1 . b1 = (g +* f) . b1
then A51: (g +* f) . i = g . i by A41, FUNCT_4:11
.= 1_ FF by A43, A47, Th9 ;
now__::_thesis:_(_(_not_i_in_J1_\/_J2_&_y1_._i_=_(g_+*_f)_._i_)_or_(_i_in_K_&_y1_._i_=_(g_+*_f)_._i_)_)
percases ( not i in J1 \/ J2 or i in K ) by A50, XBOOLE_0:def_5;
caseA52: not i in J1 \/ J2 ; ::_thesis: y1 . i = (g +* f) . i
then not i in J2 by XBOOLE_0:def_3;
then x2 . i = g . i by A15, A24, FUNCT_4:11;
then A53: x2 . i = 1_ FF by A43, A47, Th9;
not i in J1 by A52, XBOOLE_0:def_3;
then x1 . i = g . i by A13, A17, FUNCT_4:11;
then x1 . i = 1_ FF by A43, A47, Th9;
hence y1 . i = (g +* f) . i by A44, A47, A48, A51, A53, GROUP_1:def_4; ::_thesis: verum
end;
case i in K ; ::_thesis: y1 . i = (g +* f) . i
then ex GG being non empty Group-like multMagma ex k1, k2 being Element of GG st
( GG = F . i & k1 = x1 . i & k2 = x2 . i & k1 * k2 = 1_ GG & f1 . i <> 1_ GG & f2 . i <> 1_ GG ) by A34;
hence y1 . i = (g +* f) . i by A33, A43, A47, A51, Th4; ::_thesis: verum
end;
end;
end;
hence y1 . i = (g +* f) . i ; ::_thesis: verum
end;
end;
end;
dom (g +* f) = (dom g) \/ (dom f) by FUNCT_4:def_1
.= I by A2, A1, A41, XBOOLE_1:12 ;
hence y = g +* f by A36, A42, FUNCT_1:2; ::_thesis: for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G )
let j be set ; ::_thesis: ( j in J implies ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) )
assume A54: j in J ; ::_thesis: ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G )
then consider G being non empty Group-like multMagma , k1, k2 being Element of G such that
A55: G = F . j and
A56: k1 = x1 . j and
A57: k2 = x2 . j and
A58: f . j = k1 * k2 by A40;
take G ; ::_thesis: ( G = F . j & f . j in the carrier of G & f . j <> 1_ G )
thus G = F . j by A55; ::_thesis: ( f . j in the carrier of G & f . j <> 1_ G )
thus f . j in the carrier of G by A58; ::_thesis: f . j <> 1_ G
A59: j in J1 \/ J2 by A54, XBOOLE_0:def_5;
percases ( ( j in J1 & not j in J2 ) or ( not j in J1 & j in J2 ) or ( j in J1 & j in J2 ) ) by A59, XBOOLE_0:def_3;
supposeA60: ( j in J1 & not j in J2 ) ; ::_thesis: f . j <> 1_ G
then A61: x1 . j = f1 . j by A13, A17, FUNCT_4:13;
consider G1 being non empty Group-like multMagma such that
A62: G1 = F . j and
f1 . j in the carrier of G1 and
A63: f1 . j <> 1_ G1 by A14, A60;
x2 . j = g . j by A15, A24, A60, FUNCT_4:11
.= 1_ G1 by A54, A62, Th9 ;
hence f . j <> 1_ G by A55, A56, A57, A58, A61, A62, A63, GROUP_1:def_4; ::_thesis: verum
end;
supposeA64: ( not j in J1 & j in J2 ) ; ::_thesis: f . j <> 1_ G
then A65: x2 . j = f2 . j by A15, A24, FUNCT_4:13;
consider G2 being non empty Group-like multMagma such that
A66: G2 = F . j and
f2 . j in the carrier of G2 and
A67: f2 . j <> 1_ G2 by A16, A64;
x1 . j = g . j by A13, A17, A64, FUNCT_4:11
.= 1_ G2 by A54, A66, Th9 ;
hence f . j <> 1_ G by A55, A56, A57, A58, A65, A66, A67, GROUP_1:def_4; ::_thesis: verum
end;
supposeA68: ( j in J1 & j in J2 ) ; ::_thesis: f . j <> 1_ G
then A69: ex G2 being non empty Group-like multMagma st
( G2 = F . j & f2 . j in the carrier of G2 & f2 . j <> 1_ G2 ) by A16;
A70: not j in K by A54, XBOOLE_0:def_5;
ex G1 being non empty Group-like multMagma st
( G1 = F . j & f1 . j in the carrier of G1 & f1 . j <> 1_ G1 ) by A14, A68;
hence f . j <> 1_ G by A34, A54, A55, A56, A57, A58, A69, A70; ::_thesis: verum
end;
end;
end;
reconsider ff = X1 * X2 as Element of product (Carrier F) by Def2;
now__::_thesis:_ex_J_being_finite_Subset_of_I_st_
for_j_being_set_st_j_in_J_holds_
ex_G_being_non_empty_Group-like_multMagma_st_
(_G_=_F_._j_&_ff_._j_in_the_carrier_of_G_&_ff_._j_<>_1__G_)
reconsider J = {} as finite Subset of I by XBOOLE_1:2;
take J = J; ::_thesis: for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & ff . j in the carrier of G & ff . j <> 1_ G )
thus for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & ff . j in the carrier of G & ff . j <> 1_ G ) ; ::_thesis: verum
end;
hence y in A by A3, A33, A35; ::_thesis: verum
end;
then reconsider b = the multF of (product F) || A as BinOp of A by FUNCT_2:def_1, RELSET_1:4;
set H = multMagma(# A,b #);
multMagma(# A,b #) is Group-like
proof
reconsider e = g as Element of multMagma(# A,b #) by A3, A5;
take e ; :: according to GROUP_1:def_2 ::_thesis: for b1 being Element of the carrier of multMagma(# A,b #) holds
( b1 * e = b1 & e * b1 = b1 & ex b2 being Element of the carrier of multMagma(# A,b #) st
( b1 * b2 = e & b2 * b1 = e ) )
let h be Element of multMagma(# A,b #); ::_thesis: ( h * e = h & e * h = h & ex b1 being Element of the carrier of multMagma(# A,b #) st
( h * b1 = e & b1 * h = e ) )
h in the carrier of multMagma(# A,b #) ;
then reconsider h1 = h as Element of (product F) by A4;
[h,e] in [:A,A:] by ZFMISC_1:87;
hence h * e = h1 * (1_ (product F)) by FUNCT_1:49
.= h by GROUP_1:def_4 ;
::_thesis: ( e * h = h & ex b1 being Element of the carrier of multMagma(# A,b #) st
( h * b1 = e & b1 * h = e ) )
[e,h] in [:A,A:] by ZFMISC_1:87;
hence e * h = (1_ (product F)) * h1 by FUNCT_1:49
.= h by GROUP_1:def_4 ;
::_thesis: ex b1 being Element of the carrier of multMagma(# A,b #) st
( h * b1 = e & b1 * h = e )
reconsider h2 = h1, hh = h1 " as Element of product (Carrier F) by Def2;
A71: S1[h1 " ]
proof
consider J being finite Subset of I, f being ManySortedSet of J such that
A72: h = g +* f and
A73: for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) by A3;
defpred S2[ set , set ] means ex G being Group ex m being Element of G st
( G = F . $1 & m = f . $1 & $2 = m " );
A74: for i being set st i in J holds
ex j being set st S2[i,j]
proof
let i be set ; ::_thesis: ( i in J implies ex j being set st S2[i,j] )
assume A75: i in J ; ::_thesis: ex j being set st S2[i,j]
then consider Gg being non empty Group-like multMagma such that
A76: Gg = F . i by Def3;
ex Ga being non empty associative multMagma st Ga = F . i by A75, Def4;
then reconsider G = Gg as Group by A76;
ex GG being non empty Group-like multMagma st
( GG = F . i & f . i in the carrier of GG & f . i <> 1_ GG ) by A73, A75;
then reconsider m = f . i as Element of G by A76;
take m " ; ::_thesis: S2[i,m " ]
thus S2[i,m " ] by A76; ::_thesis: verum
end;
consider f9 being ManySortedSet of J such that
A77: for j being set st j in J holds
S2[j,f9 . j] from PBOOLE:sch_3(A74);
set gf9 = g +* f9;
A78: dom f9 = J by PARTFUN1:def_2;
A79: dom f = J by PARTFUN1:def_2;
A80: now__::_thesis:_for_i_being_set_st_i_in_I_holds_
hh_._i_=_(g_+*_f9)_._i
let i be set ; ::_thesis: ( i in I implies hh . b1 = (g +* f9) . b1 )
assume A81: i in I ; ::_thesis: hh . b1 = (g +* f9) . b1
then consider G3 being non empty Group-like multMagma such that
A82: G3 = F . i by Def3;
ex G4 being non empty associative multMagma st G4 = F . i by A81, Def4;
then consider G5 being Group such that
A83: G5 = F . i by A82;
percases ( i in J or not i in J ) ;
supposeA84: i in J ; ::_thesis: hh . b1 = (g +* f9) . b1
then A85: (g +* f9) . i = f9 . i by A78, FUNCT_4:13;
A86: ex G being Group ex m being Element of G st
( G = F . i & m = f . i & f9 . i = m " ) by A77, A84;
h2 . i = f . i by A72, A79, A84, FUNCT_4:13;
hence hh . i = (g +* f9) . i by A81, A86, A85, Th11; ::_thesis: verum
end;
supposeA87: not i in J ; ::_thesis: hh . b1 = (g +* f9) . b1
then A88: (g +* f9) . i = g . i by A78, FUNCT_4:11
.= 1_ G3 by A81, A82, Th9 ;
A89: 1_ G5 = (1_ G5) " by GROUP_1:8;
h2 . i = g . i by A72, A79, A87, FUNCT_4:11
.= 1_ G3 by A81, A82, Th9 ;
hence hh . i = (g +* f9) . i by A81, A82, A83, A88, A89, Th11; ::_thesis: verum
end;
end;
end;
take J ; ::_thesis: ex f being ManySortedSet of J st
( h1 " = g +* f & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) )
take f9 ; ::_thesis: ( h1 " = g +* f9 & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f9 . j in the carrier of G & f9 . j <> 1_ G ) ) )
A90: dom hh = I by A6;
dom (g +* f9) = (dom g) \/ (dom f9) by FUNCT_4:def_1
.= I by A2, A1, A78, XBOOLE_1:12 ;
hence h1 " = g +* f9 by A90, A80, FUNCT_1:2; ::_thesis: for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f9 . j in the carrier of G & f9 . j <> 1_ G )
let j be set ; ::_thesis: ( j in J implies ex G being non empty Group-like multMagma st
( G = F . j & f9 . j in the carrier of G & f9 . j <> 1_ G ) )
assume A91: j in J ; ::_thesis: ex G being non empty Group-like multMagma st
( G = F . j & f9 . j in the carrier of G & f9 . j <> 1_ G )
then consider G being Group, m being Element of G such that
A92: G = F . j and
A93: m = f . j and
A94: f9 . j = m " by A77;
take G ; ::_thesis: ( G = F . j & f9 . j in the carrier of G & f9 . j <> 1_ G )
thus ( G = F . j & f9 . j in the carrier of G ) by A92, A94; ::_thesis: f9 . j <> 1_ G
ex G1 being non empty Group-like multMagma st
( G1 = F . j & f . j in the carrier of G1 & f . j <> 1_ G1 ) by A73, A91;
hence f9 . j <> 1_ G by A92, A93, A94, GROUP_1:10; ::_thesis: verum
end;
product (Carrier F) = the carrier of (product F) by Def2;
then reconsider h9 = h1 " as Element of multMagma(# A,b #) by A3, A71;
take h9 ; ::_thesis: ( h * h9 = e & h9 * h = e )
[h,h9] in [:A,A:] by ZFMISC_1:87;
hence h * h9 = h1 * (h1 ") by FUNCT_1:49
.= e by GROUP_1:def_5 ;
::_thesis: h9 * h = e
[h9,h] in [:A,A:] by ZFMISC_1:87;
hence h9 * h = (h1 ") * h1 by FUNCT_1:49
.= e by GROUP_1:def_5 ;
::_thesis: verum
end;
then reconsider H = multMagma(# A,b #) as non empty Group-like multMagma ;
reconsider H = H as strict Subgroup of product F by A4, GROUP_2:def_5;
take H ; ::_thesis: for x being set holds
( x in the carrier of H iff ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st
( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) )
let x be set ; ::_thesis: ( x in the carrier of H iff ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st
( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) )
hereby ::_thesis: ( ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st
( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) implies x in the carrier of H )
assume x in the carrier of H ; ::_thesis: ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st
( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) )
then S1[x] by A3;
hence ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st
( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) ; ::_thesis: verum
end;
given g being Element of product (Carrier F), J being finite Subset of I, f being ManySortedSet of J such that A95: g = 1_ (product F) and
A96: x = g +* f and
A97: for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ; ::_thesis: x in the carrier of H
A98: dom g = I by A6;
set gf = g +* f;
A99: dom f = J by PARTFUN1:def_2;
A100: now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(g_+*_f)_._i_in_(Carrier_F)_._i
let i be set ; ::_thesis: ( i in I implies (g +* f) . b1 in (Carrier F) . b1 )
assume A101: i in I ; ::_thesis: (g +* f) . b1 in (Carrier F) . b1
then A102: ex R being 1-sorted st
( R = F . i & (Carrier F) . i = the carrier of R ) by PRALG_1:def_13;
percases ( i in J or not i in J ) ;
supposeA103: i in J ; ::_thesis: (g +* f) . b1 in (Carrier F) . b1
then ex G being non empty Group-like multMagma st
( G = F . i & f . i in the carrier of G & f . i <> 1_ G ) by A97;
hence (g +* f) . i in (Carrier F) . i by A99, A102, A103, FUNCT_4:13; ::_thesis: verum
end;
supposeA104: not i in J ; ::_thesis: (g +* f) . b1 in (Carrier F) . b1
consider G being non empty Group-like multMagma such that
A105: G = F . i by A101, Def3;
(g +* f) . i = g . i by A99, A104, FUNCT_4:11
.= 1_ G by A95, A101, A105, Th9 ;
hence (g +* f) . i in (Carrier F) . i by A102, A105; ::_thesis: verum
end;
end;
end;
dom (g +* f) = (dom g) \/ (dom f) by FUNCT_4:def_1
.= I by A98, A99, XBOOLE_1:12 ;
then x in product (Carrier F) by A1, A96, A100, CARD_3:9;
hence x in the carrier of H by A3, A95, A96, A97; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict Subgroup of product F st ( for x being set holds
( x in the carrier of b1 iff ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st
( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) ) ) & ( for x being set holds
( x in the carrier of b2 iff ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st
( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) ) ) holds
b1 = b2
proof
defpred S1[ set ] means ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st
( g = 1_ (product F) & $1 = g +* f & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) );
let A, B be strict Subgroup of product F; ::_thesis: ( ( for x being set holds
( x in the carrier of A iff ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st
( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) ) ) & ( for x being set holds
( x in the carrier of B iff ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st
( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) ) ) implies A = B )
assume that
A106: for x being set holds
( x in the carrier of A iff S1[x] ) and
A107: for x being set holds
( x in the carrier of B iff S1[x] ) ; ::_thesis: A = B
the carrier of A = the carrier of B from XBOOLE_0:sch_2(A106, A107);
hence A = B by GROUP_2:59; ::_thesis: verum
end;
end;
:: deftheorem Def9 defines sum GROUP_7:def_9_:_
for I being set
for F being Group-like associative multMagma-Family of I
for b3 being strict Subgroup of product F holds
( b3 = sum F iff for x being set holds
( x in the carrier of b3 iff ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st
( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) ) ) );
registration
let I be set ;
let F be Group-like associative multMagma-Family of I;
let f, g be Element of (sum F);
cluster the multF of (sum F) . (f,g) -> Relation-like Function-like ;
coherence
( the multF of (sum F) . (f,g) is Function-like & the multF of (sum F) . (f,g) is Relation-like )
proof
A1: the multF of (sum F) . (f,g) in the carrier of (sum F) ;
the carrier of (sum F) c= the carrier of (product F) by GROUP_2:def_5;
then reconsider h = the multF of (sum F) . (f,g) as Element of product (Carrier F) by A1, Def2;
h is Function ;
hence ( the multF of (sum F) . (f,g) is Function-like & the multF of (sum F) . (f,g) is Relation-like ) ; ::_thesis: verum
end;
end;
theorem :: GROUP_7:9
for I being finite set
for F being Group-like associative multMagma-Family of I holds product F = sum F
proof
let I be finite set ; ::_thesis: for F being Group-like associative multMagma-Family of I holds product F = sum F
let F be Group-like associative multMagma-Family of I; ::_thesis: product F = sum F
set GP = product F;
set S = sum F;
A1: the carrier of (sum F) = the carrier of (product F)
proof
reconsider g = 1_ (product F) as Element of product (Carrier F) by Def2;
thus the carrier of (sum F) c= the carrier of (product F) by GROUP_2:def_5; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of (product F) c= the carrier of (sum F)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (product F) or x in the carrier of (sum F) )
assume x in the carrier of (product F) ; ::_thesis: x in the carrier of (sum F)
then reconsider f = x as Element of product (Carrier F) by Def2;
A2: for p being Element of product (Carrier F) holds dom p = I by PARTFUN1:def_2;
then A3: dom f = I ;
reconsider f = f as ManySortedSet of I ;
ex g being Element of product (Carrier F) ex J being finite Subset of I ex f being ManySortedSet of J st
( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) )
proof
deffunc H1( set ) -> set = f . $1;
defpred S1[ set ] means ex G being non empty Group-like multMagma ex m being Element of G st
( G = F . $1 & m = f . $1 & m <> 1_ G );
consider J being set such that
A4: for j being set holds
( j in J iff ( j in I & S1[j] ) ) from XBOOLE_0:sch_1();
J c= I
proof
let j be set ; :: according to TARSKI:def_3 ::_thesis: ( not j in J or j in I )
assume j in J ; ::_thesis: j in I
hence j in I by A4; ::_thesis: verum
end;
then reconsider J = J as Subset of I ;
consider ff being ManySortedSet of J such that
A5: for j being set st j in J holds
ff . j = H1(j) from PBOOLE:sch_4();
A6: dom ff = J by PARTFUN1:def_2;
A7: now__::_thesis:_for_i_being_set_st_i_in_I_holds_
f_._i_=_(g_+*_ff)_._i
let i be set ; ::_thesis: ( i in I implies f . b1 = (g +* ff) . b1 )
assume A8: i in I ; ::_thesis: f . b1 = (g +* ff) . b1
percases ( i in J or not i in J ) ;
supposeA9: i in J ; ::_thesis: f . b1 = (g +* ff) . b1
hence f . i = ff . i by A5
.= (g +* ff) . i by A6, A9, FUNCT_4:13 ;
::_thesis: verum
end;
supposeA10: not i in J ; ::_thesis: f . b1 = (g +* ff) . b1
consider G being non empty Group-like multMagma such that
A11: G = F . i by A8, Def3;
f . i is Element of G by A8, A11, Lm1;
hence f . i = 1_ G by A4, A8, A10, A11
.= g . i by A8, A11, Th9
.= (g +* ff) . i by A6, A10, FUNCT_4:11 ;
::_thesis: verum
end;
end;
end;
take g ; ::_thesis: ex J being finite Subset of I ex f being ManySortedSet of J st
( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) )
take J ; ::_thesis: ex f being ManySortedSet of J st
( g = 1_ (product F) & x = g +* f & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & f . j in the carrier of G & f . j <> 1_ G ) ) )
take ff ; ::_thesis: ( g = 1_ (product F) & x = g +* ff & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & ff . j in the carrier of G & ff . j <> 1_ G ) ) )
thus g = 1_ (product F) ; ::_thesis: ( x = g +* ff & ( for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & ff . j in the carrier of G & ff . j <> 1_ G ) ) )
A12: dom g = I by A2;
dom (g +* ff) = (dom g) \/ (dom ff) by FUNCT_4:def_1
.= I by A6, A12, XBOOLE_1:12 ;
hence x = g +* ff by A3, A7, FUNCT_1:2; ::_thesis: for j being set st j in J holds
ex G being non empty Group-like multMagma st
( G = F . j & ff . j in the carrier of G & ff . j <> 1_ G )
let j be set ; ::_thesis: ( j in J implies ex G being non empty Group-like multMagma st
( G = F . j & ff . j in the carrier of G & ff . j <> 1_ G ) )
assume A13: j in J ; ::_thesis: ex G being non empty Group-like multMagma st
( G = F . j & ff . j in the carrier of G & ff . j <> 1_ G )
then consider G being non empty Group-like multMagma , m being Element of G such that
A14: G = F . j and
A15: m = f . j and
A16: m <> 1_ G by A4;
take G ; ::_thesis: ( G = F . j & ff . j in the carrier of G & ff . j <> 1_ G )
ff . j = f . j by A5, A13;
hence ( G = F . j & ff . j in the carrier of G & ff . j <> 1_ G ) by A14, A15, A16; ::_thesis: verum
end;
hence x in the carrier of (sum F) by Def9; ::_thesis: verum
end;
product F is Subgroup of product F by GROUP_2:54;
hence product F = sum F by A1, GROUP_2:59; ::_thesis: verum
end;
begin
theorem Th13: :: GROUP_7:10
for G1 being non empty multMagma holds <*G1*> is multMagma-Family of {1}
proof
let G1 be non empty multMagma ; ::_thesis: <*G1*> is multMagma-Family of {1}
dom <*G1*> = {1} by FINSEQ_1:2, FINSEQ_1:def_8;
then reconsider A = <*G1*> as ManySortedSet of {1} by PARTFUN1:def_2, RELAT_1:def_18;
A is multMagma-yielding
proof
let y be set ; :: according to GROUP_7:def_1 ::_thesis: ( y in rng A implies y is non empty multMagma )
assume y in rng A ; ::_thesis: y is non empty multMagma
then consider x being set such that
A2: x in dom A and
A3: A . x = y by FUNCT_1:def_3;
x = 1 by A2, TARSKI:def_1;
hence y is non empty multMagma by A3, FINSEQ_1:def_8; ::_thesis: verum
end;
hence <*G1*> is multMagma-Family of {1} ; ::_thesis: verum
end;
registration
let G1 be non empty multMagma ;
cluster<*G1*> -> {1} -defined ;
coherence
<*G1*> is {1} -defined by Th13;
end;
registration
let G1 be non empty multMagma ;
cluster<*G1*> -> total multMagma-yielding ;
coherence
( <*G1*> is total & <*G1*> is multMagma-yielding ) by Th13;
end;
theorem Th14: :: GROUP_7:11
for G1 being non empty Group-like multMagma holds <*G1*> is Group-like multMagma-Family of {1}
proof
let G1 be non empty Group-like multMagma ; ::_thesis: <*G1*> is Group-like multMagma-Family of {1}
reconsider A = <*G1*> as multMagma-Family of {1} ;
A is Group-like
proof
let x be Element of {1}; :: according to GROUP_7:def_6 ::_thesis: A . x is Group-like
x = 1 by TARSKI:def_1;
hence A . x is Group-like by FINSEQ_1:def_8; ::_thesis: verum
end;
hence <*G1*> is Group-like multMagma-Family of {1} ; ::_thesis: verum
end;
registration
let G1 be non empty Group-like multMagma ;
cluster<*G1*> -> Group-like ;
coherence
<*G1*> is Group-like by Th14;
end;
theorem Th15: :: GROUP_7:12
for G1 being non empty associative multMagma holds <*G1*> is associative multMagma-Family of {1}
proof
let G1 be non empty associative multMagma ; ::_thesis: <*G1*> is associative multMagma-Family of {1}
reconsider A = <*G1*> as multMagma-Family of {1} ;
A is associative
proof
let x be Element of {1}; :: according to GROUP_7:def_7 ::_thesis: A . x is associative
x = 1 by TARSKI:def_1;
hence A . x is associative by FINSEQ_1:def_8; ::_thesis: verum
end;
hence <*G1*> is associative multMagma-Family of {1} ; ::_thesis: verum
end;
registration
let G1 be non empty associative multMagma ;
cluster<*G1*> -> associative ;
coherence
<*G1*> is associative by Th15;
end;
theorem Th16: :: GROUP_7:13
for G1 being non empty commutative multMagma holds <*G1*> is commutative multMagma-Family of {1}
proof
let G1 be non empty commutative multMagma ; ::_thesis: <*G1*> is commutative multMagma-Family of {1}
reconsider A = <*G1*> as multMagma-Family of {1} ;
A is commutative
proof
let x be Element of {1}; :: according to GROUP_7:def_8 ::_thesis: A . x is commutative
x = 1 by TARSKI:def_1;
hence A . x is commutative by FINSEQ_1:def_8; ::_thesis: verum
end;
hence <*G1*> is commutative multMagma-Family of {1} ; ::_thesis: verum
end;
registration
let G1 be non empty commutative multMagma ;
cluster<*G1*> -> commutative ;
coherence
<*G1*> is commutative by Th16;
end;
theorem :: GROUP_7:14
for G1 being Group holds <*G1*> is Group-like associative multMagma-Family of {1} ;
theorem :: GROUP_7:15
for G1 being commutative Group holds <*G1*> is Group-like associative commutative multMagma-Family of {1} ;
registration
let G1 be non empty multMagma ;
cluster -> FinSequence-like for Element of product (Carrier <*G1*>);
coherence
for b1 being Element of product (Carrier <*G1*>) holds b1 is FinSequence-like
proof
let x be Element of product (Carrier <*G1*>); ::_thesis: x is FinSequence-like
take 1 ; :: according to FINSEQ_1:def_2 ::_thesis: dom x = Seg 1
thus dom x = dom (Carrier <*G1*>) by CARD_3:9
.= Seg 1 by FINSEQ_1:2, PARTFUN1:def_2 ; ::_thesis: verum
end;
end;
registration
let G1 be non empty multMagma ;
cluster -> FinSequence-like for Element of the carrier of (product <*G1*>);
coherence
for b1 being Element of (product <*G1*>) holds b1 is FinSequence-like
proof
let x be Element of (product <*G1*>); ::_thesis: x is FinSequence-like
reconsider y = x as Element of product (Carrier <*G1*>) by Def2;
y is FinSequence-like ;
hence x is FinSequence-like ; ::_thesis: verum
end;
end;
definition
let G1 be non empty multMagma ;
let x be Element of G1;
:: original: <*
redefine func<*x*> -> Element of (product <*G1*>);
coherence
<*x*> is Element of (product <*G1*>)
proof
set xy = <*x*>;
set G = <*G1*>;
A1: dom (Carrier <*G1*>) = {1} by PARTFUN1:def_2;
A2: <*G1*> . 1 = G1 by FINSEQ_1:def_8;
A3: <*x*> . 1 = x by FINSEQ_1:def_8;
A4: for a being set st a in {1} holds
<*x*> . a in (Carrier <*G1*>) . a
proof
let a be set ; ::_thesis: ( a in {1} implies <*x*> . a in (Carrier <*G1*>) . a )
assume A5: a in {1} ; ::_thesis: <*x*> . a in (Carrier <*G1*>) . a
then A6: a = 1 by TARSKI:def_1;
then ex R being 1-sorted st
( R = <*G1*> . 1 & (Carrier <*G1*>) . 1 = the carrier of R ) by A5, PRALG_1:def_13;
hence <*x*> . a in (Carrier <*G1*>) . a by A3, A2, A6; ::_thesis: verum
end;
dom <*x*> = {1} by FINSEQ_1:2, FINSEQ_1:def_8;
then <*x*> in product (Carrier <*G1*>) by A1, A4, CARD_3:9;
hence <*x*> is Element of (product <*G1*>) by Def2; ::_thesis: verum
end;
end;
theorem Th19: :: GROUP_7:16
for G1, G2 being non empty multMagma holds <*G1,G2*> is multMagma-Family of {1,2}
proof
let G1, G2 be non empty multMagma ; ::_thesis: <*G1,G2*> is multMagma-Family of {1,2}
dom <*G1,G2*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89;
then reconsider A = <*G1,G2*> as ManySortedSet of {1,2} by PARTFUN1:def_2, RELAT_1:def_18;
A is multMagma-yielding
proof
let y be set ; :: according to GROUP_7:def_1 ::_thesis: ( y in rng A implies y is non empty multMagma )
assume y in rng A ; ::_thesis: y is non empty multMagma
then consider x being set such that
A2: x in dom A and
A3: A . x = y by FUNCT_1:def_3;
( x = 1 or x = 2 ) by A2, TARSKI:def_2;
hence y is non empty multMagma by A3, FINSEQ_1:44; ::_thesis: verum
end;
hence <*G1,G2*> is multMagma-Family of {1,2} ; ::_thesis: verum
end;
registration
let G1, G2 be non empty multMagma ;
cluster<*G1,G2*> -> {1,2} -defined ;
coherence
<*G1,G2*> is {1,2} -defined by Th19;
end;
registration
let G1, G2 be non empty multMagma ;
cluster<*G1,G2*> -> total multMagma-yielding ;
coherence
( <*G1,G2*> is total & <*G1,G2*> is multMagma-yielding ) by Th19;
end;
theorem Th20: :: GROUP_7:17
for G1, G2 being non empty Group-like multMagma holds <*G1,G2*> is Group-like multMagma-Family of {1,2}
proof
let G1, G2 be non empty Group-like multMagma ; ::_thesis: <*G1,G2*> is Group-like multMagma-Family of {1,2}
reconsider A = <*G1,G2*> as multMagma-Family of {1,2} ;
A is Group-like
proof
let x be Element of {1,2}; :: according to GROUP_7:def_6 ::_thesis: A . x is Group-like
( x = 1 or x = 2 ) by TARSKI:def_2;
hence A . x is Group-like by FINSEQ_1:44; ::_thesis: verum
end;
hence <*G1,G2*> is Group-like multMagma-Family of {1,2} ; ::_thesis: verum
end;
registration
let G1, G2 be non empty Group-like multMagma ;
cluster<*G1,G2*> -> Group-like ;
coherence
<*G1,G2*> is Group-like by Th20;
end;
theorem Th21: :: GROUP_7:18
for G1, G2 being non empty associative multMagma holds <*G1,G2*> is associative multMagma-Family of {1,2}
proof
let G1, G2 be non empty associative multMagma ; ::_thesis: <*G1,G2*> is associative multMagma-Family of {1,2}
reconsider A = <*G1,G2*> as multMagma-Family of {1,2} ;
A is associative
proof
let x be Element of {1,2}; :: according to GROUP_7:def_7 ::_thesis: A . x is associative
( x = 1 or x = 2 ) by TARSKI:def_2;
hence A . x is associative by FINSEQ_1:44; ::_thesis: verum
end;
hence <*G1,G2*> is associative multMagma-Family of {1,2} ; ::_thesis: verum
end;
registration
let G1, G2 be non empty associative multMagma ;
cluster<*G1,G2*> -> associative ;
coherence
<*G1,G2*> is associative by Th21;
end;
theorem Th22: :: GROUP_7:19
for G1, G2 being non empty commutative multMagma holds <*G1,G2*> is commutative multMagma-Family of {1,2}
proof
let G1, G2 be non empty commutative multMagma ; ::_thesis: <*G1,G2*> is commutative multMagma-Family of {1,2}
reconsider A = <*G1,G2*> as multMagma-Family of {1,2} ;
A is commutative
proof
let x be Element of {1,2}; :: according to GROUP_7:def_8 ::_thesis: A . x is commutative
( x = 1 or x = 2 ) by TARSKI:def_2;
hence A . x is commutative by FINSEQ_1:44; ::_thesis: verum
end;
hence <*G1,G2*> is commutative multMagma-Family of {1,2} ; ::_thesis: verum
end;
registration
let G1, G2 be non empty commutative multMagma ;
cluster<*G1,G2*> -> commutative ;
coherence
<*G1,G2*> is commutative by Th22;
end;
theorem :: GROUP_7:20
for G1, G2 being Group holds <*G1,G2*> is Group-like associative multMagma-Family of {1,2} ;
theorem :: GROUP_7:21
for G1, G2 being commutative Group holds <*G1,G2*> is Group-like associative commutative multMagma-Family of {1,2} ;
registration
let G1, G2 be non empty multMagma ;
cluster -> FinSequence-like for Element of product (Carrier <*G1,G2*>);
coherence
for b1 being Element of product (Carrier <*G1,G2*>) holds b1 is FinSequence-like
proof
let x be Element of product (Carrier <*G1,G2*>); ::_thesis: x is FinSequence-like
take 2 ; :: according to FINSEQ_1:def_2 ::_thesis: dom x = Seg 2
thus dom x = dom (Carrier <*G1,G2*>) by CARD_3:9
.= Seg 2 by FINSEQ_1:2, PARTFUN1:def_2 ; ::_thesis: verum
end;
end;
registration
let G1, G2 be non empty multMagma ;
cluster -> FinSequence-like for Element of the carrier of (product <*G1,G2*>);
coherence
for b1 being Element of (product <*G1,G2*>) holds b1 is FinSequence-like
proof
let x be Element of (product <*G1,G2*>); ::_thesis: x is FinSequence-like
reconsider y = x as Element of product (Carrier <*G1,G2*>) by Def2;
y is FinSequence-like ;
hence x is FinSequence-like ; ::_thesis: verum
end;
end;
definition
let G1, G2 be non empty multMagma ;
let x be Element of G1;
let y be Element of G2;
:: original: <*
redefine func<*x,y*> -> Element of (product <*G1,G2*>);
coherence
<*x,y*> is Element of (product <*G1,G2*>)
proof
set xy = <*x,y*>;
set G = <*G1,G2*>;
A1: dom (Carrier <*G1,G2*>) = {1,2} by PARTFUN1:def_2;
A2: <*x,y*> . 2 = y by FINSEQ_1:44;
A3: <*G1,G2*> . 2 = G2 by FINSEQ_1:44;
A4: <*G1,G2*> . 1 = G1 by FINSEQ_1:44;
A5: <*x,y*> . 1 = x by FINSEQ_1:44;
A6: for a being set st a in {1,2} holds
<*x,y*> . a in (Carrier <*G1,G2*>) . a
proof
let a be set ; ::_thesis: ( a in {1,2} implies <*x,y*> . a in (Carrier <*G1,G2*>) . a )
assume A7: a in {1,2} ; ::_thesis: <*x,y*> . a in (Carrier <*G1,G2*>) . a
percases ( a = 1 or a = 2 ) by A7, TARSKI:def_2;
supposeA8: a = 1 ; ::_thesis: <*x,y*> . a in (Carrier <*G1,G2*>) . a
then ex R being 1-sorted st
( R = <*G1,G2*> . 1 & (Carrier <*G1,G2*>) . 1 = the carrier of R ) by A7, PRALG_1:def_13;
hence <*x,y*> . a in (Carrier <*G1,G2*>) . a by A5, A4, A8; ::_thesis: verum
end;
supposeA9: a = 2 ; ::_thesis: <*x,y*> . a in (Carrier <*G1,G2*>) . a
then ex R being 1-sorted st
( R = <*G1,G2*> . 2 & (Carrier <*G1,G2*>) . 2 = the carrier of R ) by A7, PRALG_1:def_13;
hence <*x,y*> . a in (Carrier <*G1,G2*>) . a by A2, A3, A9; ::_thesis: verum
end;
end;
end;
dom <*x,y*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89;
then <*x,y*> in product (Carrier <*G1,G2*>) by A1, A6, CARD_3:9;
hence <*x,y*> is Element of (product <*G1,G2*>) by Def2; ::_thesis: verum
end;
end;
theorem Th25: :: GROUP_7:22
for G1, G2, G3 being non empty multMagma holds <*G1,G2,G3*> is multMagma-Family of {1,2,3}
proof
let G1, G2, G3 be non empty multMagma ; ::_thesis: <*G1,G2,G3*> is multMagma-Family of {1,2,3}
dom <*G1,G2,G3*> = {1,2,3} by FINSEQ_1:89, FINSEQ_3:1;
then reconsider A = <*G1,G2,G3*> as ManySortedSet of {1,2,3} by PARTFUN1:def_2, RELAT_1:def_18;
A is multMagma-yielding
proof
let y be set ; :: according to GROUP_7:def_1 ::_thesis: ( y in rng A implies y is non empty multMagma )
assume y in rng A ; ::_thesis: y is non empty multMagma
then consider x being set such that
A2: x in dom A and
A3: A . x = y by FUNCT_1:def_3;
( x = 1 or x = 2 or x = 3 ) by A2, ENUMSET1:def_1;
hence y is non empty multMagma by A3, FINSEQ_1:45; ::_thesis: verum
end;
hence <*G1,G2,G3*> is multMagma-Family of {1,2,3} ; ::_thesis: verum
end;
registration
let G1, G2, G3 be non empty multMagma ;
cluster<*G1,G2,G3*> -> {1,2,3} -defined ;
coherence
<*G1,G2,G3*> is {1,2,3} -defined by Th25;
end;
registration
let G1, G2, G3 be non empty multMagma ;
cluster<*G1,G2,G3*> -> total multMagma-yielding ;
coherence
( <*G1,G2,G3*> is total & <*G1,G2,G3*> is multMagma-yielding ) by Th25;
end;
theorem Th26: :: GROUP_7:23
for G1, G2, G3 being non empty Group-like multMagma holds <*G1,G2,G3*> is Group-like multMagma-Family of {1,2,3}
proof
let G1, G2, G3 be non empty Group-like multMagma ; ::_thesis: <*G1,G2,G3*> is Group-like multMagma-Family of {1,2,3}
reconsider A = <*G1,G2,G3*> as multMagma-Family of {1,2,3} ;
A is Group-like
proof
let x be Element of {1,2,3}; :: according to GROUP_7:def_6 ::_thesis: A . x is Group-like
( x = 1 or x = 2 or x = 3 ) by ENUMSET1:def_1;
hence A . x is Group-like by FINSEQ_1:45; ::_thesis: verum
end;
hence <*G1,G2,G3*> is Group-like multMagma-Family of {1,2,3} ; ::_thesis: verum
end;
registration
let G1, G2, G3 be non empty Group-like multMagma ;
cluster<*G1,G2,G3*> -> Group-like ;
coherence
<*G1,G2,G3*> is Group-like by Th26;
end;
theorem Th27: :: GROUP_7:24
for G1, G2, G3 being non empty associative multMagma holds <*G1,G2,G3*> is associative multMagma-Family of {1,2,3}
proof
let G1, G2, G3 be non empty associative multMagma ; ::_thesis: <*G1,G2,G3*> is associative multMagma-Family of {1,2,3}
reconsider A = <*G1,G2,G3*> as multMagma-Family of {1,2,3} ;
A is associative
proof
let x be Element of {1,2,3}; :: according to GROUP_7:def_7 ::_thesis: A . x is associative
( x = 1 or x = 2 or x = 3 ) by ENUMSET1:def_1;
hence A . x is associative by FINSEQ_1:45; ::_thesis: verum
end;
hence <*G1,G2,G3*> is associative multMagma-Family of {1,2,3} ; ::_thesis: verum
end;
registration
let G1, G2, G3 be non empty associative multMagma ;
cluster<*G1,G2,G3*> -> associative ;
coherence
<*G1,G2,G3*> is associative by Th27;
end;
theorem Th28: :: GROUP_7:25
for G1, G2, G3 being non empty commutative multMagma holds <*G1,G2,G3*> is commutative multMagma-Family of {1,2,3}
proof
let G1, G2, G3 be non empty commutative multMagma ; ::_thesis: <*G1,G2,G3*> is commutative multMagma-Family of {1,2,3}
reconsider A = <*G1,G2,G3*> as multMagma-Family of {1,2,3} ;
A is commutative
proof
let x be Element of {1,2,3}; :: according to GROUP_7:def_8 ::_thesis: A . x is commutative
( x = 1 or x = 2 or x = 3 ) by ENUMSET1:def_1;
hence A . x is commutative by FINSEQ_1:45; ::_thesis: verum
end;
hence <*G1,G2,G3*> is commutative multMagma-Family of {1,2,3} ; ::_thesis: verum
end;
registration
let G1, G2, G3 be non empty commutative multMagma ;
cluster<*G1,G2,G3*> -> commutative ;
coherence
<*G1,G2,G3*> is commutative by Th28;
end;
theorem :: GROUP_7:26
for G1, G2, G3 being Group holds <*G1,G2,G3*> is Group-like associative multMagma-Family of {1,2,3} ;
theorem :: GROUP_7:27
for G1, G2, G3 being commutative Group holds <*G1,G2,G3*> is Group-like associative commutative multMagma-Family of {1,2,3} ;
registration
let G1, G2, G3 be non empty multMagma ;
cluster -> FinSequence-like for Element of product (Carrier <*G1,G2,G3*>);
coherence
for b1 being Element of product (Carrier <*G1,G2,G3*>) holds b1 is FinSequence-like
proof
let x be Element of product (Carrier <*G1,G2,G3*>); ::_thesis: x is FinSequence-like
take 3 ; :: according to FINSEQ_1:def_2 ::_thesis: dom x = Seg 3
thus dom x = dom (Carrier <*G1,G2,G3*>) by CARD_3:9
.= Seg 3 by FINSEQ_3:1, PARTFUN1:def_2 ; ::_thesis: verum
end;
end;
registration
let G1, G2, G3 be non empty multMagma ;
cluster -> FinSequence-like for Element of the carrier of (product <*G1,G2,G3*>);
coherence
for b1 being Element of (product <*G1,G2,G3*>) holds b1 is FinSequence-like
proof
let x be Element of (product <*G1,G2,G3*>); ::_thesis: x is FinSequence-like
reconsider y = x as Element of product (Carrier <*G1,G2,G3*>) by Def2;
y is FinSequence-like ;
hence x is FinSequence-like ; ::_thesis: verum
end;
end;
definition
let G1, G2, G3 be non empty multMagma ;
let x be Element of G1;
let y be Element of G2;
let z be Element of G3;
:: original: <*
redefine func<*x,y,z*> -> Element of (product <*G1,G2,G3*>);
coherence
<*x,y,z*> is Element of (product <*G1,G2,G3*>)
proof
set xy = <*x,y,z*>;
set G = <*G1,G2,G3*>;
A1: dom (Carrier <*G1,G2,G3*>) = {1,2,3} by PARTFUN1:def_2;
A2: <*x,y,z*> . 2 = y by FINSEQ_1:45;
A3: <*G1,G2,G3*> . 1 = G1 by FINSEQ_1:45;
A4: <*x,y,z*> . 3 = z by FINSEQ_1:45;
A5: <*G1,G2,G3*> . 3 = G3 by FINSEQ_1:45;
A6: <*G1,G2,G3*> . 2 = G2 by FINSEQ_1:45;
A7: <*x,y,z*> . 1 = x by FINSEQ_1:45;
A8: for a being set st a in {1,2,3} holds
<*x,y,z*> . a in (Carrier <*G1,G2,G3*>) . a
proof
let a be set ; ::_thesis: ( a in {1,2,3} implies <*x,y,z*> . a in (Carrier <*G1,G2,G3*>) . a )
assume A9: a in {1,2,3} ; ::_thesis: <*x,y,z*> . a in (Carrier <*G1,G2,G3*>) . a
percases ( a = 1 or a = 2 or a = 3 ) by A9, ENUMSET1:def_1;
supposeA10: a = 1 ; ::_thesis: <*x,y,z*> . a in (Carrier <*G1,G2,G3*>) . a
then ex R being 1-sorted st
( R = <*G1,G2,G3*> . 1 & (Carrier <*G1,G2,G3*>) . 1 = the carrier of R ) by A9, PRALG_1:def_13;
hence <*x,y,z*> . a in (Carrier <*G1,G2,G3*>) . a by A7, A3, A10; ::_thesis: verum
end;
supposeA11: a = 2 ; ::_thesis: <*x,y,z*> . a in (Carrier <*G1,G2,G3*>) . a
then ex R being 1-sorted st
( R = <*G1,G2,G3*> . 2 & (Carrier <*G1,G2,G3*>) . 2 = the carrier of R ) by A9, PRALG_1:def_13;
hence <*x,y,z*> . a in (Carrier <*G1,G2,G3*>) . a by A2, A6, A11; ::_thesis: verum
end;
supposeA12: a = 3 ; ::_thesis: <*x,y,z*> . a in (Carrier <*G1,G2,G3*>) . a
then ex R being 1-sorted st
( R = <*G1,G2,G3*> . 3 & (Carrier <*G1,G2,G3*>) . 3 = the carrier of R ) by A9, PRALG_1:def_13;
hence <*x,y,z*> . a in (Carrier <*G1,G2,G3*>) . a by A4, A5, A12; ::_thesis: verum
end;
end;
end;
dom <*x,y,z*> = {1,2,3} by FINSEQ_1:89, FINSEQ_3:1;
then <*x,y,z*> in product (Carrier <*G1,G2,G3*>) by A1, A8, CARD_3:9;
hence <*x,y,z*> is Element of (product <*G1,G2,G3*>) by Def2; ::_thesis: verum
end;
end;
theorem Th31: :: GROUP_7:28
for G1 being non empty multMagma
for x1, x2 being Element of G1 holds <*x1*> * <*x2*> = <*(x1 * x2)*>
proof
let G1 be non empty multMagma ; ::_thesis: for x1, x2 being Element of G1 holds <*x1*> * <*x2*> = <*(x1 * x2)*>
let x1, x2 be Element of G1; ::_thesis: <*x1*> * <*x2*> = <*(x1 * x2)*>
set G = <*G1*>;
A1: <*G1*> . 1 = G1 by FINSEQ_1:def_8;
reconsider l = <*x1*>, p = <*x2*>, lpl = <*x1*> * <*x2*>, lpp = <*(x1 * x2)*> as Element of product (Carrier <*G1*>) by Def2;
A2: l . 1 = x1 by FINSEQ_1:def_8;
A3: p . 1 = x2 by FINSEQ_1:def_8;
A4: lpp . 1 = x1 * x2 by FINSEQ_1:def_8;
A5: 1 in {1} by TARSKI:def_1;
A6: for k being Nat st 1 <= k & k <= 1 holds
lpl . k = lpp . k
proof
let k be Nat; ::_thesis: ( 1 <= k & k <= 1 implies lpl . k = lpp . k )
assume that
A7: 1 <= k and
A8: k <= 1 ; ::_thesis: lpl . k = lpp . k
k in NAT by ORDINAL1:def_12;
then k in Seg 1 by A7, A8;
then k = 1 by FINSEQ_1:2, TARSKI:def_1;
hence lpl . k = lpp . k by A5, A2, A3, A1, A4, Th4; ::_thesis: verum
end;
dom lpl = dom (Carrier <*G1*>) by CARD_3:9
.= Seg 1 by FINSEQ_1:2, PARTFUN1:def_2 ;
then A9: len lpl = 1 by FINSEQ_1:def_3;
len lpp = 1 by FINSEQ_1:39;
hence <*x1*> * <*x2*> = <*(x1 * x2)*> by A9, A6, FINSEQ_1:14; ::_thesis: verum
end;
theorem :: GROUP_7:29
for G1, G2 being non empty multMagma
for x1, x2 being Element of G1
for y1, y2 being Element of G2 holds <*x1,y1*> * <*x2,y2*> = <*(x1 * x2),(y1 * y2)*>
proof
let G1, G2 be non empty multMagma ; ::_thesis: for x1, x2 being Element of G1
for y1, y2 being Element of G2 holds <*x1,y1*> * <*x2,y2*> = <*(x1 * x2),(y1 * y2)*>
let x1, x2 be Element of G1; ::_thesis: for y1, y2 being Element of G2 holds <*x1,y1*> * <*x2,y2*> = <*(x1 * x2),(y1 * y2)*>
let y1, y2 be Element of G2; ::_thesis: <*x1,y1*> * <*x2,y2*> = <*(x1 * x2),(y1 * y2)*>
set G = <*G1,G2*>;
A1: <*G1,G2*> . 1 = G1 by FINSEQ_1:44;
A2: <*G1,G2*> . 2 = G2 by FINSEQ_1:44;
reconsider l = <*x1,y1*>, p = <*x2,y2*>, lpl = <*x1,y1*> * <*x2,y2*>, lpp = <*(x1 * x2),(y1 * y2)*> as Element of product (Carrier <*G1,G2*>) by Def2;
A3: 2 in {1,2} by TARSKI:def_2;
A4: l . 1 = x1 by FINSEQ_1:44;
A5: lpp . 1 = x1 * x2 by FINSEQ_1:44;
A6: p . 2 = y2 by FINSEQ_1:44;
A7: lpp . 2 = y1 * y2 by FINSEQ_1:44;
A8: p . 1 = x2 by FINSEQ_1:44;
A9: l . 2 = y1 by FINSEQ_1:44;
A10: 1 in {1,2} by TARSKI:def_2;
A11: for k being Nat st 1 <= k & k <= 2 holds
lpl . k = lpp . k
proof
let k be Nat; ::_thesis: ( 1 <= k & k <= 2 implies lpl . k = lpp . k )
assume that
A12: 1 <= k and
A13: k <= 2 ; ::_thesis: lpl . k = lpp . k
k in NAT by ORDINAL1:def_12;
then A14: k in Seg 2 by A12, A13;
percases ( k = 1 or k = 2 ) by A14, FINSEQ_1:2, TARSKI:def_2;
suppose k = 1 ; ::_thesis: lpl . k = lpp . k
hence lpl . k = lpp . k by A10, A4, A8, A1, A5, Th4; ::_thesis: verum
end;
suppose k = 2 ; ::_thesis: lpl . k = lpp . k
hence lpl . k = lpp . k by A3, A9, A6, A2, A7, Th4; ::_thesis: verum
end;
end;
end;
dom lpl = dom (Carrier <*G1,G2*>) by CARD_3:9
.= Seg 2 by FINSEQ_1:2, PARTFUN1:def_2 ;
then A15: len lpl = 2 by FINSEQ_1:def_3;
len lpp = 2 by FINSEQ_1:44;
hence <*x1,y1*> * <*x2,y2*> = <*(x1 * x2),(y1 * y2)*> by A15, A11, FINSEQ_1:14; ::_thesis: verum
end;
theorem :: GROUP_7:30
for G1, G2, G3 being non empty multMagma
for x1, x2 being Element of G1
for y1, y2 being Element of G2
for z1, z2 being Element of G3 holds <*x1,y1,z1*> * <*x2,y2,z2*> = <*(x1 * x2),(y1 * y2),(z1 * z2)*>
proof
let G1, G2, G3 be non empty multMagma ; ::_thesis: for x1, x2 being Element of G1
for y1, y2 being Element of G2
for z1, z2 being Element of G3 holds <*x1,y1,z1*> * <*x2,y2,z2*> = <*(x1 * x2),(y1 * y2),(z1 * z2)*>
let x1, x2 be Element of G1; ::_thesis: for y1, y2 being Element of G2
for z1, z2 being Element of G3 holds <*x1,y1,z1*> * <*x2,y2,z2*> = <*(x1 * x2),(y1 * y2),(z1 * z2)*>
let y1, y2 be Element of G2; ::_thesis: for z1, z2 being Element of G3 holds <*x1,y1,z1*> * <*x2,y2,z2*> = <*(x1 * x2),(y1 * y2),(z1 * z2)*>
let z1, z2 be Element of G3; ::_thesis: <*x1,y1,z1*> * <*x2,y2,z2*> = <*(x1 * x2),(y1 * y2),(z1 * z2)*>
set G = <*G1,G2,G3*>;
A1: 3 in {1,2,3} by ENUMSET1:def_1;
A2: <*G1,G2,G3*> . 1 = G1 by FINSEQ_1:45;
A3: <*G1,G2,G3*> . 3 = G3 by FINSEQ_1:45;
A4: <*G1,G2,G3*> . 2 = G2 by FINSEQ_1:45;
reconsider l = <*x1,y1,z1*>, p = <*x2,y2,z2*>, lpl = <*x1,y1,z1*> * <*x2,y2,z2*>, lpp = <*(x1 * x2),(y1 * y2),(z1 * z2)*> as Element of product (Carrier <*G1,G2,G3*>) by Def2;
A5: 2 in {1,2,3} by ENUMSET1:def_1;
A6: l . 1 = x1 by FINSEQ_1:45;
A7: l . 3 = z1 by FINSEQ_1:45;
A8: l . 2 = y1 by FINSEQ_1:45;
A9: lpp . 3 = z1 * z2 by FINSEQ_1:45;
A10: lpp . 2 = y1 * y2 by FINSEQ_1:45;
A11: lpp . 1 = x1 * x2 by FINSEQ_1:45;
A12: p . 3 = z2 by FINSEQ_1:45;
A13: p . 2 = y2 by FINSEQ_1:45;
A14: p . 1 = x2 by FINSEQ_1:45;
A15: 1 in {1,2,3} by ENUMSET1:def_1;
A16: for k being Nat st 1 <= k & k <= 3 holds
lpl . k = lpp . k
proof
let k be Nat; ::_thesis: ( 1 <= k & k <= 3 implies lpl . k = lpp . k )
assume that
A17: 1 <= k and
A18: k <= 3 ; ::_thesis: lpl . k = lpp . k
k in NAT by ORDINAL1:def_12;
then A19: k in Seg 3 by A17, A18;
percases ( k = 1 or k = 2 or k = 3 ) by A19, ENUMSET1:def_1, FINSEQ_3:1;
suppose k = 1 ; ::_thesis: lpl . k = lpp . k
hence lpl . k = lpp . k by A15, A6, A14, A2, A11, Th4; ::_thesis: verum
end;
suppose k = 2 ; ::_thesis: lpl . k = lpp . k
hence lpl . k = lpp . k by A5, A8, A13, A4, A10, Th4; ::_thesis: verum
end;
suppose k = 3 ; ::_thesis: lpl . k = lpp . k
hence lpl . k = lpp . k by A1, A7, A12, A3, A9, Th4; ::_thesis: verum
end;
end;
end;
dom lpl = dom (Carrier <*G1,G2,G3*>) by CARD_3:9
.= Seg 3 by FINSEQ_3:1, PARTFUN1:def_2 ;
then A20: len lpl = 3 by FINSEQ_1:def_3;
len lpp = 3 by FINSEQ_1:45;
hence <*x1,y1,z1*> * <*x2,y2,z2*> = <*(x1 * x2),(y1 * y2),(z1 * z2)*> by A20, A16, FINSEQ_1:14; ::_thesis: verum
end;
theorem :: GROUP_7:31
for G1 being non empty Group-like multMagma holds 1_ (product <*G1*>) = <*(1_ G1)*>
proof
let G1 be non empty Group-like multMagma ; ::_thesis: 1_ (product <*G1*>) = <*(1_ G1)*>
set s = <*(1_ G1)*>;
set f = <*G1*>;
dom <*(1_ G1)*> = {1} by FINSEQ_1:2, FINSEQ_1:def_8;
then reconsider s = <*(1_ G1)*> as ManySortedSet of {1} by PARTFUN1:def_2, RELAT_1:def_18;
for i being set st i in {1} holds
ex G being non empty Group-like multMagma st
( G = <*G1*> . i & s . i = 1_ G )
proof
let i be set ; ::_thesis: ( i in {1} implies ex G being non empty Group-like multMagma st
( G = <*G1*> . i & s . i = 1_ G ) )
assume i in {1} ; ::_thesis: ex G being non empty Group-like multMagma st
( G = <*G1*> . i & s . i = 1_ G )
then A1: i = 1 by TARSKI:def_1;
then reconsider G = <*G1*> . i as non empty Group-like multMagma by FINSEQ_1:def_8;
take G ; ::_thesis: ( G = <*G1*> . i & s . i = 1_ G )
<*G1*> . i = G1 by A1, FINSEQ_1:def_8;
hence ( G = <*G1*> . i & s . i = 1_ G ) by A1, FINSEQ_1:def_8; ::_thesis: verum
end;
hence 1_ (product <*G1*>) = <*(1_ G1)*> by Th8; ::_thesis: verum
end;
theorem :: GROUP_7:32
for G1, G2 being non empty Group-like multMagma holds 1_ (product <*G1,G2*>) = <*(1_ G1),(1_ G2)*>
proof
let G1, G2 be non empty Group-like multMagma ; ::_thesis: 1_ (product <*G1,G2*>) = <*(1_ G1),(1_ G2)*>
set s = <*(1_ G1),(1_ G2)*>;
set f = <*G1,G2*>;
dom <*(1_ G1),(1_ G2)*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89;
then reconsider s = <*(1_ G1),(1_ G2)*> as ManySortedSet of {1,2} by PARTFUN1:def_2, RELAT_1:def_18;
for i being set st i in {1,2} holds
ex G being non empty Group-like multMagma st
( G = <*G1,G2*> . i & s . i = 1_ G )
proof
let i be set ; ::_thesis: ( i in {1,2} implies ex G being non empty Group-like multMagma st
( G = <*G1,G2*> . i & s . i = 1_ G ) )
assume A1: i in {1,2} ; ::_thesis: ex G being non empty Group-like multMagma st
( G = <*G1,G2*> . i & s . i = 1_ G )
percases ( i = 1 or i = 2 ) by A1, TARSKI:def_2;
supposeA2: i = 1 ; ::_thesis: ex G being non empty Group-like multMagma st
( G = <*G1,G2*> . i & s . i = 1_ G )
then reconsider G = <*G1,G2*> . i as non empty Group-like multMagma by FINSEQ_1:44;
take G ; ::_thesis: ( G = <*G1,G2*> . i & s . i = 1_ G )
<*G1,G2*> . i = G1 by A2, FINSEQ_1:44;
hence ( G = <*G1,G2*> . i & s . i = 1_ G ) by A2, FINSEQ_1:44; ::_thesis: verum
end;
supposeA3: i = 2 ; ::_thesis: ex G being non empty Group-like multMagma st
( G = <*G1,G2*> . i & s . i = 1_ G )
then reconsider G = <*G1,G2*> . i as non empty Group-like multMagma by FINSEQ_1:44;
take G ; ::_thesis: ( G = <*G1,G2*> . i & s . i = 1_ G )
<*G1,G2*> . i = G2 by A3, FINSEQ_1:44;
hence ( G = <*G1,G2*> . i & s . i = 1_ G ) by A3, FINSEQ_1:44; ::_thesis: verum
end;
end;
end;
hence 1_ (product <*G1,G2*>) = <*(1_ G1),(1_ G2)*> by Th8; ::_thesis: verum
end;
theorem :: GROUP_7:33
for G1, G2, G3 being non empty Group-like multMagma holds 1_ (product <*G1,G2,G3*>) = <*(1_ G1),(1_ G2),(1_ G3)*>
proof
let G1, G2, G3 be non empty Group-like multMagma ; ::_thesis: 1_ (product <*G1,G2,G3*>) = <*(1_ G1),(1_ G2),(1_ G3)*>
set s = <*(1_ G1),(1_ G2),(1_ G3)*>;
set f = <*G1,G2,G3*>;
dom <*(1_ G1),(1_ G2),(1_ G3)*> = {1,2,3} by FINSEQ_1:89, FINSEQ_3:1;
then reconsider s = <*(1_ G1),(1_ G2),(1_ G3)*> as ManySortedSet of {1,2,3} by PARTFUN1:def_2, RELAT_1:def_18;
for i being set st i in {1,2,3} holds
ex G being non empty Group-like multMagma st
( G = <*G1,G2,G3*> . i & s . i = 1_ G )
proof
let i be set ; ::_thesis: ( i in {1,2,3} implies ex G being non empty Group-like multMagma st
( G = <*G1,G2,G3*> . i & s . i = 1_ G ) )
assume A1: i in {1,2,3} ; ::_thesis: ex G being non empty Group-like multMagma st
( G = <*G1,G2,G3*> . i & s . i = 1_ G )
percases ( i = 1 or i = 2 or i = 3 ) by A1, ENUMSET1:def_1;
supposeA2: i = 1 ; ::_thesis: ex G being non empty Group-like multMagma st
( G = <*G1,G2,G3*> . i & s . i = 1_ G )
then reconsider G = <*G1,G2,G3*> . i as non empty Group-like multMagma by FINSEQ_1:45;
take G ; ::_thesis: ( G = <*G1,G2,G3*> . i & s . i = 1_ G )
<*G1,G2,G3*> . i = G1 by A2, FINSEQ_1:45;
hence ( G = <*G1,G2,G3*> . i & s . i = 1_ G ) by A2, FINSEQ_1:45; ::_thesis: verum
end;
supposeA3: i = 2 ; ::_thesis: ex G being non empty Group-like multMagma st
( G = <*G1,G2,G3*> . i & s . i = 1_ G )
then reconsider G = <*G1,G2,G3*> . i as non empty Group-like multMagma by FINSEQ_1:45;
take G ; ::_thesis: ( G = <*G1,G2,G3*> . i & s . i = 1_ G )
<*G1,G2,G3*> . i = G2 by A3, FINSEQ_1:45;
hence ( G = <*G1,G2,G3*> . i & s . i = 1_ G ) by A3, FINSEQ_1:45; ::_thesis: verum
end;
supposeA4: i = 3 ; ::_thesis: ex G being non empty Group-like multMagma st
( G = <*G1,G2,G3*> . i & s . i = 1_ G )
then reconsider G = <*G1,G2,G3*> . i as non empty Group-like multMagma by FINSEQ_1:45;
take G ; ::_thesis: ( G = <*G1,G2,G3*> . i & s . i = 1_ G )
<*G1,G2,G3*> . i = G3 by A4, FINSEQ_1:45;
hence ( G = <*G1,G2,G3*> . i & s . i = 1_ G ) by A4, FINSEQ_1:45; ::_thesis: verum
end;
end;
end;
hence 1_ (product <*G1,G2,G3*>) = <*(1_ G1),(1_ G2),(1_ G3)*> by Th8; ::_thesis: verum
end;
theorem :: GROUP_7:34
for G1 being Group
for x being Element of G1 holds <*x*> " = <*(x ")*>
proof
let G1 be Group; ::_thesis: for x being Element of G1 holds <*x*> " = <*(x ")*>
let x be Element of G1; ::_thesis: <*x*> " = <*(x ")*>
reconsider G = <*G1*> as Group-like associative multMagma-Family of {1} ;
reconsider lF = <*x*>, p = <*(x ")*> as Element of product (Carrier G) by Def2;
A1: p . 1 = x " by FINSEQ_1:def_8;
A2: G . 1 = G1 by FINSEQ_1:def_8;
for i being set st i in {1} holds
ex H being Group ex z being Element of H st
( H = G . i & p . i = z " & z = lF . i )
proof
reconsider H = G . 1 as Group by FINSEQ_1:def_8;
reconsider z = p . 1 as Element of H by A1, FINSEQ_1:def_8;
let i be set ; ::_thesis: ( i in {1} implies ex H being Group ex z being Element of H st
( H = G . i & p . i = z " & z = lF . i ) )
assume A3: i in {1} ; ::_thesis: ex H being Group ex z being Element of H st
( H = G . i & p . i = z " & z = lF . i )
take H ; ::_thesis: ex z being Element of H st
( H = G . i & p . i = z " & z = lF . i )
take z " ; ::_thesis: ( H = G . i & p . i = (z ") " & z " = lF . i )
thus H = G . i by A3, TARSKI:def_1; ::_thesis: ( p . i = (z ") " & z " = lF . i )
thus p . i = (z ") " by A3, TARSKI:def_1; ::_thesis: z " = lF . i
i = 1 by A3, TARSKI:def_1;
hence z " = lF . i by A1, A2, FINSEQ_1:def_8; ::_thesis: verum
end;
hence <*x*> " = <*(x ")*> by Th10; ::_thesis: verum
end;
theorem :: GROUP_7:35
for G1, G2 being Group
for x being Element of G1
for y being Element of G2 holds <*x,y*> " = <*(x "),(y ")*>
proof
let G1, G2 be Group; ::_thesis: for x being Element of G1
for y being Element of G2 holds <*x,y*> " = <*(x "),(y ")*>
let x be Element of G1; ::_thesis: for y being Element of G2 holds <*x,y*> " = <*(x "),(y ")*>
let y be Element of G2; ::_thesis: <*x,y*> " = <*(x "),(y ")*>
set G = <*G1,G2*>;
A1: <*G1,G2*> . 2 = G2 by FINSEQ_1:44;
reconsider lF = <*x,y*>, p = <*(x "),(y ")*> as Element of product (Carrier <*G1,G2*>) by Def2;
A2: p . 1 = x " by FINSEQ_1:44;
A3: p . 2 = y " by FINSEQ_1:44;
A4: <*G1,G2*> . 1 = G1 by FINSEQ_1:44;
for i being set st i in {1,2} holds
ex H being Group ex z being Element of H st
( H = <*G1,G2*> . i & p . i = z " & z = lF . i )
proof
let i be set ; ::_thesis: ( i in {1,2} implies ex H being Group ex z being Element of H st
( H = <*G1,G2*> . i & p . i = z " & z = lF . i ) )
assume A5: i in {1,2} ; ::_thesis: ex H being Group ex z being Element of H st
( H = <*G1,G2*> . i & p . i = z " & z = lF . i )
percases ( i = 1 or i = 2 ) by A5, TARSKI:def_2;
supposeA6: i = 1 ; ::_thesis: ex H being Group ex z being Element of H st
( H = <*G1,G2*> . i & p . i = z " & z = lF . i )
reconsider H = <*G1,G2*> . 1 as Group by FINSEQ_1:44;
reconsider z = p . 1 as Element of H by A2, FINSEQ_1:44;
take H ; ::_thesis: ex z being Element of H st
( H = <*G1,G2*> . i & p . i = z " & z = lF . i )
take z " ; ::_thesis: ( H = <*G1,G2*> . i & p . i = (z ") " & z " = lF . i )
thus H = <*G1,G2*> . i by A6; ::_thesis: ( p . i = (z ") " & z " = lF . i )
thus p . i = (z ") " by A6; ::_thesis: z " = lF . i
thus z " = lF . i by A2, A4, A6, FINSEQ_1:44; ::_thesis: verum
end;
supposeA7: i = 2 ; ::_thesis: ex H being Group ex z being Element of H st
( H = <*G1,G2*> . i & p . i = z " & z = lF . i )
reconsider H = <*G1,G2*> . 2 as Group by FINSEQ_1:44;
reconsider z = p . 2 as Element of H by A3, FINSEQ_1:44;
take H ; ::_thesis: ex z being Element of H st
( H = <*G1,G2*> . i & p . i = z " & z = lF . i )
take z " ; ::_thesis: ( H = <*G1,G2*> . i & p . i = (z ") " & z " = lF . i )
thus H = <*G1,G2*> . i by A7; ::_thesis: ( p . i = (z ") " & z " = lF . i )
thus p . i = (z ") " by A7; ::_thesis: z " = lF . i
thus z " = lF . i by A3, A1, A7, FINSEQ_1:44; ::_thesis: verum
end;
end;
end;
hence <*x,y*> " = <*(x "),(y ")*> by Th10; ::_thesis: verum
end;
theorem :: GROUP_7:36
for G1, G2, G3 being Group
for x being Element of G1
for y being Element of G2
for z being Element of G3 holds <*x,y,z*> " = <*(x "),(y "),(z ")*>
proof
let G1, G2, G3 be Group; ::_thesis: for x being Element of G1
for y being Element of G2
for z being Element of G3 holds <*x,y,z*> " = <*(x "),(y "),(z ")*>
let x be Element of G1; ::_thesis: for y being Element of G2
for z being Element of G3 holds <*x,y,z*> " = <*(x "),(y "),(z ")*>
let y be Element of G2; ::_thesis: for z being Element of G3 holds <*x,y,z*> " = <*(x "),(y "),(z ")*>
let z be Element of G3; ::_thesis: <*x,y,z*> " = <*(x "),(y "),(z ")*>
set G = <*G1,G2,G3*>;
A1: <*G1,G2,G3*> . 2 = G2 by FINSEQ_1:45;
A2: <*G1,G2,G3*> . 3 = G3 by FINSEQ_1:45;
reconsider lF = <*x,y,z*>, p = <*(x "),(y "),(z ")*> as Element of product (Carrier <*G1,G2,G3*>) by Def2;
A3: p . 1 = x " by FINSEQ_1:45;
A4: p . 3 = z " by FINSEQ_1:45;
A5: p . 2 = y " by FINSEQ_1:45;
A6: <*G1,G2,G3*> . 1 = G1 by FINSEQ_1:45;
for i being set st i in {1,2,3} holds
ex H being Group ex z being Element of H st
( H = <*G1,G2,G3*> . i & p . i = z " & z = lF . i )
proof
let i be set ; ::_thesis: ( i in {1,2,3} implies ex H being Group ex z being Element of H st
( H = <*G1,G2,G3*> . i & p . i = z " & z = lF . i ) )
assume A7: i in {1,2,3} ; ::_thesis: ex H being Group ex z being Element of H st
( H = <*G1,G2,G3*> . i & p . i = z " & z = lF . i )
percases ( i = 1 or i = 2 or i = 3 ) by A7, ENUMSET1:def_1;
supposeA8: i = 1 ; ::_thesis: ex H being Group ex z being Element of H st
( H = <*G1,G2,G3*> . i & p . i = z " & z = lF . i )
reconsider H = <*G1,G2,G3*> . 1 as Group by FINSEQ_1:45;
reconsider z = p . 1 as Element of H by A3, FINSEQ_1:45;
take H ; ::_thesis: ex z being Element of H st
( H = <*G1,G2,G3*> . i & p . i = z " & z = lF . i )
take z " ; ::_thesis: ( H = <*G1,G2,G3*> . i & p . i = (z ") " & z " = lF . i )
thus H = <*G1,G2,G3*> . i by A8; ::_thesis: ( p . i = (z ") " & z " = lF . i )
thus p . i = (z ") " by A8; ::_thesis: z " = lF . i
thus z " = lF . i by A3, A6, A8, FINSEQ_1:45; ::_thesis: verum
end;
supposeA9: i = 2 ; ::_thesis: ex H being Group ex z being Element of H st
( H = <*G1,G2,G3*> . i & p . i = z " & z = lF . i )
reconsider H = <*G1,G2,G3*> . 2 as Group by FINSEQ_1:45;
reconsider z = p . 2 as Element of H by A5, FINSEQ_1:45;
take H ; ::_thesis: ex z being Element of H st
( H = <*G1,G2,G3*> . i & p . i = z " & z = lF . i )
take z " ; ::_thesis: ( H = <*G1,G2,G3*> . i & p . i = (z ") " & z " = lF . i )
thus H = <*G1,G2,G3*> . i by A9; ::_thesis: ( p . i = (z ") " & z " = lF . i )
thus p . i = (z ") " by A9; ::_thesis: z " = lF . i
thus z " = lF . i by A5, A1, A9, FINSEQ_1:45; ::_thesis: verum
end;
supposeA10: i = 3 ; ::_thesis: ex H being Group ex z being Element of H st
( H = <*G1,G2,G3*> . i & p . i = z " & z = lF . i )
reconsider H = <*G1,G2,G3*> . 3 as Group by FINSEQ_1:45;
reconsider z = p . 3 as Element of H by A4, FINSEQ_1:45;
take H ; ::_thesis: ex z being Element of H st
( H = <*G1,G2,G3*> . i & p . i = z " & z = lF . i )
take z " ; ::_thesis: ( H = <*G1,G2,G3*> . i & p . i = (z ") " & z " = lF . i )
thus H = <*G1,G2,G3*> . i by A10; ::_thesis: ( p . i = (z ") " & z " = lF . i )
thus p . i = (z ") " by A10; ::_thesis: z " = lF . i
thus z " = lF . i by A4, A2, A10, FINSEQ_1:45; ::_thesis: verum
end;
end;
end;
hence <*x,y,z*> " = <*(x "),(y "),(z ")*> by Th10; ::_thesis: verum
end;
theorem Th40: :: GROUP_7:37
for G1 being Group
for f being Function of the carrier of G1, the carrier of (product <*G1*>) st ( for x being Element of G1 holds f . x = <*x*> ) holds
f is Homomorphism of G1,(product <*G1*>)
proof
let G1 be Group; ::_thesis: for f being Function of the carrier of G1, the carrier of (product <*G1*>) st ( for x being Element of G1 holds f . x = <*x*> ) holds
f is Homomorphism of G1,(product <*G1*>)
let f be Function of the carrier of G1, the carrier of (product <*G1*>); ::_thesis: ( ( for x being Element of G1 holds f . x = <*x*> ) implies f is Homomorphism of G1,(product <*G1*>) )
assume A1: for x being Element of G1 holds f . x = <*x*> ; ::_thesis: f is Homomorphism of G1,(product <*G1*>)
now__::_thesis:_for_a,_b_being_Element_of_G1_holds_f_._(a_*_b)_=_(f_._a)_*_(f_._b)
let a, b be Element of G1; ::_thesis: f . (a * b) = (f . a) * (f . b)
thus f . (a * b) = <*(a * b)*> by A1
.= <*a*> * <*b*> by Th31
.= <*a*> * (f . b) by A1
.= (f . a) * (f . b) by A1 ; ::_thesis: verum
end;
hence f is Homomorphism of G1,(product <*G1*>) by GROUP_6:def_6; ::_thesis: verum
end;
theorem Th41: :: GROUP_7:38
for G1 being Group
for f being Homomorphism of G1,(product <*G1*>) st ( for x being Element of G1 holds f . x = <*x*> ) holds
f is bijective
proof
let G1 be Group; ::_thesis: for f being Homomorphism of G1,(product <*G1*>) st ( for x being Element of G1 holds f . x = <*x*> ) holds
f is bijective
let f be Homomorphism of G1,(product <*G1*>); ::_thesis: ( ( for x being Element of G1 holds f . x = <*x*> ) implies f is bijective )
assume A1: for x being Element of G1 holds f . x = <*x*> ; ::_thesis: f is bijective
A2: dom f = the carrier of G1 by FUNCT_2:def_1;
A3: rng f = the carrier of (product <*G1*>)
proof
thus rng f c= the carrier of (product <*G1*>) ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of (product <*G1*>) c= rng f
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (product <*G1*>) or x in rng f )
assume x in the carrier of (product <*G1*>) ; ::_thesis: x in rng f
then reconsider a = x as Element of (product <*G1*>) ;
A4: 1 in {1} by TARSKI:def_1;
then A5: ex R being 1-sorted st
( R = <*G1*> . 1 & (Carrier <*G1*>) . 1 = the carrier of R ) by PRALG_1:def_13;
a in the carrier of (product <*G1*>) ;
then A6: a in product (Carrier <*G1*>) by Def2;
then A7: dom a = dom (Carrier <*G1*>) by CARD_3:9;
then A8: dom a = {1} by PARTFUN1:def_2;
then a . 1 in (Carrier <*G1*>) . 1 by A6, A7, A4, CARD_3:9;
then reconsider b = a . 1 as Element of G1 by A5, FINSEQ_1:def_8;
f . b = <*b*> by A1
.= x by A8, FINSEQ_1:2, FINSEQ_1:def_8 ;
hence x in rng f by A2, FUNCT_1:def_3; ::_thesis: verum
end;
f is one-to-one
proof
let m, n be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not m in dom f or not n in dom f or not f . m = f . n or m = n )
assume that
A9: m in dom f and
A10: n in dom f and
A11: f . m = f . n ; ::_thesis: m = n
reconsider m1 = m, n1 = n as Element of G1 by A9, A10;
<*m1*> = f . m1 by A1
.= <*n1*> by A1, A11 ;
hence m = n by FINSEQ_1:76; ::_thesis: verum
end;
hence f is bijective by A3, GROUP_6:60; ::_thesis: verum
end;
theorem :: GROUP_7:39
for G1 being Group holds G1, product <*G1*> are_isomorphic
proof
let G1 be Group; ::_thesis: G1, product <*G1*> are_isomorphic
deffunc H1( Element of G1) -> Element of (product <*G1*>) = <*$1*>;
consider f being Function of the carrier of G1, the carrier of (product <*G1*>) such that
A1: for x being Element of G1 holds f . x = H1(x) from FUNCT_2:sch_4();
reconsider f = f as Homomorphism of G1,(product <*G1*>) by A1, Th40;
take f ; :: according to GROUP_6:def_11 ::_thesis: f is bijective
thus f is bijective by A1, Th41; ::_thesis: verum
end;