This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑋 = ( Base ‘ 𝐺 )
gexcl2.2 ⊢ 𝐸 = ( gEx ‘ 𝐺 )
Assertion gex1 ( 𝐺 ∈ Mnd → ( 𝐸 = 1 ↔ 𝑋 ≈ 1o ) )

Proof

Step Hyp Ref Expression
1 gexcl2.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 gexcl2.2 ⊢ 𝐸 = ( gEx ‘ 𝐺 )
3 simplr ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐸 = 1 ) ∧ 𝑥 ∈ 𝑋 ) → 𝐸 = 1 )
4 3 oveq1d ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐸 = 1 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝐸 ( .g ‘ 𝐺 ) 𝑥 ) = ( 1 ( .g ‘ 𝐺 ) 𝑥 ) )
5 eqid ⊢ ( .g ‘ 𝐺 ) = ( .g ‘ 𝐺 )
6 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
7 1 2 5 6 gexid ⊢ ( 𝑥 ∈ 𝑋 → ( 𝐸 ( .g ‘ 𝐺 ) 𝑥 ) = ( 0g ‘ 𝐺 ) )
8 7 adantl ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐸 = 1 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝐸 ( .g ‘ 𝐺 ) 𝑥 ) = ( 0g ‘ 𝐺 ) )
9 1 5 mulg1 ⊢ ( 𝑥 ∈ 𝑋 → ( 1 ( .g ‘ 𝐺 ) 𝑥 ) = 𝑥 )
10 9 adantl ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐸 = 1 ) ∧ 𝑥 ∈ 𝑋 ) → ( 1 ( .g ‘ 𝐺 ) 𝑥 ) = 𝑥 )
11 4 8 10 3eqtr3rd ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐸 = 1 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑥 = ( 0g ‘ 𝐺 ) )
12 velsn ⊢ ( 𝑥 ∈ { ( 0g ‘ 𝐺 ) } ↔ 𝑥 = ( 0g ‘ 𝐺 ) )
13 11 12 sylibr ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝐸 = 1 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ { ( 0g ‘ 𝐺 ) } )
14 13 ex ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐸 = 1 ) → ( 𝑥 ∈ 𝑋 → 𝑥 ∈ { ( 0g ‘ 𝐺 ) } ) )
15 14 ssrdv ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐸 = 1 ) → 𝑋 ⊆ { ( 0g ‘ 𝐺 ) } )
16 1 6 mndidcl ⊢ ( 𝐺 ∈ Mnd → ( 0g ‘ 𝐺 ) ∈ 𝑋 )
17 16 adantr ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐸 = 1 ) → ( 0g ‘ 𝐺 ) ∈ 𝑋 )
18 17 snssd ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐸 = 1 ) → { ( 0g ‘ 𝐺 ) } ⊆ 𝑋 )
19 15 18 eqssd ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐸 = 1 ) → 𝑋 = { ( 0g ‘ 𝐺 ) } )
20 fvex ⊢ ( 0g ‘ 𝐺 ) ∈ V
21 20 ensn1 ⊢ { ( 0g ‘ 𝐺 ) } ≈ 1o
22 19 21 eqbrtrdi ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐸 = 1 ) → 𝑋 ≈ 1o )
23 simpl ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑋 ≈ 1o ) → 𝐺 ∈ Mnd )
24 1nn ⊢ 1 ∈ ℕ
25 24 a1i ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑋 ≈ 1o ) → 1 ∈ ℕ )
26 9 adantl ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝑋 ≈ 1o ) ∧ 𝑥 ∈ 𝑋 ) → ( 1 ( .g ‘ 𝐺 ) 𝑥 ) = 𝑥 )
27 en1eqsn ⊢ ( ( ( 0g ‘ 𝐺 ) ∈ 𝑋 ∧ 𝑋 ≈ 1o ) → 𝑋 = { ( 0g ‘ 𝐺 ) } )
28 16 27 sylan ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑋 ≈ 1o ) → 𝑋 = { ( 0g ‘ 𝐺 ) } )
29 28 eleq2d ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑋 ≈ 1o ) → ( 𝑥 ∈ 𝑋 ↔ 𝑥 ∈ { ( 0g ‘ 𝐺 ) } ) )
30 29 biimpa ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝑋 ≈ 1o ) ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ { ( 0g ‘ 𝐺 ) } )
31 30 12 sylib ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝑋 ≈ 1o ) ∧ 𝑥 ∈ 𝑋 ) → 𝑥 = ( 0g ‘ 𝐺 ) )
32 26 31 eqtrd ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝑋 ≈ 1o ) ∧ 𝑥 ∈ 𝑋 ) → ( 1 ( .g ‘ 𝐺 ) 𝑥 ) = ( 0g ‘ 𝐺 ) )
33 32 ralrimiva ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑋 ≈ 1o ) → ∀ 𝑥 ∈ 𝑋 ( 1 ( .g ‘ 𝐺 ) 𝑥 ) = ( 0g ‘ 𝐺 ) )
34 1 2 5 6 gexlem2 ⊢ ( ( 𝐺 ∈ Mnd ∧ 1 ∈ ℕ ∧ ∀ 𝑥 ∈ 𝑋 ( 1 ( .g ‘ 𝐺 ) 𝑥 ) = ( 0g ‘ 𝐺 ) ) → 𝐸 ∈ ( 1 ... 1 ) )
35 23 25 33 34 syl3anc ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑋 ≈ 1o ) → 𝐸 ∈ ( 1 ... 1 ) )
36 elfz1eq ⊢ ( 𝐸 ∈ ( 1 ... 1 ) → 𝐸 = 1 )
37 35 36 syl ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑋 ≈ 1o ) → 𝐸 = 1 )
38 22 37 impbida ⊢ ( 𝐺 ∈ Mnd → ( 𝐸 = 1 ↔ 𝑋 ≈ 1o ) )