frlmlmod

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

		Ref	Expression
	Hypothesis	frlmval.f	$⊢ F = R freeLMod I$
	Assertion	frlmlmod	$⊢ (R \in Ring \land I \in W) \to F \in LMod$

Step	Hyp	Ref	Expression
1		frlmval.f	$⊢ F = R freeLMod I$
2	1	frlmval	$⊢ (R \in Ring \land I \in W) \to F = R \oplus_{m} (I \times \{ringLMod (R)\})$
3		simpr	$⊢ (R \in Ring \land I \in W) \to I \in W$
4		simpl	$⊢ (R \in Ring \land I \in W) \to R \in Ring$
5		rlmlmod	$⊢ R \in Ring \to ringLMod (R) \in LMod$
6	5	adantr	$⊢ (R \in Ring \land I \in W) \to ringLMod (R) \in LMod$
7		fconst6g	$⊢ ringLMod (R) \in LMod \to (I \times \{ringLMod (R)\}) : I ⟶ LMod$
8	6 7	syl	$⊢ (R \in Ring \land I \in W) \to (I \times \{ringLMod (R)\}) : I ⟶ LMod$
9		fvex	$⊢ ringLMod (R) \in V$
10	9	fvconst2	$⊢ i \in I \to (I \times \{ringLMod (R)\}) (i) = ringLMod (R)$
11	10	adantl	$⊢ ((R \in Ring \land I \in W) \land i \in I) \to (I \times \{ringLMod (R)\}) (i) = ringLMod (R)$
12	11	fveq2d	$⊢ ((R \in Ring \land I \in W) \land i \in I) \to Scalar ((I \times \{ringLMod (R)\}) (i)) = Scalar (ringLMod (R))$
13		rlmsca	$⊢ R \in Ring \to R = Scalar (ringLMod (R))$
14	13	ad2antrr	$⊢ ((R \in Ring \land I \in W) \land i \in I) \to R = Scalar (ringLMod (R))$
15	12 14	eqtr4d	$⊢ ((R \in Ring \land I \in W) \land i \in I) \to Scalar ((I \times \{ringLMod (R)\}) (i)) = R$
16		eqid	$⊢ R \oplus_{m} (I \times \{ringLMod (R)\}) = R \oplus_{m} (I \times \{ringLMod (R)\})$
17	3 4 8 15 16	dsmmlmod	$⊢ (R \in Ring \land I \in W) \to R \oplus_{m} (I \times \{ringLMod (R)\}) \in LMod$
18	2 17	eqeltrd	$⊢ (R \in Ring \land I \in W) \to F \in LMod$

Metamath Proof Explorer