Theorem mvmumamul1

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

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

Proof

Step	Hyp	Ref	Expression
1		mvmumamul1.x	⊢ × = ( 𝑅 maMul ⟨ 𝑀 , 𝑁 , { ∅ } ⟩ )
2		mvmumamul1.t	⊢ · = ( 𝑅 maVecMul ⟨ 𝑀 , 𝑁 ⟩ )
3		mvmumamul1.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
4		mvmumamul1.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
5		mvmumamul1.m	⊢ ( 𝜑 → 𝑀 ∈ Fin )
6		mvmumamul1.n	⊢ ( 𝜑 → 𝑁 ∈ Fin )
7		mvmumamul1.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐵 ↑m ( 𝑀 × 𝑁 ) ) )
8		mvmumamul1.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝐵 ↑m 𝑁 ) )
9		mvmumamul1.z	⊢ ( 𝜑 → 𝑍 ∈ ( 𝐵 ↑m ( 𝑁 × { ∅ } ) ) )
10		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
11	4	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) → 𝑅 ∈ Ring )
12	5	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) → 𝑀 ∈ Fin )
13	6	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) → 𝑁 ∈ Fin )
14	7	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) → 𝐴 ∈ ( 𝐵 ↑m ( 𝑀 × 𝑁 ) ) )
15	8	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) → 𝑌 ∈ ( 𝐵 ↑m 𝑁 ) )
16		simpr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) → 𝑖 ∈ 𝑀 )
17	2 3 10 11 12 13 14 15 16	mvmulfv	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) → ( ( 𝐴 · 𝑌 ) ‘ 𝑖 ) = ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝐴 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑘 ) ) ) ) )
18	17	adantlr	⊢ ( ( ( 𝜑 ∧ ∀ 𝑗 ∈ 𝑁 ( 𝑌 ‘ 𝑗 ) = ( 𝑗 𝑍 ∅ ) ) ∧ 𝑖 ∈ 𝑀 ) → ( ( 𝐴 · 𝑌 ) ‘ 𝑖 ) = ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝐴 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑘 ) ) ) ) )
19		fveq2	⊢ ( 𝑗 = 𝑘 → ( 𝑌 ‘ 𝑗 ) = ( 𝑌 ‘ 𝑘 ) )
20		oveq1	⊢ ( 𝑗 = 𝑘 → ( 𝑗 𝑍 ∅ ) = ( 𝑘 𝑍 ∅ ) )
21	19 20	eqeq12d	⊢ ( 𝑗 = 𝑘 → ( ( 𝑌 ‘ 𝑗 ) = ( 𝑗 𝑍 ∅ ) ↔ ( 𝑌 ‘ 𝑘 ) = ( 𝑘 𝑍 ∅ ) ) )
22	21	rspccv	⊢ ( ∀ 𝑗 ∈ 𝑁 ( 𝑌 ‘ 𝑗 ) = ( 𝑗 𝑍 ∅ ) → ( 𝑘 ∈ 𝑁 → ( 𝑌 ‘ 𝑘 ) = ( 𝑘 𝑍 ∅ ) ) )
23	22	adantl	⊢ ( ( 𝜑 ∧ ∀ 𝑗 ∈ 𝑁 ( 𝑌 ‘ 𝑗 ) = ( 𝑗 𝑍 ∅ ) ) → ( 𝑘 ∈ 𝑁 → ( 𝑌 ‘ 𝑘 ) = ( 𝑘 𝑍 ∅ ) ) )
24	23	imp	⊢ ( ( ( 𝜑 ∧ ∀ 𝑗 ∈ 𝑁 ( 𝑌 ‘ 𝑗 ) = ( 𝑗 𝑍 ∅ ) ) ∧ 𝑘 ∈ 𝑁 ) → ( 𝑌 ‘ 𝑘 ) = ( 𝑘 𝑍 ∅ ) )
25	24	oveq2d	⊢ ( ( ( 𝜑 ∧ ∀ 𝑗 ∈ 𝑁 ( 𝑌 ‘ 𝑗 ) = ( 𝑗 𝑍 ∅ ) ) ∧ 𝑘 ∈ 𝑁 ) → ( ( 𝑖 𝐴 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑘 ) ) = ( ( 𝑖 𝐴 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑍 ∅ ) ) )
26	25	mpteq2dva	⊢ ( ( 𝜑 ∧ ∀ 𝑗 ∈ 𝑁 ( 𝑌 ‘ 𝑗 ) = ( 𝑗 𝑍 ∅ ) ) → ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝐴 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑘 ) ) ) = ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝐴 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑍 ∅ ) ) ) )
27	26	oveq2d	⊢ ( ( 𝜑 ∧ ∀ 𝑗 ∈ 𝑁 ( 𝑌 ‘ 𝑗 ) = ( 𝑗 𝑍 ∅ ) ) → ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝐴 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑘 ) ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝐴 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑍 ∅ ) ) ) ) )
28	27	adantr	⊢ ( ( ( 𝜑 ∧ ∀ 𝑗 ∈ 𝑁 ( 𝑌 ‘ 𝑗 ) = ( 𝑗 𝑍 ∅ ) ) ∧ 𝑖 ∈ 𝑀 ) → ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝐴 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑌 ‘ 𝑘 ) ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝐴 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑍 ∅ ) ) ) ) )
29		snfi	⊢ { ∅ } ∈ Fin
30	29	a1i	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) → { ∅ } ∈ Fin )
31	9	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) → 𝑍 ∈ ( 𝐵 ↑m ( 𝑁 × { ∅ } ) ) )
32		0ex	⊢ ∅ ∈ V
33	32	snid	⊢ ∅ ∈ { ∅ }
34	33	a1i	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) → ∅ ∈ { ∅ } )
35	1 3 10 11 12 13 30 14 31 16 34	mamufv	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) → ( 𝑖 ( 𝐴 × 𝑍 ) ∅ ) = ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝐴 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑍 ∅ ) ) ) ) )
36	35	eqcomd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑀 ) → ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝐴 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑍 ∅ ) ) ) ) = ( 𝑖 ( 𝐴 × 𝑍 ) ∅ ) )
37	36	adantlr	⊢ ( ( ( 𝜑 ∧ ∀ 𝑗 ∈ 𝑁 ( 𝑌 ‘ 𝑗 ) = ( 𝑗 𝑍 ∅ ) ) ∧ 𝑖 ∈ 𝑀 ) → ( 𝑅 Σg ( 𝑘 ∈ 𝑁 ↦ ( ( 𝑖 𝐴 𝑘 ) ( .r ‘ 𝑅 ) ( 𝑘 𝑍 ∅ ) ) ) ) = ( 𝑖 ( 𝐴 × 𝑍 ) ∅ ) )
38	18 28 37	3eqtrd	⊢ ( ( ( 𝜑 ∧ ∀ 𝑗 ∈ 𝑁 ( 𝑌 ‘ 𝑗 ) = ( 𝑗 𝑍 ∅ ) ) ∧ 𝑖 ∈ 𝑀 ) → ( ( 𝐴 · 𝑌 ) ‘ 𝑖 ) = ( 𝑖 ( 𝐴 × 𝑍 ) ∅ ) )
39	38	ralrimiva	⊢ ( ( 𝜑 ∧ ∀ 𝑗 ∈ 𝑁 ( 𝑌 ‘ 𝑗 ) = ( 𝑗 𝑍 ∅ ) ) → ∀ 𝑖 ∈ 𝑀 ( ( 𝐴 · 𝑌 ) ‘ 𝑖 ) = ( 𝑖 ( 𝐴 × 𝑍 ) ∅ ) )
40	39	ex	⊢ ( 𝜑 → ( ∀ 𝑗 ∈ 𝑁 ( 𝑌 ‘ 𝑗 ) = ( 𝑗 𝑍 ∅ ) → ∀ 𝑖 ∈ 𝑀 ( ( 𝐴 · 𝑌 ) ‘ 𝑖 ) = ( 𝑖 ( 𝐴 × 𝑍 ) ∅ ) ) )