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

### Proof

Step Hyp Ref Expression
1 his2sub ${⊢}\left({B}\in ℋ\wedge {C}\in ℋ\wedge {A}\in ℋ\right)\to \left({B}{-}_{ℎ}{C}\right){\cdot }_{\mathrm{ih}}{A}=\left({B}{\cdot }_{\mathrm{ih}}{A}\right)-\left({C}{\cdot }_{\mathrm{ih}}{A}\right)$
2 1 fveq2d ${⊢}\left({B}\in ℋ\wedge {C}\in ℋ\wedge {A}\in ℋ\right)\to \stackrel{‾}{\left({B}{-}_{ℎ}{C}\right){\cdot }_{\mathrm{ih}}{A}}=\stackrel{‾}{\left({B}{\cdot }_{\mathrm{ih}}{A}\right)-\left({C}{\cdot }_{\mathrm{ih}}{A}\right)}$
3 hicl ${⊢}\left({B}\in ℋ\wedge {A}\in ℋ\right)\to {B}{\cdot }_{\mathrm{ih}}{A}\in ℂ$
4 hicl ${⊢}\left({C}\in ℋ\wedge {A}\in ℋ\right)\to {C}{\cdot }_{\mathrm{ih}}{A}\in ℂ$
5 cjsub ${⊢}\left({B}{\cdot }_{\mathrm{ih}}{A}\in ℂ\wedge {C}{\cdot }_{\mathrm{ih}}{A}\in ℂ\right)\to \stackrel{‾}{\left({B}{\cdot }_{\mathrm{ih}}{A}\right)-\left({C}{\cdot }_{\mathrm{ih}}{A}\right)}=\stackrel{‾}{{B}{\cdot }_{\mathrm{ih}}{A}}-\stackrel{‾}{{C}{\cdot }_{\mathrm{ih}}{A}}$
6 3 4 5 syl2an ${⊢}\left(\left({B}\in ℋ\wedge {A}\in ℋ\right)\wedge \left({C}\in ℋ\wedge {A}\in ℋ\right)\right)\to \stackrel{‾}{\left({B}{\cdot }_{\mathrm{ih}}{A}\right)-\left({C}{\cdot }_{\mathrm{ih}}{A}\right)}=\stackrel{‾}{{B}{\cdot }_{\mathrm{ih}}{A}}-\stackrel{‾}{{C}{\cdot }_{\mathrm{ih}}{A}}$
7 6 3impdir ${⊢}\left({B}\in ℋ\wedge {C}\in ℋ\wedge {A}\in ℋ\right)\to \stackrel{‾}{\left({B}{\cdot }_{\mathrm{ih}}{A}\right)-\left({C}{\cdot }_{\mathrm{ih}}{A}\right)}=\stackrel{‾}{{B}{\cdot }_{\mathrm{ih}}{A}}-\stackrel{‾}{{C}{\cdot }_{\mathrm{ih}}{A}}$
8 2 7 eqtrd ${⊢}\left({B}\in ℋ\wedge {C}\in ℋ\wedge {A}\in ℋ\right)\to \stackrel{‾}{\left({B}{-}_{ℎ}{C}\right){\cdot }_{\mathrm{ih}}{A}}=\stackrel{‾}{{B}{\cdot }_{\mathrm{ih}}{A}}-\stackrel{‾}{{C}{\cdot }_{\mathrm{ih}}{A}}$
9 8 3comr ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to \stackrel{‾}{\left({B}{-}_{ℎ}{C}\right){\cdot }_{\mathrm{ih}}{A}}=\stackrel{‾}{{B}{\cdot }_{\mathrm{ih}}{A}}-\stackrel{‾}{{C}{\cdot }_{\mathrm{ih}}{A}}$
10 hvsubcl ${⊢}\left({B}\in ℋ\wedge {C}\in ℋ\right)\to {B}{-}_{ℎ}{C}\in ℋ$
11 ax-his1 ${⊢}\left({A}\in ℋ\wedge {B}{-}_{ℎ}{C}\in ℋ\right)\to {A}{\cdot }_{\mathrm{ih}}\left({B}{-}_{ℎ}{C}\right)=\stackrel{‾}{\left({B}{-}_{ℎ}{C}\right){\cdot }_{\mathrm{ih}}{A}}$
12 10 11 sylan2 ${⊢}\left({A}\in ℋ\wedge \left({B}\in ℋ\wedge {C}\in ℋ\right)\right)\to {A}{\cdot }_{\mathrm{ih}}\left({B}{-}_{ℎ}{C}\right)=\stackrel{‾}{\left({B}{-}_{ℎ}{C}\right){\cdot }_{\mathrm{ih}}{A}}$
13 12 3impb ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to {A}{\cdot }_{\mathrm{ih}}\left({B}{-}_{ℎ}{C}\right)=\stackrel{‾}{\left({B}{-}_{ℎ}{C}\right){\cdot }_{\mathrm{ih}}{A}}$
14 ax-his1 ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to {A}{\cdot }_{\mathrm{ih}}{B}=\stackrel{‾}{{B}{\cdot }_{\mathrm{ih}}{A}}$
15 14 3adant3 ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to {A}{\cdot }_{\mathrm{ih}}{B}=\stackrel{‾}{{B}{\cdot }_{\mathrm{ih}}{A}}$
16 ax-his1 ${⊢}\left({A}\in ℋ\wedge {C}\in ℋ\right)\to {A}{\cdot }_{\mathrm{ih}}{C}=\stackrel{‾}{{C}{\cdot }_{\mathrm{ih}}{A}}$
17 16 3adant2 ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to {A}{\cdot }_{\mathrm{ih}}{C}=\stackrel{‾}{{C}{\cdot }_{\mathrm{ih}}{A}}$
18 15 17 oveq12d ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to \left({A}{\cdot }_{\mathrm{ih}}{B}\right)-\left({A}{\cdot }_{\mathrm{ih}}{C}\right)=\stackrel{‾}{{B}{\cdot }_{\mathrm{ih}}{A}}-\stackrel{‾}{{C}{\cdot }_{\mathrm{ih}}{A}}$
19 9 13 18 3eqtr4d ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to {A}{\cdot }_{\mathrm{ih}}\left({B}{-}_{ℎ}{C}\right)=\left({A}{\cdot }_{\mathrm{ih}}{B}\right)-\left({A}{\cdot }_{\mathrm{ih}}{C}\right)$