Metamath Proof Explorer


Theorem grpsubpropd2

Description: Strong property deduction for the group subtraction operation. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Hypotheses grpsubpropd2.1 φ B = Base G
grpsubpropd2.2 φ B = Base H
grpsubpropd2.3 φ G Grp
grpsubpropd2.4 φ x B y B x + G y = x + H y
Assertion grpsubpropd2 φ - G = - H

Proof

Step Hyp Ref Expression
1 grpsubpropd2.1 φ B = Base G
2 grpsubpropd2.2 φ B = Base H
3 grpsubpropd2.3 φ G Grp
4 grpsubpropd2.4 φ x B y B x + G y = x + H y
5 simp1 φ a Base G b Base G φ
6 simp2 φ a Base G b Base G a Base G
7 1 3ad2ant1 φ a Base G b Base G B = Base G
8 6 7 eleqtrrd φ a Base G b Base G a B
9 3 3ad2ant1 φ a Base G b Base G G Grp
10 simp3 φ a Base G b Base G b Base G
11 eqid Base G = Base G
12 eqid inv g G = inv g G
13 11 12 grpinvcl G Grp b Base G inv g G b Base G
14 9 10 13 syl2anc φ a Base G b Base G inv g G b Base G
15 14 7 eleqtrrd φ a Base G b Base G inv g G b B
16 4 oveqrspc2v φ a B inv g G b B a + G inv g G b = a + H inv g G b
17 5 8 15 16 syl12anc φ a Base G b Base G a + G inv g G b = a + H inv g G b
18 1 2 4 grpinvpropd φ inv g G = inv g H
19 18 fveq1d φ inv g G b = inv g H b
20 19 oveq2d φ a + H inv g G b = a + H inv g H b
21 20 3ad2ant1 φ a Base G b Base G a + H inv g G b = a + H inv g H b
22 17 21 eqtrd φ a Base G b Base G a + G inv g G b = a + H inv g H b
23 22 mpoeq3dva φ a Base G , b Base G a + G inv g G b = a Base G , b Base G a + H inv g H b
24 1 2 eqtr3d φ Base G = Base H
25 mpoeq12 Base G = Base H Base G = Base H a Base G , b Base G a + H inv g H b = a Base H , b Base H a + H inv g H b
26 24 24 25 syl2anc φ a Base G , b Base G a + H inv g H b = a Base H , b Base H a + H inv g H b
27 23 26 eqtrd φ a Base G , b Base G a + G inv g G b = a Base H , b Base H a + H inv g H b
28 eqid + G = + G
29 eqid - G = - G
30 11 28 12 29 grpsubfval - G = a Base G , b Base G a + G inv g G b
31 eqid Base H = Base H
32 eqid + H = + H
33 eqid inv g H = inv g H
34 eqid - H = - H
35 31 32 33 34 grpsubfval - H = a Base H , b Base H a + H inv g H b
36 27 30 35 3eqtr4g φ - G = - H