Theorem simpgntrivd

Description: Simple groups are nontrivial. (Contributed by Rohan Ridenour, 3-Aug-2023)

	Ref	Expression
Hypotheses	simpgntrivd.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
	simpgntrivd.2	⊢ 0 = ( 0g ‘ 𝐺 )
	simpgntrivd.3	⊢ ( 𝜑 → 𝐺 ∈ SimpGrp )
Assertion	simpgntrivd	⊢ ( 𝜑 → ¬ 𝐵 = { 0 } )

Proof

Step	Hyp	Ref	Expression
1		simpgntrivd.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		simpgntrivd.2	⊢ 0 = ( 0g ‘ 𝐺 )
3		simpgntrivd.3	⊢ ( 𝜑 → 𝐺 ∈ SimpGrp )
4	3	adantr	⊢ ( ( 𝜑 ∧ 𝐵 = { 0 } ) → 𝐺 ∈ SimpGrp )
5	3	simpggrpd	⊢ ( 𝜑 → 𝐺 ∈ Grp )
6	5	adantr	⊢ ( ( 𝜑 ∧ 𝐵 = { 0 } ) → 𝐺 ∈ Grp )
7		simpr	⊢ ( ( 𝜑 ∧ 𝐵 = { 0 } ) → 𝐵 = { 0 } )
8	1 2 6 7	trivnsimpgd	⊢ ( ( 𝜑 ∧ 𝐵 = { 0 } ) → ¬ 𝐺 ∈ SimpGrp )
9	4 8	pm2.65da	⊢ ( 𝜑 → ¬ 𝐵 = { 0 } )