Metamath Proof Explorer


Theorem ablsub2inv

Description: Abelian group subtraction of two inverses. (Contributed by Stefan O'Rear, 24-May-2015)

Ref Expression
Hypotheses ablsub2inv.b B = Base G
ablsub2inv.m - ˙ = - G
ablsub2inv.n N = inv g G
ablsub2inv.g φ G Abel
ablsub2inv.x φ X B
ablsub2inv.y φ Y B
Assertion ablsub2inv φ N X - ˙ N Y = Y - ˙ X

Proof

Step Hyp Ref Expression
1 ablsub2inv.b B = Base G
2 ablsub2inv.m - ˙ = - G
3 ablsub2inv.n N = inv g G
4 ablsub2inv.g φ G Abel
5 ablsub2inv.x φ X B
6 ablsub2inv.y φ Y B
7 eqid + G = + G
8 ablgrp G Abel G Grp
9 4 8 syl φ G Grp
10 1 3 grpinvcl G Grp X B N X B
11 9 5 10 syl2anc φ N X B
12 1 7 2 3 9 11 6 grpsubinv φ N X - ˙ N Y = N X + G Y
13 1 7 ablcom G Abel N X B Y B N X + G Y = Y + G N X
14 4 11 6 13 syl3anc φ N X + G Y = Y + G N X
15 1 3 grpinvinv G Grp Y B N N Y = Y
16 9 6 15 syl2anc φ N N Y = Y
17 16 oveq1d φ N N Y + G N X = Y + G N X
18 14 17 eqtr4d φ N X + G Y = N N Y + G N X
19 1 3 grpinvcl G Grp Y B N Y B
20 9 6 19 syl2anc φ N Y B
21 1 7 3 grpinvadd G Grp X B N Y B N X + G N Y = N N Y + G N X
22 9 5 20 21 syl3anc φ N X + G N Y = N N Y + G N X
23 18 22 eqtr4d φ N X + G Y = N X + G N Y
24 1 7 3 2 grpsubval X B Y B X - ˙ Y = X + G N Y
25 5 6 24 syl2anc φ X - ˙ Y = X + G N Y
26 25 fveq2d φ N X - ˙ Y = N X + G N Y
27 23 26 eqtr4d φ N X + G Y = N X - ˙ Y
28 1 2 3 grpinvsub G Grp X B Y B N X - ˙ Y = Y - ˙ X
29 9 5 6 28 syl3anc φ N X - ˙ Y = Y - ˙ X
30 12 27 29 3eqtrd φ N X - ˙ N Y = Y - ˙ X