Theorem qus0

Description: Value of the group identity operation in a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015)

	Ref	Expression
Hypotheses	qusgrp.h	$$⊢H=G{/}_{𝑠}\left(G{~}_{\mathit{QG}}S\right)$$
	qus0.p	$$⊢\underset{\dot{}}{0}=0_G$$
Assertion	qus0	$$⊢S\in \mathrm{NrmSGrp}\left(G\right)\to \left[\underset{\dot{}}{0}\right]\left(G{~}_{\mathit{QG}}S\right)=0_H$$

Proof

Step	Hyp	Ref	Expression
1		qusgrp.h	$$⊢H=G{/}_{𝑠}\left(G{~}_{\mathit{QG}}S\right)$$
2		qus0.p	$$⊢\underset{\dot{}}{0}=0_G$$
3		nsgsubg	$$⊢S\in \mathrm{NrmSGrp}\left(G\right)\to S\in \mathrm{SubGrp}\left(G\right)$$
4		subgrcl	$$⊢S\in \mathrm{SubGrp}\left(G\right)\to G\in \mathrm{Grp}$$
5	3 4	syl	$$⊢S\in \mathrm{NrmSGrp}\left(G\right)\to G\in \mathrm{Grp}$$
6		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
7	6 2	grpidcl	$$⊢G\in \mathrm{Grp}\to \underset{\dot{}}{0}\in {\mathrm{Base}}_G$$
8	5 7	syl	$$⊢S\in \mathrm{NrmSGrp}\left(G\right)\to \underset{\dot{}}{0}\in {\mathrm{Base}}_G$$
9		eqid	$$⊢{+}_G={+}_G$$
10		eqid	$$⊢{+}_H={+}_H$$
11	1 6 9 10	qusadd	$$⊢\left(S\in \mathrm{NrmSGrp}\left(G\right)\wedge \underset{\dot{}}{0}\in {\mathrm{Base}}_G\wedge \underset{\dot{}}{0}\in {\mathrm{Base}}_G\right)\to \left[\underset{\dot{}}{0}\right]\left(G{~}_{\mathit{QG}}S\right){+}_H\left[\underset{\dot{}}{0}\right]\left(G{~}_{\mathit{QG}}S\right)=\left[\left(\underset{\dot{}}{0}{+}_G\underset{\dot{}}{0}\right)\right]\left(G{~}_{\mathit{QG}}S\right)$$
12	8 8 11	mpd3an23	$$⊢S\in \mathrm{NrmSGrp}\left(G\right)\to \left[\underset{\dot{}}{0}\right]\left(G{~}_{\mathit{QG}}S\right){+}_H\left[\underset{\dot{}}{0}\right]\left(G{~}_{\mathit{QG}}S\right)=\left[\left(\underset{\dot{}}{0}{+}_G\underset{\dot{}}{0}\right)\right]\left(G{~}_{\mathit{QG}}S\right)$$
13	6 9 2	grplid	$$⊢\left(G\in \mathrm{Grp}\wedge \underset{\dot{}}{0}\in {\mathrm{Base}}_G\right)\to \underset{\dot{}}{0}{+}_G\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
14	5 8 13	syl2anc	$$⊢S\in \mathrm{NrmSGrp}\left(G\right)\to \underset{\dot{}}{0}{+}_G\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
15	14	eceq1d	$$⊢S\in \mathrm{NrmSGrp}\left(G\right)\to \left[\left(\underset{\dot{}}{0}{+}_G\underset{\dot{}}{0}\right)\right]\left(G{~}_{\mathit{QG}}S\right)=\left[\underset{\dot{}}{0}\right]\left(G{~}_{\mathit{QG}}S\right)$$
16	12 15	eqtrd	$$⊢S\in \mathrm{NrmSGrp}\left(G\right)\to \left[\underset{\dot{}}{0}\right]\left(G{~}_{\mathit{QG}}S\right){+}_H\left[\underset{\dot{}}{0}\right]\left(G{~}_{\mathit{QG}}S\right)=\left[\underset{\dot{}}{0}\right]\left(G{~}_{\mathit{QG}}S\right)$$
17	1	qusgrp	$$⊢S\in \mathrm{NrmSGrp}\left(G\right)\to H\in \mathrm{Grp}$$
18		eqid	$$⊢{\mathrm{Base}}_H={\mathrm{Base}}_H$$
19	1 6 18	quseccl	$$⊢\left(S\in \mathrm{NrmSGrp}\left(G\right)\wedge \underset{\dot{}}{0}\in {\mathrm{Base}}_G\right)\to \left[\underset{\dot{}}{0}\right]\left(G{~}_{\mathit{QG}}S\right)\in {\mathrm{Base}}_H$$
20	8 19	mpdan	$$⊢S\in \mathrm{NrmSGrp}\left(G\right)\to \left[\underset{\dot{}}{0}\right]\left(G{~}_{\mathit{QG}}S\right)\in {\mathrm{Base}}_H$$
21		eqid	$$⊢0_H=0_H$$
22	18 10 21	grpid	$$⊢\left(H\in \mathrm{Grp}\wedge \left[\underset{\dot{}}{0}\right]\left(G{~}_{\mathit{QG}}S\right)\in {\mathrm{Base}}_H\right)\to \left(\left[\underset{\dot{}}{0}\right]\left(G{~}_{\mathit{QG}}S\right){+}_H\left[\underset{\dot{}}{0}\right]\left(G{~}_{\mathit{QG}}S\right)=\left[\underset{\dot{}}{0}\right]\left(G{~}_{\mathit{QG}}S\right)\leftrightarrow 0_H=\left[\underset{\dot{}}{0}\right]\left(G{~}_{\mathit{QG}}S\right)\right)$$
23	17 20 22	syl2anc	$$⊢S\in \mathrm{NrmSGrp}\left(G\right)\to \left(\left[\underset{\dot{}}{0}\right]\left(G{~}_{\mathit{QG}}S\right){+}_H\left[\underset{\dot{}}{0}\right]\left(G{~}_{\mathit{QG}}S\right)=\left[\underset{\dot{}}{0}\right]\left(G{~}_{\mathit{QG}}S\right)\leftrightarrow 0_H=\left[\underset{\dot{}}{0}\right]\left(G{~}_{\mathit{QG}}S\right)\right)$$
24	16 23	mpbid	$$⊢S\in \mathrm{NrmSGrp}\left(G\right)\to 0_H=\left[\underset{\dot{}}{0}\right]\left(G{~}_{\mathit{QG}}S\right)$$
25	24	eqcomd	$$⊢S\in \mathrm{NrmSGrp}\left(G\right)\to \left[\underset{\dot{}}{0}\right]\left(G{~}_{\mathit{QG}}S\right)=0_H$$