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

Metamath Proof Explorer

Theorem hvsubcan2i

Description: Vector cancellation law. (Contributed by NM, 3-Sep-1999) (New usage is discouraged.)

Ref Expression
Hypotheses hvnegdi.1 ⊢ 𝐴 ∈ ℋ
hvnegdi.2 ⊢ 𝐵 ∈ ℋ
Assertion hvsubcan2i ( ( 𝐴 +ℎ 𝐵 ) +ℎ ( 𝐴 −ℎ 𝐵 ) ) = ( 2 ·ℎ 𝐴 )

Proof

Step Hyp Ref Expression
1 hvnegdi.1 ⊢ 𝐴 ∈ ℋ
2 hvnegdi.2 ⊢ 𝐵 ∈ ℋ
3 1 2 hvsubvali ⊢ ( 𝐴 −ℎ 𝐵 ) = ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) )
4 3 oveq2i ⊢ ( ( 𝐴 +ℎ 𝐵 ) +ℎ ( 𝐴 −ℎ 𝐵 ) ) = ( ( 𝐴 +ℎ 𝐵 ) +ℎ ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) )
5 neg1cn ⊢ - 1 ∈ ℂ
6 5 2 hvmulcli ⊢ ( - 1 ·ℎ 𝐵 ) ∈ ℋ
7 1 2 1 6 hvadd4i ⊢ ( ( 𝐴 +ℎ 𝐵 ) +ℎ ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) ) = ( ( 𝐴 +ℎ 𝐴 ) +ℎ ( 𝐵 +ℎ ( - 1 ·ℎ 𝐵 ) ) )
8 hv2times ⊢ ( 𝐴 ∈ ℋ → ( 2 ·ℎ 𝐴 ) = ( 𝐴 +ℎ 𝐴 ) )
9 1 8 ax-mp ⊢ ( 2 ·ℎ 𝐴 ) = ( 𝐴 +ℎ 𝐴 )
10 9 eqcomi ⊢ ( 𝐴 +ℎ 𝐴 ) = ( 2 ·ℎ 𝐴 )
11 2 hvnegidi ⊢ ( 𝐵 +ℎ ( - 1 ·ℎ 𝐵 ) ) = 0ℎ
12 10 11 oveq12i ⊢ ( ( 𝐴 +ℎ 𝐴 ) +ℎ ( 𝐵 +ℎ ( - 1 ·ℎ 𝐵 ) ) ) = ( ( 2 ·ℎ 𝐴 ) +ℎ 0ℎ )
13 7 12 eqtri ⊢ ( ( 𝐴 +ℎ 𝐵 ) +ℎ ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) ) = ( ( 2 ·ℎ 𝐴 ) +ℎ 0ℎ )
14 2cn ⊢ 2 ∈ ℂ
15 14 1 hvmulcli ⊢ ( 2 ·ℎ 𝐴 ) ∈ ℋ
16 ax-hvaddid ⊢ ( ( 2 ·ℎ 𝐴 ) ∈ ℋ → ( ( 2 ·ℎ 𝐴 ) +ℎ 0ℎ ) = ( 2 ·ℎ 𝐴 ) )
17 15 16 ax-mp ⊢ ( ( 2 ·ℎ 𝐴 ) +ℎ 0ℎ ) = ( 2 ·ℎ 𝐴 )
18 13 17 eqtri ⊢ ( ( 𝐴 +ℎ 𝐵 ) +ℎ ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) ) = ( 2 ·ℎ 𝐴 )
19 4 18 eqtri ⊢ ( ( 𝐴 +ℎ 𝐵 ) +ℎ ( 𝐴 −ℎ 𝐵 ) ) = ( 2 ·ℎ 𝐴 )