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

Metamath Proof Explorer

Theorem 1nsgtrivd

Description: A group with exactly one normal subgroup is trivial. (Contributed by Rohan Ridenour, 3-Aug-2023)

Ref Expression
Hypotheses 1nsgtrivd.1 ⊢ 𝐵 = ( Base ‘ 𝐺 )
1nsgtrivd.2 ⊢ 0 = ( 0g ‘ 𝐺 )
1nsgtrivd.3 ⊢ ( 𝜑 → 𝐺 ∈ Grp )
1nsgtrivd.4 ⊢ ( 𝜑 → ( NrmSGrp ‘ 𝐺 ) ≈ 1o )
Assertion 1nsgtrivd ( 𝜑 → 𝐵 = { 0 } )

Proof

Step Hyp Ref Expression
1 1nsgtrivd.1 ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 1nsgtrivd.2 ⊢ 0 = ( 0g ‘ 𝐺 )
3 1nsgtrivd.3 ⊢ ( 𝜑 → 𝐺 ∈ Grp )
4 1nsgtrivd.4 ⊢ ( 𝜑 → ( NrmSGrp ‘ 𝐺 ) ≈ 1o )
5 1 nsgid ⊢ ( 𝐺 ∈ Grp → 𝐵 ∈ ( NrmSGrp ‘ 𝐺 ) )
6 3 5 syl ⊢ ( 𝜑 → 𝐵 ∈ ( NrmSGrp ‘ 𝐺 ) )
7 2 0nsg ⊢ ( 𝐺 ∈ Grp → { 0 } ∈ ( NrmSGrp ‘ 𝐺 ) )
8 3 7 syl ⊢ ( 𝜑 → { 0 } ∈ ( NrmSGrp ‘ 𝐺 ) )
9 en1eqsn ⊢ ( ( { 0 } ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( NrmSGrp ‘ 𝐺 ) ≈ 1o ) → ( NrmSGrp ‘ 𝐺 ) = { { 0 } } )
10 8 4 9 syl2anc ⊢ ( 𝜑 → ( NrmSGrp ‘ 𝐺 ) = { { 0 } } )
11 6 10 eleqtrd ⊢ ( 𝜑 → 𝐵 ∈ { { 0 } } )
12 snex ⊢ { 0 } ∈ V
13 elsn2g ⊢ ( { 0 } ∈ V → ( 𝐵 ∈ { { 0 } } ↔ 𝐵 = { 0 } ) )
14 12 13 mp1i ⊢ ( 𝜑 → ( 𝐵 ∈ { { 0 } } ↔ 𝐵 = { 0 } ) )
15 11 14 mpbid ⊢ ( 𝜑 → 𝐵 = { 0 } )