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	|- .x. = ( .s ` W )
	slmdvscl.k	|- K = ( Base ` F )
Assertion	slmdvscl	|- ( ( W e. SLMod /\ R e. K /\ X e. V ) -> ( R .x. X ) e. V )

Proof

Step	Hyp	Ref	Expression
1		slmdvscl.v	|- V = ( Base ` W )
2		slmdvscl.f	|- F = ( Scalar ` W )
3		slmdvscl.s	|- .x. = ( .s ` W )
4		slmdvscl.k	|- K = ( Base ` F )
5		biid	|- ( W e. SLMod <-> W e. SLMod )
6		pm4.24	|- ( R e. K <-> ( R e. K /\ R e. K ) )
7		pm4.24	|- ( X e. V <-> ( X e. V /\ X e. V ) )
8		eqid	|- ( +g ` W ) = ( +g ` W )
9		eqid	|- ( 0g ` W ) = ( 0g ` W )
10		eqid	|- ( +g ` F ) = ( +g ` F )
11		eqid	|- ( .r ` F ) = ( .r ` F )
12		eqid	|- ( 1r ` F ) = ( 1r ` F )
13		eqid	|- ( 0g ` F ) = ( 0g ` F )
14	1 8 3 9 2 4 10 11 12 13	slmdlema	|- ( ( W e. SLMod /\ ( R e. K /\ R e. K ) /\ ( X e. V /\ X e. V ) ) -> ( ( ( R .x. X ) e. V /\ ( R .x. ( X ( +g ` W ) X ) ) = ( ( R .x. X ) ( +g ` W ) ( R .x. X ) ) /\ ( ( R ( +g ` F ) R ) .x. X ) = ( ( R .x. X ) ( +g ` W ) ( R .x. X ) ) ) /\ ( ( ( R ( .r ` F ) R ) .x. X ) = ( R .x. ( R .x. X ) ) /\ ( ( 1r ` F ) .x. X ) = X /\ ( ( 0g ` F ) .x. X ) = ( 0g ` W ) ) ) )
15	14	simpld	|- ( ( W e. SLMod /\ ( R e. K /\ R e. K ) /\ ( X e. V /\ X e. V ) ) -> ( ( R .x. X ) e. V /\ ( R .x. ( X ( +g ` W ) X ) ) = ( ( R .x. X ) ( +g ` W ) ( R .x. X ) ) /\ ( ( R ( +g ` F ) R ) .x. X ) = ( ( R .x. X ) ( +g ` W ) ( R .x. X ) ) ) )
16	15	simp1d	|- ( ( W e. SLMod /\ ( R e. K /\ R e. K ) /\ ( X e. V /\ X e. V ) ) -> ( R .x. X ) e. V )
17	5 6 7 16	syl3anb	|- ( ( W e. SLMod /\ R e. K /\ X e. V ) -> ( R .x. X ) e. V )