Metamath Proof Explorer

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	$⊢ \underset{˙}{0} = 0_{G}$
		simpgnsgbid.3	$⊢ φ \to G \in Grp$
		simpgnsgbid.4	$⊢ φ \to \neg \{\underset{˙}{0}\} = B$
	Assertion	simpgnsgbid	$⊢ φ \to (G \in SimpGrp \leftrightarrow NrmSGrp (G) = \{\{\underset{˙}{0}\}, B\})$

Proof

Step	Hyp	Ref	Expression
1		simpgnsgbid.1	$⊢ B = {Base}_{G}$
2		simpgnsgbid.2	$⊢ \underset{˙}{0} = 0_{G}$
3		simpgnsgbid.3	$⊢ φ \to G \in Grp$
4		simpgnsgbid.4	$⊢ φ \to \neg \{\underset{˙}{0}\} = B$
5		simpr	$⊢ (φ \land G \in SimpGrp) \to G \in SimpGrp$
6	1 2 5	simpgnsgd	$⊢ (φ \land G \in SimpGrp) \to NrmSGrp (G) = \{\{\underset{˙}{0}\}, B\}$
7	3	adantr	$⊢ (φ \land NrmSGrp (G) = \{\{\underset{˙}{0}\}, B\}) \to G \in Grp$
8	4	adantr	$⊢ (φ \land NrmSGrp (G) = \{\{\underset{˙}{0}\}, B\}) \to \neg \{\underset{˙}{0}\} = B$
9		simpr	$⊢ ((φ \land NrmSGrp (G) = \{\{\underset{˙}{0}\}, B\}) \land x \in NrmSGrp (G)) \to x \in NrmSGrp (G)$
10		simplr	$⊢ ((φ \land NrmSGrp (G) = \{\{\underset{˙}{0}\}, B\}) \land x \in NrmSGrp (G)) \to NrmSGrp (G) = \{\{\underset{˙}{0}\}, B\}$
11	9 10	eleqtrd	$⊢ ((φ \land NrmSGrp (G) = \{\{\underset{˙}{0}\}, B\}) \land x \in NrmSGrp (G)) \to x \in \{\{\underset{˙}{0}\}, B\}$
12		elpri	$⊢ x \in \{\{\underset{˙}{0}\}, B\} \to (x = \{\underset{˙}{0}\} \lor x = B)$
13	11 12	syl	$⊢ ((φ \land NrmSGrp (G) = \{\{\underset{˙}{0}\}, B\}) \land x \in NrmSGrp (G)) \to (x = \{\underset{˙}{0}\} \lor x = B)$
14	1 2 7 8 13	2nsgsimpgd	$⊢ (φ \land NrmSGrp (G) = \{\{\underset{˙}{0}\}, B\}) \to G \in SimpGrp$
15	6 14	impbida	$⊢ φ \to (G \in SimpGrp \leftrightarrow NrmSGrp (G) = \{\{\underset{˙}{0}\}, B\})$