let G be addGroup; :: thesis: for a being Element of G
for A being Subset of G holds (con_class a) + A = A + (con_class a)
let a be Element of G; :: thesis: for A being Subset of G holds (con_class a) + A = A + (con_class a)
let A be Subset of G; :: thesis: (con_class a) + A = A + (con_class a)
thus (con_class a) + A c= A + (con_class a) :: according to XBOOLE_0:def 10 :: thesis: A + (con_class a) c= (con_class a) + A
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (con_class a) + A or x in A + (con_class a) )
assume x in (con_class a) + A ; :: thesis: x in A + (con_class a)
then consider b, c being Element of G such that
A1: x = b + c and
A2: b in con_class a and
A3: c in A ;
reconsider h = x as Element of G by A1;
b,a are_conjugated by A2, Th81;
then consider g being Element of G such that
A4: b = a * g ;
h * (- c) = c + (((a * g) + c) + (- c)) by A1, A4, RLVECT_1:def 3
.= c + (a * g) by Th1 ;
then A5: x = (c + (a * g)) * c by ThB25
.= (c * c) + ((a * g) * c) by Th23
.= c + ((a * g) * c) by Th20
.= c + (a * (g + c)) by Th24 ;
a * (g + c) in con_class a by Th80, Th74;
hence x in A + (con_class a) by A3, A5; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A + (con_class a) or x in (con_class a) + A )
assume x in A + (con_class a) ; :: thesis: x in (con_class a) + A
then consider b, c being Element of G such that
A6: x = b + c and
A7: b in A and
A8: c in con_class a ;
reconsider h = x as Element of G by A6;
c,a are_conjugated by A8, Th81;
then consider g being Element of G such that
A9: c = a * g ;
h * b = (a * g) + b by A6, A9, Th1;
then A10: x = ((a * g) + b) * (- b) by ThB25
.= ((a * g) * (- b)) + (b * (- b)) by Th23
.= (a * (g + (- b))) + (b * (- b)) by Th24
.= (a * (g + (- b))) + b by Th1 ;
a * (g + (- b)) in con_class a by Th80, Th74;
hence x in (con_class a) + A by A7, A10; :: thesis: verum