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 )