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;
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 ;
( 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)
;
(the_left_translation_of (s1 * s2),Z) . x = (the_left_translation_of s1,Z) . ((the_left_translation_of s2,Z) . x)then reconsider z19 =
x as
Element of
[:the carrier of S,Z:] ;
reconsider z1999 =
x as
Element of
[:the carrier of S,Z:] by A5;
consider z29 being
Element of
[:the carrier of S,Z:],
s19,
s29 being
Element of
S,
z9 being
Element of
Z such that A6:
z29 = (the_left_translation_of s2,Z) . z19
and A7:
s29 = s2 * s19
and A8:
z19 = [s19,z9]
and A9:
z29 = [s29,z9]
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 z199 =
(the_left_translation_of s2,Z) . x as
Element of
[:the carrier of S,Z:] ;
consider z299 being
Element of
[:the carrier of S,Z:],
s199,
s299 being
Element of
S,
z99 being
Element of
Z such that A10:
z299 = (the_left_translation_of s1,Z) . z199
and A11:
s299 = s1 * s199
and A12:
z199 = [s199,z99]
and A13:
z299 = [s299,z99]
by Def6;
A14:
z99 = z9
by A6, A9, A12, ZFMISC_1:33;
consider z2999 being
Element of
[:the carrier of S,Z:],
s1999,
s2999 being
Element of
S,
z999 being
Element of
Z such that A15:
z2999 = (the_left_translation_of (s1 * s2),Z) . z1999
and A16:
s2999 = (s1 * s2) * s1999
and A17:
z1999 = [s1999,z999]
and A18:
z2999 = [s2999,z999]
by Def6;
s2999 =
(s1 * s2) * s19
by A8, A16, A17, ZFMISC_1:33
.=
s1 * (s2 * s19)
by GROUP_1:def 4
.=
s299
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;
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 ;
( ( 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 ( 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)
;
( 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;
(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;
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)
;
x in dom (the_left_translation_of (s1 * s2),Z)thus
x in dom (the_left_translation_of (s1 * s2),Z)
by A19, A21;
verum end;
hence
H1(
s1 * s2)
= H1(
s1)
* H1(
s2)
by A4, FUNCT_1:20;
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 ;
( 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:]
;
(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;
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
f9 being
Function st
(
the_left_translation_of (1_ S),
Z = f9 &
dom f9 = [:the carrier of S,Z:] &
rng f9 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;
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
; verum