# Metamath Proof Explorer

## Theorem frlmpws

Description: The free module as a restriction of the power module. (Contributed by Stefan O'Rear, 1-Feb-2015)

Ref Expression
Hypotheses frlmval.f ${⊢}{F}={R}\mathrm{freeLMod}{I}$
frlmpws.b ${⊢}{B}={\mathrm{Base}}_{{F}}$
Assertion frlmpws ${⊢}\left({R}\in {V}\wedge {I}\in {W}\right)\to {F}=\left(\mathrm{ringLMod}\left({R}\right){↑}_{𝑠}{I}\right){↾}_{𝑠}{B}$

### Proof

Step Hyp Ref Expression
1 frlmval.f ${⊢}{F}={R}\mathrm{freeLMod}{I}$
2 frlmpws.b ${⊢}{B}={\mathrm{Base}}_{{F}}$
3 eqid ${⊢}{\mathrm{Base}}_{\left({R}{\oplus }_{m}\left({I}×\left\{\mathrm{ringLMod}\left({R}\right)\right\}\right)\right)}={\mathrm{Base}}_{\left({R}{\oplus }_{m}\left({I}×\left\{\mathrm{ringLMod}\left({R}\right)\right\}\right)\right)}$
4 3 dsmmval2 ${⊢}{R}{\oplus }_{m}\left({I}×\left\{\mathrm{ringLMod}\left({R}\right)\right\}\right)=\left({R}{⨉}_{𝑠}\left({I}×\left\{\mathrm{ringLMod}\left({R}\right)\right\}\right)\right){↾}_{𝑠}{\mathrm{Base}}_{\left({R}{\oplus }_{m}\left({I}×\left\{\mathrm{ringLMod}\left({R}\right)\right\}\right)\right)}$
5 rlmsca ${⊢}{R}\in {V}\to {R}=\mathrm{Scalar}\left(\mathrm{ringLMod}\left({R}\right)\right)$
6 5 adantr ${⊢}\left({R}\in {V}\wedge {I}\in {W}\right)\to {R}=\mathrm{Scalar}\left(\mathrm{ringLMod}\left({R}\right)\right)$
7 6 oveq1d ${⊢}\left({R}\in {V}\wedge {I}\in {W}\right)\to {R}{⨉}_{𝑠}\left({I}×\left\{\mathrm{ringLMod}\left({R}\right)\right\}\right)=\mathrm{Scalar}\left(\mathrm{ringLMod}\left({R}\right)\right){⨉}_{𝑠}\left({I}×\left\{\mathrm{ringLMod}\left({R}\right)\right\}\right)$
8 1 frlmval ${⊢}\left({R}\in {V}\wedge {I}\in {W}\right)\to {F}={R}{\oplus }_{m}\left({I}×\left\{\mathrm{ringLMod}\left({R}\right)\right\}\right)$
9 8 eqcomd ${⊢}\left({R}\in {V}\wedge {I}\in {W}\right)\to {R}{\oplus }_{m}\left({I}×\left\{\mathrm{ringLMod}\left({R}\right)\right\}\right)={F}$
10 9 fveq2d ${⊢}\left({R}\in {V}\wedge {I}\in {W}\right)\to {\mathrm{Base}}_{\left({R}{\oplus }_{m}\left({I}×\left\{\mathrm{ringLMod}\left({R}\right)\right\}\right)\right)}={\mathrm{Base}}_{{F}}$
11 10 2 eqtr4di ${⊢}\left({R}\in {V}\wedge {I}\in {W}\right)\to {\mathrm{Base}}_{\left({R}{\oplus }_{m}\left({I}×\left\{\mathrm{ringLMod}\left({R}\right)\right\}\right)\right)}={B}$
12 7 11 oveq12d ${⊢}\left({R}\in {V}\wedge {I}\in {W}\right)\to \left({R}{⨉}_{𝑠}\left({I}×\left\{\mathrm{ringLMod}\left({R}\right)\right\}\right)\right){↾}_{𝑠}{\mathrm{Base}}_{\left({R}{\oplus }_{m}\left({I}×\left\{\mathrm{ringLMod}\left({R}\right)\right\}\right)\right)}=\left(\mathrm{Scalar}\left(\mathrm{ringLMod}\left({R}\right)\right){⨉}_{𝑠}\left({I}×\left\{\mathrm{ringLMod}\left({R}\right)\right\}\right)\right){↾}_{𝑠}{B}$
13 4 12 syl5eq ${⊢}\left({R}\in {V}\wedge {I}\in {W}\right)\to {R}{\oplus }_{m}\left({I}×\left\{\mathrm{ringLMod}\left({R}\right)\right\}\right)=\left(\mathrm{Scalar}\left(\mathrm{ringLMod}\left({R}\right)\right){⨉}_{𝑠}\left({I}×\left\{\mathrm{ringLMod}\left({R}\right)\right\}\right)\right){↾}_{𝑠}{B}$
14 fvex ${⊢}\mathrm{ringLMod}\left({R}\right)\in \mathrm{V}$
15 eqid ${⊢}\mathrm{ringLMod}\left({R}\right){↑}_{𝑠}{I}=\mathrm{ringLMod}\left({R}\right){↑}_{𝑠}{I}$
16 eqid ${⊢}\mathrm{Scalar}\left(\mathrm{ringLMod}\left({R}\right)\right)=\mathrm{Scalar}\left(\mathrm{ringLMod}\left({R}\right)\right)$
17 15 16 pwsval ${⊢}\left(\mathrm{ringLMod}\left({R}\right)\in \mathrm{V}\wedge {I}\in {W}\right)\to \mathrm{ringLMod}\left({R}\right){↑}_{𝑠}{I}=\mathrm{Scalar}\left(\mathrm{ringLMod}\left({R}\right)\right){⨉}_{𝑠}\left({I}×\left\{\mathrm{ringLMod}\left({R}\right)\right\}\right)$
18 14 17 mpan ${⊢}{I}\in {W}\to \mathrm{ringLMod}\left({R}\right){↑}_{𝑠}{I}=\mathrm{Scalar}\left(\mathrm{ringLMod}\left({R}\right)\right){⨉}_{𝑠}\left({I}×\left\{\mathrm{ringLMod}\left({R}\right)\right\}\right)$
19 18 adantl ${⊢}\left({R}\in {V}\wedge {I}\in {W}\right)\to \mathrm{ringLMod}\left({R}\right){↑}_{𝑠}{I}=\mathrm{Scalar}\left(\mathrm{ringLMod}\left({R}\right)\right){⨉}_{𝑠}\left({I}×\left\{\mathrm{ringLMod}\left({R}\right)\right\}\right)$
20 19 oveq1d ${⊢}\left({R}\in {V}\wedge {I}\in {W}\right)\to \left(\mathrm{ringLMod}\left({R}\right){↑}_{𝑠}{I}\right){↾}_{𝑠}{B}=\left(\mathrm{Scalar}\left(\mathrm{ringLMod}\left({R}\right)\right){⨉}_{𝑠}\left({I}×\left\{\mathrm{ringLMod}\left({R}\right)\right\}\right)\right){↾}_{𝑠}{B}$
21 13 8 20 3eqtr4d ${⊢}\left({R}\in {V}\wedge {I}\in {W}\right)\to {F}=\left(\mathrm{ringLMod}\left({R}\right){↑}_{𝑠}{I}\right){↾}_{𝑠}{B}$