let G be finite Group; for E, T being non empty set
for LO being LeftOperation of G,E
for n being Nat 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 ; for LO being LeftOperation of G,E
for n being Nat 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; for n being Nat 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 Nat; ( 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)
; ( 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 } )
set EE = the_subsets_of_card (n,E);
set LO9 = the_extension_of_left_operation_of (n,LO);
assume A2:
n = card G
; ( 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:]
; ( 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
; the_fixed_points_of (the_extension_of_left_operation_of (n,LO)) = { [: the carrier of G,{t}:] where t is Element of T : verum }
now for z being object holds
( ( z in the_fixed_points_of (the_extension_of_left_operation_of (n,LO)) implies z in { [: the carrier of G,{t9}:] where t9 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)) ) )let z be
object ;
( ( z in the_fixed_points_of (the_extension_of_left_operation_of (n,LO)) implies z in { [: the carrier of G,{t9}:] where t9 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)) ) )reconsider zz =
z as
set by TARSKI:1;
hereby ( 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))
;
z in { [: the carrier of G,{t9}:] where t9 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
and A6:
e is_fixed_under the_extension_of_left_operation_of (
n,
LO)
;
not
the_subsets_of_card (
n,
E) is
empty
by A4, Th1;
then
z in the_subsets_of_card (
n,
E)
by A5;
then consider X being
Subset of
E such that A7:
z = X
and A8:
card X = n
;
A9:
for
g being
Element of
G holds
e = (the_left_translation_of (g,T)) .: e
proof
let g be
Element of
G;
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 A10:
((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 A6;
hence
e = (the_left_translation_of (g,T)) .: e
by A1, A10, Def7;
verum
end;
ex
t being
Element of
T st
[: the carrier of G,{t}:] c= zz
proof
not
X is
empty
by A2, A8;
then consider x1 being
object such that A11:
x1 in X
by XBOOLE_0:def 1;
consider g1,
t being
object such that A12:
g1 in the
carrier of
G
and A13:
t in T
and A14:
x1 = [g1,t]
by A3, A11, ZFMISC_1:def 2;
reconsider t =
t as
Element of
T by A13;
reconsider g1 =
g1 as
Element of
G by A12;
take
t
;
[: the carrier of G,{t}:] c= zz
now for x2 being object st x2 in [: the carrier of G,{t}:] holds
x2 in zzreconsider z19 =
x1 as
Element of
[: the carrier of G,T:] by A3, A11;
let x2 be
object ;
( x2 in [: the carrier of G,{t}:] implies x2 in zz )assume
x2 in [: the carrier of G,{t}:]
;
x2 in zzthen consider g2,
t9 being
object such that A15:
g2 in the
carrier of
G
and A16:
(
t9 in {t} &
x2 = [g2,t9] )
by ZFMISC_1:def 2;
reconsider g2 =
g2 as
Element of
G by A15;
set g =
g2 * (g1 ");
consider z29 being
Element of
[: the carrier of G,T:],
g19,
g29 being
Element of
G,
t99 being
Element of
T such that A17:
z29 = (the_left_translation_of ((g2 * (g1 ")),T)) . z19
and A18:
g29 = (g2 * (g1 ")) * g19
and A19:
z19 = [g19,t99]
and A20:
z29 = [g29,t99]
by Def6;
A21:
t = t99
by A14, A19, XTUPLE_0:1;
dom (the_left_translation_of ((g2 * (g1 ")),T)) = E
by A3, FUNCT_2:def 1;
then A22:
(the_left_translation_of ((g2 * (g1 ")),T)) . x1 in (the_left_translation_of ((g2 * (g1 ")),T)) .: e
by A5, A7, A11, FUNCT_1:def 6;
g29 =
(g2 * (g1 ")) * g1
by A14, A18, A19, XTUPLE_0:1
.=
g2 * ((g1 ") * g1)
by GROUP_1:def 3
.=
g2 * (1_ G)
by GROUP_1:def 5
.=
g2
by GROUP_1:def 4
;
then
z29 = x2
by A16, A20, A21, TARSKI:def 1;
hence
x2 in zz
by A5, A9, A17, A22;
verum end;
hence
[: the carrier of G,{t}:] c= zz
;
verum
end; then consider t being
Element of
T such that A23:
[: the carrier of G,{t}:] c= zz
;
n,
X are_equipotent
by A8, CARD_1:def 2;
then consider f being
Function such that
f is
one-to-one
and A24:
dom f = n
and A25:
rng f = X
;
dom f in omega
by A24, ORDINAL1:def 12;
then reconsider X =
X as
finite set by A25, FINSET_1:def 1;
card [: the carrier of G,{t}:] = n
by A2, CARD_1:69;
then
[: the carrier of G,{t}:] = X
by A7, A8, A23, CARD_2:102;
hence
z in { [: the carrier of G,{t9}:] where t9 is Element of T : verum }
by A7;
verum
end; assume
z in { [: the carrier of G,{t}:] where t is Element of T : verum }
;
z in the_fixed_points_of (the_extension_of_left_operation_of (n,LO))then consider t being
Element of
T such that A26:
z = [: the carrier of G,{t}:]
;
then reconsider X =
z as
Subset of
E by A3, TARSKI:def 3;
card X = card the
carrier of
G
by A26, CARD_1:69;
then
z in the_subsets_of_card (
n,
E)
by A2;
then reconsider e =
z as
Element of
the_subsets_of_card (
n,
E) ;
A28:
zz c= [: the carrier of G,T:]
by A27;
A29:
for
g being
Element of
G holds
e = (LO ^ g) .: e
proof
let g be
Element of
G;
e = (LO ^ g) .: e
A30:
LO ^ g = the_left_translation_of (
g,
T)
by A1, Def7;
now for e2 being object holds
( ( e2 in e implies ex e1 being object st
( e1 in dom (LO ^ g) & e1 in e & e2 = (LO ^ g) . e1 ) ) & ( ex e1 being object st
( e1 in dom (LO ^ g) & e1 in e & e2 = (LO ^ g) . e1 ) implies e2 in e ) )let e2 be
object ;
( ( e2 in e implies ex e1 being object st
( e1 in dom (LO ^ g) & e1 in e & e2 = (LO ^ g) . e1 ) ) & ( ex e1 being object st
( e1 in dom (LO ^ g) & e1 in e & e2 = (LO ^ g) . e1 ) implies e2 in e ) )hereby ( ex e1 being object st
( e1 in dom (LO ^ g) & e1 in e & e2 = (LO ^ g) . e1 ) implies e2 in e )
assume
e2 in e
;
ex e1 being object st
( e1 in dom (LO ^ g) & e1 in e & e2 = (LO ^ g) . e1 )then consider g2,
t2 being
object such that A31:
g2 in the
carrier of
G
and A32:
t2 in {t}
and A33:
e2 = [g2,t2]
by A26, ZFMISC_1:def 2;
reconsider g2 =
g2 as
Element of
G by A31;
reconsider e1 =
[((g ") * g2),t2] as
object ;
take e1 =
e1;
( e1 in dom (LO ^ g) & e1 in e & e2 = (LO ^ g) . e1 )A34:
zz c= dom (LO ^ g)
by A3, A28, FUNCT_2:def 1;
e1 in e
by A26, A32, ZFMISC_1:def 2;
hence
(
e1 in dom (LO ^ g) &
e1 in e )
by A34;
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:],
g19,
g29 being
Element of
G,
t9 being
Element of
T such that A35:
z2 = (LO ^ g) . z1
and A36:
g29 = g * g19
and A37:
z1 = [g19,t9]
and A38:
z2 = [g29,t9]
by A30, Def6;
g29 =
g * ((g ") * g2)
by A36, A37, XTUPLE_0:1
.=
(g * (g ")) * g2
by GROUP_1:def 3
.=
(1_ G) * g2
by GROUP_1:def 5
.=
g2
by GROUP_1:def 4
;
hence
e2 = (LO ^ g) . e1
by A33, A35, A37, A38, XTUPLE_0:1;
verum
end; given e1 being
object such that A39:
e1 in dom (LO ^ g)
and A40:
e1 in e
and A41:
e2 = (LO ^ g) . e1
;
e2 in ereconsider z1 =
e1 as
Element of
[: the carrier of G,T:] by A3, A39;
consider z2 being
Element of
[: the carrier of G,T:],
g19,
g29 being
Element of
G,
t9 being
Element of
T such that A42:
z2 = (LO ^ g) . z1
and
g29 = g * g19
and A43:
z1 = [g19,t9]
and A44:
z2 = [g29,t9]
by A30, Def6;
A45:
t9 in {t9}
by TARSKI:def 1;
consider g1,
t1 being
object such that
g1 in the
carrier of
G
and A46:
t1 in {t}
and A47:
e1 = [g1,t1]
by A26, A40, ZFMISC_1:def 2;
t1 = t
by A46, TARSKI:def 1;
then
t9 = t
by A47, A43, XTUPLE_0:1;
hence
e2 in e
by A26, A41, A42, A44, A45, ZFMISC_1:def 2;
verum end;
hence
e = (LO ^ g) .: e
by FUNCT_1:def 6;
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;
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 A48:
[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 A48, XTUPLE_0:1;
hence
e = ((the_extension_of_left_operation_of (n,LO)) ^ g) . e
by A29;
verum
end; then
e is_fixed_under the_extension_of_left_operation_of (
n,
LO)
;
then A49:
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) }
;
not
the_subsets_of_card (
n,
E) is
empty
by A4, Th1;
hence
z in the_fixed_points_of (the_extension_of_left_operation_of (n,LO))
by A49, Def13;
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; verum