Theorem simpgnideld

Description: A simple group contains a nonidentity element. (Contributed by Rohan Ridenour, 3-Aug-2023)

	Ref	Expression
Hypotheses	simpgnideld.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
	simpgnideld.2	⊢ 0 = ( 0g ‘ 𝐺 )
	simpgnideld.3	⊢ ( 𝜑 → 𝐺 ∈ SimpGrp )
Assertion	simpgnideld	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐵 ¬ 𝑥 = 0 )

Proof

Step	Hyp	Ref	Expression
1		simpgnideld.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		simpgnideld.2	⊢ 0 = ( 0g ‘ 𝐺 )
3		simpgnideld.3	⊢ ( 𝜑 → 𝐺 ∈ SimpGrp )
4	1 2 3	simpgntrivd	⊢ ( 𝜑 → ¬ 𝐵 = { 0 } )
5	3	simpggrpd	⊢ ( 𝜑 → 𝐺 ∈ Grp )
6		grpmnd	⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd )
7	1 2	mndidcl	⊢ ( 𝐺 ∈ Mnd → 0 ∈ 𝐵 )
8	5 6 7	3syl	⊢ ( 𝜑 → 0 ∈ 𝐵 )
9	8	ne0d	⊢ ( 𝜑 → 𝐵 ≠ ∅ )
10		eqsn	⊢ ( 𝐵 ≠ ∅ → ( 𝐵 = { 0 } ↔ ∀ 𝑥 ∈ 𝐵 𝑥 = 0 ) )
11	9 10	syl	⊢ ( 𝜑 → ( 𝐵 = { 0 } ↔ ∀ 𝑥 ∈ 𝐵 𝑥 = 0 ) )
12	4 11	mtbid	⊢ ( 𝜑 → ¬ ∀ 𝑥 ∈ 𝐵 𝑥 = 0 )
13		rexnal	⊢ ( ∃ 𝑥 ∈ 𝐵 ¬ 𝑥 = 0 ↔ ¬ ∀ 𝑥 ∈ 𝐵 𝑥 = 0 )
14	12 13	sylibr	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐵 ¬ 𝑥 = 0 )