Metamath Proof Explorer


Theorem rlmsca2

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

Ref Expression
Assertion rlmsca2 I R = Scalar ringLMod R

Proof

Step Hyp Ref Expression
1 fvi R V I R = R
2 eqid Base R = Base R
3 2 ressid R V R 𝑠 Base R = R
4 1 3 eqtr4d R V I R = R 𝑠 Base R
5 fvprc ¬ R V I R =
6 reldmress Rel dom 𝑠
7 6 ovprc1 ¬ R V R 𝑠 Base R =
8 5 7 eqtr4d ¬ R V 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 ringLMod R = subringAlg R Base R
12 ssidd Base R Base R
13 11 12 srasca R 𝑠 Base R = Scalar ringLMod R
14 13 mptru R 𝑠 Base R = Scalar ringLMod R
15 9 14 eqtri I R = Scalar ringLMod R