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 = Base G
gexcl2.2 ⊢ E = gEx ⁡ G
Assertion gex1 ⊢ G ∈ Mnd → E = 1 ↔ X ≈ 1 𝑜

Proof

Step Hyp Ref Expression
1 gexcl2.1 ⊢ X = Base G
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 ⋅ G x = 1 ⋅ G x
5 eqid ⊢ ⋅ G = ⋅ G
6 eqid ⊢ 0 G = 0 G
7 1 2 5 6 gexid ⊢ x ∈ X → E ⋅ G x = 0 G
8 7 adantl ⊢ G ∈ Mnd ∧ E = 1 ∧ x ∈ X → E ⋅ G x = 0 G
9 1 5 mulg1 ⊢ x ∈ X → 1 ⋅ G x = x
10 9 adantl ⊢ G ∈ Mnd ∧ E = 1 ∧ x ∈ X → 1 ⋅ G x = x
11 4 8 10 3eqtr3rd ⊢ G ∈ Mnd ∧ E = 1 ∧ x ∈ X → x = 0 G
12 velsn ⊢ x ∈ 0 G ↔ x = 0 G
13 11 12 sylibr ⊢ G ∈ Mnd ∧ E = 1 ∧ x ∈ X → x ∈ 0 G
14 13 ex ⊢ G ∈ Mnd ∧ E = 1 → x ∈ X → x ∈ 0 G
15 14 ssrdv ⊢ G ∈ Mnd ∧ E = 1 → X ⊆ 0 G
16 1 6 mndidcl ⊢ G ∈ Mnd → 0 G ∈ X
17 16 adantr ⊢ G ∈ Mnd ∧ E = 1 → 0 G ∈ X
18 17 snssd ⊢ G ∈ Mnd ∧ E = 1 → 0 G ⊆ X
19 15 18 eqssd ⊢ G ∈ Mnd ∧ E = 1 → X = 0 G
20 fvex ⊢ 0 G ∈ V
21 20 ensn1 ⊢ 0 G ≈ 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 ⋅ G x = x
27 en1eqsn ⊢ 0 G ∈ X ∧ X ≈ 1 𝑜 → X = 0 G
28 16 27 sylan ⊢ G ∈ Mnd ∧ X ≈ 1 𝑜 → X = 0 G
29 28 eleq2d ⊢ G ∈ Mnd ∧ X ≈ 1 𝑜 → x ∈ X ↔ x ∈ 0 G
30 29 biimpa ⊢ G ∈ Mnd ∧ X ≈ 1 𝑜 ∧ x ∈ X → x ∈ 0 G
31 30 12 sylib ⊢ G ∈ Mnd ∧ X ≈ 1 𝑜 ∧ x ∈ X → x = 0 G
32 26 31 eqtrd ⊢ G ∈ Mnd ∧ X ≈ 1 𝑜 ∧ x ∈ X → 1 ⋅ G x = 0 G
33 32 ralrimiva ⊢ G ∈ Mnd ∧ X ≈ 1 𝑜 → ∀ x ∈ X 1 ⋅ G x = 0 G
34 1 2 5 6 gexlem2 ⊢ G ∈ Mnd ∧ 1 ∈ ℕ ∧ ∀ x ∈ X 1 ⋅ G x = 0 G → 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 𝑜