Theorem ablsimpnosubgd

Description: A subgroup of an abelian simple group containing a nonidentity element is the whole group. (Contributed by Rohan Ridenour, 3-Aug-2023)

	Ref	Expression
Hypotheses	ablsimpnosubgd.1	$$⊢B={\mathrm{Base}}_G$$
	ablsimpnosubgd.2	$$⊢\underset{\dot{}}{0}=0_G$$
	ablsimpnosubgd.3	$$⊢\phi \to G\in \mathrm{Abel}$$
	ablsimpnosubgd.4	$$⊢\phi \to G\in \mathrm{SimpGrp}$$
	ablsimpnosubgd.5	$$⊢\phi \to S\in \mathrm{SubGrp}\left(G\right)$$
	ablsimpnosubgd.6	$$⊢\phi \to A\in S$$
	ablsimpnosubgd.7	$$⊢\phi \to \neg A=\underset{\dot{}}{0}$$
Assertion	ablsimpnosubgd	$$⊢\phi \to S=B$$

Proof

Step	Hyp	Ref	Expression
1		ablsimpnosubgd.1	$$⊢B={\mathrm{Base}}_G$$
2		ablsimpnosubgd.2	$$⊢\underset{\dot{}}{0}=0_G$$
3		ablsimpnosubgd.3	$$⊢\phi \to G\in \mathrm{Abel}$$
4		ablsimpnosubgd.4	$$⊢\phi \to G\in \mathrm{SimpGrp}$$
5		ablsimpnosubgd.5	$$⊢\phi \to S\in \mathrm{SubGrp}\left(G\right)$$
6		ablsimpnosubgd.6	$$⊢\phi \to A\in S$$
7		ablsimpnosubgd.7	$$⊢\phi \to \neg A=\underset{\dot{}}{0}$$
8		elsni	$$⊢A\in \left\{\underset{\dot{}}{0}\right\}\to A=\underset{\dot{}}{0}$$
9	7 8	nsyl	$$⊢\phi \to \neg A\in \left\{\underset{\dot{}}{0}\right\}$$
10		eleq2	$$⊢S=\left\{\underset{\dot{}}{0}\right\}\to \left(A\in S\leftrightarrow A\in \left\{\underset{\dot{}}{0}\right\}\right)$$
11	6 10	syl5ibcom	$$⊢\phi \to \left(S=\left\{\underset{\dot{}}{0}\right\}\to A\in \left\{\underset{\dot{}}{0}\right\}\right)$$
12	9 11	mtod	$$⊢\phi \to \neg S=\left\{\underset{\dot{}}{0}\right\}$$
13	12	pm2.21d	$$⊢\phi \to \left(S=\left\{\underset{\dot{}}{0}\right\}\to S=B\right)$$
14		idd	$$⊢\phi \to \left(S=B\to S=B\right)$$
15		ablnsg	$$⊢G\in \mathrm{Abel}\to \mathrm{NrmSGrp}\left(G\right)=\mathrm{SubGrp}\left(G\right)$$
16	15	eqcomd	$$⊢G\in \mathrm{Abel}\to \mathrm{SubGrp}\left(G\right)=\mathrm{NrmSGrp}\left(G\right)$$
17	3 16	syl	$$⊢\phi \to \mathrm{SubGrp}\left(G\right)=\mathrm{NrmSGrp}\left(G\right)$$
18	5 17	eleqtrd	$$⊢\phi \to S\in \mathrm{NrmSGrp}\left(G\right)$$
19	1 2 4 18	simpgnsgeqd	$$⊢\phi \to \left(S=\left\{\underset{\dot{}}{0}\right\}\vee S=B\right)$$
20	13 14 19	mpjaod	$$⊢\phi \to S=B$$