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