frlmval

Description: Value of the "free module" function. (Contributed by Stefan O'Rear, 1-Feb-2015)

		Ref	Expression
	Hypothesis	frlmval.f	$⊢ F = R freeLMod I$
	Assertion	frlmval	$⊢ (R \in V \land I \in W) \to F = R \oplus_{m} (I \times \{ringLMod (R)\})$

Step	Hyp	Ref	Expression
1		frlmval.f	$⊢ F = R freeLMod I$
2		elex	$⊢ R \in V \to R \in V$
3		elex	$⊢ I \in W \to I \in V$
4		id	$⊢ r = R \to r = R$
5		fveq2	$⊢ r = R \to ringLMod (r) = ringLMod (R)$
6	5	sneqd	$⊢ r = R \to \{ringLMod (r)\} = \{ringLMod (R)\}$
7	6	xpeq2d	$⊢ r = R \to i \times \{ringLMod (r)\} = i \times \{ringLMod (R)\}$
8	4 7	oveq12d	$⊢ r = R \to r \oplus_{m} (i \times \{ringLMod (r)\}) = R \oplus_{m} (i \times \{ringLMod (R)\})$
9		xpeq1	$⊢ i = I \to i \times \{ringLMod (R)\} = I \times \{ringLMod (R)\}$
10	9	oveq2d	$⊢ i = I \to R \oplus_{m} (i \times \{ringLMod (R)\}) = R \oplus_{m} (I \times \{ringLMod (R)\})$
11		df-frlm	$⊢ freeLMod = (r \in V, i \in V ⟼ r \oplus_{m} (i \times \{ringLMod (r)\}))$
12		ovex	$⊢ R \oplus_{m} (I \times \{ringLMod (R)\}) \in V$
13	8 10 11 12	ovmpo	$⊢ (R \in V \land I \in V) \to R freeLMod I = R \oplus_{m} (I \times \{ringLMod (R)\})$
14	2 3 13	syl2an	$⊢ (R \in V \land I \in W) \to R freeLMod I = R \oplus_{m} (I \times \{ringLMod (R)\})$
15	1 14	syl5eq	$⊢ (R \in V \land I \in W) \to F = R \oplus_{m} (I \times \{ringLMod (R)\})$

Metamath Proof Explorer