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

Metamath Proof Explorer

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 eqtrid ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → 𝐹 = ( 𝑅 ⊕m ( 𝐼 × { ( ringLMod ‘ 𝑅 ) } ) ) )