# 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}\mathrm{freeLMod}{I}$
Assertion frlmsca ${⊢}\left({R}\in {V}\wedge {I}\in {W}\right)\to {R}=\mathrm{Scalar}\left({F}\right)$

### Proof

Step Hyp Ref Expression
1 frlmval.f ${⊢}{F}={R}\mathrm{freeLMod}{I}$
2 fvex ${⊢}\mathrm{ringLMod}\left({R}\right)\in \mathrm{V}$
3 eqid ${⊢}\mathrm{ringLMod}\left({R}\right){↑}_{𝑠}{I}=\mathrm{ringLMod}\left({R}\right){↑}_{𝑠}{I}$
4 eqid ${⊢}\mathrm{Scalar}\left(\mathrm{ringLMod}\left({R}\right)\right)=\mathrm{Scalar}\left(\mathrm{ringLMod}\left({R}\right)\right)$
5 3 4 pwssca ${⊢}\left(\mathrm{ringLMod}\left({R}\right)\in \mathrm{V}\wedge {I}\in {W}\right)\to \mathrm{Scalar}\left(\mathrm{ringLMod}\left({R}\right)\right)=\mathrm{Scalar}\left(\mathrm{ringLMod}\left({R}\right){↑}_{𝑠}{I}\right)$
6 2 5 mpan ${⊢}{I}\in {W}\to \mathrm{Scalar}\left(\mathrm{ringLMod}\left({R}\right)\right)=\mathrm{Scalar}\left(\mathrm{ringLMod}\left({R}\right){↑}_{𝑠}{I}\right)$
7 6 adantl ${⊢}\left({R}\in {V}\wedge {I}\in {W}\right)\to \mathrm{Scalar}\left(\mathrm{ringLMod}\left({R}\right)\right)=\mathrm{Scalar}\left(\mathrm{ringLMod}\left({R}\right){↑}_{𝑠}{I}\right)$
8 fvex ${⊢}{\mathrm{Base}}_{{F}}\in \mathrm{V}$
9 eqid ${⊢}\left(\mathrm{ringLMod}\left({R}\right){↑}_{𝑠}{I}\right){↾}_{𝑠}{\mathrm{Base}}_{{F}}=\left(\mathrm{ringLMod}\left({R}\right){↑}_{𝑠}{I}\right){↾}_{𝑠}{\mathrm{Base}}_{{F}}$
10 eqid ${⊢}\mathrm{Scalar}\left(\mathrm{ringLMod}\left({R}\right){↑}_{𝑠}{I}\right)=\mathrm{Scalar}\left(\mathrm{ringLMod}\left({R}\right){↑}_{𝑠}{I}\right)$
11 9 10 resssca ${⊢}{\mathrm{Base}}_{{F}}\in \mathrm{V}\to \mathrm{Scalar}\left(\mathrm{ringLMod}\left({R}\right){↑}_{𝑠}{I}\right)=\mathrm{Scalar}\left(\left(\mathrm{ringLMod}\left({R}\right){↑}_{𝑠}{I}\right){↾}_{𝑠}{\mathrm{Base}}_{{F}}\right)$
12 8 11 ax-mp ${⊢}\mathrm{Scalar}\left(\mathrm{ringLMod}\left({R}\right){↑}_{𝑠}{I}\right)=\mathrm{Scalar}\left(\left(\mathrm{ringLMod}\left({R}\right){↑}_{𝑠}{I}\right){↾}_{𝑠}{\mathrm{Base}}_{{F}}\right)$
13 7 12 syl6eq ${⊢}\left({R}\in {V}\wedge {I}\in {W}\right)\to \mathrm{Scalar}\left(\mathrm{ringLMod}\left({R}\right)\right)=\mathrm{Scalar}\left(\left(\mathrm{ringLMod}\left({R}\right){↑}_{𝑠}{I}\right){↾}_{𝑠}{\mathrm{Base}}_{{F}}\right)$
14 rlmsca ${⊢}{R}\in {V}\to {R}=\mathrm{Scalar}\left(\mathrm{ringLMod}\left({R}\right)\right)$
15 14 adantr ${⊢}\left({R}\in {V}\wedge {I}\in {W}\right)\to {R}=\mathrm{Scalar}\left(\mathrm{ringLMod}\left({R}\right)\right)$
16 eqid ${⊢}{\mathrm{Base}}_{{F}}={\mathrm{Base}}_{{F}}$
17 1 16 frlmpws ${⊢}\left({R}\in {V}\wedge {I}\in {W}\right)\to {F}=\left(\mathrm{ringLMod}\left({R}\right){↑}_{𝑠}{I}\right){↾}_{𝑠}{\mathrm{Base}}_{{F}}$
18 17 fveq2d ${⊢}\left({R}\in {V}\wedge {I}\in {W}\right)\to \mathrm{Scalar}\left({F}\right)=\mathrm{Scalar}\left(\left(\mathrm{ringLMod}\left({R}\right){↑}_{𝑠}{I}\right){↾}_{𝑠}{\mathrm{Base}}_{{F}}\right)$
19 13 15 18 3eqtr4d ${⊢}\left({R}\in {V}\wedge {I}\in {W}\right)\to {R}=\mathrm{Scalar}\left({F}\right)$