Metamath Proof Explorer


Theorem qussub

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

Ref Expression
Hypotheses qusgrp.h H = G / 𝑠 G ~ QG S
qusinv.v V = Base G
qussub.p - ˙ = - G
qussub.a N = - H
Assertion qussub S NrmSGrp G X V Y V X G ~ QG S N Y G ~ QG S = X - ˙ Y G ~ QG S

Proof

Step Hyp Ref Expression
1 qusgrp.h H = G / 𝑠 G ~ QG S
2 qusinv.v V = Base G
3 qussub.p - ˙ = - G
4 qussub.a N = - H
5 eqid Base H = Base H
6 1 2 5 quseccl S NrmSGrp G X V X G ~ QG S Base H
7 6 3adant3 S NrmSGrp G X V Y V X G ~ QG S Base H
8 1 2 5 quseccl S NrmSGrp G Y V Y G ~ QG S Base H
9 eqid + H = + H
10 eqid inv g H = inv g H
11 5 9 10 4 grpsubval X G ~ QG S Base H Y G ~ QG S Base H X G ~ QG S N Y G ~ QG S = X G ~ QG S + H inv g H Y G ~ QG S
12 7 8 11 3imp3i2an S NrmSGrp G X V Y V X G ~ QG S N Y G ~ QG S = X G ~ QG S + H inv g H Y G ~ QG S
13 eqid inv g G = inv g G
14 1 2 13 10 qusinv S NrmSGrp G Y V inv g H Y G ~ QG S = inv g G Y G ~ QG S
15 14 3adant2 S NrmSGrp G X V Y V inv g H Y G ~ QG S = inv g G Y G ~ QG S
16 15 oveq2d S NrmSGrp G X V Y V X G ~ QG S + H inv g H Y G ~ QG S = X G ~ QG S + H inv g G Y G ~ QG S
17 nsgsubg S NrmSGrp G S SubGrp G
18 subgrcl S SubGrp G G Grp
19 17 18 syl S NrmSGrp G G Grp
20 2 13 grpinvcl G Grp Y V inv g G Y V
21 19 20 sylan S NrmSGrp G Y V inv g G Y V
22 21 3adant2 S NrmSGrp G X V Y V inv g G Y V
23 eqid + G = + G
24 1 2 23 9 qusadd S NrmSGrp G X V inv g G Y V X G ~ QG S + H inv g G Y G ~ QG S = X + G inv g G Y G ~ QG S
25 22 24 syld3an3 S NrmSGrp G X V Y V X G ~ QG S + H inv g G Y G ~ QG S = X + G inv g G Y G ~ QG S
26 2 23 13 3 grpsubval X V Y V X - ˙ Y = X + G inv g G Y
27 26 3adant1 S NrmSGrp G X V Y V X - ˙ Y = X + G inv g G Y
28 27 eceq1d S NrmSGrp G X V Y V X - ˙ Y G ~ QG S = X + G inv g G Y G ~ QG S
29 25 28 eqtr4d S NrmSGrp G X V Y V X G ~ QG S + H inv g G Y G ~ QG S = X - ˙ Y G ~ QG S
30 12 16 29 3eqtrd S NrmSGrp G X V Y V X G ~ QG S N Y G ~ QG S = X - ˙ Y G ~ QG S