qus0g

Description: The identity element of a quotient group. (Contributed by Thierry Arnoux, 13-Mar-2025)

		Ref	Expression
	Hypothesis	qus0g.1	$⊢ Q = G /_{𝑠} (G ~_{QG} N)$
	Assertion	qus0g	$⊢ N \in NrmSGrp (G) \to 0_{Q} = N$

Step	Hyp	Ref	Expression
1		qus0g.1	$⊢ Q = G /_{𝑠} (G ~_{QG} N)$
2		eqid	$⊢ {Base}_{G} = {Base}_{G}$
3		eqid	$⊢ LSSum (G) = LSSum (G)$
4		nsgsubg	$⊢ N \in NrmSGrp (G) \to N \in SubGrp (G)$
5		subgrcl	$⊢ N \in SubGrp (G) \to G \in Grp$
6		eqid	$⊢ 0_{G} = 0_{G}$
7	2 6	grpidcl	$⊢ G \in Grp \to 0_{G} \in {Base}_{G}$
8	4 5 7	3syl	$⊢ N \in NrmSGrp (G) \to 0_{G} \in {Base}_{G}$
9	2 3 4 8	quslsm	$⊢ N \in NrmSGrp (G) \to [0_{G}] (G ~_{QG} N) = \{0_{G}\} LSSum (G) N$
10	1 6	qus0	$⊢ N \in NrmSGrp (G) \to [0_{G}] (G ~_{QG} N) = 0_{Q}$
11	6 3	lsm02	$⊢ N \in SubGrp (G) \to \{0_{G}\} LSSum (G) N = N$
12	4 11	syl	$⊢ N \in NrmSGrp (G) \to \{0_{G}\} LSSum (G) N = N$
13	9 10 12	3eqtr3d	$⊢ N \in NrmSGrp (G) \to 0_{Q} = N$

Metamath Proof Explorer