mamufval

Description: Functional value of the matrix multiplication operator. (Contributed by Stefan O'Rear, 2-Sep-2015)

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

Proof

Step	Hyp	Ref	Expression
1		mamufval.f	$⊢ F = R maMul ⟨M, N, P⟩$
2		mamufval.b	$⊢ B = {Base}_{R}$
3		mamufval.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		mamufval.r	$⊢ φ \to R \in V$
5		mamufval.m	$⊢ φ \to M \in Fin$
6		mamufval.n	$⊢ φ \to N \in Fin$
7		mamufval.p	$⊢ φ \to P \in Fin$
8		df-mamu	$⊢ maMul = (r \in V, o \in V ⟼ ⦋ 1^{st} (1^{st} (o)) / m ⦌ ⦋ 2^{nd} (1^{st} (o)) / n ⦌ ⦋ 2^{nd} (o) / p ⦌ (x \in ({Base}_{r}^{(m \times n)}), y \in ({Base}_{r}^{(n \times p)}) ⟼ (i \in m, k \in p ⟼ \underset{j \in n}{\sum_{r}} ((i x j) \cdot_{r} (j y k)))))$
9	8	a1i	$⊢ φ \to maMul = (r \in V, o \in V ⟼ ⦋ 1^{st} (1^{st} (o)) / m ⦌ ⦋ 2^{nd} (1^{st} (o)) / n ⦌ ⦋ 2^{nd} (o) / p ⦌ (x \in ({Base}_{r}^{(m \times n)}), y \in ({Base}_{r}^{(n \times p)}) ⟼ (i \in m, k \in p ⟼ \underset{j \in n}{\sum_{r}} ((i x j) \cdot_{r} (j y k)))))$
10		fvex	$⊢ 1^{st} (1^{st} (o)) \in V$
11		fvex	$⊢ 2^{nd} (1^{st} (o)) \in V$
12		fvex	$⊢ 2^{nd} (o) \in V$
13		eqidd	$⊢ p = 2^{nd} (o) \to {Base}_{r}^{(m \times n)} = {Base}_{r}^{(m \times n)}$
14		xpeq2	$⊢ p = 2^{nd} (o) \to n \times p = n \times 2^{nd} (o)$
15	14	oveq2d	$⊢ p = 2^{nd} (o) \to {Base}_{r}^{(n \times p)} = {Base}_{r}^{(n \times 2^{nd} (o))}$
16		eqidd	$⊢ p = 2^{nd} (o) \to m = m$
17		id	$⊢ p = 2^{nd} (o) \to p = 2^{nd} (o)$
18		eqidd	$⊢ p = 2^{nd} (o) \to \underset{j \in n}{\sum_{r}} ((i x j) \cdot_{r} (j y k)) = \underset{j \in n}{\sum_{r}} ((i x j) \cdot_{r} (j y k))$
19	16 17 18	mpoeq123dv	$⊢ p = 2^{nd} (o) \to (i \in m, k \in p ⟼ \underset{j \in n}{\sum_{r}} ((i x j) \cdot_{r} (j y k))) = (i \in m, k \in 2^{nd} (o) ⟼ \underset{j \in n}{\sum_{r}} ((i x j) \cdot_{r} (j y k)))$
20	13 15 19	mpoeq123dv	$⊢ p = 2^{nd} (o) \to (x \in ({Base}_{r}^{(m \times n)}), y \in ({Base}_{r}^{(n \times p)}) ⟼ (i \in m, k \in p ⟼ \underset{j \in n}{\sum_{r}} ((i x j) \cdot_{r} (j y k)))) = (x \in ({Base}_{r}^{(m \times n)}), y \in ({Base}_{r}^{(n \times 2^{nd} (o))}) ⟼ (i \in m, k \in 2^{nd} (o) ⟼ \underset{j \in n}{\sum_{r}} ((i x j) \cdot_{r} (j y k))))$
21	12 20	csbie	$⊢ ⦋ 2^{nd} (o) / p ⦌ (x \in ({Base}_{r}^{(m \times n)}), y \in ({Base}_{r}^{(n \times p)}) ⟼ (i \in m, k \in p ⟼ \underset{j \in n}{\sum_{r}} ((i x j) \cdot_{r} (j y k)))) = (x \in ({Base}_{r}^{(m \times n)}), y \in ({Base}_{r}^{(n \times 2^{nd} (o))}) ⟼ (i \in m, k \in 2^{nd} (o) ⟼ \underset{j \in n}{\sum_{r}} ((i x j) \cdot_{r} (j y k))))$
22		xpeq12	$⊢ (m = 1^{st} (1^{st} (o)) \land n = 2^{nd} (1^{st} (o))) \to m \times n = 1^{st} (1^{st} (o)) \times 2^{nd} (1^{st} (o))$
23	22	oveq2d	$⊢ (m = 1^{st} (1^{st} (o)) \land n = 2^{nd} (1^{st} (o))) \to {Base}_{r}^{(m \times n)} = {Base}_{r}^{(1^{st} (1^{st} (o)) \times 2^{nd} (1^{st} (o)))}$
24		simpr	$⊢ (m = 1^{st} (1^{st} (o)) \land n = 2^{nd} (1^{st} (o))) \to n = 2^{nd} (1^{st} (o))$
25	24	xpeq1d	$⊢ (m = 1^{st} (1^{st} (o)) \land n = 2^{nd} (1^{st} (o))) \to n \times 2^{nd} (o) = 2^{nd} (1^{st} (o)) \times 2^{nd} (o)$
26	25	oveq2d	$⊢ (m = 1^{st} (1^{st} (o)) \land n = 2^{nd} (1^{st} (o))) \to {Base}_{r}^{(n \times 2^{nd} (o))} = {Base}_{r}^{(2^{nd} (1^{st} (o)) \times 2^{nd} (o))}$
27		id	$⊢ m = 1^{st} (1^{st} (o)) \to m = 1^{st} (1^{st} (o))$
28	27	adantr	$⊢ (m = 1^{st} (1^{st} (o)) \land n = 2^{nd} (1^{st} (o))) \to m = 1^{st} (1^{st} (o))$
29		eqidd	$⊢ (m = 1^{st} (1^{st} (o)) \land n = 2^{nd} (1^{st} (o))) \to 2^{nd} (o) = 2^{nd} (o)$
30		eqidd	$⊢ (m = 1^{st} (1^{st} (o)) \land n = 2^{nd} (1^{st} (o))) \to (i x j) \cdot_{r} (j y k) = (i x j) \cdot_{r} (j y k)$
31	24 30	mpteq12dv	$⊢ (m = 1^{st} (1^{st} (o)) \land n = 2^{nd} (1^{st} (o))) \to (j \in n ⟼ (i x j) \cdot_{r} (j y k)) = (j \in 2^{nd} (1^{st} (o)) ⟼ (i x j) \cdot_{r} (j y k))$
32	31	oveq2d	$⊢ (m = 1^{st} (1^{st} (o)) \land n = 2^{nd} (1^{st} (o))) \to \underset{j \in n}{\sum_{r}} ((i x j) \cdot_{r} (j y k)) = \underset{j \in 2^{nd} (1^{st} (o))}{\sum_{r}} ((i x j) \cdot_{r} (j y k))$
33	28 29 32	mpoeq123dv	$⊢ (m = 1^{st} (1^{st} (o)) \land n = 2^{nd} (1^{st} (o))) \to (i \in m, k \in 2^{nd} (o) ⟼ \underset{j \in n}{\sum_{r}} ((i x j) \cdot_{r} (j y k))) = (i \in 1^{st} (1^{st} (o)), k \in 2^{nd} (o) ⟼ \underset{j \in 2^{nd} (1^{st} (o))}{\sum_{r}} ((i x j) \cdot_{r} (j y k)))$
34	23 26 33	mpoeq123dv	$⊢ (m = 1^{st} (1^{st} (o)) \land n = 2^{nd} (1^{st} (o))) \to (x \in ({Base}_{r}^{(m \times n)}), y \in ({Base}_{r}^{(n \times 2^{nd} (o))}) ⟼ (i \in m, k \in 2^{nd} (o) ⟼ \underset{j \in n}{\sum_{r}} ((i x j) \cdot_{r} (j y k)))) = (x \in ({Base}_{r}^{(1^{st} (1^{st} (o)) \times 2^{nd} (1^{st} (o)))}), y \in ({Base}_{r}^{(2^{nd} (1^{st} (o)) \times 2^{nd} (o))}) ⟼ (i \in 1^{st} (1^{st} (o)), k \in 2^{nd} (o) ⟼ \underset{j \in 2^{nd} (1^{st} (o))}{\sum_{r}} ((i x j) \cdot_{r} (j y k))))$
35	21 34	syl5eq	$⊢ (m = 1^{st} (1^{st} (o)) \land n = 2^{nd} (1^{st} (o))) \to ⦋ 2^{nd} (o) / p ⦌ (x \in ({Base}_{r}^{(m \times n)}), y \in ({Base}_{r}^{(n \times p)}) ⟼ (i \in m, k \in p ⟼ \underset{j \in n}{\sum_{r}} ((i x j) \cdot_{r} (j y k)))) = (x \in ({Base}_{r}^{(1^{st} (1^{st} (o)) \times 2^{nd} (1^{st} (o)))}), y \in ({Base}_{r}^{(2^{nd} (1^{st} (o)) \times 2^{nd} (o))}) ⟼ (i \in 1^{st} (1^{st} (o)), k \in 2^{nd} (o) ⟼ \underset{j \in 2^{nd} (1^{st} (o))}{\sum_{r}} ((i x j) \cdot_{r} (j y k))))$
36	10 11 35	csbie2	$⊢ ⦋ 1^{st} (1^{st} (o)) / m ⦌ ⦋ 2^{nd} (1^{st} (o)) / n ⦌ ⦋ 2^{nd} (o) / p ⦌ (x \in ({Base}_{r}^{(m \times n)}), y \in ({Base}_{r}^{(n \times p)}) ⟼ (i \in m, k \in p ⟼ \underset{j \in n}{\sum_{r}} ((i x j) \cdot_{r} (j y k)))) = (x \in ({Base}_{r}^{(1^{st} (1^{st} (o)) \times 2^{nd} (1^{st} (o)))}), y \in ({Base}_{r}^{(2^{nd} (1^{st} (o)) \times 2^{nd} (o))}) ⟼ (i \in 1^{st} (1^{st} (o)), k \in 2^{nd} (o) ⟼ \underset{j \in 2^{nd} (1^{st} (o))}{\sum_{r}} ((i x j) \cdot_{r} (j y k))))$
37		simprl	$⊢ (φ \land (r = R \land o = ⟨M, N, P⟩)) \to r = R$
38	37	fveq2d	$⊢ (φ \land (r = R \land o = ⟨M, N, P⟩)) \to {Base}_{r} = {Base}_{R}$
39	38 2	eqtr4di	$⊢ (φ \land (r = R \land o = ⟨M, N, P⟩)) \to {Base}_{r} = B$
40		fveq2	$⊢ o = ⟨M, N, P⟩ \to 1^{st} (o) = 1^{st} (⟨M, N, P⟩)$
41	40	fveq2d	$⊢ o = ⟨M, N, P⟩ \to 1^{st} (1^{st} (o)) = 1^{st} (1^{st} (⟨M, N, P⟩))$
42	41	ad2antll	$⊢ (φ \land (r = R \land o = ⟨M, N, P⟩)) \to 1^{st} (1^{st} (o)) = 1^{st} (1^{st} (⟨M, N, P⟩))$
43		ot1stg	$⊢ (M \in Fin \land N \in Fin \land P \in Fin) \to 1^{st} (1^{st} (⟨M, N, P⟩)) = M$
44	5 6 7 43	syl3anc	$⊢ φ \to 1^{st} (1^{st} (⟨M, N, P⟩)) = M$
45	44	adantr	$⊢ (φ \land (r = R \land o = ⟨M, N, P⟩)) \to 1^{st} (1^{st} (⟨M, N, P⟩)) = M$
46	42 45	eqtrd	$⊢ (φ \land (r = R \land o = ⟨M, N, P⟩)) \to 1^{st} (1^{st} (o)) = M$
47	40	fveq2d	$⊢ o = ⟨M, N, P⟩ \to 2^{nd} (1^{st} (o)) = 2^{nd} (1^{st} (⟨M, N, P⟩))$
48	47	ad2antll	$⊢ (φ \land (r = R \land o = ⟨M, N, P⟩)) \to 2^{nd} (1^{st} (o)) = 2^{nd} (1^{st} (⟨M, N, P⟩))$
49		ot2ndg	$⊢ (M \in Fin \land N \in Fin \land P \in Fin) \to 2^{nd} (1^{st} (⟨M, N, P⟩)) = N$
50	5 6 7 49	syl3anc	$⊢ φ \to 2^{nd} (1^{st} (⟨M, N, P⟩)) = N$
51	50	adantr	$⊢ (φ \land (r = R \land o = ⟨M, N, P⟩)) \to 2^{nd} (1^{st} (⟨M, N, P⟩)) = N$
52	48 51	eqtrd	$⊢ (φ \land (r = R \land o = ⟨M, N, P⟩)) \to 2^{nd} (1^{st} (o)) = N$
53	46 52	xpeq12d	$⊢ (φ \land (r = R \land o = ⟨M, N, P⟩)) \to 1^{st} (1^{st} (o)) \times 2^{nd} (1^{st} (o)) = M \times N$
54	39 53	oveq12d	$⊢ (φ \land (r = R \land o = ⟨M, N, P⟩)) \to {Base}_{r}^{(1^{st} (1^{st} (o)) \times 2^{nd} (1^{st} (o)))} = B^{(M \times N)}$
55		fveq2	$⊢ o = ⟨M, N, P⟩ \to 2^{nd} (o) = 2^{nd} (⟨M, N, P⟩)$
56	55	ad2antll	$⊢ (φ \land (r = R \land o = ⟨M, N, P⟩)) \to 2^{nd} (o) = 2^{nd} (⟨M, N, P⟩)$
57		ot3rdg	$⊢ P \in Fin \to 2^{nd} (⟨M, N, P⟩) = P$
58	7 57	syl	$⊢ φ \to 2^{nd} (⟨M, N, P⟩) = P$
59	58	adantr	$⊢ (φ \land (r = R \land o = ⟨M, N, P⟩)) \to 2^{nd} (⟨M, N, P⟩) = P$
60	56 59	eqtrd	$⊢ (φ \land (r = R \land o = ⟨M, N, P⟩)) \to 2^{nd} (o) = P$
61	52 60	xpeq12d	$⊢ (φ \land (r = R \land o = ⟨M, N, P⟩)) \to 2^{nd} (1^{st} (o)) \times 2^{nd} (o) = N \times P$
62	39 61	oveq12d	$⊢ (φ \land (r = R \land o = ⟨M, N, P⟩)) \to {Base}_{r}^{(2^{nd} (1^{st} (o)) \times 2^{nd} (o))} = B^{(N \times P)}$
63	37	fveq2d	$⊢ (φ \land (r = R \land o = ⟨M, N, P⟩)) \to \cdot_{r} = \cdot_{R}$
64	63 3	eqtr4di	$⊢ (φ \land (r = R \land o = ⟨M, N, P⟩)) \to \cdot_{r} = \underset{˙}{\cdot}$
65	64	oveqd	$⊢ (φ \land (r = R \land o = ⟨M, N, P⟩)) \to (i x j) \cdot_{r} (j y k) = (i x j) \underset{˙}{\cdot} (j y k)$
66	52 65	mpteq12dv	$⊢ (φ \land (r = R \land o = ⟨M, N, P⟩)) \to (j \in 2^{nd} (1^{st} (o)) ⟼ (i x j) \cdot_{r} (j y k)) = (j \in N ⟼ (i x j) \underset{˙}{\cdot} (j y k))$
67	37 66	oveq12d	$⊢ (φ \land (r = R \land o = ⟨M, N, P⟩)) \to \underset{j \in 2^{nd} (1^{st} (o))}{\sum_{r}} ((i x j) \cdot_{r} (j y k)) = \underset{j \in N}{\sum_{R}} ((i x j) \underset{˙}{\cdot} (j y k))$
68	46 60 67	mpoeq123dv	$⊢ (φ \land (r = R \land o = ⟨M, N, P⟩)) \to (i \in 1^{st} (1^{st} (o)), k \in 2^{nd} (o) ⟼ \underset{j \in 2^{nd} (1^{st} (o))}{\sum_{r}} ((i x j) \cdot_{r} (j y k))) = (i \in M, k \in P ⟼ \underset{j \in N}{\sum_{R}} ((i x j) \underset{˙}{\cdot} (j y k)))$
69	54 62 68	mpoeq123dv	$⊢ (φ \land (r = R \land o = ⟨M, N, P⟩)) \to (x \in ({Base}_{r}^{(1^{st} (1^{st} (o)) \times 2^{nd} (1^{st} (o)))}), y \in ({Base}_{r}^{(2^{nd} (1^{st} (o)) \times 2^{nd} (o))}) ⟼ (i \in 1^{st} (1^{st} (o)), k \in 2^{nd} (o) ⟼ \underset{j \in 2^{nd} (1^{st} (o))}{\sum_{r}} ((i x j) \cdot_{r} (j y k)))) = (x \in (B^{(M \times N)}), y \in (B^{(N \times P)}) ⟼ (i \in M, k \in P ⟼ \underset{j \in N}{\sum_{R}} ((i x j) \underset{˙}{\cdot} (j y k))))$
70	36 69	syl5eq	$⊢ (φ \land (r = R \land o = ⟨M, N, P⟩)) \to ⦋ 1^{st} (1^{st} (o)) / m ⦌ ⦋ 2^{nd} (1^{st} (o)) / n ⦌ ⦋ 2^{nd} (o) / p ⦌ (x \in ({Base}_{r}^{(m \times n)}), y \in ({Base}_{r}^{(n \times p)}) ⟼ (i \in m, k \in p ⟼ \underset{j \in n}{\sum_{r}} ((i x j) \cdot_{r} (j y k)))) = (x \in (B^{(M \times N)}), y \in (B^{(N \times P)}) ⟼ (i \in M, k \in P ⟼ \underset{j \in N}{\sum_{R}} ((i x j) \underset{˙}{\cdot} (j y k))))$
71	4	elexd	$⊢ φ \to R \in V$
72		otex	$⊢ ⟨M, N, P⟩ \in V$
73	72	a1i	$⊢ φ \to ⟨M, N, P⟩ \in V$
74		ovex	$⊢ B^{(M \times N)} \in V$
75		ovex	$⊢ B^{(N \times P)} \in V$
76	74 75	mpoex	$⊢ (x \in (B^{(M \times N)}), y \in (B^{(N \times P)}) ⟼ (i \in M, k \in P ⟼ \underset{j \in N}{\sum_{R}} ((i x j) \underset{˙}{\cdot} (j y k)))) \in V$
77	76	a1i	$⊢ φ \to (x \in (B^{(M \times N)}), y \in (B^{(N \times P)}) ⟼ (i \in M, k \in P ⟼ \underset{j \in N}{\sum_{R}} ((i x j) \underset{˙}{\cdot} (j y k)))) \in V$
78	9 70 71 73 77	ovmpod	$⊢ φ \to R maMul ⟨M, N, P⟩ = (x \in (B^{(M \times N)}), y \in (B^{(N \times P)}) ⟼ (i \in M, k \in P ⟼ \underset{j \in N}{\sum_{R}} ((i x j) \underset{˙}{\cdot} (j y k))))$
79	1 78	syl5eq	$⊢ φ \to F = (x \in (B^{(M \times N)}), y \in (B^{(N \times P)}) ⟼ (i \in M, k \in P ⟼ \underset{j \in N}{\sum_{R}} ((i x j) \underset{˙}{\cdot} (j y k))))$

Metamath Proof Explorer

Theorem mamufval

Proof