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 ) )