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	|- B = ( Base ` G )
	simpgnsgd.2	|- .0. = ( 0g ` G )
	simpgnsgd.3	|- ( ph -> G e. SimpGrp )
Assertion	simpgnsgd	|- ( ph -> ( NrmSGrp ` G ) = { { .0. } , B } )

Proof

Step	Hyp	Ref	Expression
1		simpgnsgd.1	|- B = ( Base ` G )
2		simpgnsgd.2	|- .0. = ( 0g ` G )
3		simpgnsgd.3	|- ( ph -> G e. SimpGrp )
4		2onn	|- 2o e. _om
5	4	a1i	|- ( ph -> 2o e. _om )
6		nnfi	|- ( 2o e. _om -> 2o e. Fin )
7	5 6	syl	|- ( ph -> 2o e. Fin )
8		simpg2nsg	|- ( G e. SimpGrp -> ( NrmSGrp ` G ) ~~ 2o )
9	3 8	syl	|- ( ph -> ( NrmSGrp ` G ) ~~ 2o )
10		enfii	|- ( ( 2o e. Fin /\ ( NrmSGrp ` G ) ~~ 2o ) -> ( NrmSGrp ` G ) e. Fin )
11	7 9 10	syl2anc	|- ( ph -> ( NrmSGrp ` G ) e. Fin )
12	3	simpggrpd	|- ( ph -> G e. Grp )
13	1 2 12	0idnsgd	|- ( ph -> { { .0. } , B } C_ ( NrmSGrp ` G ) )
14		snex	|- { .0. } e. _V
15	14	a1i	|- ( ph -> { .0. } e. _V )
16	1	a1i	|- ( ph -> B = ( Base ` G ) )
17		fvex	|- ( Base ` G ) e. _V
18	16 17	eqeltrdi	|- ( ph -> B e. _V )
19	1 2 3	simpgntrivd	|- ( ph -> -. B = { .0. } )
20	19	neqcomd	|- ( ph -> -. { .0. } = B )
21	15 18 20	enpr2d	|- ( ph -> { { .0. } , B } ~~ 2o )
22	21	ensymd	|- ( ph -> 2o ~~ { { .0. } , B } )
23		entr	|- ( ( ( NrmSGrp ` G ) ~~ 2o /\ 2o ~~ { { .0. } , B } ) -> ( NrmSGrp ` G ) ~~ { { .0. } , B } )
24	9 22 23	syl2anc	|- ( ph -> ( NrmSGrp ` G ) ~~ { { .0. } , B } )
25	11 13 24	phpeqd	|- ( ph -> ( NrmSGrp ` G ) = { { .0. } , B } )