Metamath Proof Explorer


Theorem ablnnncan

Description: Cancellation law for group subtraction. ( nnncan analog.) (Contributed by NM, 29-Feb-2008) (Revised by AV, 27-Aug-2021)

Ref Expression
Hypotheses ablnncan.b B = Base G
ablnncan.m - ˙ = - G
ablnncan.g φ G Abel
ablnncan.x φ X B
ablnncan.y φ Y B
ablsub32.z φ Z B
Assertion ablnnncan φ X - ˙ Y - ˙ Z - ˙ Z = X - ˙ Y

Proof

Step Hyp Ref Expression
1 ablnncan.b B = Base G
2 ablnncan.m - ˙ = - G
3 ablnncan.g φ G Abel
4 ablnncan.x φ X B
5 ablnncan.y φ Y B
6 ablsub32.z φ Z B
7 eqid + G = + G
8 ablgrp G Abel G Grp
9 3 8 syl φ G Grp
10 1 2 grpsubcl G Grp Y B Z B Y - ˙ Z B
11 9 5 6 10 syl3anc φ Y - ˙ Z B
12 1 7 2 3 4 11 6 ablsubsub4 φ X - ˙ Y - ˙ Z - ˙ Z = X - ˙ Y - ˙ Z + G Z
13 1 7 ablcom G Abel Y - ˙ Z B Z B Y - ˙ Z + G Z = Z + G Y - ˙ Z
14 3 11 6 13 syl3anc φ Y - ˙ Z + G Z = Z + G Y - ˙ Z
15 1 7 2 ablpncan3 G Abel Z B Y B Z + G Y - ˙ Z = Y
16 3 6 5 15 syl12anc φ Z + G Y - ˙ Z = Y
17 14 16 eqtrd φ Y - ˙ Z + G Z = Y
18 17 oveq2d φ X - ˙ Y - ˙ Z + G Z = X - ˙ Y
19 12 18 eqtrd φ X - ˙ Y - ˙ Z - ˙ Z = X - ˙ Y