Theorem slmdsrg

Description: The scalar component of a semimodule is a semiring. (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 19-Jun-2014) (Revised by Thierry Arnoux, 1-Apr-2018)

	Ref	Expression
Hypothesis	slmdsrg.1	|- F = ( Scalar ` W )
Assertion	slmdsrg	|- ( W e. SLMod -> F e. SRing )

Proof

Step	Hyp	Ref	Expression
1		slmdsrg.1	|- F = ( Scalar ` W )
2		eqid	|- ( Base ` W ) = ( Base ` W )
3		eqid	|- ( +g ` W ) = ( +g ` W )
4		eqid	|- ( .s ` W ) = ( .s ` W )
5		eqid	|- ( 0g ` W ) = ( 0g ` W )
6		eqid	|- ( Base ` F ) = ( Base ` F )
7		eqid	|- ( +g ` F ) = ( +g ` F )
8		eqid	|- ( .r ` F ) = ( .r ` F )
9		eqid	|- ( 1r ` F ) = ( 1r ` F )
10		eqid	|- ( 0g ` F ) = ( 0g ` F )
11	2 3 4 5 1 6 7 8 9 10	isslmd	|- ( W e. SLMod <-> ( W e. CMnd /\ F e. SRing /\ A. w e. ( Base ` F ) A. z e. ( Base ` F ) A. x e. ( Base ` W ) A. y e. ( Base ` W ) ( ( ( z ( .s ` W ) y ) e. ( Base ` W ) /\ ( z ( .s ` W ) ( y ( +g ` W ) x ) ) = ( ( z ( .s ` W ) y ) ( +g ` W ) ( z ( .s ` W ) x ) ) /\ ( ( w ( +g ` F ) z ) ( .s ` W ) y ) = ( ( w ( .s ` W ) y ) ( +g ` W ) ( z ( .s ` W ) y ) ) ) /\ ( ( ( w ( .r ` F ) z ) ( .s ` W ) y ) = ( w ( .s ` W ) ( z ( .s ` W ) y ) ) /\ ( ( 1r ` F ) ( .s ` W ) y ) = y /\ ( ( 0g ` F ) ( .s ` W ) y ) = ( 0g ` W ) ) ) ) )
12	11	simp2bi	|- ( W e. SLMod -> F e. SRing )