let O be set ; for G being strict Group ex H being non empty HGrWOpStr over O st
( H is strict & H is distributive & H is Group-like & H is associative & G = multMagma(# the carrier of H, the multF of H #) )
let G be strict Group; ex H being non empty HGrWOpStr over O st
( H is strict & H is distributive & H is Group-like & H is associative & G = multMagma(# the carrier of H, the multF of H #) )
reconsider h = [:O,{(id the carrier of G)}:] as Action of O, the carrier of G by Lm1;
set A = the carrier of G;
set m = the multF of G;
set GO = HGrWOpStr(# the carrier of G, the multF of G,h #);
reconsider GO = HGrWOpStr(# the carrier of G, the multF of G,h #) as non empty HGrWOpStr over O ;
reconsider G9 = GO as non empty multMagma ;
A1:
now ex e9 being Element of G9 st
for h9 being Element of G9 holds
( h9 * e9 = h9 & e9 * h9 = h9 & ex g9 being Element of G9 st
( h9 * g9 = e9 & g9 * h9 = e9 ) )end;
take
GO
; ( GO is strict & GO is distributive & GO is Group-like & GO is associative & G = multMagma(# the carrier of GO, the multF of GO #) )
A2:
now for G99 being Group
for a being Action of O, the carrier of G99 st a = the action of GO & multMagma(# the carrier of G99, the multF of G99 #) = multMagma(# the carrier of GO, the multF of GO #) holds
a is distributive let G99 be
Group;
for a being Action of O, the carrier of G99 st a = the action of GO & multMagma(# the carrier of G99, the multF of G99 #) = multMagma(# the carrier of GO, the multF of GO #) holds
a is distributive let a be
Action of
O, the
carrier of
G99;
( a = the action of GO & multMagma(# the carrier of G99, the multF of G99 #) = multMagma(# the carrier of GO, the multF of GO #) implies a is distributive )assume A3:
a = the
action of
GO
;
( multMagma(# the carrier of G99, the multF of G99 #) = multMagma(# the carrier of GO, the multF of GO #) implies a is distributive )assume A4:
multMagma(# the
carrier of
G99, the
multF of
G99 #)
= multMagma(# the
carrier of
GO, the
multF of
GO #)
;
a is distributive now for o being Element of O st o in O holds
a . o is Homomorphism of G99,G99let o be
Element of
O;
( o in O implies a . o is Homomorphism of G99,G99 )assume
o in O
;
a . o is Homomorphism of G99,G99then
o in dom h
by FUNCT_2:def 1;
then
[o,(h . o)] in [:O,{(id the carrier of G99)}:]
by A4, FUNCT_1:1;
then consider x,
y being
object such that
x in O
and A5:
(
y in {(id the carrier of G99)} &
[o,(h . o)] = [x,y] )
by ZFMISC_1:def 2;
(
y = id the
carrier of
G99 &
h . o = y )
by A5, TARSKI:def 1, XTUPLE_0:1;
hence
a . o is
Homomorphism of
G99,
G99
by A3, GROUP_6:38;
verum end; hence
a is
distributive
;
verum end;
now for x9, y9, z9 being Element of G9 holds (x9 * y9) * z9 = x9 * (y9 * z9)let x9,
y9,
z9 be
Element of
G9;
(x9 * y9) * z9 = x9 * (y9 * z9)reconsider x =
x9,
y =
y9,
z =
z9 as
Element of
G ;
(x9 * y9) * z9 =
(x * y) * z
.=
x * (y * z)
by GROUP_1:def 3
;
hence
(x9 * y9) * z9 = x9 * (y9 * z9)
;
verum end;
hence
( GO is strict & GO is distributive & GO is Group-like & GO is associative & G = multMagma(# the carrier of GO, the multF of GO #) )
by A1, A2, GROUP_1:def 2, GROUP_1:def 3; verum