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

Metamath Proof Explorer

Theorem mavmumamul1

Description: The multiplication of an NxN matrix with an N-dimensional vector corresponds to the matrix multiplication of an NxN matrix with an Nx1 matrix. (Contributed by AV, 14-Mar-2019)

		Ref	Expression
	Hypotheses	mavmumamul1.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
		mavmumamul1.m	⊢ × = ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , { ∅ } ⟩ )
		mavmumamul1.t	⊢ · = ( 𝑅 maVecMul ⟨ 𝑁 , 𝑁 ⟩ )
		mavmumamul1.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
		mavmumamul1.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
		mavmumamul1.n	⊢ ( 𝜑 → 𝑁 ∈ Fin )
		mavmumamul1.x	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐴 ) )
		mavmumamul1.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝐵 ↑_m 𝑁 ) )
		mavmumamul1.z	⊢ ( 𝜑 → 𝑍 ∈ ( 𝐵 ↑_m ( 𝑁 × { ∅ } ) ) )
	Assertion	mavmumamul1	⊢ ( 𝜑 → ( ∀ 𝑗 ∈ 𝑁 ( 𝑌 ‘ 𝑗 ) = ( 𝑗 𝑍 ∅ ) → ∀ 𝑖 ∈ 𝑁 ( ( 𝑋 · 𝑌 ) ‘ 𝑖 ) = ( 𝑖 ( 𝑋 × 𝑍 ) ∅ ) ) )

Proof

Step	Hyp	Ref	Expression
1		mavmumamul1.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		mavmumamul1.m	⊢ × = ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , { ∅ } ⟩ )
3		mavmumamul1.t	⊢ · = ( 𝑅 maVecMul ⟨ 𝑁 , 𝑁 ⟩ )
4		mavmumamul1.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
5		mavmumamul1.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
6		mavmumamul1.n	⊢ ( 𝜑 → 𝑁 ∈ Fin )
7		mavmumamul1.x	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐴 ) )
8		mavmumamul1.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝐵 ↑_m 𝑁 ) )
9		mavmumamul1.z	⊢ ( 𝜑 → 𝑍 ∈ ( 𝐵 ↑_m ( 𝑁 × { ∅ } ) ) )
10	1 4	matbas2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝐵 ↑_m ( 𝑁 × 𝑁 ) ) = ( Base ‘ 𝐴 ) )
11	6 5 10	syl2anc	⊢ ( 𝜑 → ( 𝐵 ↑_m ( 𝑁 × 𝑁 ) ) = ( Base ‘ 𝐴 ) )
12	7 11	eleqtrrd	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐵 ↑_m ( 𝑁 × 𝑁 ) ) )
13	2 3 4 5 6 6 12 8 9	mvmumamul1	⊢ ( 𝜑 → ( ∀ 𝑗 ∈ 𝑁 ( 𝑌 ‘ 𝑗 ) = ( 𝑗 𝑍 ∅ ) → ∀ 𝑖 ∈ 𝑁 ( ( 𝑋 · 𝑌 ) ‘ 𝑖 ) = ( 𝑖 ( 𝑋 × 𝑍 ) ∅ ) ) )