rlmsca

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

		Ref	Expression
	Assertion	rlmsca	$⊢ R \in X \to R = Scalar (ringLMod (R))$

Step	Hyp	Ref	Expression
1		eqid	$⊢ {Base}_{R} = {Base}_{R}$
2	1	ressid	$⊢ R \in X \to R ↾_{𝑠} {Base}_{R} = R$
3		rlmval	$⊢ ringLMod (R) = subringAlg (R) ({Base}_{R})$
4	3	a1i	$⊢ R \in X \to ringLMod (R) = subringAlg (R) ({Base}_{R})$
5		ssidd	$⊢ R \in X \to {Base}_{R} \subseteq {Base}_{R}$
6	4 5	srasca	$⊢ R \in X \to R ↾_{𝑠} {Base}_{R} = Scalar (ringLMod (R))$
7	2 6	eqtr3d	$⊢ R \in X \to R = Scalar (ringLMod (R))$

Metamath Proof Explorer