mpomatmul

Description: Multiplication of two N x N matrices given in maps-to notation. (Contributed by AV, 29-Oct-2019)

	Ref	Expression
Hypotheses	mpomatmul.a	$⊢ A = N Mat R$
	mpomatmul.b	$⊢ B = {Base}_{R}$
	mpomatmul.m	$⊢ \underset{˙}{\times} = \cdot_{A}$
	mpomatmul.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	mpomatmul.r	$⊢ φ \to R \in V$
	mpomatmul.n	$⊢ φ \to N \in Fin$
	mpomatmul.x	$⊢ X = (i \in N, j \in N ⟼ C)$
	mpomatmul.y	$⊢ Y = (i \in N, j \in N ⟼ E)$
	mpomatmul.c	$⊢ (φ \land i \in N \land j \in N) \to C \in B$
	mpomatmul.e	$⊢ (φ \land i \in N \land j \in N) \to E \in B$
	mpomatmul.d	$⊢ (φ \land (k = i \land m = j)) \to D = C$
	mpomatmul.f	$⊢ (φ \land (m = i \land l = j)) \to F = E$
	mpomatmul.1	$⊢ (φ \land k \in N \land m \in N) \to D \in U$
	mpomatmul.2	$⊢ (φ \land m \in N \land l \in N) \to F \in W$
Assertion	mpomatmul	$⊢ φ \to X \underset{˙}{\times} Y = (k \in N, l \in N ⟼ \underset{m \in N}{\sum_{R}} (D \underset{˙}{\cdot} F))$

Proof

