Theorem hv2times

Description: Two times a vector. (Contributed by NM, 22-Jun-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	hv2times	$$⊢A\in \mathscr{H}\to 2{\cdot }_{ℎ}A=A{+}_{ℎ}A$$

Proof

Step	Hyp	Ref	Expression
1		df-2	$$⊢2=1+1$$
2	1	oveq1i	$$⊢2{\cdot }_{ℎ}A=\left(1+1\right){\cdot }_{ℎ}A$$
3		ax-1cn	$$⊢1\in ℂ$$
4		ax-hvdistr2	$$⊢\left(1\in ℂ\wedge 1\in ℂ\wedge A\in \mathscr{H}\right)\to \left(1+1\right){\cdot }_{ℎ}A=\left(1{\cdot }_{ℎ}A\right){+}_{ℎ}\left(1{\cdot }_{ℎ}A\right)$$
5	3 3 4	mp3an12	$$⊢A\in \mathscr{H}\to \left(1+1\right){\cdot }_{ℎ}A=\left(1{\cdot }_{ℎ}A\right){+}_{ℎ}\left(1{\cdot }_{ℎ}A\right)$$
6	2 5	syl5eq	$$⊢A\in \mathscr{H}\to 2{\cdot }_{ℎ}A=\left(1{\cdot }_{ℎ}A\right){+}_{ℎ}\left(1{\cdot }_{ℎ}A\right)$$
7		ax-hvdistr1	$$⊢\left(1\in ℂ\wedge A\in \mathscr{H}\wedge A\in \mathscr{H}\right)\to 1{\cdot }_{ℎ}\left(A{+}_{ℎ}A\right)=\left(1{\cdot }_{ℎ}A\right){+}_{ℎ}\left(1{\cdot }_{ℎ}A\right)$$
8	3 7	mp3an1	$$⊢\left(A\in \mathscr{H}\wedge A\in \mathscr{H}\right)\to 1{\cdot }_{ℎ}\left(A{+}_{ℎ}A\right)=\left(1{\cdot }_{ℎ}A\right){+}_{ℎ}\left(1{\cdot }_{ℎ}A\right)$$
9	8	anidms	$$⊢A\in \mathscr{H}\to 1{\cdot }_{ℎ}\left(A{+}_{ℎ}A\right)=\left(1{\cdot }_{ℎ}A\right){+}_{ℎ}\left(1{\cdot }_{ℎ}A\right)$$
10		hvaddcl	$$⊢\left(A\in \mathscr{H}\wedge A\in \mathscr{H}\right)\to A{+}_{ℎ}A\in \mathscr{H}$$
11	10	anidms	$$⊢A\in \mathscr{H}\to A{+}_{ℎ}A\in \mathscr{H}$$
12		ax-hvmulid	$$⊢A{+}_{ℎ}A\in \mathscr{H}\to 1{\cdot }_{ℎ}\left(A{+}_{ℎ}A\right)=A{+}_{ℎ}A$$
13	11 12	syl	$$⊢A\in \mathscr{H}\to 1{\cdot }_{ℎ}\left(A{+}_{ℎ}A\right)=A{+}_{ℎ}A$$
14	6 9 13	3eqtr2d	$$⊢A\in \mathscr{H}\to 2{\cdot }_{ℎ}A=A{+}_{ℎ}A$$