This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ablsubsub4

Description: Law for double subtraction. (Contributed by NM, 7-Apr-2015)

Ref Expression
Hypotheses ablsubadd.b ⊢ B = Base G
ablsubadd.p ⊢ + ˙ = + G
ablsubadd.m ⊢ - ˙ = - G
ablsubsub.g ⊢ φ → G ∈ Abel
ablsubsub.x ⊢ φ → X ∈ B
ablsubsub.y ⊢ φ → Y ∈ B
ablsubsub.z ⊢ φ → Z ∈ B
Assertion ablsubsub4 ⊢ φ → X - ˙ Y - ˙ Z = X - ˙ Y + ˙ Z

Proof

Step Hyp Ref Expression
1 ablsubadd.b ⊢ B = Base G
2 ablsubadd.p ⊢ + ˙ = + G
3 ablsubadd.m ⊢ - ˙ = - G
4 ablsubsub.g ⊢ φ → G ∈ Abel
5 ablsubsub.x ⊢ φ → X ∈ B
6 ablsubsub.y ⊢ φ → Y ∈ B
7 ablsubsub.z ⊢ φ → Z ∈ B
8 ablgrp ⊢ G ∈ Abel → G ∈ Grp
9 4 8 syl ⊢ φ → G ∈ Grp
10 1 3 grpsubcl ⊢ G ∈ Grp ∧ X ∈ B ∧ Y ∈ B → X - ˙ Y ∈ B
11 9 5 6 10 syl3anc ⊢ φ → X - ˙ Y ∈ B
12 eqid ⊢ inv g ⁡ G = inv g ⁡ G
13 1 2 12 3 grpsubval ⊢ X - ˙ Y ∈ B ∧ Z ∈ B → X - ˙ Y - ˙ Z = X - ˙ Y + ˙ inv g ⁡ G ⁡ Z
14 11 7 13 syl2anc ⊢ φ → X - ˙ Y - ˙ Z = X - ˙ Y + ˙ inv g ⁡ G ⁡ Z
15 1 12 grpinvcl ⊢ G ∈ Grp ∧ Z ∈ B → inv g ⁡ G ⁡ Z ∈ B
16 9 7 15 syl2anc ⊢ φ → inv g ⁡ G ⁡ Z ∈ B
17 1 2 3 4 5 6 16 ablsubsub ⊢ φ → X - ˙ Y - ˙ inv g ⁡ G ⁡ Z = X - ˙ Y + ˙ inv g ⁡ G ⁡ Z
18 1 2 3 12 9 6 7 grpsubinv ⊢ φ → Y - ˙ inv g ⁡ G ⁡ Z = Y + ˙ Z
19 18 oveq2d ⊢ φ → X - ˙ Y - ˙ inv g ⁡ G ⁡ Z = X - ˙ Y + ˙ Z
20 14 17 19 3eqtr2d ⊢ φ → X - ˙ Y - ˙ Z = X - ˙ Y + ˙ Z