rlmsca2

Description: Scalars in the ring module. (Contributed by Stefan O'Rear, 1-Apr-2015)

		Ref	Expression
	Assertion	rlmsca2	$⊢ I (R) = Scalar (ringLMod (R))$

Step	Hyp	Ref	Expression
1		fvi	$⊢ R \in V \to I (R) = R$
2		eqid	$⊢ {Base}_{R} = {Base}_{R}$
3	2	ressid	$⊢ R \in V \to R ↾_{𝑠} {Base}_{R} = R$
4	1 3	eqtr4d	$⊢ R \in V \to I (R) = R ↾_{𝑠} {Base}_{R}$
5		fvprc	$⊢ \neg R \in V \to I (R) = \emptyset$
6		reldmress	$⊢ Rel dom ↾_{𝑠}$
7	6	ovprc1	$⊢ \neg R \in V \to R ↾_{𝑠} {Base}_{R} = \emptyset$
8	5 7	eqtr4d	$⊢ \neg R \in V \to I (R) = R ↾_{𝑠} {Base}_{R}$
9	4 8	pm2.61i	$⊢ I (R) = R ↾_{𝑠} {Base}_{R}$
10		rlmval	$⊢ ringLMod (R) = subringAlg (R) ({Base}_{R})$
11	10	a1i	$⊢ ⊤ \to ringLMod (R) = subringAlg (R) ({Base}_{R})$
12		ssidd	$⊢ ⊤ \to {Base}_{R} \subseteq {Base}_{R}$
13	11 12	srasca	$⊢ ⊤ \to R ↾_{𝑠} {Base}_{R} = Scalar (ringLMod (R))$
14	13	mptru	$⊢ R ↾_{𝑠} {Base}_{R} = Scalar (ringLMod (R))$
15	9 14	eqtri	$⊢ I (R) = Scalar (ringLMod (R))$

Metamath Proof Explorer