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