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 |^ (n - 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 |^ (n - 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 |^ (n - 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 |^ (n - 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 |^ (n - 1)) * y )
assume A2: x = <*g1,(1_ (INT.Group 2))*> ; :: thesis: ( not y = <*(1_ (INT.Group n)),a2*> or y * x = (x |^ (n - 1)) * y )
assume A3: y = <*(1_ (INT.Group n)),a2*> ; :: thesis: y * x = (x |^ (n - 1)) * y
A5: x " = <*(g1 "),(1_ (INT.Group 2))*> by A2, Th24
.= <*(g1 |^ (n - 1)),(1_ (INT.Group 2))*> by Th86
.= x |^ (n - 1) by A2, Th25 ;
thus y * x = (x ") * y by A1, A2, A3, Th99
.= (x |^ (n - 1)) * y by A5 ; :: thesis: verum