Theorem clmvs2

Description: A vector plus itself is two times the vector. (Contributed by NM, 1-Feb-2007) (Revised by AV, 21-Sep-2021)

	Ref	Expression
Hypotheses	clmvs1.v	$$⊢V={\mathrm{Base}}_W$$
	clmvs1.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	clmvs2.a	$$⊢\underset{\dot{}}{+}={+}_W$$
Assertion	clmvs2	$$⊢\left(W\in \mathrm{CMod}\wedge A\in V\right)\to A\underset{\dot{}}{+}A=2\underset{\dot{}}{·}A$$

Proof

Step	Hyp	Ref	Expression
1		clmvs1.v	$$⊢V={\mathrm{Base}}_W$$
2		clmvs1.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
3		clmvs2.a	$$⊢\underset{\dot{}}{+}={+}_W$$
4		df-2	$$⊢2=1+1$$
5	4	oveq1i	$$⊢2\underset{\dot{}}{·}A=\left(1+1\right)\underset{\dot{}}{·}A$$
6	5	a1i	$$⊢\left(W\in \mathrm{CMod}\wedge A\in V\right)\to 2\underset{\dot{}}{·}A=\left(1+1\right)\underset{\dot{}}{·}A$$
7		simpl	$$⊢\left(W\in \mathrm{CMod}\wedge A\in V\right)\to W\in \mathrm{CMod}$$
8		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
9	8	clm1	$$⊢W\in \mathrm{CMod}\to 1=1_{\mathrm{Scalar}\left(W\right)}$$
10		clmlmod	$$⊢W\in \mathrm{CMod}\to W\in \mathrm{LMod}$$
11		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
12		eqid	$$⊢1_{\mathrm{Scalar}\left(W\right)}=1_{\mathrm{Scalar}\left(W\right)}$$
13	8 11 12	lmod1cl	$$⊢W\in \mathrm{LMod}\to 1_{\mathrm{Scalar}\left(W\right)}\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
14	10 13	syl	$$⊢W\in \mathrm{CMod}\to 1_{\mathrm{Scalar}\left(W\right)}\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
15	9 14	eqeltrd	$$⊢W\in \mathrm{CMod}\to 1\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
16	15	adantr	$$⊢\left(W\in \mathrm{CMod}\wedge A\in V\right)\to 1\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
17		simpr	$$⊢\left(W\in \mathrm{CMod}\wedge A\in V\right)\to A\in V$$
18	1 8 2 11 3	clmvsdir	$$⊢\left(W\in \mathrm{CMod}\wedge \left(1\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge 1\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge A\in V\right)\right)\to \left(1+1\right)\underset{\dot{}}{·}A=\left(1\underset{\dot{}}{·}A\right)\underset{\dot{}}{+}\left(1\underset{\dot{}}{·}A\right)$$
19	7 16 16 17 18	syl13anc	$$⊢\left(W\in \mathrm{CMod}\wedge A\in V\right)\to \left(1+1\right)\underset{\dot{}}{·}A=\left(1\underset{\dot{}}{·}A\right)\underset{\dot{}}{+}\left(1\underset{\dot{}}{·}A\right)$$
20	1 2	clmvs1	$$⊢\left(W\in \mathrm{CMod}\wedge A\in V\right)\to 1\underset{\dot{}}{·}A=A$$
21	20 20	oveq12d	$$⊢\left(W\in \mathrm{CMod}\wedge A\in V\right)\to \left(1\underset{\dot{}}{·}A\right)\underset{\dot{}}{+}\left(1\underset{\dot{}}{·}A\right)=A\underset{\dot{}}{+}A$$
22	6 19 21	3eqtrrd	$$⊢\left(W\in \mathrm{CMod}\wedge A\in V\right)\to A\underset{\dot{}}{+}A=2\underset{\dot{}}{·}A$$