Theorem mavmulval

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

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

Proof

Step	Hyp	Ref	Expression
1		mavmulval.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		mavmulval.m	⊢ × = ( 𝑅 maVecMul ⟨ 𝑁 , 𝑁 ⟩ )
3		mavmulval.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
4		mavmulval.t	⊢ · = ( .r ‘ 𝑅 )
5		mavmulval.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
6		mavmulval.n	⊢ ( 𝜑 → 𝑁 ∈ Fin )
7		mavmulval.x	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐴 ) )
8		mavmulval.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝐵 ↑m 𝑁 ) )
9	1 3	matbas2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ( 𝐵 ↑m ( 𝑁 × 𝑁 ) ) = ( Base ‘ 𝐴 ) )
10	6 5 9	syl2anc	⊢ ( 𝜑 → ( 𝐵 ↑m ( 𝑁 × 𝑁 ) ) = ( Base ‘ 𝐴 ) )
11	7 10	eleqtrrd	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐵 ↑m ( 𝑁 × 𝑁 ) ) )
12	2 3 4 5 6 6 11 8	mvmulval	⊢ ( 𝜑 → ( 𝑋 × 𝑌 ) = ( 𝑖 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌 ‘ 𝑗 ) ) ) ) ) )