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