Metamath Proof Explorer


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 / 𝑠 G ~ QG S
qus0.p 0 ˙ = 0 G
Assertion qus0 S NrmSGrp G 0 ˙ G ~ QG S = 0 H

Proof

Step Hyp Ref Expression
1 qusgrp.h H = G / 𝑠 G ~ QG S
2 qus0.p 0 ˙ = 0 G
3 nsgsubg S NrmSGrp G S SubGrp G
4 subgrcl S SubGrp G G Grp
5 3 4 syl S NrmSGrp G G Grp
6 eqid Base G = Base G
7 6 2 grpidcl G Grp 0 ˙ Base G
8 5 7 syl S NrmSGrp G 0 ˙ Base G
9 eqid + G = + G
10 eqid + H = + H
11 1 6 9 10 qusadd S NrmSGrp G 0 ˙ Base G 0 ˙ Base G 0 ˙ G ~ QG S + H 0 ˙ G ~ QG S = 0 ˙ + G 0 ˙ G ~ QG S
12 8 8 11 mpd3an23 S NrmSGrp G 0 ˙ G ~ QG S + H 0 ˙ G ~ QG S = 0 ˙ + G 0 ˙ G ~ QG S
13 6 9 2 grplid G Grp 0 ˙ Base G 0 ˙ + G 0 ˙ = 0 ˙
14 5 8 13 syl2anc S NrmSGrp G 0 ˙ + G 0 ˙ = 0 ˙
15 14 eceq1d S NrmSGrp G 0 ˙ + G 0 ˙ G ~ QG S = 0 ˙ G ~ QG S
16 12 15 eqtrd S NrmSGrp G 0 ˙ G ~ QG S + H 0 ˙ G ~ QG S = 0 ˙ G ~ QG S
17 1 qusgrp S NrmSGrp G H Grp
18 eqid Base H = Base H
19 1 6 18 quseccl S NrmSGrp G 0 ˙ Base G 0 ˙ G ~ QG S Base H
20 8 19 mpdan S NrmSGrp G 0 ˙ G ~ QG S Base H
21 eqid 0 H = 0 H
22 18 10 21 grpid H Grp 0 ˙ G ~ QG S Base H 0 ˙ G ~ QG S + H 0 ˙ G ~ QG S = 0 ˙ G ~ QG S 0 H = 0 ˙ G ~ QG S
23 17 20 22 syl2anc S NrmSGrp G 0 ˙ G ~ QG S + H 0 ˙ G ~ QG S = 0 ˙ G ~ QG S 0 H = 0 ˙ G ~ QG S
24 16 23 mpbid S NrmSGrp G 0 H = 0 ˙ G ~ QG S
25 24 eqcomd S NrmSGrp G 0 ˙ G ~ QG S = 0 H