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 = ( Base ` G )
	ablsimpnosubgd.2	|- .0. = ( 0g ` G )
	ablsimpnosubgd.3	|- ( ph -> G e. Abel )
	ablsimpnosubgd.4	|- ( ph -> G e. SimpGrp )
	ablsimpnosubgd.5	|- ( ph -> S e. ( SubGrp ` G ) )
	ablsimpnosubgd.6	|- ( ph -> A e. S )
	ablsimpnosubgd.7	|- ( ph -> -. A = .0. )
Assertion	ablsimpnosubgd	|- ( ph -> S = B )

Proof

Step	Hyp	Ref	Expression
1		ablsimpnosubgd.1	|- B = ( Base ` G )
2		ablsimpnosubgd.2	|- .0. = ( 0g ` G )
3		ablsimpnosubgd.3	|- ( ph -> G e. Abel )
4		ablsimpnosubgd.4	|- ( ph -> G e. SimpGrp )
5		ablsimpnosubgd.5	|- ( ph -> S e. ( SubGrp ` G ) )
6		ablsimpnosubgd.6	|- ( ph -> A e. S )
7		ablsimpnosubgd.7	|- ( ph -> -. A = .0. )
8		elsni	|- ( A e. { .0. } -> A = .0. )
9	7 8	nsyl	|- ( ph -> -. A e. { .0. } )
10		eleq2	|- ( S = { .0. } -> ( A e. S <-> A e. { .0. } ) )
11	6 10	syl5ibcom	|- ( ph -> ( S = { .0. } -> A e. { .0. } ) )
12	9 11	mtod	|- ( ph -> -. S = { .0. } )
13	12	pm2.21d	|- ( ph -> ( S = { .0. } -> S = B ) )
14		idd	|- ( ph -> ( S = B -> S = B ) )
15		ablnsg	|- ( G e. Abel -> ( NrmSGrp ` G ) = ( SubGrp ` G ) )
16	15	eqcomd	|- ( G e. Abel -> ( SubGrp ` G ) = ( NrmSGrp ` G ) )
17	3 16	syl	|- ( ph -> ( SubGrp ` G ) = ( NrmSGrp ` G ) )
18	5 17	eleqtrd	|- ( ph -> S e. ( NrmSGrp ` G ) )
19	1 2 4 18	simpgnsgeqd	|- ( ph -> ( S = { .0. } \/ S = B ) )
20	13 14 19	mpjaod	|- ( ph -> S = B )