# 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 ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to \left({A}{-}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}{C}=\left({A}{\cdot }_{\mathrm{ih}}{C}\right)-\left({B}{\cdot }_{\mathrm{ih}}{C}\right)$

### Proof

Step Hyp Ref Expression
1 hvsubval ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to {A}{-}_{ℎ}{B}={A}{+}_{ℎ}\left(-1{\cdot }_{ℎ}{B}\right)$
2 1 oveq1d ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to \left({A}{-}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}{C}=\left({A}{+}_{ℎ}\left(-1{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}{C}$
3 2 3adant3 ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to \left({A}{-}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}{C}=\left({A}{+}_{ℎ}\left(-1{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}{C}$
4 neg1cn ${⊢}-1\in ℂ$
5 hvmulcl ${⊢}\left(-1\in ℂ\wedge {B}\in ℋ\right)\to -1{\cdot }_{ℎ}{B}\in ℋ$
6 4 5 mpan ${⊢}{B}\in ℋ\to -1{\cdot }_{ℎ}{B}\in ℋ$
7 ax-his2 ${⊢}\left({A}\in ℋ\wedge -1{\cdot }_{ℎ}{B}\in ℋ\wedge {C}\in ℋ\right)\to \left({A}{+}_{ℎ}\left(-1{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}{C}=\left({A}{\cdot }_{\mathrm{ih}}{C}\right)+\left(\left(-1{\cdot }_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}{C}\right)$
8 6 7 syl3an2 ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to \left({A}{+}_{ℎ}\left(-1{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}{C}=\left({A}{\cdot }_{\mathrm{ih}}{C}\right)+\left(\left(-1{\cdot }_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}{C}\right)$
9 ax-his3 ${⊢}\left(-1\in ℂ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to \left(-1{\cdot }_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}{C}=-1\left({B}{\cdot }_{\mathrm{ih}}{C}\right)$
10 4 9 mp3an1 ${⊢}\left({B}\in ℋ\wedge {C}\in ℋ\right)\to \left(-1{\cdot }_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}{C}=-1\left({B}{\cdot }_{\mathrm{ih}}{C}\right)$
11 hicl ${⊢}\left({B}\in ℋ\wedge {C}\in ℋ\right)\to {B}{\cdot }_{\mathrm{ih}}{C}\in ℂ$
12 11 mulm1d ${⊢}\left({B}\in ℋ\wedge {C}\in ℋ\right)\to -1\left({B}{\cdot }_{\mathrm{ih}}{C}\right)=-\left({B}{\cdot }_{\mathrm{ih}}{C}\right)$
13 10 12 eqtrd ${⊢}\left({B}\in ℋ\wedge {C}\in ℋ\right)\to \left(-1{\cdot }_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}{C}=-\left({B}{\cdot }_{\mathrm{ih}}{C}\right)$
14 13 oveq2d ${⊢}\left({B}\in ℋ\wedge {C}\in ℋ\right)\to \left({A}{\cdot }_{\mathrm{ih}}{C}\right)+\left(\left(-1{\cdot }_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}{C}\right)=\left({A}{\cdot }_{\mathrm{ih}}{C}\right)+\left(-\left({B}{\cdot }_{\mathrm{ih}}{C}\right)\right)$
15 14 3adant1 ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to \left({A}{\cdot }_{\mathrm{ih}}{C}\right)+\left(\left(-1{\cdot }_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}{C}\right)=\left({A}{\cdot }_{\mathrm{ih}}{C}\right)+\left(-\left({B}{\cdot }_{\mathrm{ih}}{C}\right)\right)$
16 8 15 eqtrd ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to \left({A}{+}_{ℎ}\left(-1{\cdot }_{ℎ}{B}\right)\right){\cdot }_{\mathrm{ih}}{C}=\left({A}{\cdot }_{\mathrm{ih}}{C}\right)+\left(-\left({B}{\cdot }_{\mathrm{ih}}{C}\right)\right)$
17 hicl ${⊢}\left({A}\in ℋ\wedge {C}\in ℋ\right)\to {A}{\cdot }_{\mathrm{ih}}{C}\in ℂ$
18 17 3adant2 ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to {A}{\cdot }_{\mathrm{ih}}{C}\in ℂ$
19 11 3adant1 ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to {B}{\cdot }_{\mathrm{ih}}{C}\in ℂ$
20 18 19 negsubd ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to \left({A}{\cdot }_{\mathrm{ih}}{C}\right)+\left(-\left({B}{\cdot }_{\mathrm{ih}}{C}\right)\right)=\left({A}{\cdot }_{\mathrm{ih}}{C}\right)-\left({B}{\cdot }_{\mathrm{ih}}{C}\right)$
21 3 16 20 3eqtrd ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to \left({A}{-}_{ℎ}{B}\right){\cdot }_{\mathrm{ih}}{C}=\left({A}{\cdot }_{\mathrm{ih}}{C}\right)-\left({B}{\cdot }_{\mathrm{ih}}{C}\right)$