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	|- B = ( Base ` G )
	simpgnsgeqd.2	|- .0. = ( 0g ` G )
	simpgnsgeqd.3	|- ( ph -> G e. SimpGrp )
	simpgnsgeqd.4	|- ( ph -> A e. ( NrmSGrp ` G ) )
Assertion	simpgnsgeqd	|- ( ph -> ( A = { .0. } \/ A = B ) )

Proof

Step	Hyp	Ref	Expression
1		simpgnsgeqd.1	|- B = ( Base ` G )
2		simpgnsgeqd.2	|- .0. = ( 0g ` G )
3		simpgnsgeqd.3	|- ( ph -> G e. SimpGrp )
4		simpgnsgeqd.4	|- ( ph -> A e. ( NrmSGrp ` G ) )
5	1 2 3	simpgnsgd	|- ( ph -> ( NrmSGrp ` G ) = { { .0. } , B } )
6	4 5	eleqtrd	|- ( ph -> A e. { { .0. } , B } )
7		elpri	|- ( A e. { { .0. } , B } -> ( A = { .0. } \/ A = B ) )
8	6 7	syl	|- ( ph -> ( A = { .0. } \/ A = B ) )