let G be Group; for E being non empty set
for x, y being Element of E
for T being LeftOperation of G,E holds
( the_orbit_of (x,T) misses the_orbit_of (y,T) or the_orbit_of (x,T) = the_orbit_of (y,T) )
let E be non empty set ; for x, y being Element of E
for T being LeftOperation of G,E holds
( the_orbit_of (x,T) misses the_orbit_of (y,T) or the_orbit_of (x,T) = the_orbit_of (y,T) )
let x, y be Element of E; for T being LeftOperation of G,E holds
( the_orbit_of (x,T) misses the_orbit_of (y,T) or the_orbit_of (x,T) = the_orbit_of (y,T) )
let T be LeftOperation of G,E; ( the_orbit_of (x,T) misses the_orbit_of (y,T) or the_orbit_of (x,T) = the_orbit_of (y,T) )
assume
not the_orbit_of (x,T) misses the_orbit_of (y,T)
; the_orbit_of (x,T) = the_orbit_of (y,T)
then
(the_orbit_of (x,T)) /\ (the_orbit_of (y,T)) <> {}
by XBOOLE_0:def 7;
then consider z1 being object such that
A1:
z1 in (the_orbit_of (x,T)) /\ (the_orbit_of (y,T))
by XBOOLE_0:def 1;
z1 in the_orbit_of (y,T)
by A1, XBOOLE_0:def 4;
then consider z199 being Element of E such that
A2:
z1 = z199
and
A3:
y,z199 are_conjugated_under T
;
z1 in the_orbit_of (x,T)
by A1, XBOOLE_0:def 4;
then consider z19 being Element of E such that
A4:
z1 = z19
and
A5:
x,z19 are_conjugated_under T
;
now for z2 being object holds
( ( z2 in the_orbit_of (x,T) implies z2 in the_orbit_of (y,T) ) & ( z2 in the_orbit_of (y,T) implies z2 in the_orbit_of (x,T) ) )let z2 be
object ;
( ( z2 in the_orbit_of (x,T) implies z2 in the_orbit_of (y,T) ) & ( z2 in the_orbit_of (y,T) implies z2 in the_orbit_of (x,T) ) )hereby ( z2 in the_orbit_of (y,T) implies z2 in the_orbit_of (x,T) )
assume
z2 in the_orbit_of (
x,
T)
;
z2 in the_orbit_of (y,T)then consider z29 being
Element of
E such that A6:
z2 = z29
and A7:
x,
z29 are_conjugated_under T
;
z29,
x are_conjugated_under T
by A7, Th4;
then
z29,
z199 are_conjugated_under T
by A4, A5, A2, Th5;
then
z199,
z29 are_conjugated_under T
by Th4;
then
y,
z29 are_conjugated_under T
by A3, Th5;
hence
z2 in the_orbit_of (
y,
T)
by A6;
verum
end; assume
z2 in the_orbit_of (
y,
T)
;
z2 in the_orbit_of (x,T)then consider z29 being
Element of
E such that A8:
z2 = z29
and A9:
y,
z29 are_conjugated_under T
;
z29,
y are_conjugated_under T
by A9, Th4;
then
z29,
z19 are_conjugated_under T
by A4, A2, A3, Th5;
then
z19,
z29 are_conjugated_under T
by Th4;
then
x,
z29 are_conjugated_under T
by A5, Th5;
hence
z2 in the_orbit_of (
x,
T)
by A8;
verum end;
hence
the_orbit_of (x,T) = the_orbit_of (y,T)
by TARSKI:2; verum