Metamath Proof Explorer

Theorem gex1

Description: A group or monoid has exponent 1 iff it is trivial. (Contributed by Mario Carneiro, 24-Apr-2016)

Ref Expression
Hypotheses gexcl2.1 ⊢X=BaseG
gexcl2.2 ⊢E=gEx⁡G
Assertion gex1 ⊢G∈Mnd→E=1↔X≈1𝑜

Proof

Step Hyp Ref Expression
1 gexcl2.1 ⊢X=BaseG
2 gexcl2.2 ⊢E=gEx⁡G
3 simplr ⊢G∈Mnd∧E=1∧x∈X→E=1
4 3 oveq1d ⊢G∈Mnd∧E=1∧x∈X→E⋅Gx=1⋅Gx
5 eqid ⊢⋅G=⋅G
6 eqid ⊢0G=0G
7 1 2 5 6 gexid ⊢x∈X→E⋅Gx=0G
8 7 adantl ⊢G∈Mnd∧E=1∧x∈X→E⋅Gx=0G
9 1 5 mulg1 ⊢x∈X→1⋅Gx=x
10 9 adantl ⊢G∈Mnd∧E=1∧x∈X→1⋅Gx=x
11 4 8 10 3eqtr3rd ⊢G∈Mnd∧E=1∧x∈X→x=0G
12 velsn ⊢x∈0G↔x=0G
13 11 12 sylibr ⊢G∈Mnd∧E=1∧x∈X→x∈0G
14 13 ex ⊢G∈Mnd∧E=1→x∈X→x∈0G
15 14 ssrdv ⊢G∈Mnd∧E=1→X⊆0G
16 1 6 mndidcl ⊢G∈Mnd→0G∈X
17 16 adantr ⊢G∈Mnd∧E=1→0G∈X
18 17 snssd ⊢G∈Mnd∧E=1→0G⊆X
19 15 18 eqssd ⊢G∈Mnd∧E=1→X=0G
20 fvex ⊢0G∈V
21 20 ensn1 ⊢0G≈1𝑜
22 19 21 eqbrtrdi ⊢G∈Mnd∧E=1→X≈1𝑜
23 simpl ⊢G∈Mnd∧X≈1𝑜→G∈Mnd
24 1nn ⊢1∈ℕ
25 24 a1i ⊢G∈Mnd∧X≈1𝑜→1∈ℕ
26 9 adantl ⊢G∈Mnd∧X≈1𝑜∧x∈X→1⋅Gx=x
27 en1eqsn ⊢0G∈X∧X≈1𝑜→X=0G
28 16 27 sylan ⊢G∈Mnd∧X≈1𝑜→X=0G
29 28 eleq2d ⊢G∈Mnd∧X≈1𝑜→x∈X↔x∈0G
30 29 biimpa ⊢G∈Mnd∧X≈1𝑜∧x∈X→x∈0G
31 30 12 sylib ⊢G∈Mnd∧X≈1𝑜∧x∈X→x=0G
32 26 31 eqtrd ⊢G∈Mnd∧X≈1𝑜∧x∈X→1⋅Gx=0G
33 32 ralrimiva ⊢G∈Mnd∧X≈1𝑜→∀x∈X1⋅Gx=0G
34 1 2 5 6 gexlem2 ⊢G∈Mnd∧1∈ℕ∧∀x∈X1⋅Gx=0G→E∈1…1
35 23 25 33 34 syl3anc ⊢G∈Mnd∧X≈1𝑜→E∈1…1
36 elfz1eq ⊢E∈1…1→E=1
37 35 36 syl ⊢G∈Mnd∧X≈1𝑜→E=1
38 22 37 impbida ⊢G∈Mnd→E=1↔X≈1𝑜