let G be finite Group; :: thesis: for E, T being non empty set
for LO being LeftOperation of G,E
for n being natural number st LO = the_left_operation_of G,T & n = card G & E = [:the carrier of G,T:] & card n c= card E holds
the_fixed_points_of (the_extension_of_left_operation_of n,LO) = { [:the carrier of G,{t}:] where t is Element of T : verum }
let E, T be non empty set ; :: thesis: for LO being LeftOperation of G,E
for n being natural number st LO = the_left_operation_of G,T & n = card G & E = [:the carrier of G,T:] & card n c= card E holds
the_fixed_points_of (the_extension_of_left_operation_of n,LO) = { [:the carrier of G,{t}:] where t is Element of T : verum }
let LO be LeftOperation of G,E; :: thesis: for n being natural number st LO = the_left_operation_of G,T & n = card G & E = [:the carrier of G,T:] & card n c= card E holds
the_fixed_points_of (the_extension_of_left_operation_of n,LO) = { [:the carrier of G,{t}:] where t is Element of T : verum }
let n be natural number ; :: thesis: ( LO = the_left_operation_of G,T & n = card G & E = [:the carrier of G,T:] & card n c= card E implies the_fixed_points_of (the_extension_of_left_operation_of n,LO) = { [:the carrier of G,{t}:] where t is Element of T : verum } )
assume A1:
LO = the_left_operation_of G,T
; :: thesis: ( not n = card G or not E = [:the carrier of G,T:] or not card n c= card E or the_fixed_points_of (the_extension_of_left_operation_of n,LO) = { [:the carrier of G,{t}:] where t is Element of T : verum } )
assume A2:
n = card G
; :: thesis: ( not E = [:the carrier of G,T:] or not card n c= card E or the_fixed_points_of (the_extension_of_left_operation_of n,LO) = { [:the carrier of G,{t}:] where t is Element of T : verum } )
assume A3:
E = [:the carrier of G,T:]
; :: thesis: ( not card n c= card E or the_fixed_points_of (the_extension_of_left_operation_of n,LO) = { [:the carrier of G,{t}:] where t is Element of T : verum } )
assume A4:
card n c= card E
; :: thesis: the_fixed_points_of (the_extension_of_left_operation_of n,LO) = { [:the carrier of G,{t}:] where t is Element of T : verum }
set LO' = the_extension_of_left_operation_of n,LO;
set EE = the_subsets_of_card n,E;
now let z be
set ;
:: thesis: ( ( z in the_fixed_points_of (the_extension_of_left_operation_of n,LO) implies z in { [:the carrier of G,{t'}:] where t' is Element of T : verum } ) & ( z in { [:the carrier of G,{t}:] where t is Element of T : verum } implies z in the_fixed_points_of (the_extension_of_left_operation_of n,LO) ) )hereby :: thesis: ( z in { [:the carrier of G,{t}:] where t is Element of T : verum } implies z in the_fixed_points_of (the_extension_of_left_operation_of n,LO) )
assume
z in the_fixed_points_of (the_extension_of_left_operation_of n,LO)
;
:: thesis: z in { [:the carrier of G,{t'}:] where t' is Element of T : verum } then
z in { x where x is Element of the_subsets_of_card n,E : x is_fixed_under the_extension_of_left_operation_of n,LO }
by Def13;
then consider e being
Element of
the_subsets_of_card n,
E such that A5:
(
z = e &
e is_fixed_under the_extension_of_left_operation_of n,
LO )
;
A6:
for
g being
Element of
G holds
e = (the_left_translation_of g,T) .: e
proof
let g be
Element of
G;
:: thesis: e = (the_left_translation_of g,T) .: e
(the_extension_of_left_operation_of n,LO) . g = the_extension_of_left_translation_of n,
g,
LO
by A4, Def5;
then A7:
((the_extension_of_left_operation_of n,LO) ^ g) . e = (LO ^ g) .: e
by A4, Def4;
e = ((the_extension_of_left_operation_of n,LO) ^ g) . e
by A5, Def12;
hence
e = (the_left_translation_of g,T) .: e
by A1, A7, Def7;
:: thesis: verum
end;
not
the_subsets_of_card n,
E is
empty
by A4, Th2;
then
z in the_subsets_of_card n,
E
by A5;
then consider X being
Subset of
E such that A8:
(
z = X &
card X = n )
;
ex
t being
Element of
T st
[:the carrier of G,{t}:] c= z
proof
not
X is
empty
by A2, A8;
then consider x1 being
set such that A9:
x1 in X
by XBOOLE_0:def 1;
consider g1,
t being
set such that A10:
(
g1 in the
carrier of
G &
t in T &
x1 = [g1,t] )
by A3, A9, ZFMISC_1:def 2;
reconsider g1 =
g1 as
Element of
G by A10;
reconsider t =
t as
Element of
T by A10;
take
t
;
:: thesis: [:the carrier of G,{t}:] c= z
now let x2 be
set ;
:: thesis: ( x2 in [:the carrier of G,{t}:] implies x2 in z )assume
x2 in [:the carrier of G,{t}:]
;
:: thesis: x2 in zthen consider g2,
t' being
set such that A11:
(
g2 in the
carrier of
G &
t' in {t} &
x2 = [g2,t'] )
by ZFMISC_1:def 2;
reconsider g2 =
g2 as
Element of
G by A11;
set g =
g2 * (g1 " );
A12:
dom (the_left_translation_of (g2 * (g1 " )),T) = E
by A3, FUNCT_2:def 1;
reconsider z1' =
x1 as
Element of
[:the carrier of G,T:] by A3, A9;
consider z2' being
Element of
[:the carrier of G,T:],
g1',
g2' being
Element of
G,
t'' being
Element of
T such that A13:
(
z2' = (the_left_translation_of (g2 * (g1 " )),T) . z1' &
g2' = (g2 * (g1 " )) * g1' &
z1' = [g1',t''] &
z2' = [g2',t''] )
by Def6;
A14:
(
g1 = g1' &
t = t'' )
by A10, A13, ZFMISC_1:33;
g2' =
(g2 * (g1 " )) * g1
by A10, A13, ZFMISC_1:33
.=
g2 * ((g1 " ) * g1)
by GROUP_1:def 4
.=
g2 * (1_ G)
by GROUP_1:def 6
.=
g2
by GROUP_1:def 5
;
then A15:
z2' = x2
by A11, A13, A14, TARSKI:def 1;
(the_left_translation_of (g2 * (g1 " )),T) . x1 in (the_left_translation_of (g2 * (g1 " )),T) .: e
by A5, A8, A9, A12, FUNCT_1:def 12;
hence
x2 in z
by A5, A6, A13, A15;
:: thesis: verum end;
hence
[:the carrier of G,{t}:] c= z
by TARSKI:def 3;
:: thesis: verum
end; then consider t being
Element of
T such that A16:
[:the carrier of G,{t}:] c= z
;
A17:
card [:the carrier of G,{t}:] =
card the
carrier of
G
by CARD_2:13
.=
n
by A2
;
n,
X are_equipotent
by A8, CARD_1:def 5;
then consider f being
Function such that A18:
(
f is
one-to-one &
dom f = n &
rng f = X )
by WELLORD2:def 4;
dom f in omega
by A18, ORDINAL1:def 13;
then reconsider X =
X as
finite set by A18, FINSET_1:def 1;
[:the carrier of G,{t}:] = X
by A8, A16, A17, CARD_FIN:1;
hence
z in { [:the carrier of G,{t'}:] where t' is Element of T : verum }
by A8;
:: thesis: verum
end; assume
z in { [:the carrier of G,{t}:] where t is Element of T : verum }
;
:: thesis: z in the_fixed_points_of (the_extension_of_left_operation_of n,LO)then consider t being
Element of
T such that A19:
z = [:the carrier of G,{t}:]
;
then A21:
z c= [:the carrier of G,T:]
by TARSKI:def 3;
reconsider X =
z as
Subset of
E by A3, A20, TARSKI:def 3;
card X = card the
carrier of
G
by A19, CARD_2:13;
then
z in the_subsets_of_card n,
E
by A2;
then reconsider e =
z as
Element of
the_subsets_of_card n,
E ;
A22:
for
g being
Element of
G holds
e = (LO ^ g) .: e
proof
let g be
Element of
G;
:: thesis: e = (LO ^ g) .: e
A23:
LO ^ g = the_left_translation_of g,
T
by A1, Def7;
now let e2 be
set ;
:: thesis: ( ( e2 in e implies ex e1 being set st
( e1 in dom (LO ^ g) & e1 in e & e2 = (LO ^ g) . e1 ) ) & ( ex e1 being set st
( e1 in dom (LO ^ g) & e1 in e & e2 = (LO ^ g) . e1 ) implies e2 in e ) )hereby :: thesis: ( ex e1 being set st
( e1 in dom (LO ^ g) & e1 in e & e2 = (LO ^ g) . e1 ) implies e2 in e )
assume
e2 in e
;
:: thesis: ex e1 being set st
( e1 in dom (LO ^ g) & e1 in e & e2 = (LO ^ g) . e1 )then consider g2,
t2 being
set such that A24:
(
g2 in the
carrier of
G &
t2 in {t} &
e2 = [g2,t2] )
by A19, ZFMISC_1:def 2;
reconsider g2 =
g2 as
Element of
G by A24;
reconsider e1 =
[((g " ) * g2),t2] as
set ;
take e1 =
e1;
:: thesis: ( e1 in dom (LO ^ g) & e1 in e & e2 = (LO ^ g) . e1 )A25:
e1 in e
by A19, A24, ZFMISC_1:def 2;
z c= dom (LO ^ g)
by A3, A21, FUNCT_2:def 1;
hence
(
e1 in dom (LO ^ g) &
e1 in e )
by A25;
:: thesis: e2 = (LO ^ g) . e1then reconsider z1 =
e1 as
Element of
[:the carrier of G,T:] by A3;
consider z2 being
Element of
[:the carrier of G,T:],
g1',
g2' being
Element of
G,
t' being
Element of
T such that A26:
(
z2 = (LO ^ g) . z1 &
g2' = g * g1' &
z1 = [g1',t'] &
z2 = [g2',t'] )
by A23, Def6;
g2' =
g * ((g " ) * g2)
by A26, ZFMISC_1:33
.=
(g * (g " )) * g2
by GROUP_1:def 4
.=
(1_ G) * g2
by GROUP_1:def 6
.=
g2
by GROUP_1:def 5
;
hence
e2 = (LO ^ g) . e1
by A24, A26, ZFMISC_1:33;
:: thesis: verum
end; given e1 being
set such that A27:
(
e1 in dom (LO ^ g) &
e1 in e &
e2 = (LO ^ g) . e1 )
;
:: thesis: e2 in econsider g1,
t1 being
set such that A28:
(
g1 in the
carrier of
G &
t1 in {t} &
e1 = [g1,t1] )
by A19, A27, ZFMISC_1:def 2;
reconsider z1 =
e1 as
Element of
[:the carrier of G,T:] by A3, A27;
consider z2 being
Element of
[:the carrier of G,T:],
g1',
g2' being
Element of
G,
t' being
Element of
T such that A29:
(
z2 = (LO ^ g) . z1 &
g2' = g * g1' &
z1 = [g1',t'] &
z2 = [g2',t'] )
by A23, Def6;
t1 = t
by A28, TARSKI:def 1;
then A30:
t' = t
by A28, A29, ZFMISC_1:33;
t' in {t'}
by TARSKI:def 1;
hence
e2 in e
by A19, A27, A29, A30, ZFMISC_1:def 2;
:: thesis: verum end;
hence
e = (LO ^ g) .: e
by FUNCT_1:def 12;
:: thesis: verum
end;
for
g being
Element of
G holds
e = ((the_extension_of_left_operation_of n,LO) ^ g) . e
proof
let g be
Element of
G;
:: thesis: e = ((the_extension_of_left_operation_of n,LO) ^ g) . e
(the_extension_of_left_operation_of n,LO) . g = the_extension_of_left_translation_of n,
g,
LO
by A4, Def5;
then
((the_extension_of_left_operation_of n,LO) ^ g) . e = (LO ^ g) .: e
by A4, Def4;
then consider Y being
Element of
the_subsets_of_card n,
E such that A31:
[Y,((LO ^ g) .: Y)] = [e,(((the_extension_of_left_operation_of n,LO) ^ g) . e)]
;
(
Y = e &
(LO ^ g) .: Y = ((the_extension_of_left_operation_of n,LO) ^ g) . e )
by A31, ZFMISC_1:33;
hence
e = ((the_extension_of_left_operation_of n,LO) ^ g) . e
by A22;
:: thesis: verum
end; then A32:
e is_fixed_under the_extension_of_left_operation_of n,
LO
by Def12;
A33:
not
the_subsets_of_card n,
E is
empty
by A4, Th2;
z in { x where x is Element of the_subsets_of_card n,E : x is_fixed_under the_extension_of_left_operation_of n,LO }
by A32;
hence
z in the_fixed_points_of (the_extension_of_left_operation_of n,LO)
by A33, Def13;
:: thesis: verum end;
hence
the_fixed_points_of (the_extension_of_left_operation_of n,LO) = { [:the carrier of G,{t}:] where t is Element of T : verum }
by TARSKI:2; :: thesis: verum