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 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → A - ℎ B ⋅ ih C = A ⋅ ih C − B ⋅ ih C

Proof

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