let g1 be Element of INT.Group; :: thesis: for a2 being Element of (INT.Group 2) st a2 = 1 holds
for x, y being Element of (Dihedral_group +infty) st x = <*g1,(1_ (INT.Group 2))*> & y = <*(1_ INT.Group),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 +infty) st x = <*g1,(1_ (INT.Group 2))*> & y = <*(1_ INT.Group),a2*> holds
y * x = (x ") * y )
assume A1: a2 = 1 ; :: thesis: for x, y being Element of (Dihedral_group +infty) st x = <*g1,(1_ (INT.Group 2))*> & y = <*(1_ INT.Group),a2*> holds
y * x = (x ") * y
let x, y be Element of (Dihedral_group +infty); :: thesis: ( x = <*g1,(1_ (INT.Group 2))*> & y = <*(1_ INT.Group),a2*> implies y * x = (x ") * y )
set a1 = 1_ (INT.Group 2);
set g2 = 1_ INT.Group;
assume A2: x = <*g1,(1_ (INT.Group 2))*> ; :: thesis: ( not y = <*(1_ INT.Group),a2*> or y * x = (x ") * y )
assume A3: y = <*(1_ INT.Group),a2*> ; :: thesis: y * x = (x ") * y
reconsider phi1 = (inversions INT.Group) . (1_ (INT.Group 2)), phi2 = (inversions INT.Group) . a2 as Homomorphism of INT.Group,INT.Group by AUTGROUP:def 1;
A4: phi2 = inverse_op INT.Group by A1, DefInversions;
x " = <*(g1 "),(1_ (INT.Group 2))*> by A2, Th24;
then A5: (x ") * y = <*((g1 ") * (phi1 . (1_ INT.Group))),((1_ (INT.Group 2)) * a2)*> by A3, Th14
.= <*((g1 ") * (1_ INT.Group)),((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) * (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