Metamath Proof Explorer

Theorem his2sub2

Description: Distributive law for inner product of vector subtraction. (Contributed by NM, 13-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion his2sub2 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ⋅ ih B - ℎ C = A ⋅ ih B − A ⋅ ih C

Proof

Step Hyp Ref Expression
1 his2sub ⊢ B ∈ ℋ ∧ C ∈ ℋ ∧ A ∈ ℋ → B - ℎ C ⋅ ih A = B ⋅ ih A − C ⋅ ih A
2 1 fveq2d ⊢ B ∈ ℋ ∧ C ∈ ℋ ∧ A ∈ ℋ → B - ℎ C ⋅ ih A ‾ = B ⋅ ih A − C ⋅ ih A ‾
3 hicl ⊢ B ∈ ℋ ∧ A ∈ ℋ → B ⋅ ih A ∈ ℂ
4 hicl ⊢ C ∈ ℋ ∧ A ∈ ℋ → C ⋅ ih A ∈ ℂ
5 cjsub ⊢ B ⋅ ih A ∈ ℂ ∧ C ⋅ ih A ∈ ℂ → B ⋅ ih A − C ⋅ ih A ‾ = B ⋅ ih A ‾ − C ⋅ ih A ‾
6 3 4 5 syl2an ⊢ B ∈ ℋ ∧ A ∈ ℋ ∧ C ∈ ℋ ∧ A ∈ ℋ → B ⋅ ih A − C ⋅ ih A ‾ = B ⋅ ih A ‾ − C ⋅ ih A ‾
7 6 3impdir ⊢ B ∈ ℋ ∧ C ∈ ℋ ∧ A ∈ ℋ → B ⋅ ih A − C ⋅ ih A ‾ = B ⋅ ih A ‾ − C ⋅ ih A ‾
8 2 7 eqtrd ⊢ B ∈ ℋ ∧ C ∈ ℋ ∧ A ∈ ℋ → B - ℎ C ⋅ ih A ‾ = B ⋅ ih A ‾ − C ⋅ ih A ‾
9 8 3comr ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → B - ℎ C ⋅ ih A ‾ = B ⋅ ih A ‾ − C ⋅ ih A ‾
10 hvsubcl ⊢ B ∈ ℋ ∧ C ∈ ℋ → B - ℎ C ∈ ℋ
11 ax-his1 ⊢ A ∈ ℋ ∧ B - ℎ C ∈ ℋ → A ⋅ ih B - ℎ C = B - ℎ C ⋅ ih A ‾
12 10 11 sylan2 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ⋅ ih B - ℎ C = B - ℎ C ⋅ ih A ‾
13 12 3impb ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ⋅ ih B - ℎ C = B - ℎ C ⋅ ih A ‾
14 ax-his1 ⊢ A ∈ ℋ ∧ B ∈ ℋ → A ⋅ ih B = B ⋅ ih A ‾
15 14 3adant3 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ⋅ ih B = B ⋅ ih A ‾
16 ax-his1 ⊢ A ∈ ℋ ∧ C ∈ ℋ → A ⋅ ih C = C ⋅ ih A ‾
17 16 3adant2 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ⋅ ih C = C ⋅ ih A ‾
18 15 17 oveq12d ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ⋅ ih B − A ⋅ ih C = B ⋅ ih A ‾ − C ⋅ ih A ‾
19 9 13 18 3eqtr4d ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ⋅ ih B - ℎ C = A ⋅ ih B − A ⋅ ih C