Theorem simpgntrivd

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

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

Proof

Step	Hyp	Ref	Expression
1		simpgntrivd.1	$$⊢B={\mathrm{Base}}_G$$
2		simpgntrivd.2	$$⊢\underset{\dot{}}{0}=0_G$$
3		simpgntrivd.3	$$⊢\phi \to G\in \mathrm{SimpGrp}$$
4	3	adantr	$$⊢\left(\phi \wedge B=\left\{\underset{\dot{}}{0}\right\}\right)\to G\in \mathrm{SimpGrp}$$
5	3	simpggrpd	$$⊢\phi \to G\in \mathrm{Grp}$$
6	5	adantr	$$⊢\left(\phi \wedge B=\left\{\underset{\dot{}}{0}\right\}\right)\to G\in \mathrm{Grp}$$
7		simpr	$$⊢\left(\phi \wedge B=\left\{\underset{\dot{}}{0}\right\}\right)\to B=\left\{\underset{\dot{}}{0}\right\}$$
8	1 2 6 7	trivnsimpgd	$$⊢\left(\phi \wedge B=\left\{\underset{\dot{}}{0}\right\}\right)\to \neg G\in \mathrm{SimpGrp}$$
9	4 8	pm2.65da	$$⊢\phi \to \neg B=\left\{\underset{\dot{}}{0}\right\}$$