Metamath Proof Explorer


Theorem simpgnsgbid

Description: A nontrivial group is simple if and only if its normal subgroups are exactly the group itself and the trivial subgroup. (Contributed by Rohan Ridenour, 4-Aug-2023)

Ref Expression
Hypotheses simpgnsgbid.1 𝐵 = ( Base ‘ 𝐺 )
simpgnsgbid.2 0 = ( 0g𝐺 )
simpgnsgbid.3 ( 𝜑𝐺 ∈ Grp )
simpgnsgbid.4 ( 𝜑 → ¬ { 0 } = 𝐵 )
Assertion simpgnsgbid ( 𝜑 → ( 𝐺 ∈ SimpGrp ↔ ( NrmSGrp ‘ 𝐺 ) = { { 0 } , 𝐵 } ) )

Proof

Step Hyp Ref Expression
1 simpgnsgbid.1 𝐵 = ( Base ‘ 𝐺 )
2 simpgnsgbid.2 0 = ( 0g𝐺 )
3 simpgnsgbid.3 ( 𝜑𝐺 ∈ Grp )
4 simpgnsgbid.4 ( 𝜑 → ¬ { 0 } = 𝐵 )
5 simpr ( ( 𝜑𝐺 ∈ SimpGrp ) → 𝐺 ∈ SimpGrp )
6 1 2 5 simpgnsgd ( ( 𝜑𝐺 ∈ SimpGrp ) → ( NrmSGrp ‘ 𝐺 ) = { { 0 } , 𝐵 } )
7 3 adantr ( ( 𝜑 ∧ ( NrmSGrp ‘ 𝐺 ) = { { 0 } , 𝐵 } ) → 𝐺 ∈ Grp )
8 4 adantr ( ( 𝜑 ∧ ( NrmSGrp ‘ 𝐺 ) = { { 0 } , 𝐵 } ) → ¬ { 0 } = 𝐵 )
9 simpr ( ( ( 𝜑 ∧ ( NrmSGrp ‘ 𝐺 ) = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( NrmSGrp ‘ 𝐺 ) ) → 𝑥 ∈ ( NrmSGrp ‘ 𝐺 ) )
10 simplr ( ( ( 𝜑 ∧ ( NrmSGrp ‘ 𝐺 ) = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( NrmSGrp ‘ 𝐺 ) ) → ( NrmSGrp ‘ 𝐺 ) = { { 0 } , 𝐵 } )
11 9 10 eleqtrd ( ( ( 𝜑 ∧ ( NrmSGrp ‘ 𝐺 ) = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( NrmSGrp ‘ 𝐺 ) ) → 𝑥 ∈ { { 0 } , 𝐵 } )
12 elpri ( 𝑥 ∈ { { 0 } , 𝐵 } → ( 𝑥 = { 0 } ∨ 𝑥 = 𝐵 ) )
13 11 12 syl ( ( ( 𝜑 ∧ ( NrmSGrp ‘ 𝐺 ) = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( NrmSGrp ‘ 𝐺 ) ) → ( 𝑥 = { 0 } ∨ 𝑥 = 𝐵 ) )
14 1 2 7 8 13 2nsgsimpgd ( ( 𝜑 ∧ ( NrmSGrp ‘ 𝐺 ) = { { 0 } , 𝐵 } ) → 𝐺 ∈ SimpGrp )
15 6 14 impbida ( 𝜑 → ( 𝐺 ∈ SimpGrp ↔ ( NrmSGrp ‘ 𝐺 ) = { { 0 } , 𝐵 } ) )