Metamath Proof Explorer

Theorem slmdvscl

Description: Closure of scalar product for a semiring left module. ( hvmulcl analog.) (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 19-Jun-2014) (Revised by Thierry Arnoux, 1-Apr-2018)

		Ref	Expression
	Hypotheses	slmdvscl.v	$⊢ V = {Base}_{W}$
		slmdvscl.f	$⊢ F = Scalar (W)$
		slmdvscl.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
		slmdvscl.k	$⊢ K = {Base}_{F}$
	Assertion	slmdvscl	$⊢ (W \in SLMod \land R \in K \land X \in V) \to R \underset{˙}{\cdot} X \in V$

Proof

Step	Hyp	Ref	Expression
1		slmdvscl.v	$⊢ V = {Base}_{W}$
2		slmdvscl.f	$⊢ F = Scalar (W)$
3		slmdvscl.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
4		slmdvscl.k	$⊢ K = {Base}_{F}$
5		biid	$⊢ W \in SLMod \leftrightarrow W \in SLMod$
6		pm4.24	$⊢ R \in K \leftrightarrow (R \in K \land R \in K)$
7		pm4.24	$⊢ X \in V \leftrightarrow (X \in V \land X \in V)$
8		eqid	$⊢ +_{W} = +_{W}$
9		eqid	$⊢ 0_{W} = 0_{W}$
10		eqid	$⊢ +_{F} = +_{F}$
11		eqid	$⊢ \cdot_{F} = \cdot_{F}$
12		eqid	$⊢ 1_{F} = 1_{F}$
13		eqid	$⊢ 0_{F} = 0_{F}$
14	1 8 3 9 2 4 10 11 12 13	slmdlema	$⊢ (W \in SLMod \land (R \in K \land R \in K) \land (X \in V \land X \in V)) \to ((R \underset{˙}{\cdot} X \in V \land R \underset{˙}{\cdot} (X +_{W} X) = (R \underset{˙}{\cdot} X) +_{W} (R \underset{˙}{\cdot} X) \land (R +_{F} R) \underset{˙}{\cdot} X = (R \underset{˙}{\cdot} X) +_{W} (R \underset{˙}{\cdot} X)) \land ((R \cdot_{F} R) \underset{˙}{\cdot} X = R \underset{˙}{\cdot} (R \underset{˙}{\cdot} X) \land 1_{F} \underset{˙}{\cdot} X = X \land 0_{F} \underset{˙}{\cdot} X = 0_{W}))$
15	14	simpld	$⊢ (W \in SLMod \land (R \in K \land R \in K) \land (X \in V \land X \in V)) \to (R \underset{˙}{\cdot} X \in V \land R \underset{˙}{\cdot} (X +_{W} X) = (R \underset{˙}{\cdot} X) +_{W} (R \underset{˙}{\cdot} X) \land (R +_{F} R) \underset{˙}{\cdot} X = (R \underset{˙}{\cdot} X) +_{W} (R \underset{˙}{\cdot} X))$
16	15	simp1d	$⊢ (W \in SLMod \land (R \in K \land R \in K) \land (X \in V \land X \in V)) \to R \underset{˙}{\cdot} X \in V$
17	5 6 7 16	syl3anb	$⊢ (W \in SLMod \land R \in K \land X \in V) \to R \underset{˙}{\cdot} X \in V$