Metamath Proof Explorer


Theorem gexdvds

Description: The only N that annihilate all the elements of the group are the multiples of the group exponent. (Contributed by Mario Carneiro, 24-Apr-2016)

Ref Expression
Hypotheses gexcl.1 X = Base G
gexcl.2 E = gEx G
gexid.3 · ˙ = G
gexid.4 0 ˙ = 0 G
Assertion gexdvds G Grp N E N x X N · ˙ x = 0 ˙

Proof

Step Hyp Ref Expression
1 gexcl.1 X = Base G
2 gexcl.2 E = gEx G
3 gexid.3 · ˙ = G
4 gexid.4 0 ˙ = 0 G
5 1 2 3 4 gexdvdsi G Grp x X E N N · ˙ x = 0 ˙
6 5 3expia G Grp x X E N N · ˙ x = 0 ˙
7 6 ralrimdva G Grp E N x X N · ˙ x = 0 ˙
8 7 adantr G Grp N E N x X N · ˙ x = 0 ˙
9 noel ¬ N
10 simprr G Grp N E = 0 y | x X y · ˙ x = 0 ˙ = y | x X y · ˙ x = 0 ˙ =
11 10 eleq2d G Grp N E = 0 y | x X y · ˙ x = 0 ˙ = N y | x X y · ˙ x = 0 ˙ N
12 oveq1 y = N y · ˙ x = N · ˙ x
13 12 eqeq1d y = N y · ˙ x = 0 ˙ N · ˙ x = 0 ˙
14 13 ralbidv y = N x X y · ˙ x = 0 ˙ x X N · ˙ x = 0 ˙
15 14 elrab N y | x X y · ˙ x = 0 ˙ N x X N · ˙ x = 0 ˙
16 11 15 bitr3di G Grp N E = 0 y | x X y · ˙ x = 0 ˙ = N N x X N · ˙ x = 0 ˙
17 16 rbaibd G Grp N E = 0 y | x X y · ˙ x = 0 ˙ = x X N · ˙ x = 0 ˙ N N
18 9 17 mtbii G Grp N E = 0 y | x X y · ˙ x = 0 ˙ = x X N · ˙ x = 0 ˙ ¬ N
19 18 ex G Grp N E = 0 y | x X y · ˙ x = 0 ˙ = x X N · ˙ x = 0 ˙ ¬ N
20 nn0abscl N N 0
21 20 ad2antlr G Grp N E = 0 y | x X y · ˙ x = 0 ˙ = N 0
22 elnn0 N 0 N N = 0
23 21 22 sylib G Grp N E = 0 y | x X y · ˙ x = 0 ˙ = N N = 0
24 23 ord G Grp N E = 0 y | x X y · ˙ x = 0 ˙ = ¬ N N = 0
25 19 24 syld G Grp N E = 0 y | x X y · ˙ x = 0 ˙ = x X N · ˙ x = 0 ˙ N = 0
26 simpr G Grp N x X N = N N = N
27 26 oveq1d G Grp N x X N = N N · ˙ x = N · ˙ x
28 27 eqeq1d G Grp N x X N = N N · ˙ x = 0 ˙ N · ˙ x = 0 ˙
29 oveq1 N = N N · ˙ x = -N · ˙ x
30 29 eqeq1d N = N N · ˙ x = 0 ˙ -N · ˙ x = 0 ˙
31 eqid inv g G = inv g G
32 1 3 31 mulgneg G Grp N x X -N · ˙ x = inv g G N · ˙ x
33 32 3expa G Grp N x X -N · ˙ x = inv g G N · ˙ x
34 4 31 grpinvid G Grp inv g G 0 ˙ = 0 ˙
35 34 ad2antrr G Grp N x X inv g G 0 ˙ = 0 ˙
36 35 eqcomd G Grp N x X 0 ˙ = inv g G 0 ˙
37 33 36 eqeq12d G Grp N x X -N · ˙ x = 0 ˙ inv g G N · ˙ x = inv g G 0 ˙
38 simpll G Grp N x X G Grp
39 1 3 mulgcl G Grp N x X N · ˙ x X
40 39 3expa G Grp N x X N · ˙ x X
41 1 4 grpidcl G Grp 0 ˙ X
42 41 ad2antrr G Grp N x X 0 ˙ X
43 1 31 38 40 42 grpinv11 G Grp N x X inv g G N · ˙ x = inv g G 0 ˙ N · ˙ x = 0 ˙
44 37 43 bitrd G Grp N x X -N · ˙ x = 0 ˙ N · ˙ x = 0 ˙
45 30 44 sylan9bbr G Grp N x X N = N N · ˙ x = 0 ˙ N · ˙ x = 0 ˙
46 zre N N
47 46 ad2antlr G Grp N x X N
48 47 absord G Grp N x X N = N N = N
49 28 45 48 mpjaodan G Grp N x X N · ˙ x = 0 ˙ N · ˙ x = 0 ˙
50 49 ralbidva G Grp N x X N · ˙ x = 0 ˙ x X N · ˙ x = 0 ˙
51 50 adantr G Grp N E = 0 y | x X y · ˙ x = 0 ˙ = x X N · ˙ x = 0 ˙ x X N · ˙ x = 0 ˙
52 0dvds N 0 N N = 0
53 52 ad2antlr G Grp N E = 0 y | x X y · ˙ x = 0 ˙ = 0 N N = 0
54 simprl G Grp N E = 0 y | x X y · ˙ x = 0 ˙ = E = 0
55 54 breq1d G Grp N E = 0 y | x X y · ˙ x = 0 ˙ = E N 0 N
56 zcn N N
57 56 ad2antlr G Grp N E = 0 y | x X y · ˙ x = 0 ˙ = N
58 57 abs00ad G Grp N E = 0 y | x X y · ˙ x = 0 ˙ = N = 0 N = 0
59 53 55 58 3bitr4rd G Grp N E = 0 y | x X y · ˙ x = 0 ˙ = N = 0 E N
60 25 51 59 3imtr3d G Grp N E = 0 y | x X y · ˙ x = 0 ˙ = x X N · ˙ x = 0 ˙ E N
61 elrabi E y | x X y · ˙ x = 0 ˙ E
62 46 adantl G Grp N N
63 nnrp E E +
64 modval N E + N mod E = N E N E
65 62 63 64 syl2an G Grp N E N mod E = N E N E
66 65 adantr G Grp N E x X N · ˙ x = 0 ˙ N mod E = N E N E
67 66 oveq1d G Grp N E x X N · ˙ x = 0 ˙ N mod E · ˙ x = N E N E · ˙ x
68 simplll G Grp N E x X N · ˙ x = 0 ˙ G Grp
69 simpllr G Grp N E x X N · ˙ x = 0 ˙ N
70 nnz E E
71 70 ad2antlr G Grp N E x X N · ˙ x = 0 ˙ E
72 rerpdivcl N E + N E
73 62 63 72 syl2an G Grp N E N E
74 73 flcld G Grp N E N E
75 74 adantr G Grp N E x X N · ˙ x = 0 ˙ N E
76 71 75 zmulcld G Grp N E x X N · ˙ x = 0 ˙ E N E
77 simprl G Grp N E x X N · ˙ x = 0 ˙ x X
78 eqid - G = - G
79 1 3 78 mulgsubdir G Grp N E N E x X N E N E · ˙ x = N · ˙ x - G E N E · ˙ x
80 68 69 76 77 79 syl13anc G Grp N E x X N · ˙ x = 0 ˙ N E N E · ˙ x = N · ˙ x - G E N E · ˙ x
81 simprr G Grp N E x X N · ˙ x = 0 ˙ N · ˙ x = 0 ˙
82 dvdsmul1 E N E E E N E
83 71 75 82 syl2anc G Grp N E x X N · ˙ x = 0 ˙ E E N E
84 1 2 3 4 gexdvdsi G Grp x X E E N E E N E · ˙ x = 0 ˙
85 68 77 83 84 syl3anc G Grp N E x X N · ˙ x = 0 ˙ E N E · ˙ x = 0 ˙
86 81 85 oveq12d G Grp N E x X N · ˙ x = 0 ˙ N · ˙ x - G E N E · ˙ x = 0 ˙ - G 0 ˙
87 simpll G Grp N E G Grp
88 1 4 78 grpsubid G Grp 0 ˙ X 0 ˙ - G 0 ˙ = 0 ˙
89 87 41 88 syl2anc2 G Grp N E 0 ˙ - G 0 ˙ = 0 ˙
90 89 adantr G Grp N E x X N · ˙ x = 0 ˙ 0 ˙ - G 0 ˙ = 0 ˙
91 86 90 eqtrd G Grp N E x X N · ˙ x = 0 ˙ N · ˙ x - G E N E · ˙ x = 0 ˙
92 67 80 91 3eqtrd G Grp N E x X N · ˙ x = 0 ˙ N mod E · ˙ x = 0 ˙
93 92 expr G Grp N E x X N · ˙ x = 0 ˙ N mod E · ˙ x = 0 ˙
94 93 ralimdva G Grp N E x X N · ˙ x = 0 ˙ x X N mod E · ˙ x = 0 ˙
95 modlt N E + N mod E < E
96 62 63 95 syl2an G Grp N E N mod E < E
97 zmodcl N E N mod E 0
98 97 adantll G Grp N E N mod E 0
99 98 nn0red G Grp N E N mod E
100 nnre E E
101 100 adantl G Grp N E E
102 99 101 ltnled G Grp N E N mod E < E ¬ E N mod E
103 96 102 mpbid G Grp N E ¬ E N mod E
104 1 2 3 4 gexlem2 G Grp N mod E x X N mod E · ˙ x = 0 ˙ E 1 N mod E
105 elfzle2 E 1 N mod E E N mod E
106 104 105 syl G Grp N mod E x X N mod E · ˙ x = 0 ˙ E N mod E
107 106 3expia G Grp N mod E x X N mod E · ˙ x = 0 ˙ E N mod E
108 107 impancom G Grp x X N mod E · ˙ x = 0 ˙ N mod E E N mod E
109 108 con3d G Grp x X N mod E · ˙ x = 0 ˙ ¬ E N mod E ¬ N mod E
110 109 ex G Grp x X N mod E · ˙ x = 0 ˙ ¬ E N mod E ¬ N mod E
111 110 ad2antrr G Grp N E x X N mod E · ˙ x = 0 ˙ ¬ E N mod E ¬ N mod E
112 103 111 mpid G Grp N E x X N mod E · ˙ x = 0 ˙ ¬ N mod E
113 elnn0 N mod E 0 N mod E N mod E = 0
114 98 113 sylib G Grp N E N mod E N mod E = 0
115 114 ord G Grp N E ¬ N mod E N mod E = 0
116 94 112 115 3syld G Grp N E x X N · ˙ x = 0 ˙ N mod E = 0
117 simpr G Grp N E E
118 simplr G Grp N E N
119 dvdsval3 E N E N N mod E = 0
120 117 118 119 syl2anc G Grp N E E N N mod E = 0
121 116 120 sylibrd G Grp N E x X N · ˙ x = 0 ˙ E N
122 61 121 sylan2 G Grp N E y | x X y · ˙ x = 0 ˙ x X N · ˙ x = 0 ˙ E N
123 eqid y | x X y · ˙ x = 0 ˙ = y | x X y · ˙ x = 0 ˙
124 1 3 4 2 123 gexlem1 G Grp E = 0 y | x X y · ˙ x = 0 ˙ = E y | x X y · ˙ x = 0 ˙
125 124 adantr G Grp N E = 0 y | x X y · ˙ x = 0 ˙ = E y | x X y · ˙ x = 0 ˙
126 60 122 125 mpjaodan G Grp N x X N · ˙ x = 0 ˙ E N
127 8 126 impbid G Grp N E N x X N · ˙ x = 0 ˙