# 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 𝐹 = ( 𝑅 freeLMod 𝐼 )
Assertion frlmlmod ( ( 𝑅 ∈ Ring ∧ 𝐼𝑊 ) → 𝐹 ∈ LMod )

### Proof

Step Hyp Ref Expression
1 frlmval.f 𝐹 = ( 𝑅 freeLMod 𝐼 )
2 1 frlmval ( ( 𝑅 ∈ Ring ∧ 𝐼𝑊 ) → 𝐹 = ( 𝑅m ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) )
3 simpr ( ( 𝑅 ∈ Ring ∧ 𝐼𝑊 ) → 𝐼𝑊 )
4 simpl ( ( 𝑅 ∈ Ring ∧ 𝐼𝑊 ) → 𝑅 ∈ Ring )
5 rlmlmod ( 𝑅 ∈ Ring → ( ringLMod ‘ 𝑅 ) ∈ LMod )
6 5 adantr ( ( 𝑅 ∈ Ring ∧ 𝐼𝑊 ) → ( ringLMod ‘ 𝑅 ) ∈ LMod )
7 fconst6g ( ( ringLMod ‘ 𝑅 ) ∈ LMod → ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) : 𝐼 ⟶ LMod )
8 6 7 syl ( ( 𝑅 ∈ Ring ∧ 𝐼𝑊 ) → ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) : 𝐼 ⟶ LMod )
9 fvex ( ringLMod ‘ 𝑅 ) ∈ V
10 9 fvconst2 ( 𝑖𝐼 → ( ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ‘ 𝑖 ) = ( ringLMod ‘ 𝑅 ) )
11 10 adantl ( ( ( 𝑅 ∈ Ring ∧ 𝐼𝑊 ) ∧ 𝑖𝐼 ) → ( ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ‘ 𝑖 ) = ( ringLMod ‘ 𝑅 ) )
12 11 fveq2d ( ( ( 𝑅 ∈ Ring ∧ 𝐼𝑊 ) ∧ 𝑖𝐼 ) → ( Scalar ‘ ( ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ‘ 𝑖 ) ) = ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) )
13 rlmsca ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) )
14 13 ad2antrr ( ( ( 𝑅 ∈ Ring ∧ 𝐼𝑊 ) ∧ 𝑖𝐼 ) → 𝑅 = ( Scalar ‘ ( ringLMod ‘ 𝑅 ) ) )
15 12 14 eqtr4d ( ( ( 𝑅 ∈ Ring ∧ 𝐼𝑊 ) ∧ 𝑖𝐼 ) → ( Scalar ‘ ( ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ‘ 𝑖 ) ) = 𝑅 )
16 eqid ( 𝑅m ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) = ( 𝑅m ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) )
17 3 4 8 15 16 dsmmlmod ( ( 𝑅 ∈ Ring ∧ 𝐼𝑊 ) → ( 𝑅m ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ∈ LMod )
18 2 17 eqeltrd ( ( 𝑅 ∈ Ring ∧ 𝐼𝑊 ) → 𝐹 ∈ LMod )