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

Metamath Proof Explorer

Theorem hvaddcani

Description: Cancellation law for vector addition. (Contributed by NM, 11-Sep-1999) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 hvnegdi.1 ⊢ 𝐴 ∈ ℋ
2 hvnegdi.2 ⊢ 𝐵 ∈ ℋ
3 hvaddcan.3 ⊢ 𝐶 ∈ ℋ
4 oveq1 ⊢ ( ( 𝐴 +ℎ 𝐵 ) = ( 𝐴 +ℎ 𝐶 ) → ( ( 𝐴 +ℎ 𝐵 ) +ℎ ( - 1 ·ℎ 𝐴 ) ) = ( ( 𝐴 +ℎ 𝐶 ) +ℎ ( - 1 ·ℎ 𝐴 ) ) )
5 neg1cn ⊢ - 1 ∈ ℂ
6 5 1 hvmulcli ⊢ ( - 1 ·ℎ 𝐴 ) ∈ ℋ
7 1 2 6 hvadd32i ⊢ ( ( 𝐴 +ℎ 𝐵 ) +ℎ ( - 1 ·ℎ 𝐴 ) ) = ( ( 𝐴 +ℎ ( - 1 ·ℎ 𝐴 ) ) +ℎ 𝐵 )
8 1 hvnegidi ⊢ ( 𝐴 +ℎ ( - 1 ·ℎ 𝐴 ) ) = 0ℎ
9 8 oveq1i ⊢ ( ( 𝐴 +ℎ ( - 1 ·ℎ 𝐴 ) ) +ℎ 𝐵 ) = ( 0ℎ +ℎ 𝐵 )
10 2 hvaddlidi ⊢ ( 0ℎ +ℎ 𝐵 ) = 𝐵
11 7 9 10 3eqtri ⊢ ( ( 𝐴 +ℎ 𝐵 ) +ℎ ( - 1 ·ℎ 𝐴 ) ) = 𝐵
12 1 3 6 hvadd32i ⊢ ( ( 𝐴 +ℎ 𝐶 ) +ℎ ( - 1 ·ℎ 𝐴 ) ) = ( ( 𝐴 +ℎ ( - 1 ·ℎ 𝐴 ) ) +ℎ 𝐶 )
13 8 oveq1i ⊢ ( ( 𝐴 +ℎ ( - 1 ·ℎ 𝐴 ) ) +ℎ 𝐶 ) = ( 0ℎ +ℎ 𝐶 )
14 3 hvaddlidi ⊢ ( 0ℎ +ℎ 𝐶 ) = 𝐶
15 12 13 14 3eqtri ⊢ ( ( 𝐴 +ℎ 𝐶 ) +ℎ ( - 1 ·ℎ 𝐴 ) ) = 𝐶
16 4 11 15 3eqtr3g ⊢ ( ( 𝐴 +ℎ 𝐵 ) = ( 𝐴 +ℎ 𝐶 ) → 𝐵 = 𝐶 )
17 oveq2 ⊢ ( 𝐵 = 𝐶 → ( 𝐴 +ℎ 𝐵 ) = ( 𝐴 +ℎ 𝐶 ) )
18 16 17 impbii ⊢ ( ( 𝐴 +ℎ 𝐵 ) = ( 𝐴 +ℎ 𝐶 ) ↔ 𝐵 = 𝐶 )