Metamath Proof Explorer


Theorem frlmsca

Description: The ring of scalars of a free module. (Contributed by Stefan O'Rear, 1-Feb-2015)

Ref Expression
Hypothesis frlmval.f F = R freeLMod I
Assertion frlmsca R V I W R = Scalar F

Proof

Step Hyp Ref Expression
1 frlmval.f F = R freeLMod I
2 fvex ringLMod R V
3 eqid ringLMod R 𝑠 I = ringLMod R 𝑠 I
4 eqid Scalar ringLMod R = Scalar ringLMod R
5 3 4 pwssca ringLMod R V I W Scalar ringLMod R = Scalar ringLMod R 𝑠 I
6 2 5 mpan I W Scalar ringLMod R = Scalar ringLMod R 𝑠 I
7 6 adantl R V I W Scalar ringLMod R = Scalar ringLMod R 𝑠 I
8 fvex Base F V
9 eqid ringLMod R 𝑠 I 𝑠 Base F = ringLMod R 𝑠 I 𝑠 Base F
10 eqid Scalar ringLMod R 𝑠 I = Scalar ringLMod R 𝑠 I
11 9 10 resssca Base F V Scalar ringLMod R 𝑠 I = Scalar ringLMod R 𝑠 I 𝑠 Base F
12 8 11 ax-mp Scalar ringLMod R 𝑠 I = Scalar ringLMod R 𝑠 I 𝑠 Base F
13 7 12 syl6eq R V I W Scalar ringLMod R = Scalar ringLMod R 𝑠 I 𝑠 Base F
14 rlmsca R V R = Scalar ringLMod R
15 14 adantr R V I W R = Scalar ringLMod R
16 eqid Base F = Base F
17 1 16 frlmpws R V I W F = ringLMod R 𝑠 I 𝑠 Base F
18 17 fveq2d R V I W Scalar F = Scalar ringLMod R 𝑠 I 𝑠 Base F
19 13 15 18 3eqtr4d R V I W R = Scalar F