let n be odd Nat; :: thesis: ( n > 1 implies center (Dihedral_group n) is trivial )
assume A1: n > 1 ; :: thesis: center (Dihedral_group n) is trivial
for z being Element of (Dihedral_group n) holds
( z = 1_ (Dihedral_group n) iff z in center (Dihedral_group n) )
proof
let z be Element of (Dihedral_group n); :: thesis: ( z = 1_ (Dihedral_group n) iff z in center (Dihedral_group n) )
thus ( z = 1_ (Dihedral_group n) implies z in center (Dihedral_group n) ) by GROUP_2:46; :: thesis: ( z in center (Dihedral_group n) implies z = 1_ (Dihedral_group n) )
assume A2: z in center (Dihedral_group n) ; :: thesis: z = 1_ (Dihedral_group n)
1 in Segm n by A1, NAT_1:44;
then 1 in the carrier of (INT.Group n) by Th76;
then reconsider g1 = 1 as Element of (INT.Group n) ;
1 in INT.Group 2 by EltsOfINTGroup2;
then reconsider a2 = 1 as Element of (INT.Group 2) ;
reconsider x = <*g1,(1_ (INT.Group 2))*>, y = <*(1_ (INT.Group n)),a2*> as Element of (Dihedral_group n) by Th9;
consider j being Nat such that
A4: ( z = (x |^ j) * y or z = x |^ j ) by Th107;
A6: n > 2
proof
n mod 2 = 1 by NAT_2:22;
then consider n0 being Nat such that
B1: ( n = (2 * n0) + 1 & 1 < 2 ) by NAT_D:def 2;
1 < (2 * n0) + 1 by A1, B1;
then 0 + 1 < (2 * n0) + 1 ;
then 0 < n0 ;
then 1 <= n0 by NAT_1:25;
then 2 * 1 <= 2 * n0 by XREAL_1:64;
then 2 + 1 <= (2 * n0) + 1 by XREAL_1:6;
then ( 3 <= n & 2 < 3 ) by B1;
hence n > 2 by XXREAL_0:2; :: thesis: verum
end;
per cases ( z = (x |^ j) * y or z = x |^ j ) by A4;
suppose A7: z = (x |^ j) * y ; :: thesis: z = 1_ (Dihedral_group n)
(x |^ 1) * z <> z * (x |^ 1)
proof
assume B1: (x |^ 1) * z = z * (x |^ 1) ; :: thesis: contradiction
B2: x |^ 2 = 1_ (Dihedral_group n)
proof
B3: z * (x |^ 1) = (x |^ ((n + j) - 1)) * y by A7, Th109;
(x |^ 1) * z = (x |^ 1) * ((x |^ j) * y) by A7
.= ((x |^ 1) * (x |^ j)) * y by GROUP_1:def 3
.= (x |^ (1 + j)) * y by GROUP_1:33 ;
then (x |^ ((n + j) - 1)) * y = (x |^ (1 + j)) * y by B1, B3;
then B4: x |^ ((n + j) - 1) = x |^ (1 + j) by GROUP_1:6;
x |^ ((n + j) - 1) = x |^ (n + (j - 1))
.= (x |^ n) * (x |^ (j - 1)) by GROUP_1:33
.= (1_ (Dihedral_group n)) * (x |^ (j - 1)) by Th101
.= x |^ (j - 1) by GROUP_1:def 4
.= x |^ (j + (- 1))
.= (x |^ j) * (x |^ (- 1)) by GROUP_1:33 ;
then (x |^ j) * (x |^ (- 1)) = x |^ (1 + j) by B4
.= (x |^ j) * (x |^ 1) by GROUP_1:33 ;
then x |^ (- 1) = x |^ 1 by GROUP_1:6
.= x by GROUP_1:26 ;
then x " = x by GROUP_1:32;
hence x |^ 2 = 1_ (Dihedral_group n) by GROUP_1:29; :: thesis: verum
end;
( n > 2 & a2 = 1 ) by A6;
then x |^ 2 <> 1_ (Dihedral_group n) by Th102;
hence contradiction by B2; :: thesis: verum
end;
hence z = 1_ (Dihedral_group n) by A2, GROUP_5:77; :: thesis: verum
end;
suppose A8: z = x |^ j ; :: thesis: z = 1_ (Dihedral_group n)
set k1 = j div n;
A9: ( j = (n * (j div n)) + (j mod n) & j mod n < n ) by NAT_D:1, NAT_D:2;
reconsider j1 = j mod n as Nat ;
A10: z = x |^ j by A8
.= x |^ ((n * (j div n)) + (j mod n)) by A9
.= (x |^ (n * (j div n))) * (x |^ (j mod n)) by GROUP_1:33
.= ((x |^ n) |^ (j div n)) * (x |^ (j mod n)) by GROUP_1:35
.= ((1_ (Dihedral_group n)) |^ (j div n)) * (x |^ (j mod n)) by Th101
.= (1_ (Dihedral_group n)) * (x |^ (j mod n)) by GROUP_1:31
.= x |^ j1 by GROUP_1:def 4 ;
A11: x |^ j1 = x |^ (n - j1)
proof
B1: y * z = y * (x |^ j1) by A10
.= (x |^ (n - j1)) * y by Th106 ;
(x |^ j1) * y = z * y by A10
.= y * z by A2, GROUP_5:77
.= (x |^ (n - j1)) * y by B1 ;
hence x |^ j1 = x |^ (n - j1) by GROUP_1:6; :: thesis: verum
end;
end;
end;
end;
hence center (Dihedral_group n) is trivial by Th78; :: thesis: verum