clmvs1

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

	Ref	Expression
Hypotheses	clmvs1.v	$⊢ V = {Base}_{W}$
	clmvs1.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
Assertion	clmvs1	$⊢ (W \in CMod \land X \in V) \to 1 \underset{˙}{\cdot} X = X$

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

Metamath Proof Explorer