Step	Hyp	Ref	Expression
1		mpomatmul.a	$⊢ A = N Mat R$
2		mpomatmul.b	$⊢ B = {Base}_{R}$
3		mpomatmul.m	$⊢ \underset{˙}{\times} = \cdot_{A}$
4		mpomatmul.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
5		mpomatmul.r	$⊢ φ \to R \in V$
6		mpomatmul.n	$⊢ φ \to N \in Fin$
7		mpomatmul.x	$⊢ X = (i \in N, j \in N ⟼ C)$
8		mpomatmul.y	$⊢ Y = (i \in N, j \in N ⟼ E)$
9		mpomatmul.c	$⊢ (φ \land i \in N \land j \in N) \to C \in B$
10		mpomatmul.e	$⊢ (φ \land i \in N \land j \in N) \to E \in B$
11		mpomatmul.d	$⊢ (φ \land (k = i \land m = j)) \to D = C$
12		mpomatmul.f	$⊢ (φ \land (m = i \land l = j)) \to F = E$
13		mpomatmul.1	$⊢ (φ \land k \in N \land m \in N) \to D \in U$
14		mpomatmul.2	$⊢ (φ \land m \in N \land l \in N) \to F \in W$
15		eqid	$⊢ R maMul ⟨N, N, N⟩ = R maMul ⟨N, N, N⟩$
16	1 15	matmulr	$⊢ (N \in Fin \land R \in V) \to R maMul ⟨N, N, N⟩ = \cdot_{A}$
17	16 3	eqtr4di	$⊢ (N \in Fin \land R \in V) \to R maMul ⟨N, N, N⟩ = \underset{˙}{\times}$
18	17	oveqd	$⊢ (N \in Fin \land R \in V) \to X (R maMul ⟨N, N, N⟩) Y = X \underset{˙}{\times} Y$
19	18	eqcomd	$⊢ (N \in Fin \land R \in V) \to X \underset{˙}{\times} Y = X (R maMul ⟨N, N, N⟩) Y$
20	6 5 19	syl2anc	$⊢ φ \to X \underset{˙}{\times} Y = X (R maMul ⟨N, N, N⟩) Y$
21		eqid	$⊢ {Base}_{R} = {Base}_{R}$
22		eqid	$⊢ {Base}_{A} = {Base}_{A}$
23	9 2	eleqtrdi	$⊢ (φ \land i \in N \land j \in N) \to C \in {Base}_{R}$
24	1 21 22 6 5 23	matbas2d	$⊢ φ \to (i \in N, j \in N ⟼ C) \in {Base}_{A}$
25	7 24	eqeltrid	$⊢ φ \to X \in {Base}_{A}$
26	1 21	matbas2	$⊢ (N \in Fin \land R \in V) \to {Base}_{R}^{(N \times N)} = {Base}_{A}$
27	6 5 26	syl2anc	$⊢ φ \to {Base}_{R}^{(N \times N)} = {Base}_{A}$
28	25 27	eleqtrrd	$⊢ φ \to X \in ({Base}_{R}^{(N \times N)})$
29	10 2	eleqtrdi	$⊢ (φ \land i \in N \land j \in N) \to E \in {Base}_{R}$
30	1 21 22 6 5 29	matbas2d	$⊢ φ \to (i \in N, j \in N ⟼ E) \in {Base}_{A}$
31	8 30	eqeltrid	$⊢ φ \to Y \in {Base}_{A}$
32	31 27	eleqtrrd	$⊢ φ \to Y \in ({Base}_{R}^{(N \times N)})$
33	15 21 4 5 6 6 6 28 32	mamuval	$⊢ φ \to X (R maMul ⟨N, N, N⟩) Y = (k \in N, l \in N ⟼ \underset{m \in N}{\sum_{R}} ((k X m) \underset{˙}{\cdot} (m Y l)))$
34	7	a1i	$⊢ ((φ \land k \in N \land l \in N) \land m \in N) \to X = (i \in N, j \in N ⟼ C)$
35		equcom	$⊢ i = k \leftrightarrow k = i$
36		equcom	$⊢ j = m \leftrightarrow m = j$
37	35 36	anbi12i	$⊢ (i = k \land j = m) \leftrightarrow (k = i \land m = j)$
38	37 11	sylan2b	$⊢ (φ \land (i = k \land j = m)) \to D = C$
39	38	eqcomd	$⊢ (φ \land (i = k \land j = m)) \to C = D$
40	39	ex	$⊢ φ \to ((i = k \land j = m) \to C = D)$
41	40	3ad2ant1	$⊢ (φ \land k \in N \land l \in N) \to ((i = k \land j = m) \to C = D)$
42	41	adantr	$⊢ ((φ \land k \in N \land l \in N) \land m \in N) \to ((i = k \land j = m) \to C = D)$
43	42	imp	$⊢ (((φ \land k \in N \land l \in N) \land m \in N) \land (i = k \land j = m)) \to C = D$
44		simpl2	$⊢ ((φ \land k \in N \land l \in N) \land m \in N) \to k \in N$
45		simpr	$⊢ ((φ \land k \in N \land l \in N) \land m \in N) \to m \in N$
46		simpl1	$⊢ ((φ \land k \in N \land l \in N) \land m \in N) \to φ$
47	46 44 45 13	syl3anc	$⊢ ((φ \land k \in N \land l \in N) \land m \in N) \to D \in U$
48	34 43 44 45 47	ovmpod	$⊢ ((φ \land k \in N \land l \in N) \land m \in N) \to k X m = D$
49	8	a1i	$⊢ ((φ \land k \in N \land l \in N) \land m \in N) \to Y = (i \in N, j \in N ⟼ E)$
50		equcomi	$⊢ i = m \to m = i$
51		equcomi	$⊢ j = l \to l = j$
52	50 51	anim12i	$⊢ (i = m \land j = l) \to (m = i \land l = j)$
53	52 12	sylan2	$⊢ (φ \land (i = m \land j = l)) \to F = E$
54	53	ex	$⊢ φ \to ((i = m \land j = l) \to F = E)$
55	54	3ad2ant1	$⊢ (φ \land k \in N \land l \in N) \to ((i = m \land j = l) \to F = E)$
56	55	adantr	$⊢ ((φ \land k \in N \land l \in N) \land m \in N) \to ((i = m \land j = l) \to F = E)$
57	56	imp	$⊢ (((φ \land k \in N \land l \in N) \land m \in N) \land (i = m \land j = l)) \to F = E$
58	57	eqcomd	$⊢ (((φ \land k \in N \land l \in N) \land m \in N) \land (i = m \land j = l)) \to E = F$
59		simpl3	$⊢ ((φ \land k \in N \land l \in N) \land m \in N) \to l \in N$
60	46 45 59 14	syl3anc	$⊢ ((φ \land k \in N \land l \in N) \land m \in N) \to F \in W$
61	49 58 45 59 60	ovmpod	$⊢ ((φ \land k \in N \land l \in N) \land m \in N) \to m Y l = F$
62	48 61	oveq12d	$⊢ ((φ \land k \in N \land l \in N) \land m \in N) \to (k X m) \underset{˙}{\cdot} (m Y l) = D \underset{˙}{\cdot} F$
63	62	mpteq2dva	$⊢ (φ \land k \in N \land l \in N) \to (m \in N ⟼ (k X m) \underset{˙}{\cdot} (m Y l)) = (m \in N ⟼ D \underset{˙}{\cdot} F)$
64	63	oveq2d	$⊢ (φ \land k \in N \land l \in N) \to \underset{m \in N}{\sum_{R}} ((k X m) \underset{˙}{\cdot} (m Y l)) = \underset{m \in N}{\sum_{R}} (D \underset{˙}{\cdot} F)$
65	64	mpoeq3dva	$⊢ φ \to (k \in N, l \in N ⟼ \underset{m \in N}{\sum_{R}} ((k X m) \underset{˙}{\cdot} (m Y l))) = (k \in N, l \in N ⟼ \underset{m \in N}{\sum_{R}} (D \underset{˙}{\cdot} F))$
66	20 33 65	3eqtrd	$⊢ φ \to X \underset{˙}{\times} Y = (k \in N, l \in N ⟼ \underset{m \in N}{\sum_{R}} (D \underset{˙}{\cdot} F))$

Metamath Proof Explorer

Theorem mpomatmul

Proof