Theorem simpgnsgbid

Description: A nontrivial group is simple if and only if its normal subgroups are exactly the group itself and the trivial subgroup. (Contributed by Rohan Ridenour, 4-Aug-2023)

	Ref	Expression
Hypotheses	simpgnsgbid.1	|- B = ( Base ` G )
	simpgnsgbid.2	|- .0. = ( 0g ` G )
	simpgnsgbid.3	|- ( ph -> G e. Grp )
	simpgnsgbid.4	|- ( ph -> -. { .0. } = B )
Assertion	simpgnsgbid	|- ( ph -> ( G e. SimpGrp <-> ( NrmSGrp ` G ) = { { .0. } , B } ) )

Proof

Step	Hyp	Ref	Expression
1		simpgnsgbid.1	|- B = ( Base ` G )
2		simpgnsgbid.2	|- .0. = ( 0g ` G )
3		simpgnsgbid.3	|- ( ph -> G e. Grp )
4		simpgnsgbid.4	|- ( ph -> -. { .0. } = B )
5		simpr	|- ( ( ph /\ G e. SimpGrp ) -> G e. SimpGrp )
6	1 2 5	simpgnsgd	|- ( ( ph /\ G e. SimpGrp ) -> ( NrmSGrp ` G ) = { { .0. } , B } )
7	3	adantr	|- ( ( ph /\ ( NrmSGrp ` G ) = { { .0. } , B } ) -> G e. Grp )
8	4	adantr	|- ( ( ph /\ ( NrmSGrp ` G ) = { { .0. } , B } ) -> -. { .0. } = B )
9		simpr	|- ( ( ( ph /\ ( NrmSGrp ` G ) = { { .0. } , B } ) /\ x e. ( NrmSGrp ` G ) ) -> x e. ( NrmSGrp ` G ) )
10		simplr	|- ( ( ( ph /\ ( NrmSGrp ` G ) = { { .0. } , B } ) /\ x e. ( NrmSGrp ` G ) ) -> ( NrmSGrp ` G ) = { { .0. } , B } )
11	9 10	eleqtrd	|- ( ( ( ph /\ ( NrmSGrp ` G ) = { { .0. } , B } ) /\ x e. ( NrmSGrp ` G ) ) -> x e. { { .0. } , B } )
12		elpri	|- ( x e. { { .0. } , B } -> ( x = { .0. } \/ x = B ) )
13	11 12	syl	|- ( ( ( ph /\ ( NrmSGrp ` G ) = { { .0. } , B } ) /\ x e. ( NrmSGrp ` G ) ) -> ( x = { .0. } \/ x = B ) )
14	1 2 7 8 13	2nsgsimpgd	|- ( ( ph /\ ( NrmSGrp ` G ) = { { .0. } , B } ) -> G e. SimpGrp )
15	6 14	impbida	|- ( ph -> ( G e. SimpGrp <-> ( NrmSGrp ` G ) = { { .0. } , B } ) )