Theorem trivnsimpgd

Description: Trivial groups are not simple. (Contributed by Rohan Ridenour, 3-Aug-2023)

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

Proof

Step	Hyp	Ref	Expression
1		trivnsimpgd.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		trivnsimpgd.2	⊢ 0 = ( 0g ‘ 𝐺 )
3		trivnsimpgd.3	⊢ ( 𝜑 → 𝐺 ∈ Grp )
4		trivnsimpgd.4	⊢ ( 𝜑 → 𝐵 = { 0 } )
5		snnen2o	⊢ ¬ { 𝐵 } ≈ 2o
6	1 2 3 4	trivnsgd	⊢ ( 𝜑 → ( NrmSGrp ‘ 𝐺 ) = { 𝐵 } )
7	6	breq1d	⊢ ( 𝜑 → ( ( NrmSGrp ‘ 𝐺 ) ≈ 2o ↔ { 𝐵 } ≈ 2o ) )
8	5 7	mtbiri	⊢ ( 𝜑 → ¬ ( NrmSGrp ‘ 𝐺 ) ≈ 2o )
9		simpg2nsg	⊢ ( 𝐺 ∈ SimpGrp → ( NrmSGrp ‘ 𝐺 ) ≈ 2o )
10	8 9	nsyl	⊢ ( 𝜑 → ¬ 𝐺 ∈ SimpGrp )