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

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

A2:
for c being Element of G holds (Conjugate (a * b)) . c = (Conjugate b) . (c |^ a)
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;c |^ (a * b) = (c |^ a) |^ b by GROUP_3:24;

hence (Conjugate (a * b)) . c = (c |^ a) |^ b by Def6; :: thesis: verum

proof

A3:
for c being Element of G holds (Conjugate (a * b)) . c = (Conjugate b) . ((Conjugate a) . c)
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;(c |^ a) |^ b = (Conjugate b) . (c |^ a) by Def6;

hence (Conjugate (a * b)) . c = (Conjugate b) . (c |^ a) by A1; :: thesis: verum

proof

for c being Element of G holds (Conjugate (a * b)) . c = ((Conjugate b) * (Conjugate a)) . c
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;(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

proof

hence
Conjugate (a * b) = (Conjugate b) * (Conjugate a)
; :: thesis: verum
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;(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