nsgqus0

Description: A normal subgroup N is a member of all subgroups F of the quotient group by N . In fact, it is the identity element of the quotient group. (Contributed by Thierry Arnoux, 27-Jul-2024)

		Ref	Expression
	Hypothesis	nsgqus0.q	$⊢ Q = G /_{𝑠} (G ~_{QG} N)$
	Assertion	nsgqus0	$⊢ (N \in NrmSGrp (G) \land F \in SubGrp (Q)) \to N \in F$

Proof

Step	Hyp	Ref	Expression
1		nsgqus0.q	$⊢ Q = G /_{𝑠} (G ~_{QG} N)$
2		simpl	$⊢ (N \in NrmSGrp (G) \land F \in SubGrp (Q)) \to N \in NrmSGrp (G)$
3		nsgsubg	$⊢ N \in NrmSGrp (G) \to N \in SubGrp (G)$
4		eqid	$⊢ 0_{G} = 0_{G}$
5		eqid	$⊢ LSSum (G) = LSSum (G)$
6	4 5	lsm02	$⊢ N \in SubGrp (G) \to \{0_{G}\} LSSum (G) N = N$
7	2 3 6	3syl	$⊢ (N \in NrmSGrp (G) \land F \in SubGrp (Q)) \to \{0_{G}\} LSSum (G) N = N$
8	1 4	qus0	$⊢ N \in NrmSGrp (G) \to [0_{G}] (G ~_{QG} N) = 0_{Q}$
9	8	adantr	$⊢ (N \in NrmSGrp (G) \land F \in SubGrp (Q)) \to [0_{G}] (G ~_{QG} N) = 0_{Q}$
10		eqid	$⊢ {Base}_{G} = {Base}_{G}$
11	3	adantr	$⊢ (N \in NrmSGrp (G) \land F \in SubGrp (Q)) \to N \in SubGrp (G)$
12		subgrcl	$⊢ N \in SubGrp (G) \to G \in Grp$
13	3 12	syl	$⊢ N \in NrmSGrp (G) \to G \in Grp$
14	13	adantr	$⊢ (N \in NrmSGrp (G) \land F \in SubGrp (Q)) \to G \in Grp$
15	10 4	grpidcl	$⊢ G \in Grp \to 0_{G} \in {Base}_{G}$
16	14 15	syl	$⊢ (N \in NrmSGrp (G) \land F \in SubGrp (Q)) \to 0_{G} \in {Base}_{G}$
17	10 5 11 16	quslsm	$⊢ (N \in NrmSGrp (G) \land F \in SubGrp (Q)) \to [0_{G}] (G ~_{QG} N) = \{0_{G}\} LSSum (G) N$
18	9 17	eqtr3d	$⊢ (N \in NrmSGrp (G) \land F \in SubGrp (Q)) \to 0_{Q} = \{0_{G}\} LSSum (G) N$
19		eqid	$⊢ 0_{Q} = 0_{Q}$
20	19	subg0cl	$⊢ F \in SubGrp (Q) \to 0_{Q} \in F$
21	20	adantl	$⊢ (N \in NrmSGrp (G) \land F \in SubGrp (Q)) \to 0_{Q} \in F$
22	18 21	eqeltrrd	$⊢ (N \in NrmSGrp (G) \land F \in SubGrp (Q)) \to \{0_{G}\} LSSum (G) N \in F$
23	7 22	eqeltrrd	$⊢ (N \in NrmSGrp (G) \land F \in SubGrp (Q)) \to N \in F$

Metamath Proof Explorer

Theorem nsgqus0

Proof