deffunc H1( Element of S) -> Function of [:the carrier of S,Z:],[:the carrier of S,Z:] = the_left_translation_of $1,Z;
set E = [:the carrier of S,Z:];
A1:
for s1, s2 being Element of S holds H1(s1 * s2) = H1(s1) * H1(s2)
proof
let s1,
s2 be
Element of
S;
:: thesis: H1(s1 * s2) = H1(s1) * H1(s2)
set f12 =
the_left_translation_of (s1 * s2),
Z;
set f1 =
the_left_translation_of s1,
Z;
set f2 =
the_left_translation_of s2,
Z;
the_left_translation_of s1,
Z in Funcs [:the carrier of S,Z:],
[:the carrier of S,Z:]
by FUNCT_2:12;
then A2:
ex
f being
Function st
(
the_left_translation_of s1,
Z = f &
dom f = [:the carrier of S,Z:] &
rng f c= [:the carrier of S,Z:] )
by FUNCT_2:def 2;
the_left_translation_of s2,
Z in Funcs [:the carrier of S,Z:],
[:the carrier of S,Z:]
by FUNCT_2:12;
then A3:
ex
f being
Function st
(
the_left_translation_of s2,
Z = f &
dom f = [:the carrier of S,Z:] &
rng f c= [:the carrier of S,Z:] )
by FUNCT_2:def 2;
A4:
now let x be
set ;
:: thesis: ( x in dom (the_left_translation_of (s1 * s2),Z) implies (the_left_translation_of (s1 * s2),Z) . x = (the_left_translation_of s1,Z) . ((the_left_translation_of s2,Z) . x) )assume A5:
x in dom (the_left_translation_of (s1 * s2),Z)
;
:: thesis: (the_left_translation_of (s1 * s2),Z) . x = (the_left_translation_of s1,Z) . ((the_left_translation_of s2,Z) . x)then reconsider z1' =
x as
Element of
[:the carrier of S,Z:] ;
reconsider z1''' =
x as
Element of
[:the carrier of S,Z:] by A5;
consider z2' being
Element of
[:the carrier of S,Z:],
s1',
s2' being
Element of
S,
z' being
Element of
Z such that A6:
z2' = (the_left_translation_of s2,Z) . z1'
and A7:
s2' = s2 * s1'
and A8:
z1' = [s1',z']
and A9:
z2' = [s2',z']
by Def6;
(the_left_translation_of s2,Z) . x in rng (the_left_translation_of s2,Z)
by A3, A5, FUNCT_1:12;
then reconsider z1'' =
(the_left_translation_of s2,Z) . x as
Element of
[:the carrier of S,Z:] ;
consider z2'' being
Element of
[:the carrier of S,Z:],
s1'',
s2'' being
Element of
S,
z'' being
Element of
Z such that A10:
z2'' = (the_left_translation_of s1,Z) . z1''
and A11:
s2'' = s1 * s1''
and A12:
z1'' = [s1'',z'']
and A13:
z2'' = [s2'',z'']
by Def6;
A14:
z'' = z'
by A6, A9, A12, ZFMISC_1:33;
consider z2''' being
Element of
[:the carrier of S,Z:],
s1''',
s2''' being
Element of
S,
z''' being
Element of
Z such that A15:
z2''' = (the_left_translation_of (s1 * s2),Z) . z1'''
and A16:
s2''' = (s1 * s2) * s1'''
and A17:
z1''' = [s1''',z''']
and A18:
z2''' = [s2''',z''']
by Def6;
s2''' =
(s1 * s2) * s1'
by A8, A16, A17, ZFMISC_1:33
.=
s1 * (s2 * s1')
by GROUP_1:def 4
.=
s2''
by A6, A7, A9, A11, A12, ZFMISC_1:33
;
hence
(the_left_translation_of (s1 * s2),Z) . x = (the_left_translation_of s1,Z) . ((the_left_translation_of s2,Z) . x)
by A8, A10, A13, A15, A17, A18, A14, ZFMISC_1:33;
:: thesis: verum end;
the_left_translation_of (s1 * s2),
Z in Funcs [:the carrier of S,Z:],
[:the carrier of S,Z:]
by FUNCT_2:12;
then A19:
ex
f being
Function st
(
the_left_translation_of (s1 * s2),
Z = f &
dom f = [:the carrier of S,Z:] &
rng f c= [:the carrier of S,Z:] )
by FUNCT_2:def 2;
now let x be
set ;
:: thesis: ( ( x in dom (the_left_translation_of (s1 * s2),Z) implies ( x in dom (the_left_translation_of s2,Z) & (the_left_translation_of s2,Z) . x in dom (the_left_translation_of s1,Z) ) ) & ( x in dom (the_left_translation_of s2,Z) & (the_left_translation_of s2,Z) . x in dom (the_left_translation_of s1,Z) implies x in dom (the_left_translation_of (s1 * s2),Z) ) )hereby :: thesis: ( x in dom (the_left_translation_of s2,Z) & (the_left_translation_of s2,Z) . x in dom (the_left_translation_of s1,Z) implies x in dom (the_left_translation_of (s1 * s2),Z) )
assume A20:
x in dom (the_left_translation_of (s1 * s2),Z)
;
:: thesis: ( x in dom (the_left_translation_of s2,Z) & (the_left_translation_of s2,Z) . x in dom (the_left_translation_of s1,Z) )hence
x in dom (the_left_translation_of s2,Z)
by A3;
:: thesis: (the_left_translation_of s2,Z) . x in dom (the_left_translation_of s1,Z)
(the_left_translation_of s2,Z) . x in rng (the_left_translation_of s2,Z)
by A3, A20, FUNCT_1:12;
hence
(the_left_translation_of s2,Z) . x in dom (the_left_translation_of s1,Z)
by A2;
:: thesis: verum
end; assume that A21:
x in dom (the_left_translation_of s2,Z)
and
(the_left_translation_of s2,Z) . x in dom (the_left_translation_of s1,Z)
;
:: thesis: x in dom (the_left_translation_of (s1 * s2),Z)thus
x in dom (the_left_translation_of (s1 * s2),Z)
by A19, A21;
:: thesis: verum end;
hence
H1(
s1 * s2)
= H1(
s1)
* H1(
s2)
by A4, FUNCT_1:20;
:: thesis: verum
end;
A22:
H1( 1_ S) = id [:the carrier of S,Z:]
proof
set f =
the_left_translation_of (1_ S),
Z;
A23:
now let x be
set ;
:: thesis: ( x in [:the carrier of S,Z:] implies (the_left_translation_of (1_ S),Z) . x = x )assume
x in [:the carrier of S,Z:]
;
:: thesis: (the_left_translation_of (1_ S),Z) . x = xthen reconsider z1 =
x as
Element of
[:the carrier of S,Z:] ;
ex
z2 being
Element of
[:the carrier of S,Z:] ex
s1,
s2 being
Element of
S ex
z being
Element of
Z st
(
z2 = (the_left_translation_of (1_ S),Z) . z1 &
s2 = (1_ S) * s1 &
z1 = [s1,z] &
z2 = [s2,z] )
by Def6;
hence
(the_left_translation_of (1_ S),Z) . x = x
by GROUP_1:def 5;
:: thesis: verum end;
the_left_translation_of (1_ S),
Z in Funcs [:the carrier of S,Z:],
[:the carrier of S,Z:]
by FUNCT_2:12;
then
ex
f' being
Function st
(
the_left_translation_of (1_ S),
Z = f' &
dom f' = [:the carrier of S,Z:] &
rng f' c= [:the carrier of S,Z:] )
by FUNCT_2:def 2;
hence
H1(
1_ S)
= id [:the carrier of S,Z:]
by A23, FUNCT_1:34;
:: thesis: verum
end;
ex T being LeftOperation of S,[:the carrier of S,Z:] st
for s being Element of S holds T . s = H1(s)
from GROUP_10:sch 1(A22, A1);
hence
ex b1 being LeftOperation of S,[:the carrier of S,Z:] st
for s being Element of S holds b1 . s = the_left_translation_of s,Z
; :: thesis: verum