Metamath Proof Explorer


Theorem grpsubadd

Description: Relationship between group subtraction and addition. (Contributed by NM, 31-Mar-2014)

Ref Expression
Hypotheses grpsubadd.b B = Base G
grpsubadd.p + ˙ = + G
grpsubadd.m - ˙ = - G
Assertion grpsubadd G Grp X B Y B Z B X - ˙ Y = Z Z + ˙ Y = X

Proof

Step Hyp Ref Expression
1 grpsubadd.b B = Base G
2 grpsubadd.p + ˙ = + G
3 grpsubadd.m - ˙ = - G
4 eqid inv g G = inv g G
5 1 2 4 3 grpsubval X B Y B X - ˙ Y = X + ˙ inv g G Y
6 5 3adant3 X B Y B Z B X - ˙ Y = X + ˙ inv g G Y
7 6 adantl G Grp X B Y B Z B X - ˙ Y = X + ˙ inv g G Y
8 7 eqeq1d G Grp X B Y B Z B X - ˙ Y = Z X + ˙ inv g G Y = Z
9 simpl G Grp X B Y B Z B G Grp
10 simpr1 G Grp X B Y B Z B X B
11 1 4 grpinvcl G Grp Y B inv g G Y B
12 11 3ad2antr2 G Grp X B Y B Z B inv g G Y B
13 1 2 grpcl G Grp X B inv g G Y B X + ˙ inv g G Y B
14 9 10 12 13 syl3anc G Grp X B Y B Z B X + ˙ inv g G Y B
15 simpr3 G Grp X B Y B Z B Z B
16 simpr2 G Grp X B Y B Z B Y B
17 1 2 grprcan G Grp X + ˙ inv g G Y B Z B Y B X + ˙ inv g G Y + ˙ Y = Z + ˙ Y X + ˙ inv g G Y = Z
18 9 14 15 16 17 syl13anc G Grp X B Y B Z B X + ˙ inv g G Y + ˙ Y = Z + ˙ Y X + ˙ inv g G Y = Z
19 1 2 grpass G Grp X B inv g G Y B Y B X + ˙ inv g G Y + ˙ Y = X + ˙ inv g G Y + ˙ Y
20 9 10 12 16 19 syl13anc G Grp X B Y B Z B X + ˙ inv g G Y + ˙ Y = X + ˙ inv g G Y + ˙ Y
21 eqid 0 G = 0 G
22 1 2 21 4 grplinv G Grp Y B inv g G Y + ˙ Y = 0 G
23 22 3ad2antr2 G Grp X B Y B Z B inv g G Y + ˙ Y = 0 G
24 23 oveq2d G Grp X B Y B Z B X + ˙ inv g G Y + ˙ Y = X + ˙ 0 G
25 1 2 21 grprid G Grp X B X + ˙ 0 G = X
26 25 3ad2antr1 G Grp X B Y B Z B X + ˙ 0 G = X
27 20 24 26 3eqtrd G Grp X B Y B Z B X + ˙ inv g G Y + ˙ Y = X
28 27 eqeq1d G Grp X B Y B Z B X + ˙ inv g G Y + ˙ Y = Z + ˙ Y X = Z + ˙ Y
29 8 18 28 3bitr2d G Grp X B Y B Z B X - ˙ Y = Z X = Z + ˙ Y
30 eqcom X = Z + ˙ Y Z + ˙ Y = X
31 29 30 bitrdi G Grp X B Y B Z B X - ˙ Y = Z Z + ˙ Y = X