Theorem simpgnideld

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

	Ref	Expression
Hypotheses	simpgnideld.1	|- B = ( Base ` G )
	simpgnideld.2	|- .0. = ( 0g ` G )
	simpgnideld.3	|- ( ph -> G e. SimpGrp )
Assertion	simpgnideld	|- ( ph -> E. x e. B -. x = .0. )

Proof

Step	Hyp	Ref	Expression
1		simpgnideld.1	|- B = ( Base ` G )
2		simpgnideld.2	|- .0. = ( 0g ` G )
3		simpgnideld.3	|- ( ph -> G e. SimpGrp )
4	1 2 3	simpgntrivd	|- ( ph -> -. B = { .0. } )
5	3	simpggrpd	|- ( ph -> G e. Grp )
6		grpmnd	|- ( G e. Grp -> G e. Mnd )
7	1 2	mndidcl	|- ( G e. Mnd -> .0. e. B )
8	5 6 7	3syl	|- ( ph -> .0. e. B )
9	8	ne0d	|- ( ph -> B =/= (/) )
10		eqsn	|- ( B =/= (/) -> ( B = { .0. } <-> A. x e. B x = .0. ) )
11	9 10	syl	|- ( ph -> ( B = { .0. } <-> A. x e. B x = .0. ) )
12	4 11	mtbid	|- ( ph -> -. A. x e. B x = .0. )
13		rexnal	|- ( E. x e. B -. x = .0. <-> -. A. x e. B x = .0. )
14	12 13	sylibr	|- ( ph -> E. x e. B -. x = .0. )