mvmulfval

Description: Functional value of the matrix vector multiplication operator. (Contributed by AV, 23-Feb-2019)

	Ref	Expression
Hypotheses	mvmulfval.x	$⊢ \underset{˙}{\times} = R maVecMul ⟨M, N⟩$
	mvmulfval.b	$⊢ B = {Base}_{R}$
	mvmulfval.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	mvmulfval.r	$⊢ φ \to R \in V$
	mvmulfval.m	$⊢ φ \to M \in Fin$
	mvmulfval.n	$⊢ φ \to N \in Fin$
Assertion	mvmulfval	$⊢ φ \to \underset{˙}{\times} = (x \in (B^{(M \times N)}), y \in (B^{N}) ⟼ (i \in M ⟼ \underset{j \in N}{\sum_{R}} ((i x j) \underset{˙}{\cdot} y (j))))$

Proof

Step	Hyp	Ref	Expression
1		mvmulfval.x	$⊢ \underset{˙}{\times} = R maVecMul ⟨M, N⟩$
2		mvmulfval.b	$⊢ B = {Base}_{R}$
3		mvmulfval.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		mvmulfval.r	$⊢ φ \to R \in V$
5		mvmulfval.m	$⊢ φ \to M \in Fin$
6		mvmulfval.n	$⊢ φ \to N \in Fin$
7		df-mvmul	$⊢ maVecMul = (r \in V, o \in V ⟼ ⦋ 1^{st} (o) / m ⦌ ⦋ 2^{nd} (o) / n ⦌ (x \in ({Base}_{r}^{(m \times n)}), y \in ({Base}_{r}^{n}) ⟼ (i \in m ⟼ \underset{j \in n}{\sum_{r}} ((i x j) \cdot_{r} y (j)))))$
8	7	a1i	$⊢ φ \to maVecMul = (r \in V, o \in V ⟼ ⦋ 1^{st} (o) / m ⦌ ⦋ 2^{nd} (o) / n ⦌ (x \in ({Base}_{r}^{(m \times n)}), y \in ({Base}_{r}^{n}) ⟼ (i \in m ⟼ \underset{j \in n}{\sum_{r}} ((i x j) \cdot_{r} y (j)))))$
9		fvex	$⊢ 1^{st} (o) \in V$
10		fvex	$⊢ 2^{nd} (o) \in V$
11		xpeq12	$⊢ (m = 1^{st} (o) \land n = 2^{nd} (o)) \to m \times n = 1^{st} (o) \times 2^{nd} (o)$
12	11	oveq2d	$⊢ (m = 1^{st} (o) \land n = 2^{nd} (o)) \to {Base}_{r}^{(m \times n)} = {Base}_{r}^{(1^{st} (o) \times 2^{nd} (o))}$
13		oveq2	$⊢ n = 2^{nd} (o) \to {Base}_{r}^{n} = {Base}_{r}^{2^{nd} (o)}$
14	13	adantl	$⊢ (m = 1^{st} (o) \land n = 2^{nd} (o)) \to {Base}_{r}^{n} = {Base}_{r}^{2^{nd} (o)}$
15		simpl	$⊢ (m = 1^{st} (o) \land n = 2^{nd} (o)) \to m = 1^{st} (o)$
16		simpr	$⊢ (m = 1^{st} (o) \land n = 2^{nd} (o)) \to n = 2^{nd} (o)$
17	16	mpteq1d	$⊢ (m = 1^{st} (o) \land n = 2^{nd} (o)) \to (j \in n ⟼ (i x j) \cdot_{r} y (j)) = (j \in 2^{nd} (o) ⟼ (i x j) \cdot_{r} y (j))$
18	17	oveq2d	$⊢ (m = 1^{st} (o) \land n = 2^{nd} (o)) \to \underset{j \in n}{\sum_{r}} ((i x j) \cdot_{r} y (j)) = \underset{j \in 2^{nd} (o)}{\sum_{r}} ((i x j) \cdot_{r} y (j))$
19	15 18	mpteq12dv	$⊢ (m = 1^{st} (o) \land n = 2^{nd} (o)) \to (i \in m ⟼ \underset{j \in n}{\sum_{r}} ((i x j) \cdot_{r} y (j))) = (i \in 1^{st} (o) ⟼ \underset{j \in 2^{nd} (o)}{\sum_{r}} ((i x j) \cdot_{r} y (j)))$
20	12 14 19	mpoeq123dv	$⊢ (m = 1^{st} (o) \land n = 2^{nd} (o)) \to (x \in ({Base}_{r}^{(m \times n)}), y \in ({Base}_{r}^{n}) ⟼ (i \in m ⟼ \underset{j \in n}{\sum_{r}} ((i x j) \cdot_{r} y (j)))) = (x \in ({Base}_{r}^{(1^{st} (o) \times 2^{nd} (o))}), y \in ({Base}_{r}^{2^{nd} (o)}) ⟼ (i \in 1^{st} (o) ⟼ \underset{j \in 2^{nd} (o)}{\sum_{r}} ((i x j) \cdot_{r} y (j))))$
21	9 10 20	csbie2	$⊢ ⦋ 1^{st} (o) / m ⦌ ⦋ 2^{nd} (o) / n ⦌ (x \in ({Base}_{r}^{(m \times n)}), y \in ({Base}_{r}^{n}) ⟼ (i \in m ⟼ \underset{j \in n}{\sum_{r}} ((i x j) \cdot_{r} y (j)))) = (x \in ({Base}_{r}^{(1^{st} (o) \times 2^{nd} (o))}), y \in ({Base}_{r}^{2^{nd} (o)}) ⟼ (i \in 1^{st} (o) ⟼ \underset{j \in 2^{nd} (o)}{\sum_{r}} ((i x j) \cdot_{r} y (j))))$
22		simprl	$⊢ (φ \land (r = R \land o = ⟨M, N⟩)) \to r = R$
23	22	fveq2d	$⊢ (φ \land (r = R \land o = ⟨M, N⟩)) \to {Base}_{r} = {Base}_{R}$
24	23 2	eqtr4di	$⊢ (φ \land (r = R \land o = ⟨M, N⟩)) \to {Base}_{r} = B$
25		fveq2	$⊢ o = ⟨M, N⟩ \to 1^{st} (o) = 1^{st} (⟨M, N⟩)$
26	25	ad2antll	$⊢ (φ \land (r = R \land o = ⟨M, N⟩)) \to 1^{st} (o) = 1^{st} (⟨M, N⟩)$
27		op1stg	$⊢ (M \in Fin \land N \in Fin) \to 1^{st} (⟨M, N⟩) = M$
28	5 6 27	syl2anc	$⊢ φ \to 1^{st} (⟨M, N⟩) = M$
29	28	adantr	$⊢ (φ \land (r = R \land o = ⟨M, N⟩)) \to 1^{st} (⟨M, N⟩) = M$
30	26 29	eqtrd	$⊢ (φ \land (r = R \land o = ⟨M, N⟩)) \to 1^{st} (o) = M$
31		fveq2	$⊢ o = ⟨M, N⟩ \to 2^{nd} (o) = 2^{nd} (⟨M, N⟩)$
32	31	ad2antll	$⊢ (φ \land (r = R \land o = ⟨M, N⟩)) \to 2^{nd} (o) = 2^{nd} (⟨M, N⟩)$
33		op2ndg	$⊢ (M \in Fin \land N \in Fin) \to 2^{nd} (⟨M, N⟩) = N$
34	5 6 33	syl2anc	$⊢ φ \to 2^{nd} (⟨M, N⟩) = N$
35	34	adantr	$⊢ (φ \land (r = R \land o = ⟨M, N⟩)) \to 2^{nd} (⟨M, N⟩) = N$
36	32 35	eqtrd	$⊢ (φ \land (r = R \land o = ⟨M, N⟩)) \to 2^{nd} (o) = N$
37	30 36	xpeq12d	$⊢ (φ \land (r = R \land o = ⟨M, N⟩)) \to 1^{st} (o) \times 2^{nd} (o) = M \times N$
38	24 37	oveq12d	$⊢ (φ \land (r = R \land o = ⟨M, N⟩)) \to {Base}_{r}^{(1^{st} (o) \times 2^{nd} (o))} = B^{(M \times N)}$
39	24 36	oveq12d	$⊢ (φ \land (r = R \land o = ⟨M, N⟩)) \to {Base}_{r}^{2^{nd} (o)} = B^{N}$
40		fveq2	$⊢ r = R \to \cdot_{r} = \cdot_{R}$
41	40	adantr	$⊢ (r = R \land o = ⟨M, N⟩) \to \cdot_{r} = \cdot_{R}$
42	41	adantl	$⊢ (φ \land (r = R \land o = ⟨M, N⟩)) \to \cdot_{r} = \cdot_{R}$
43	42 3	eqtr4di	$⊢ (φ \land (r = R \land o = ⟨M, N⟩)) \to \cdot_{r} = \underset{˙}{\cdot}$
44	43	oveqd	$⊢ (φ \land (r = R \land o = ⟨M, N⟩)) \to (i x j) \cdot_{r} y (j) = (i x j) \underset{˙}{\cdot} y (j)$
45	36 44	mpteq12dv	$⊢ (φ \land (r = R \land o = ⟨M, N⟩)) \to (j \in 2^{nd} (o) ⟼ (i x j) \cdot_{r} y (j)) = (j \in N ⟼ (i x j) \underset{˙}{\cdot} y (j))$
46	22 45	oveq12d	$⊢ (φ \land (r = R \land o = ⟨M, N⟩)) \to \underset{j \in 2^{nd} (o)}{\sum_{r}} ((i x j) \cdot_{r} y (j)) = \underset{j \in N}{\sum_{R}} ((i x j) \underset{˙}{\cdot} y (j))$
47	30 46	mpteq12dv	$⊢ (φ \land (r = R \land o = ⟨M, N⟩)) \to (i \in 1^{st} (o) ⟼ \underset{j \in 2^{nd} (o)}{\sum_{r}} ((i x j) \cdot_{r} y (j))) = (i \in M ⟼ \underset{j \in N}{\sum_{R}} ((i x j) \underset{˙}{\cdot} y (j)))$
48	38 39 47	mpoeq123dv	$⊢ (φ \land (r = R \land o = ⟨M, N⟩)) \to (x \in ({Base}_{r}^{(1^{st} (o) \times 2^{nd} (o))}), y \in ({Base}_{r}^{2^{nd} (o)}) ⟼ (i \in 1^{st} (o) ⟼ \underset{j \in 2^{nd} (o)}{\sum_{r}} ((i x j) \cdot_{r} y (j)))) = (x \in (B^{(M \times N)}), y \in (B^{N}) ⟼ (i \in M ⟼ \underset{j \in N}{\sum_{R}} ((i x j) \underset{˙}{\cdot} y (j))))$
49	21 48	syl5eq	$⊢ (φ \land (r = R \land o = ⟨M, N⟩)) \to ⦋ 1^{st} (o) / m ⦌ ⦋ 2^{nd} (o) / n ⦌ (x \in ({Base}_{r}^{(m \times n)}), y \in ({Base}_{r}^{n}) ⟼ (i \in m ⟼ \underset{j \in n}{\sum_{r}} ((i x j) \cdot_{r} y (j)))) = (x \in (B^{(M \times N)}), y \in (B^{N}) ⟼ (i \in M ⟼ \underset{j \in N}{\sum_{R}} ((i x j) \underset{˙}{\cdot} y (j))))$
50	4	elexd	$⊢ φ \to R \in V$
51		opex	$⊢ ⟨M, N⟩ \in V$
52	51	a1i	$⊢ φ \to ⟨M, N⟩ \in V$
53		ovex	$⊢ B^{(M \times N)} \in V$
54		ovex	$⊢ B^{N} \in V$
55	53 54	mpoex	$⊢ (x \in (B^{(M \times N)}), y \in (B^{N}) ⟼ (i \in M ⟼ \underset{j \in N}{\sum_{R}} ((i x j) \underset{˙}{\cdot} y (j)))) \in V$
56	55	a1i	$⊢ φ \to (x \in (B^{(M \times N)}), y \in (B^{N}) ⟼ (i \in M ⟼ \underset{j \in N}{\sum_{R}} ((i x j) \underset{˙}{\cdot} y (j)))) \in V$
57	8 49 50 52 56	ovmpod	$⊢ φ \to R maVecMul ⟨M, N⟩ = (x \in (B^{(M \times N)}), y \in (B^{N}) ⟼ (i \in M ⟼ \underset{j \in N}{\sum_{R}} ((i x j) \underset{˙}{\cdot} y (j))))$
58	1 57	syl5eq	$⊢ φ \to \underset{˙}{\times} = (x \in (B^{(M \times N)}), y \in (B^{N}) ⟼ (i \in M ⟼ \underset{j \in N}{\sum_{R}} ((i x j) \underset{˙}{\cdot} y (j))))$

Metamath Proof Explorer

Theorem mvmulfval

Proof