Theorem rlmsca

Description: Scalars in the ring module. (Contributed by Stefan O'Rear, 6-Dec-2014)

	Ref	Expression
Assertion	rlmsca	|- ( R e. X -> R = ( Scalar ` ( ringLMod ` R ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( Base ` R ) = ( Base ` R )
2	1	ressid	|- ( R e. X -> ( R |`s ( Base ` R ) ) = R )
3		rlmval	|- ( ringLMod ` R ) = ( ( subringAlg ` R ) ` ( Base ` R ) )
4	3	a1i	|- ( R e. X -> ( ringLMod ` R ) = ( ( subringAlg ` R ) ` ( Base ` R ) ) )
5		ssidd	|- ( R e. X -> ( Base ` R ) C_ ( Base ` R ) )
6	4 5	srasca	|- ( R e. X -> ( R |`s ( Base ` R ) ) = ( Scalar ` ( ringLMod ` R ) ) )
7	2 6	eqtr3d	|- ( R e. X -> R = ( Scalar ` ( ringLMod ` R ) ) )