Theorem hvsubdistr1i

Description: Scalar multiplication distributive law. (Contributed by NM, 3-Sep-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hvdistr1.1	$$⊢A\in ℂ$$
	hvdistr1.2	$$⊢B\in \mathscr{H}$$
	hvdistr1.3	$$⊢C\in \mathscr{H}$$
Assertion	hvsubdistr1i	$$⊢A{\cdot }_{ℎ}\left(B{-}_{ℎ}C\right)=\left(A{\cdot }_{ℎ}B\right){-}_{ℎ}\left(A{\cdot }_{ℎ}C\right)$$

Proof

Step	Hyp	Ref	Expression
1		hvdistr1.1	$$⊢A\in ℂ$$
2		hvdistr1.2	$$⊢B\in \mathscr{H}$$
3		hvdistr1.3	$$⊢C\in \mathscr{H}$$
4		hvsubdistr1	$$⊢\left(A\in ℂ\wedge B\in \mathscr{H}\wedge C\in \mathscr{H}\right)\to A{\cdot }_{ℎ}\left(B{-}_{ℎ}C\right)=\left(A{\cdot }_{ℎ}B\right){-}_{ℎ}\left(A{\cdot }_{ℎ}C\right)$$
5	1 2 3 4	mp3an	$$⊢A{\cdot }_{ℎ}\left(B{-}_{ℎ}C\right)=\left(A{\cdot }_{ℎ}B\right){-}_{ℎ}\left(A{\cdot }_{ℎ}C\right)$$