Theorem simpgntrivd

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

	Ref	Expression
Hypotheses	simpgntrivd.1	|- B = ( Base ` G )
	simpgntrivd.2	|- .0. = ( 0g ` G )
	simpgntrivd.3	|- ( ph -> G e. SimpGrp )
Assertion	simpgntrivd	|- ( ph -> -. B = { .0. } )

Proof

Step	Hyp	Ref	Expression
1		simpgntrivd.1	|- B = ( Base ` G )
2		simpgntrivd.2	|- .0. = ( 0g ` G )
3		simpgntrivd.3	|- ( ph -> G e. SimpGrp )
4	3	adantr	|- ( ( ph /\ B = { .0. } ) -> G e. SimpGrp )
5	3	simpggrpd	|- ( ph -> G e. Grp )
6	5	adantr	|- ( ( ph /\ B = { .0. } ) -> G e. Grp )
7		simpr	|- ( ( ph /\ B = { .0. } ) -> B = { .0. } )
8	1 2 6 7	trivnsimpgd	|- ( ( ph /\ B = { .0. } ) -> -. G e. SimpGrp )
9	4 8	pm2.65da	|- ( ph -> -. B = { .0. } )