This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lmodmcl

Description: Closure of ring multiplication for a left module. (Contributed by NM, 14-Jan-2014) (Revised by Mario Carneiro, 19-Jun-2014)

	Ref	Expression
Hypotheses	lmodmcl.f	$⊢ F = Scalar (W)$
	lmodmcl.k	$⊢ K = {Base}_{F}$
	lmodmcl.t	$⊢ \underset{˙}{\cdot} = \cdot_{F}$
Assertion	lmodmcl	$⊢ (W \in LMod \land X \in K \land Y \in K) \to X \underset{˙}{\cdot} Y \in K$

Step	Hyp	Ref	Expression
1		lmodmcl.f	$⊢ F = Scalar (W)$
2		lmodmcl.k	$⊢ K = {Base}_{F}$
3		lmodmcl.t	$⊢ \underset{˙}{\cdot} = \cdot_{F}$
4	1	lmodring	$⊢ W \in LMod \to F \in Ring$
5	2 3	ringcl	$⊢ (F \in Ring \land X \in K \land Y \in K) \to X \underset{˙}{\cdot} Y \in K$
6	4 5	syl3an1	$⊢ (W \in LMod \land X \in K \land Y \in K) \to X \underset{˙}{\cdot} Y \in K$