This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )