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
for i, j being Nat holds ((x |^ i) * y) * (x |^ j) = (x |^ ((n + i) - j)) * 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
for i, j being Nat holds ((x |^ i) * y) * (x |^ j) = (x |^ ((n + i) - j)) * 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
for i, j being Nat holds ((x |^ i) * y) * (x |^ j) = (x |^ ((n + i) - j)) * 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
for i, j being Nat holds ((x |^ i) * y) * (x |^ j) = (x |^ ((n + i) - j)) * y
let x, y be Element of (Dihedral_group n); :: thesis: ( x = <*g1,(1_ (INT.Group 2))*> & y = <*(1_ (INT.Group n)),a2*> implies for i, j being Nat holds ((x |^ i) * y) * (x |^ j) = (x |^ ((n + i) - j)) * y )
assume A2: x = <*g1,(1_ (INT.Group 2))*> ; :: thesis: ( not y = <*(1_ (INT.Group n)),a2*> or for i, j being Nat holds ((x |^ i) * y) * (x |^ j) = (x |^ ((n + i) - j)) * y )
assume A3: y = <*(1_ (INT.Group n)),a2*> ; :: thesis: for i, j being Nat holds ((x |^ i) * y) * (x |^ j) = (x |^ ((n + i) - j)) * y
let i, j be Nat; :: thesis: ((x |^ i) * y) * (x |^ j) = (x |^ ((n + i) - j)) * y
thus ((x |^ i) * y) * (x |^ j) = (x |^ i) * (y * (x |^ j)) by GROUP_1:def 3
.= (x |^ i) * ((x |^ (n - j)) * y) by A1, A2, A3, Th106
.= ((x |^ i) * (x |^ (n - j))) * y by GROUP_1:def 3
.= (x |^ (i + (n - j))) * y by GROUP_1:33
.= (x |^ ((n + i) - j)) * y ; :: thesis: verum