Theorem simpgnideld

Description: A simple group contains a nonidentity element. (Contributed by Rohan Ridenour, 3-Aug-2023)

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

Proof

Step	Hyp	Ref	Expression
1		simpgnideld.1	$$⊢B={\mathrm{Base}}_G$$
2		simpgnideld.2	$$⊢\underset{\dot{}}{0}=0_G$$
3		simpgnideld.3	$$⊢\phi \to G\in \mathrm{SimpGrp}$$
4	1 2 3	simpgntrivd	$$⊢\phi \to \neg B=\left\{\underset{\dot{}}{0}\right\}$$
5	3	simpggrpd	$$⊢\phi \to G\in \mathrm{Grp}$$
6		grpmnd	$$⊢G\in \mathrm{Grp}\to G\in \mathrm{Mnd}$$
7	1 2	mndidcl	$$⊢G\in \mathrm{Mnd}\to \underset{\dot{}}{0}\in B$$
8	5 6 7	3syl	$$⊢\phi \to \underset{\dot{}}{0}\in B$$
9	8	ne0d	$$⊢\phi \to B\ne \varnothing$$
10		eqsn	$$⊢B\ne \varnothing \to \left(B=\left\{\underset{\dot{}}{0}\right\}\leftrightarrow \forall x\in Bx=\underset{\dot{}}{0}\right)$$
11	9 10	syl	$$⊢\phi \to \left(B=\left\{\underset{\dot{}}{0}\right\}\leftrightarrow \forall x\in Bx=\underset{\dot{}}{0}\right)$$
12	4 11	mtbid	$$⊢\phi \to \neg \forall x\in Bx=\underset{\dot{}}{0}$$
13		rexnal	$$⊢\exists x\in B\neg x=\underset{\dot{}}{0}\leftrightarrow \neg \forall x\in Bx=\underset{\dot{}}{0}$$
14	12 13	sylibr	$$⊢\phi \to \exists x\in B\neg x=\underset{\dot{}}{0}$$