# Metamath Proof Explorer

## 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
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
Assertion ablsimpnosubgd ${⊢}{\phi }\to {S}={B}$

### Proof

Step Hyp Ref Expression
1 ablsimpnosubgd.1 ${⊢}{B}={\mathrm{Base}}_{{G}}$
2 ablsimpnosubgd.2
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
8 elsni
9 7 8 nsyl
10 eleq2
11 6 10 syl5ibcom
12 9 11 mtod
13 12 pm2.21d
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
20 13 14 19 mpjaod ${⊢}{\phi }\to {S}={B}$