Theorem slmdacl

Description: Closure of ring addition for a semimodule. (Contributed by Thierry Arnoux, 1-Apr-2018)

	Ref	Expression
Hypotheses	slmdacl.f	|- F = ( Scalar ` W )
	slmdacl.k	|- K = ( Base ` F )
	slmdacl.p	|- .+ = ( +g ` F )
Assertion	slmdacl	|- ( ( W e. SLMod /\ X e. K /\ Y e. K ) -> ( X .+ Y ) e. K )

Proof

Step	Hyp	Ref	Expression
1		slmdacl.f	|- F = ( Scalar ` W )
2		slmdacl.k	|- K = ( Base ` F )
3		slmdacl.p	|- .+ = ( +g ` F )
4	1	slmdsrg	|- ( W e. SLMod -> F e. SRing )
5		srgmnd	|- ( F e. SRing -> F e. Mnd )
6	4 5	syl	|- ( W e. SLMod -> F e. Mnd )
7	2 3	mndcl	|- ( ( F e. Mnd /\ X e. K /\ Y e. K ) -> ( X .+ Y ) e. K )
8	6 7	syl3an1	|- ( ( W e. SLMod /\ X e. K /\ Y e. K ) -> ( X .+ Y ) e. K )