Theorem simpgnsgeqd

Description: A normal subgroup of a simple group is either the whole group or the trivial subgroup. (Contributed by Rohan Ridenour, 3-Aug-2023)

	Ref	Expression
Hypotheses	simpgnsgeqd.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
	simpgnsgeqd.2	⊢ 0 = ( 0g ‘ 𝐺 )
	simpgnsgeqd.3	⊢ ( 𝜑 → 𝐺 ∈ SimpGrp )
	simpgnsgeqd.4	⊢ ( 𝜑 → 𝐴 ∈ ( NrmSGrp ‘ 𝐺 ) )
Assertion	simpgnsgeqd	⊢ ( 𝜑 → ( 𝐴 = { 0 } ∨ 𝐴 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		simpgnsgeqd.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		simpgnsgeqd.2	⊢ 0 = ( 0g ‘ 𝐺 )
3		simpgnsgeqd.3	⊢ ( 𝜑 → 𝐺 ∈ SimpGrp )
4		simpgnsgeqd.4	⊢ ( 𝜑 → 𝐴 ∈ ( NrmSGrp ‘ 𝐺 ) )
5	1 2 3	simpgnsgd	⊢ ( 𝜑 → ( NrmSGrp ‘ 𝐺 ) = { { 0 } , 𝐵 } )
6	4 5	eleqtrd	⊢ ( 𝜑 → 𝐴 ∈ { { 0 } , 𝐵 } )
7		elpri	⊢ ( 𝐴 ∈ { { 0 } , 𝐵 } → ( 𝐴 = { 0 } ∨ 𝐴 = 𝐵 ) )
8	6 7	syl	⊢ ( 𝜑 → ( 𝐴 = { 0 } ∨ 𝐴 = 𝐵 ) )