let n be non zero Nat; :: thesis: for g1 being Element of (INT.Group n)
for a2 being Element of (INT.Group 2) st a2 = 1 holds
for x, y being Element of (Dihedral_group n) st x = <*g1,(1_ (INT.Group 2))*> & y = <*(1_ (INT.Group n)),a2*> holds
y * x = (x |^ (- 1)) * y
let g1 be Element of (INT.Group n); :: thesis: for a2 being Element of (INT.Group 2) st a2 = 1 holds
for x, y being Element of (Dihedral_group n) st x = <*g1,(1_ (INT.Group 2))*> & y = <*(1_ (INT.Group n)),a2*> holds
y * x = (x |^ (- 1)) * y
let a2 be Element of (INT.Group 2); :: thesis: ( a2 = 1 implies for x, y being Element of (Dihedral_group n) st x = <*g1,(1_ (INT.Group 2))*> & y = <*(1_ (INT.Group n)),a2*> holds
y * x = (x |^ (- 1)) * y )
assume A1: a2 = 1 ; :: thesis: for x, y being Element of (Dihedral_group n) st x = <*g1,(1_ (INT.Group 2))*> & y = <*(1_ (INT.Group n)),a2*> holds
y * x = (x |^ (- 1)) * y
let x, y be Element of (Dihedral_group n); :: thesis: ( x = <*g1,(1_ (INT.Group 2))*> & y = <*(1_ (INT.Group n)),a2*> implies y * x = (x |^ (- 1)) * y )
assume A2: x = <*g1,(1_ (INT.Group 2))*> ; :: thesis: ( not y = <*(1_ (INT.Group n)),a2*> or y * x = (x |^ (- 1)) * y )
assume A3: y = <*(1_ (INT.Group n)),a2*> ; :: thesis: y * x = (x |^ (- 1)) * y
x |^ (n - 1) = x " by A2, Th103;
then x |^ (n - 1) = x |^ (- 1) by GROUP_1:32;
hence y * x = (x |^ (- 1)) * y by A1, A2, A3, Th100; :: thesis: verum