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

Metamath Proof Explorer

Theorem lmodacl

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

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

Step	Hyp	Ref	Expression
1		lmodacl.f	$⊢ F = Scalar (W)$
2		lmodacl.k	$⊢ K = {Base}_{F}$
3		lmodacl.p	$⊢ \underset{˙}{+} = +_{F}$
4	1	lmodfgrp	$⊢ W \in LMod \to F \in Grp$
5	2 3	grpcl	$⊢ (F \in Grp \land X \in K \land Y \in K) \to X \underset{˙}{+} Y \in K$
6	4 5	syl3an1	$⊢ (W \in LMod \land X \in K \land Y \in K) \to X \underset{˙}{+} Y \in K$