Theorem clmvs1

Description: Scalar product with ring unit. ( lmodvs1 analog.) (Contributed by Mario Carneiro, 16-Oct-2015)

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

Proof

Step	Hyp	Ref	Expression
1		clmvs1.v	$$⊢V={\mathrm{Base}}_W$$
2		clmvs1.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
3		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
4	3	clm1	$$⊢W\in \mathrm{CMod}\to 1=1_{\mathrm{Scalar}\left(W\right)}$$
5	4	adantr	$$⊢\left(W\in \mathrm{CMod}\wedge X\in V\right)\to 1=1_{\mathrm{Scalar}\left(W\right)}$$
6	5	oveq1d	$$⊢\left(W\in \mathrm{CMod}\wedge X\in V\right)\to 1\underset{\dot{}}{·}X=1_{\mathrm{Scalar}\left(W\right)}\underset{\dot{}}{·}X$$
7		clmlmod	$$⊢W\in \mathrm{CMod}\to W\in \mathrm{LMod}$$
8		eqid	$$⊢1_{\mathrm{Scalar}\left(W\right)}=1_{\mathrm{Scalar}\left(W\right)}$$
9	1 3 2 8	lmodvs1	$$⊢\left(W\in \mathrm{LMod}\wedge X\in V\right)\to 1_{\mathrm{Scalar}\left(W\right)}\underset{\dot{}}{·}X=X$$
10	7 9	sylan	$$⊢\left(W\in \mathrm{CMod}\wedge X\in V\right)\to 1_{\mathrm{Scalar}\left(W\right)}\underset{\dot{}}{·}X=X$$
11	6 10	eqtrd	$$⊢\left(W\in \mathrm{CMod}\wedge X\in V\right)\to 1\underset{\dot{}}{·}X=X$$