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 ") * 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 ") * 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 ") * 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 ") * 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 ") * y )
set a1 = 1_ (INT.Group 2);
set g2 = 1_ (INT.Group n);
assume A2: x = <*g1,(1_ (INT.Group 2))*> ; :: thesis: ( not y = <*(1_ (INT.Group n)),a2*> or y * x = (x ") * y )
assume A3: y = <*(1_ (INT.Group n)),a2*> ; :: thesis: y * x = (x ") * y
reconsider phi1 = (inversions (INT.Group n)) . (1_ (INT.Group 2)), phi2 = (inversions (INT.Group n)) . a2 as Homomorphism of (INT.Group n),(INT.Group n) by AUTGROUP:def 1;
A4: phi2 = inverse_op (INT.Group n) by A1, DefInversions;
x " = <*(g1 "),(1_ (INT.Group 2))*> by A2, Th24;
then A5: (x ") * y = <*((g1 ") * (phi1 . (1_ (INT.Group n)))),((1_ (INT.Group 2)) * a2)*> by A3, Th14
.= <*((g1 ") * (1_ (INT.Group n))),((1_ (INT.Group 2)) * a2)*> by GROUP_6:31
.= <*(g1 "),((1_ (INT.Group 2)) * a2)*> by GROUP_1:def 4
.= <*(g1 "),a2*> by GROUP_1:def 4 ;
thus y * x = <*((1_ (INT.Group n)) * (phi2 . g1)),(a2 * (1_ (INT.Group 2)))*> by A2, A3, Th14
.= <*(phi2 . g1),(a2 * (1_ (INT.Group 2)))*> by GROUP_1:def 4
.= <*(phi2 . g1),a2*> by GROUP_1:def 4
.= <*(g1 "),a2*> by A4, GROUP_1:def 6
.= (x ") * y by A5 ; :: thesis: verum