Theorem simpgnsgd

Description: The only normal subgroups of a simple group are the group itself and the trivial group. (Contributed by Rohan Ridenour, 3-Aug-2023)

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

Proof

Step	Hyp	Ref	Expression
1		simpgnsgd.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		simpgnsgd.2	⊢ 0 = ( 0g ‘ 𝐺 )
3		simpgnsgd.3	⊢ ( 𝜑 → 𝐺 ∈ SimpGrp )
4		2onn	⊢ 2o ∈ ω
5	4	a1i	⊢ ( 𝜑 → 2o ∈ ω )
6		nnfi	⊢ ( 2o ∈ ω → 2o ∈ Fin )
7	5 6	syl	⊢ ( 𝜑 → 2o ∈ Fin )
8		simpg2nsg	⊢ ( 𝐺 ∈ SimpGrp → ( NrmSGrp ‘ 𝐺 ) ≈ 2o )
9	3 8	syl	⊢ ( 𝜑 → ( NrmSGrp ‘ 𝐺 ) ≈ 2o )
10		enfii	⊢ ( ( 2o ∈ Fin ∧ ( NrmSGrp ‘ 𝐺 ) ≈ 2o ) → ( NrmSGrp ‘ 𝐺 ) ∈ Fin )
11	7 9 10	syl2anc	⊢ ( 𝜑 → ( NrmSGrp ‘ 𝐺 ) ∈ Fin )
12	3	simpggrpd	⊢ ( 𝜑 → 𝐺 ∈ Grp )
13	1 2 12	0idnsgd	⊢ ( 𝜑 → { { 0 } , 𝐵 } ⊆ ( NrmSGrp ‘ 𝐺 ) )
14		snex	⊢ { 0 } ∈ V
15	14	a1i	⊢ ( 𝜑 → { 0 } ∈ V )
16	1	a1i	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐺 ) )
17		fvex	⊢ ( Base ‘ 𝐺 ) ∈ V
18	16 17	eqeltrdi	⊢ ( 𝜑 → 𝐵 ∈ V )
19	1 2 3	simpgntrivd	⊢ ( 𝜑 → ¬ 𝐵 = { 0 } )
20	19	neqcomd	⊢ ( 𝜑 → ¬ { 0 } = 𝐵 )
21	15 18 20	enpr2d	⊢ ( 𝜑 → { { 0 } , 𝐵 } ≈ 2o )
22	21	ensymd	⊢ ( 𝜑 → 2o ≈ { { 0 } , 𝐵 } )
23		entr	⊢ ( ( ( NrmSGrp ‘ 𝐺 ) ≈ 2o ∧ 2o ≈ { { 0 } , 𝐵 } ) → ( NrmSGrp ‘ 𝐺 ) ≈ { { 0 } , 𝐵 } )
24	9 22 23	syl2anc	⊢ ( 𝜑 → ( NrmSGrp ‘ 𝐺 ) ≈ { { 0 } , 𝐵 } )
25	11 13 24	phpeqd	⊢ ( 𝜑 → ( NrmSGrp ‘ 𝐺 ) = { { 0 } , 𝐵 } )