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

Metamath Proof Explorer

Theorem mamufv

Description: A cell in the multiplication of two matrices. (Contributed by Stefan O'Rear, 2-Sep-2015)

Ref Expression
Hypotheses mamufval.f ⊢ 𝐹 = ( 𝑅 maMul ⟨ 𝑀 , 𝑁 , 𝑃 ⟩ )
mamufval.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
mamufval.t ⊢ · = ( .r ‘ 𝑅 )
mamufval.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
mamufval.m ⊢ ( 𝜑 → 𝑀 ∈ Fin )
mamufval.n ⊢ ( 𝜑 → 𝑁 ∈ Fin )
mamufval.p ⊢ ( 𝜑 → 𝑃 ∈ Fin )
mamuval.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐵 ↑m ( 𝑀 × 𝑁 ) ) )
mamuval.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐵 ↑m ( 𝑁 × 𝑃 ) ) )
mamufv.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑀 )
mamufv.k ⊢ ( 𝜑 → 𝐾 ∈ 𝑃 )
Assertion mamufv ( 𝜑 → ( 𝐼 ( 𝑋 𝐹 𝑌 ) 𝐾 ) = ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝐼 𝑋 𝑗 ) · ( 𝑗 𝑌 𝐾 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mamufval.f ⊢ 𝐹 = ( 𝑅 maMul ⟨ 𝑀 , 𝑁 , 𝑃 ⟩ )
2 mamufval.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 mamufval.t ⊢ · = ( .r ‘ 𝑅 )
4 mamufval.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
5 mamufval.m ⊢ ( 𝜑 → 𝑀 ∈ Fin )
6 mamufval.n ⊢ ( 𝜑 → 𝑁 ∈ Fin )
7 mamufval.p ⊢ ( 𝜑 → 𝑃 ∈ Fin )
8 mamuval.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐵 ↑m ( 𝑀 × 𝑁 ) ) )
9 mamuval.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐵 ↑m ( 𝑁 × 𝑃 ) ) )
10 mamufv.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑀 )
11 mamufv.k ⊢ ( 𝜑 → 𝐾 ∈ 𝑃 )
12 1 2 3 4 5 6 7 8 9 mamuval ⊢ ( 𝜑 → ( 𝑋 𝐹 𝑌 ) = ( 𝑖 ∈ 𝑀 , 𝑘 ∈ 𝑃 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 𝑌 𝑘 ) ) ) ) ) )
13 oveq1 ⊢ ( 𝑖 = 𝐼 → ( 𝑖 𝑋 𝑗 ) = ( 𝐼 𝑋 𝑗 ) )
14 oveq2 ⊢ ( 𝑘 = 𝐾 → ( 𝑗 𝑌 𝑘 ) = ( 𝑗 𝑌 𝐾 ) )
15 13 14 oveqan12d ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑘 = 𝐾 ) → ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 𝑌 𝑘 ) ) = ( ( 𝐼 𝑋 𝑗 ) · ( 𝑗 𝑌 𝐾 ) ) )
16 15 adantl ⊢ ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑘 = 𝐾 ) ) → ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 𝑌 𝑘 ) ) = ( ( 𝐼 𝑋 𝑗 ) · ( 𝑗 𝑌 𝐾 ) ) )
17 16 mpteq2dv ⊢ ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑘 = 𝐾 ) ) → ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 𝑌 𝑘 ) ) ) = ( 𝑗 ∈ 𝑁 ↦ ( ( 𝐼 𝑋 𝑗 ) · ( 𝑗 𝑌 𝐾 ) ) ) )
18 17 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑘 = 𝐾 ) ) → ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 𝑌 𝑘 ) ) ) ) = ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝐼 𝑋 𝑗 ) · ( 𝑗 𝑌 𝐾 ) ) ) ) )
19 ovexd ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝐼 𝑋 𝑗 ) · ( 𝑗 𝑌 𝐾 ) ) ) ) ∈ V )
20 12 18 10 11 19 ovmpod ⊢ ( 𝜑 → ( 𝐼 ( 𝑋 𝐹 𝑌 ) 𝐾 ) = ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝐼 𝑋 𝑗 ) · ( 𝑗 𝑌 𝐾 ) ) ) ) )