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	⊢ 𝐵 = ( Base ‘ 𝐺 )
	ablsimpnosubgd.2	⊢ 0 = ( 0g ‘ 𝐺 )
	ablsimpnosubgd.3	⊢ ( 𝜑 → 𝐺 ∈ Abel )
	ablsimpnosubgd.4	⊢ ( 𝜑 → 𝐺 ∈ SimpGrp )
	ablsimpnosubgd.5	⊢ ( 𝜑 → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
	ablsimpnosubgd.6	⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
	ablsimpnosubgd.7	⊢ ( 𝜑 → ¬ 𝐴 = 0 )
Assertion	ablsimpnosubgd	⊢ ( 𝜑 → 𝑆 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		ablsimpnosubgd.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		ablsimpnosubgd.2	⊢ 0 = ( 0g ‘ 𝐺 )
3		ablsimpnosubgd.3	⊢ ( 𝜑 → 𝐺 ∈ Abel )
4		ablsimpnosubgd.4	⊢ ( 𝜑 → 𝐺 ∈ SimpGrp )
5		ablsimpnosubgd.5	⊢ ( 𝜑 → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
6		ablsimpnosubgd.6	⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
7		ablsimpnosubgd.7	⊢ ( 𝜑 → ¬ 𝐴 = 0 )
8		elsni	⊢ ( 𝐴 ∈ { 0 } → 𝐴 = 0 )
9	7 8	nsyl	⊢ ( 𝜑 → ¬ 𝐴 ∈ { 0 } )
10		eleq2	⊢ ( 𝑆 = { 0 } → ( 𝐴 ∈ 𝑆 ↔ 𝐴 ∈ { 0 } ) )
11	6 10	syl5ibcom	⊢ ( 𝜑 → ( 𝑆 = { 0 } → 𝐴 ∈ { 0 } ) )
12	9 11	mtod	⊢ ( 𝜑 → ¬ 𝑆 = { 0 } )
13	12	pm2.21d	⊢ ( 𝜑 → ( 𝑆 = { 0 } → 𝑆 = 𝐵 ) )
14		idd	⊢ ( 𝜑 → ( 𝑆 = 𝐵 → 𝑆 = 𝐵 ) )
15		ablnsg	⊢ ( 𝐺 ∈ Abel → ( NrmSGrp ‘ 𝐺 ) = ( SubGrp ‘ 𝐺 ) )
16	15	eqcomd	⊢ ( 𝐺 ∈ Abel → ( SubGrp ‘ 𝐺 ) = ( NrmSGrp ‘ 𝐺 ) )
17	3 16	syl	⊢ ( 𝜑 → ( SubGrp ‘ 𝐺 ) = ( NrmSGrp ‘ 𝐺 ) )
18	5 17	eleqtrd	⊢ ( 𝜑 → 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) )
19	1 2 4 18	simpgnsgeqd	⊢ ( 𝜑 → ( 𝑆 = { 0 } ∨ 𝑆 = 𝐵 ) )
20	13 14 19	mpjaod	⊢ ( 𝜑 → 𝑆 = 𝐵 )