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

Metamath Proof Explorer

Theorem mvmulval

Description: Multiplication of a vector with a matrix. (Contributed by AV, 23-Feb-2019)

Ref Expression
Hypotheses mvmulfval.x ⊢ × = ( 𝑅 maVecMul ⟨ 𝑀 , 𝑁 ⟩ )
mvmulfval.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
mvmulfval.t ⊢ · = ( .r ‘ 𝑅 )
mvmulfval.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
mvmulfval.m ⊢ ( 𝜑 → 𝑀 ∈ Fin )
mvmulfval.n ⊢ ( 𝜑 → 𝑁 ∈ Fin )
mvmulval.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐵 ↑m ( 𝑀 × 𝑁 ) ) )
mvmulval.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐵 ↑m 𝑁 ) )
Assertion mvmulval ( 𝜑 → ( 𝑋 × 𝑌 ) = ( 𝑖 ∈ 𝑀 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌 ‘ 𝑗 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mvmulfval.x ⊢ × = ( 𝑅 maVecMul ⟨ 𝑀 , 𝑁 ⟩ )
2 mvmulfval.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 mvmulfval.t ⊢ · = ( .r ‘ 𝑅 )
4 mvmulfval.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
5 mvmulfval.m ⊢ ( 𝜑 → 𝑀 ∈ Fin )
6 mvmulfval.n ⊢ ( 𝜑 → 𝑁 ∈ Fin )
7 mvmulval.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐵 ↑m ( 𝑀 × 𝑁 ) ) )
8 mvmulval.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐵 ↑m 𝑁 ) )
9 1 2 3 4 5 6 mvmulfval ⊢ ( 𝜑 → × = ( 𝑥 ∈ ( 𝐵 ↑m ( 𝑀 × 𝑁 ) ) , 𝑦 ∈ ( 𝐵 ↑m 𝑁 ) ↦ ( 𝑖 ∈ 𝑀 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑗 ) · ( 𝑦 ‘ 𝑗 ) ) ) ) ) ) )
10 oveq ⊢ ( 𝑥 = 𝑋 → ( 𝑖 𝑥 𝑗 ) = ( 𝑖 𝑋 𝑗 ) )
11 fveq1 ⊢ ( 𝑦 = 𝑌 → ( 𝑦 ‘ 𝑗 ) = ( 𝑌 ‘ 𝑗 ) )
12 10 11 oveqan12d ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( ( 𝑖 𝑥 𝑗 ) · ( 𝑦 ‘ 𝑗 ) ) = ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌 ‘ 𝑗 ) ) )
13 12 adantl ⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( ( 𝑖 𝑥 𝑗 ) · ( 𝑦 ‘ 𝑗 ) ) = ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌 ‘ 𝑗 ) ) )
14 13 mpteq2dv ⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑗 ) · ( 𝑦 ‘ 𝑗 ) ) ) = ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌 ‘ 𝑗 ) ) ) )
15 14 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑗 ) · ( 𝑦 ‘ 𝑗 ) ) ) ) = ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌 ‘ 𝑗 ) ) ) ) )
16 15 mpteq2dv ⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( 𝑖 ∈ 𝑀 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑗 ) · ( 𝑦 ‘ 𝑗 ) ) ) ) ) = ( 𝑖 ∈ 𝑀 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌 ‘ 𝑗 ) ) ) ) ) )
17 5 mptexd ⊢ ( 𝜑 → ( 𝑖 ∈ 𝑀 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌 ‘ 𝑗 ) ) ) ) ) ∈ V )
18 9 16 7 8 17 ovmpod ⊢ ( 𝜑 → ( 𝑋 × 𝑌 ) = ( 𝑖 ∈ 𝑀 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌 ‘ 𝑗 ) ) ) ) ) )