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⋅ihC=A⋅ihC−B⋅ihC

Proof

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