Metamath Proof Explorer


Theorem mamuval

Description: 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 ( 𝑁 × 𝑃 ) ) )
Assertion mamuval ( 𝜑 → ( 𝑋 𝐹 𝑌 ) = ( 𝑖𝑀 , 𝑘𝑃 ↦ ( 𝑅 Σ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 1 2 3 4 5 6 7 mamufval ( 𝜑𝐹 = ( 𝑥 ∈ ( 𝐵m ( 𝑀 × 𝑁 ) ) , 𝑦 ∈ ( 𝐵m ( 𝑁 × 𝑃 ) ) ↦ ( 𝑖𝑀 , 𝑘𝑃 ↦ ( 𝑅 Σg ( 𝑗𝑁 ↦ ( ( 𝑖 𝑥 𝑗 ) · ( 𝑗 𝑦 𝑘 ) ) ) ) ) ) )
11 oveq ( 𝑥 = 𝑋 → ( 𝑖 𝑥 𝑗 ) = ( 𝑖 𝑋 𝑗 ) )
12 oveq ( 𝑦 = 𝑌 → ( 𝑗 𝑦 𝑘 ) = ( 𝑗 𝑌 𝑘 ) )
13 11 12 oveqan12d ( ( 𝑥 = 𝑋𝑦 = 𝑌 ) → ( ( 𝑖 𝑥 𝑗 ) · ( 𝑗 𝑦 𝑘 ) ) = ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 𝑌 𝑘 ) ) )
14 13 adantl ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) → ( ( 𝑖 𝑥 𝑗 ) · ( 𝑗 𝑦 𝑘 ) ) = ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 𝑌 𝑘 ) ) )
15 14 mpteq2dv ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) → ( 𝑗𝑁 ↦ ( ( 𝑖 𝑥 𝑗 ) · ( 𝑗 𝑦 𝑘 ) ) ) = ( 𝑗𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 𝑌 𝑘 ) ) ) )
16 15 oveq2d ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) → ( 𝑅 Σg ( 𝑗𝑁 ↦ ( ( 𝑖 𝑥 𝑗 ) · ( 𝑗 𝑦 𝑘 ) ) ) ) = ( 𝑅 Σg ( 𝑗𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 𝑌 𝑘 ) ) ) ) )
17 16 mpoeq3dv ( ( 𝜑 ∧ ( 𝑥 = 𝑋𝑦 = 𝑌 ) ) → ( 𝑖𝑀 , 𝑘𝑃 ↦ ( 𝑅 Σg ( 𝑗𝑁 ↦ ( ( 𝑖 𝑥 𝑗 ) · ( 𝑗 𝑦 𝑘 ) ) ) ) ) = ( 𝑖𝑀 , 𝑘𝑃 ↦ ( 𝑅 Σg ( 𝑗𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 𝑌 𝑘 ) ) ) ) ) )
18 mpoexga ( ( 𝑀 ∈ Fin ∧ 𝑃 ∈ Fin ) → ( 𝑖𝑀 , 𝑘𝑃 ↦ ( 𝑅 Σg ( 𝑗𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 𝑌 𝑘 ) ) ) ) ) ∈ V )
19 5 7 18 syl2anc ( 𝜑 → ( 𝑖𝑀 , 𝑘𝑃 ↦ ( 𝑅 Σg ( 𝑗𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 𝑌 𝑘 ) ) ) ) ) ∈ V )
20 10 17 8 9 19 ovmpod ( 𝜑 → ( 𝑋 𝐹 𝑌 ) = ( 𝑖𝑀 , 𝑘𝑃 ↦ ( 𝑅 Σg ( 𝑗𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 𝑌 𝑘 ) ) ) ) ) )