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

Metamath Proof Explorer

Theorem hvsubaddi

Description: Relationship between vector subtraction and addition. (Contributed by NM, 11-Sep-1999) (New usage is discouraged.)

Ref Expression
Hypotheses hvnegdi.1 ⊢ 𝐴 ∈ ℋ
hvnegdi.2 ⊢ 𝐵 ∈ ℋ
hvaddcan.3 ⊢ 𝐶 ∈ ℋ
Assertion hvsubaddi ( ( 𝐴 −ℎ 𝐵 ) = 𝐶 ↔ ( 𝐵 +ℎ 𝐶 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 hvnegdi.1 ⊢ 𝐴 ∈ ℋ
2 hvnegdi.2 ⊢ 𝐵 ∈ ℋ
3 hvaddcan.3 ⊢ 𝐶 ∈ ℋ
4 1 2 hvsubvali ⊢ ( 𝐴 −ℎ 𝐵 ) = ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) )
5 4 eqeq1i ⊢ ( ( 𝐴 −ℎ 𝐵 ) = 𝐶 ↔ ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) = 𝐶 )
6 neg1cn ⊢ - 1 ∈ ℂ
7 6 2 hvmulcli ⊢ ( - 1 ·ℎ 𝐵 ) ∈ ℋ
8 2 1 7 hvadd12i ⊢ ( 𝐵 +ℎ ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) ) = ( 𝐴 +ℎ ( 𝐵 +ℎ ( - 1 ·ℎ 𝐵 ) ) )
9 2 hvnegidi ⊢ ( 𝐵 +ℎ ( - 1 ·ℎ 𝐵 ) ) = 0ℎ
10 9 oveq2i ⊢ ( 𝐴 +ℎ ( 𝐵 +ℎ ( - 1 ·ℎ 𝐵 ) ) ) = ( 𝐴 +ℎ 0ℎ )
11 ax-hvaddid ⊢ ( 𝐴 ∈ ℋ → ( 𝐴 +ℎ 0ℎ ) = 𝐴 )
12 1 11 ax-mp ⊢ ( 𝐴 +ℎ 0ℎ ) = 𝐴
13 8 10 12 3eqtri ⊢ ( 𝐵 +ℎ ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) ) = 𝐴
14 13 eqeq1i ⊢ ( ( 𝐵 +ℎ ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) ) = ( 𝐵 +ℎ 𝐶 ) ↔ 𝐴 = ( 𝐵 +ℎ 𝐶 ) )
15 1 7 hvaddcli ⊢ ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) ∈ ℋ
16 2 15 3 hvaddcani ⊢ ( ( 𝐵 +ℎ ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) ) = ( 𝐵 +ℎ 𝐶 ) ↔ ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) = 𝐶 )
17 eqcom ⊢ ( 𝐴 = ( 𝐵 +ℎ 𝐶 ) ↔ ( 𝐵 +ℎ 𝐶 ) = 𝐴 )
18 14 16 17 3bitr3i ⊢ ( ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) = 𝐶 ↔ ( 𝐵 +ℎ 𝐶 ) = 𝐴 )
19 5 18 bitri ⊢ ( ( 𝐴 −ℎ 𝐵 ) = 𝐶 ↔ ( 𝐵 +ℎ 𝐶 ) = 𝐴 )