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

Metamath Proof Explorer

Theorem his2sub

Description: Distributive law for inner product of vector subtraction. (Contributed by NM, 16-Nov-1999) (New usage is discouraged.)

Ref Expression
Assertion his2sub ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) = ( ( 𝐴 ·ih 𝐶 ) − ( 𝐵 ·ih 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 hvsubval ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 −ℎ 𝐵 ) = ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) )
2 1 oveq1d ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) = ( ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) ·ih 𝐶 ) )
3 2 3adant3 ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) = ( ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) ·ih 𝐶 ) )
4 neg1cn ⊢ - 1 ∈ ℂ
5 hvmulcl ⊢ ( ( - 1 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( - 1 ·ℎ 𝐵 ) ∈ ℋ )
6 4 5 mpan ⊢ ( 𝐵 ∈ ℋ → ( - 1 ·ℎ 𝐵 ) ∈ ℋ )
7 ax-his2 ⊢ ( ( 𝐴 ∈ ℋ ∧ ( - 1 ·ℎ 𝐵 ) ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) ·ih 𝐶 ) = ( ( 𝐴 ·ih 𝐶 ) + ( ( - 1 ·ℎ 𝐵 ) ·ih 𝐶 ) ) )
8 6 7 syl3an2 ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) ·ih 𝐶 ) = ( ( 𝐴 ·ih 𝐶 ) + ( ( - 1 ·ℎ 𝐵 ) ·ih 𝐶 ) ) )
9 ax-his3 ⊢ ( ( - 1 ∈ ℂ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( - 1 ·ℎ 𝐵 ) ·ih 𝐶 ) = ( - 1 · ( 𝐵 ·ih 𝐶 ) ) )
10 4 9 mp3an1 ⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( - 1 ·ℎ 𝐵 ) ·ih 𝐶 ) = ( - 1 · ( 𝐵 ·ih 𝐶 ) ) )
11 hicl ⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝐵 ·ih 𝐶 ) ∈ ℂ )
12 11 mulm1d ⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( - 1 · ( 𝐵 ·ih 𝐶 ) ) = - ( 𝐵 ·ih 𝐶 ) )
13 10 12 eqtrd ⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( - 1 ·ℎ 𝐵 ) ·ih 𝐶 ) = - ( 𝐵 ·ih 𝐶 ) )
14 13 oveq2d ⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 ·ih 𝐶 ) + ( ( - 1 ·ℎ 𝐵 ) ·ih 𝐶 ) ) = ( ( 𝐴 ·ih 𝐶 ) + - ( 𝐵 ·ih 𝐶 ) ) )
15 14 3adant1 ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 ·ih 𝐶 ) + ( ( - 1 ·ℎ 𝐵 ) ·ih 𝐶 ) ) = ( ( 𝐴 ·ih 𝐶 ) + - ( 𝐵 ·ih 𝐶 ) ) )
16 8 15 eqtrd ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) ·ih 𝐶 ) = ( ( 𝐴 ·ih 𝐶 ) + - ( 𝐵 ·ih 𝐶 ) ) )
17 hicl ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝐴 ·ih 𝐶 ) ∈ ℂ )
18 17 3adant2 ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝐴 ·ih 𝐶 ) ∈ ℂ )
19 11 3adant1 ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝐵 ·ih 𝐶 ) ∈ ℂ )
20 18 19 negsubd ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 ·ih 𝐶 ) + - ( 𝐵 ·ih 𝐶 ) ) = ( ( 𝐴 ·ih 𝐶 ) − ( 𝐵 ·ih 𝐶 ) ) )
21 3 16 20 3eqtrd ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 −ℎ 𝐵 ) ·ih 𝐶 ) = ( ( 𝐴 ·ih 𝐶 ) − ( 𝐵 ·ih 𝐶 ) ) )