Theorem frlmval

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

	Ref	Expression
Hypothesis	frlmval.f	⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
Assertion	frlmval	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝐹 = ( 𝑅 ⊕m ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) )

Proof

Step	Hyp	Ref	Expression
1		frlmval.f	⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
2		elex	⊢ ( 𝑅 ∈ 𝑉 → 𝑅 ∈ V )
3		elex	⊢ ( 𝐼 ∈ 𝑊 → 𝐼 ∈ V )
4		id	⊢ ( 𝑟 = 𝑅 → 𝑟 = 𝑅 )
5		fveq2	⊢ ( 𝑟 = 𝑅 → ( ringLMod ‘ 𝑟 ) = ( ringLMod ‘ 𝑅 ) )
6	5	sneqd	⊢ ( 𝑟 = 𝑅 → { ( ringLMod ‘ 𝑟 ) } = { ( ringLMod ‘ 𝑅 ) } )
7	6	xpeq2d	⊢ ( 𝑟 = 𝑅 → ( 𝑖 × { ( ringLMod ‘ 𝑟 ) } ) = ( 𝑖 × { ( ringLMod ‘ 𝑅 ) } ) )
8	4 7	oveq12d	⊢ ( 𝑟 = 𝑅 → ( 𝑟 ⊕m ( 𝑖 × { ( ringLMod ‘ 𝑟 ) } ) ) = ( 𝑅 ⊕m ( 𝑖 × { ( ringLMod ‘ 𝑅 ) } ) ) )
9		xpeq1	⊢ ( 𝑖 = 𝐼 → ( 𝑖 × { ( ringLMod ‘ 𝑅 ) } ) = ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) )
10	9	oveq2d	⊢ ( 𝑖 = 𝐼 → ( 𝑅 ⊕m ( 𝑖 × { ( ringLMod ‘ 𝑅 ) } ) ) = ( 𝑅 ⊕m ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) )
11		df-frlm	⊢ freeLMod = ( 𝑟 ∈ V , 𝑖 ∈ V ↦ ( 𝑟 ⊕m ( 𝑖 × { ( ringLMod ‘ 𝑟 ) } ) ) )
12		ovex	⊢ ( 𝑅 ⊕m ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) ∈ V
13	8 10 11 12	ovmpo	⊢ ( ( 𝑅 ∈ V ∧ 𝐼 ∈ V ) → ( 𝑅 freeLMod 𝐼 ) = ( 𝑅 ⊕m ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) )
14	2 3 13	syl2an	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( 𝑅 freeLMod 𝐼 ) = ( 𝑅 ⊕m ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) )
15	1 14	syl5eq	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝐹 = ( 𝑅 ⊕m ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) )