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 ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 𝑌 𝑘 ) ) ) ) ) )