Metamath Proof Explorer


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 )