# Metamath Proof Explorer

## Theorem frlmlmod

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

Ref Expression
Hypothesis frlmval.f ${⊢}{F}={R}\mathrm{freeLMod}{I}$
Assertion frlmlmod ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {W}\right)\to {F}\in \mathrm{LMod}$

### Proof

Step Hyp Ref Expression
1 frlmval.f ${⊢}{F}={R}\mathrm{freeLMod}{I}$
2 1 frlmval ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {W}\right)\to {F}={R}{\oplus }_{m}\left({I}×\left\{\mathrm{ringLMod}\left({R}\right)\right\}\right)$
3 simpr ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {W}\right)\to {I}\in {W}$
4 simpl ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {W}\right)\to {R}\in \mathrm{Ring}$
5 rlmlmod ${⊢}{R}\in \mathrm{Ring}\to \mathrm{ringLMod}\left({R}\right)\in \mathrm{LMod}$
6 5 adantr ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {W}\right)\to \mathrm{ringLMod}\left({R}\right)\in \mathrm{LMod}$
7 fconst6g ${⊢}\mathrm{ringLMod}\left({R}\right)\in \mathrm{LMod}\to \left({I}×\left\{\mathrm{ringLMod}\left({R}\right)\right\}\right):{I}⟶\mathrm{LMod}$
8 6 7 syl ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {W}\right)\to \left({I}×\left\{\mathrm{ringLMod}\left({R}\right)\right\}\right):{I}⟶\mathrm{LMod}$
9 fvex ${⊢}\mathrm{ringLMod}\left({R}\right)\in \mathrm{V}$
10 9 fvconst2 ${⊢}{i}\in {I}\to \left({I}×\left\{\mathrm{ringLMod}\left({R}\right)\right\}\right)\left({i}\right)=\mathrm{ringLMod}\left({R}\right)$
11 10 adantl ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {W}\right)\wedge {i}\in {I}\right)\to \left({I}×\left\{\mathrm{ringLMod}\left({R}\right)\right\}\right)\left({i}\right)=\mathrm{ringLMod}\left({R}\right)$
12 11 fveq2d ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {W}\right)\wedge {i}\in {I}\right)\to \mathrm{Scalar}\left(\left({I}×\left\{\mathrm{ringLMod}\left({R}\right)\right\}\right)\left({i}\right)\right)=\mathrm{Scalar}\left(\mathrm{ringLMod}\left({R}\right)\right)$
13 rlmsca ${⊢}{R}\in \mathrm{Ring}\to {R}=\mathrm{Scalar}\left(\mathrm{ringLMod}\left({R}\right)\right)$
14 13 ad2antrr ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {W}\right)\wedge {i}\in {I}\right)\to {R}=\mathrm{Scalar}\left(\mathrm{ringLMod}\left({R}\right)\right)$
15 12 14 eqtr4d ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {W}\right)\wedge {i}\in {I}\right)\to \mathrm{Scalar}\left(\left({I}×\left\{\mathrm{ringLMod}\left({R}\right)\right\}\right)\left({i}\right)\right)={R}$
16 eqid ${⊢}{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)$
17 3 4 8 15 16 dsmmlmod ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {W}\right)\to {R}{\oplus }_{m}\left({I}×\left\{\mathrm{ringLMod}\left({R}\right)\right\}\right)\in \mathrm{LMod}$
18 2 17 eqeltrd ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {W}\right)\to {F}\in \mathrm{LMod}$