# Metamath Proof Explorer

## Theorem frlmval

Description: Value of the "free module" function. (Contributed by Stefan O'Rear, 1-Feb-2015)

Ref Expression
Hypothesis frlmval.f ${⊢}{F}={R}\mathrm{freeLMod}{I}$
Assertion 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)$

### Proof

Step Hyp Ref Expression
1 frlmval.f ${⊢}{F}={R}\mathrm{freeLMod}{I}$
2 elex ${⊢}{R}\in {V}\to {R}\in \mathrm{V}$
3 elex ${⊢}{I}\in {W}\to {I}\in \mathrm{V}$
4 id ${⊢}{r}={R}\to {r}={R}$
5 fveq2 ${⊢}{r}={R}\to \mathrm{ringLMod}\left({r}\right)=\mathrm{ringLMod}\left({R}\right)$
6 5 sneqd ${⊢}{r}={R}\to \left\{\mathrm{ringLMod}\left({r}\right)\right\}=\left\{\mathrm{ringLMod}\left({R}\right)\right\}$
7 6 xpeq2d ${⊢}{r}={R}\to {i}×\left\{\mathrm{ringLMod}\left({r}\right)\right\}={i}×\left\{\mathrm{ringLMod}\left({R}\right)\right\}$
8 4 7 oveq12d ${⊢}{r}={R}\to {r}{\oplus }_{m}\left({i}×\left\{\mathrm{ringLMod}\left({r}\right)\right\}\right)={R}{\oplus }_{m}\left({i}×\left\{\mathrm{ringLMod}\left({R}\right)\right\}\right)$
9 xpeq1 ${⊢}{i}={I}\to {i}×\left\{\mathrm{ringLMod}\left({R}\right)\right\}={I}×\left\{\mathrm{ringLMod}\left({R}\right)\right\}$
10 9 oveq2d ${⊢}{i}={I}\to {R}{\oplus }_{m}\left({i}×\left\{\mathrm{ringLMod}\left({R}\right)\right\}\right)={R}{\oplus }_{m}\left({I}×\left\{\mathrm{ringLMod}\left({R}\right)\right\}\right)$
11 df-frlm ${⊢}\mathrm{freeLMod}=\left({r}\in \mathrm{V},{i}\in \mathrm{V}⟼{r}{\oplus }_{m}\left({i}×\left\{\mathrm{ringLMod}\left({r}\right)\right\}\right)\right)$
12 ovex ${⊢}{R}{\oplus }_{m}\left({I}×\left\{\mathrm{ringLMod}\left({R}\right)\right\}\right)\in \mathrm{V}$
13 8 10 11 12 ovmpo ${⊢}\left({R}\in \mathrm{V}\wedge {I}\in \mathrm{V}\right)\to {R}\mathrm{freeLMod}{I}={R}{\oplus }_{m}\left({I}×\left\{\mathrm{ringLMod}\left({R}\right)\right\}\right)$
14 2 3 13 syl2an ${⊢}\left({R}\in {V}\wedge {I}\in {W}\right)\to {R}\mathrm{freeLMod}{I}={R}{\oplus }_{m}\left({I}×\left\{\mathrm{ringLMod}\left({R}\right)\right\}\right)$
15 1 14 syl5eq ${⊢}\left({R}\in {V}\wedge {I}\in {W}\right)\to {F}={R}{\oplus }_{m}\left({I}×\left\{\mathrm{ringLMod}\left({R}\right)\right\}\right)$