Theorem trivnsimpgd

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

	Ref	Expression
Hypotheses	trivnsimpgd.1	$$⊢B={\mathrm{Base}}_G$$
	trivnsimpgd.2	$$⊢\underset{\dot{}}{0}=0_G$$
	trivnsimpgd.3	$$⊢\phi \to G\in \mathrm{Grp}$$
	trivnsimpgd.4	$$⊢\phi \to B=\left\{\underset{\dot{}}{0}\right\}$$
Assertion	trivnsimpgd	$$⊢\phi \to \neg G\in \mathrm{SimpGrp}$$

Proof

Step	Hyp	Ref	Expression
1		trivnsimpgd.1	$$⊢B={\mathrm{Base}}_G$$
2		trivnsimpgd.2	$$⊢\underset{\dot{}}{0}=0_G$$
3		trivnsimpgd.3	$$⊢\phi \to G\in \mathrm{Grp}$$
4		trivnsimpgd.4	$$⊢\phi \to B=\left\{\underset{\dot{}}{0}\right\}$$
5		snnen2o	$$⊢\neg \left\{B\right\}\approx 2_{𝑜}$$
6	1 2 3 4	trivnsgd	$$⊢\phi \to \mathrm{NrmSGrp}\left(G\right)=\left\{B\right\}$$
7	6	breq1d	$$⊢\phi \to \left(\mathrm{NrmSGrp}\left(G\right)\approx 2_{𝑜}\leftrightarrow \left\{B\right\}\approx 2_{𝑜}\right)$$
8	5 7	mtbiri	$$⊢\phi \to \neg \mathrm{NrmSGrp}\left(G\right)\approx 2_{𝑜}$$
9		simpg2nsg	$$⊢G\in \mathrm{SimpGrp}\to \mathrm{NrmSGrp}\left(G\right)\approx 2_{𝑜}$$
10	8 9	nsyl	$$⊢\phi \to \neg G\in \mathrm{SimpGrp}$$