Metamath Proof Explorer


Theorem ablsub32

Description: Swap the second and third terms in a double group subtraction. (Contributed by NM, 7-Apr-2015)

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 ablsub32 φ X - ˙ Y - ˙ Z = X - ˙ Z - ˙ 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 1 7 ablcom G Abel Y B Z B Y + G Z = Z + G Y
9 3 5 6 8 syl3anc φ Y + G Z = Z + G Y
10 9 oveq2d φ X - ˙ Y + G Z = X - ˙ Z + G Y
11 1 7 2 3 4 5 6 ablsubsub4 φ X - ˙ Y - ˙ Z = X - ˙ Y + G Z
12 1 7 2 3 4 6 5 ablsubsub4 φ X - ˙ Z - ˙ Y = X - ˙ Z + G Y
13 10 11 12 3eqtr4d φ X - ˙ Y - ˙ Z = X - ˙ Z - ˙ Y