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={\mathrm{Base}}_G$$
	simpgnsgeqd.2	$$⊢\underset{\dot{}}{0}=0_G$$
	simpgnsgeqd.3	$$⊢\phi \to G\in \mathrm{SimpGrp}$$
	simpgnsgeqd.4	$$⊢\phi \to A\in \mathrm{NrmSGrp}\left(G\right)$$
Assertion	simpgnsgeqd	$$⊢\phi \to \left(A=\left\{\underset{\dot{}}{0}\right\}\vee A=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		simpgnsgeqd.1	$$⊢B={\mathrm{Base}}_G$$
2		simpgnsgeqd.2	$$⊢\underset{\dot{}}{0}=0_G$$
3		simpgnsgeqd.3	$$⊢\phi \to G\in \mathrm{SimpGrp}$$
4		simpgnsgeqd.4	$$⊢\phi \to A\in \mathrm{NrmSGrp}\left(G\right)$$
5	1 2 3	simpgnsgd	$$⊢\phi \to \mathrm{NrmSGrp}\left(G\right)=\left\{\left\{\underset{\dot{}}{0}\right\},B\right\}$$
6	4 5	eleqtrd	$$⊢\phi \to A\in \left\{\left\{\underset{\dot{}}{0}\right\},B\right\}$$
7		elpri	$$⊢A\in \left\{\left\{\underset{\dot{}}{0}\right\},B\right\}\to \left(A=\left\{\underset{\dot{}}{0}\right\}\vee A=B\right)$$
8	6 7	syl	$$⊢\phi \to \left(A=\left\{\underset{\dot{}}{0}\right\}\vee A=B\right)$$