let G be strict Group; :: thesis: for a, b being Element of G holds Conjugate (a * b) = (Conjugate b) * (Conjugate a)
let a, b be Element of G; :: thesis: Conjugate (a * b) = (Conjugate b) * (Conjugate a)
set f1 = Conjugate (a * b);
set f2 = (Conjugate b) * (Conjugate a);
A1: for c being Element of G holds (Conjugate (a * b)) . c = (c |^ a) |^ b
proof
let c be Element of G; :: thesis: (Conjugate (a * b)) . c = (c |^ a) |^ b
c |^ (a * b) = (c |^ a) |^ b by GROUP_3:24;
hence (Conjugate (a * b)) . c = (c |^ a) |^ b by Def6; :: thesis: verum
end;
A2: for c being Element of G holds (Conjugate (a * b)) . c = (Conjugate b) . (c |^ a)
proof
let c be Element of G; :: thesis: (Conjugate (a * b)) . c = (Conjugate b) . (c |^ a)
(c |^ a) |^ b = (Conjugate b) . (c |^ a) by Def6;
hence (Conjugate (a * b)) . c = (Conjugate b) . (c |^ a) by A1; :: thesis: verum
end;
A3: for c being Element of G holds (Conjugate (a * b)) . c = (Conjugate b) . ((Conjugate a) . c)
proof
let c be Element of G; :: thesis: (Conjugate (a * b)) . c = (Conjugate b) . ((Conjugate a) . c)
(Conjugate b) . (c |^ a) = (Conjugate b) . ((Conjugate a) . c) by Def6;
hence (Conjugate (a * b)) . c = (Conjugate b) . ((Conjugate a) . c) by A2; :: thesis: verum
end;
for c being Element of G holds (Conjugate (a * b)) . c = ((Conjugate b) * (Conjugate a)) . c
proof
let c be Element of G; :: thesis: (Conjugate (a * b)) . c = ((Conjugate b) * (Conjugate a)) . c
(Conjugate b) . ((Conjugate a) . c) = ((Conjugate b) * (Conjugate a)) . c by FUNCT_2:15;
hence (Conjugate (a * b)) . c = ((Conjugate b) * (Conjugate a)) . c by A3; :: thesis: verum
end;
hence Conjugate (a * b) = (Conjugate b) * (Conjugate a) ; :: thesis: verum