mamuass

Description: Matrix multiplication is associative, see also statement in Lang p. 505. (Contributed by Stefan O'Rear, 5-Sep-2015)

	Ref	Expression
Hypotheses	mamucl.b	$⊢ B = {Base}_{R}$
	mamucl.r	$⊢ φ \to R \in Ring$
	mamuass.m	$⊢ φ \to M \in Fin$
	mamuass.n	$⊢ φ \to N \in Fin$
	mamuass.o	$⊢ φ \to O \in Fin$
	mamuass.p	$⊢ φ \to P \in Fin$
	mamuass.x	$⊢ φ \to X \in (B^{(M \times N)})$
	mamuass.y	$⊢ φ \to Y \in (B^{(N \times O)})$
	mamuass.z	$⊢ φ \to Z \in (B^{(O \times P)})$
	mamuass.f	$⊢ F = R maMul ⟨M, N, O⟩$
	mamuass.g	$⊢ G = R maMul ⟨M, O, P⟩$
	mamuass.h	$⊢ H = R maMul ⟨M, N, P⟩$
	mamuass.i	$⊢ I = R maMul ⟨N, O, P⟩$
Assertion	mamuass	$⊢ φ \to (X F Y) G Z = X H (Y I Z)$

Proof

Step	Hyp	Ref	Expression
1		mamucl.b	$⊢ B = {Base}_{R}$
2		mamucl.r	$⊢ φ \to R \in Ring$
3		mamuass.m	$⊢ φ \to M \in Fin$
4		mamuass.n	$⊢ φ \to N \in Fin$
5		mamuass.o	$⊢ φ \to O \in Fin$
6		mamuass.p	$⊢ φ \to P \in Fin$
7		mamuass.x	$⊢ φ \to X \in (B^{(M \times N)})$
8		mamuass.y	$⊢ φ \to Y \in (B^{(N \times O)})$
9		mamuass.z	$⊢ φ \to Z \in (B^{(O \times P)})$
10		mamuass.f	$⊢ F = R maMul ⟨M, N, O⟩$
11		mamuass.g	$⊢ G = R maMul ⟨M, O, P⟩$
12		mamuass.h	$⊢ H = R maMul ⟨M, N, P⟩$
13		mamuass.i	$⊢ I = R maMul ⟨N, O, P⟩$
14		ringcmn	$⊢ R \in Ring \to R \in CMnd$
15	2 14	syl	$⊢ φ \to R \in CMnd$
16	15	adantr	$⊢ (φ \land (i \in M \land k \in P)) \to R \in CMnd$
17	5	adantr	$⊢ (φ \land (i \in M \land k \in P)) \to O \in Fin$
18	4	adantr	$⊢ (φ \land (i \in M \land k \in P)) \to N \in Fin$
19	2	ad2antrr	$⊢ ((φ \land (i \in M \land k \in P)) \land (j \in O \land l \in N)) \to R \in Ring$
20		elmapi	$⊢ X \in (B^{(M \times N)}) \to X : M \times N ⟶ B$
21	7 20	syl	$⊢ φ \to X : M \times N ⟶ B$
22	21	ad2antrr	$⊢ ((φ \land (i \in M \land k \in P)) \land l \in N) \to X : M \times N ⟶ B$
23		simplrl	$⊢ ((φ \land (i \in M \land k \in P)) \land l \in N) \to i \in M$
24		simpr	$⊢ ((φ \land (i \in M \land k \in P)) \land l \in N) \to l \in N$
25	22 23 24	fovrnd	$⊢ ((φ \land (i \in M \land k \in P)) \land l \in N) \to i X l \in B$
26	25	adantrl	$⊢ ((φ \land (i \in M \land k \in P)) \land (j \in O \land l \in N)) \to i X l \in B$
27		elmapi	$⊢ Y \in (B^{(N \times O)}) \to Y : N \times O ⟶ B$
28	8 27	syl	$⊢ φ \to Y : N \times O ⟶ B$
29	28	ad2antrr	$⊢ ((φ \land (i \in M \land k \in P)) \land (j \in O \land l \in N)) \to Y : N \times O ⟶ B$
30		simprr	$⊢ ((φ \land (i \in M \land k \in P)) \land (j \in O \land l \in N)) \to l \in N$
31		simprl	$⊢ ((φ \land (i \in M \land k \in P)) \land (j \in O \land l \in N)) \to j \in O$
32	29 30 31	fovrnd	$⊢ ((φ \land (i \in M \land k \in P)) \land (j \in O \land l \in N)) \to l Y j \in B$
33		elmapi	$⊢ Z \in (B^{(O \times P)}) \to Z : O \times P ⟶ B$
34	9 33	syl	$⊢ φ \to Z : O \times P ⟶ B$
35	34	ad2antrr	$⊢ ((φ \land (i \in M \land k \in P)) \land j \in O) \to Z : O \times P ⟶ B$
36		simpr	$⊢ ((φ \land (i \in M \land k \in P)) \land j \in O) \to j \in O$
37		simplrr	$⊢ ((φ \land (i \in M \land k \in P)) \land j \in O) \to k \in P$
38	35 36 37	fovrnd	$⊢ ((φ \land (i \in M \land k \in P)) \land j \in O) \to j Z k \in B$
39	38	adantrr	$⊢ ((φ \land (i \in M \land k \in P)) \land (j \in O \land l \in N)) \to j Z k \in B$
40		eqid	$⊢ \cdot_{R} = \cdot_{R}$
41	1 40	ringcl	$⊢ (R \in Ring \land l Y j \in B \land j Z k \in B) \to (l Y j) \cdot_{R} (j Z k) \in B$
42	19 32 39 41	syl3anc	$⊢ ((φ \land (i \in M \land k \in P)) \land (j \in O \land l \in N)) \to (l Y j) \cdot_{R} (j Z k) \in B$
43	1 40	ringcl	$⊢ (R \in Ring \land i X l \in B \land (l Y j) \cdot_{R} (j Z k) \in B) \to (i X l) \cdot_{R} ((l Y j) \cdot_{R} (j Z k)) \in B$
44	19 26 42 43	syl3anc	$⊢ ((φ \land (i \in M \land k \in P)) \land (j \in O \land l \in N)) \to (i X l) \cdot_{R} ((l Y j) \cdot_{R} (j Z k)) \in B$
45	1 16 17 18 44	gsumcom3fi	$⊢ (φ \land (i \in M \land k \in P)) \to \underset{j \in O}{\sum_{R}} (\underset{l \in N}{\sum_{R}}, ((i X l) \cdot_{R} ((l Y j) \cdot_{R} (j Z k)))) = \underset{l \in N}{\sum_{R}} (\underset{j \in O}{\sum_{R}}, ((i X l) \cdot_{R} ((l Y j) \cdot_{R} (j Z k))))$
46	2	ad2antrr	$⊢ ((φ \land (i \in M \land k \in P)) \land j \in O) \to R \in Ring$
47	3	ad2antrr	$⊢ ((φ \land (i \in M \land k \in P)) \land j \in O) \to M \in Fin$
48	4	ad2antrr	$⊢ ((φ \land (i \in M \land k \in P)) \land j \in O) \to N \in Fin$
49	5	ad2antrr	$⊢ ((φ \land (i \in M \land k \in P)) \land j \in O) \to O \in Fin$
50	7	ad2antrr	$⊢ ((φ \land (i \in M \land k \in P)) \land j \in O) \to X \in (B^{(M \times N)})$
51	8	ad2antrr	$⊢ ((φ \land (i \in M \land k \in P)) \land j \in O) \to Y \in (B^{(N \times O)})$
52		simplrl	$⊢ ((φ \land (i \in M \land k \in P)) \land j \in O) \to i \in M$
53	10 1 40 46 47 48 49 50 51 52 36	mamufv	$⊢ ((φ \land (i \in M \land k \in P)) \land j \in O) \to i (X F Y) j = \underset{l \in N}{\sum_{R}} ((i X l) \cdot_{R} (l Y j))$
54	53	oveq1d	$⊢ ((φ \land (i \in M \land k \in P)) \land j \in O) \to (i (X F Y) j) \cdot_{R} (j Z k) = (\underset{l \in N}{\sum_{R}}, ((i X l) \cdot_{R} (l Y j))) \cdot_{R} (j Z k)$
55		eqid	$⊢ 0_{R} = 0_{R}$
56		eqid	$⊢ +_{R} = +_{R}$
57	1 40	ringcl	$⊢ (R \in Ring \land i X l \in B \land l Y j \in B) \to (i X l) \cdot_{R} (l Y j) \in B$
58	19 26 32 57	syl3anc	$⊢ ((φ \land (i \in M \land k \in P)) \land (j \in O \land l \in N)) \to (i X l) \cdot_{R} (l Y j) \in B$
59	58	anassrs	$⊢ (((φ \land (i \in M \land k \in P)) \land j \in O) \land l \in N) \to (i X l) \cdot_{R} (l Y j) \in B$
60		eqid	$⊢ (l \in N ⟼ (i X l) \cdot_{R} (l Y j)) = (l \in N ⟼ (i X l) \cdot_{R} (l Y j))$
61		ovexd	$⊢ (((φ \land (i \in M \land k \in P)) \land j \in O) \land l \in N) \to (i X l) \cdot_{R} (l Y j) \in V$
62		fvexd	$⊢ ((φ \land (i \in M \land k \in P)) \land j \in O) \to 0_{R} \in V$
63	60 48 61 62	fsuppmptdm	$⊢ ((φ \land (i \in M \land k \in P)) \land j \in O) \to {finSupp}_{0_{R}} ((l \in N ⟼ (i X l) \cdot_{R} (l Y j)))$
64	1 55 56 40 46 48 38 59 63	gsummulc1	$⊢ ((φ \land (i \in M \land k \in P)) \land j \in O) \to \underset{l \in N}{\sum_{R}} (((i X l) \cdot_{R} (l Y j)) \cdot_{R} (j Z k)) = (\underset{l \in N}{\sum_{R}}, ((i X l) \cdot_{R} (l Y j))) \cdot_{R} (j Z k)$
65	1 40	ringass	$⊢ (R \in Ring \land (i X l \in B \land l Y j \in B \land j Z k \in B)) \to ((i X l) \cdot_{R} (l Y j)) \cdot_{R} (j Z k) = (i X l) \cdot_{R} ((l Y j) \cdot_{R} (j Z k))$
66	19 26 32 39 65	syl13anc	$⊢ ((φ \land (i \in M \land k \in P)) \land (j \in O \land l \in N)) \to ((i X l) \cdot_{R} (l Y j)) \cdot_{R} (j Z k) = (i X l) \cdot_{R} ((l Y j) \cdot_{R} (j Z k))$
67	66	anassrs	$⊢ (((φ \land (i \in M \land k \in P)) \land j \in O) \land l \in N) \to ((i X l) \cdot_{R} (l Y j)) \cdot_{R} (j Z k) = (i X l) \cdot_{R} ((l Y j) \cdot_{R} (j Z k))$
68	67	mpteq2dva	$⊢ ((φ \land (i \in M \land k \in P)) \land j \in O) \to (l \in N ⟼ ((i X l) \cdot_{R} (l Y j)) \cdot_{R} (j Z k)) = (l \in N ⟼ (i X l) \cdot_{R} ((l Y j) \cdot_{R} (j Z k)))$
69	68	oveq2d	$⊢ ((φ \land (i \in M \land k \in P)) \land j \in O) \to \underset{l \in N}{\sum_{R}} (((i X l) \cdot_{R} (l Y j)) \cdot_{R} (j Z k)) = \underset{l \in N}{\sum_{R}} ((i X l) \cdot_{R} ((l Y j) \cdot_{R} (j Z k)))$
70	54 64 69	3eqtr2d	$⊢ ((φ \land (i \in M \land k \in P)) \land j \in O) \to (i (X F Y) j) \cdot_{R} (j Z k) = \underset{l \in N}{\sum_{R}} ((i X l) \cdot_{R} ((l Y j) \cdot_{R} (j Z k)))$
71	70	mpteq2dva	$⊢ (φ \land (i \in M \land k \in P)) \to (j \in O ⟼ (i (X F Y) j) \cdot_{R} (j Z k)) = (j \in O ⟼ \underset{l \in N}{\sum_{R}} ((i X l) \cdot_{R} ((l Y j) \cdot_{R} (j Z k))))$
72	71	oveq2d	$⊢ (φ \land (i \in M \land k \in P)) \to \underset{j \in O}{\sum_{R}} ((i (X F Y) j) \cdot_{R} (j Z k)) = \underset{j \in O}{\sum_{R}} (\underset{l \in N}{\sum_{R}}, ((i X l) \cdot_{R} ((l Y j) \cdot_{R} (j Z k))))$
73	2	ad2antrr	$⊢ ((φ \land (i \in M \land k \in P)) \land l \in N) \to R \in Ring$
74	4	ad2antrr	$⊢ ((φ \land (i \in M \land k \in P)) \land l \in N) \to N \in Fin$
75	5	ad2antrr	$⊢ ((φ \land (i \in M \land k \in P)) \land l \in N) \to O \in Fin$
76	6	ad2antrr	$⊢ ((φ \land (i \in M \land k \in P)) \land l \in N) \to P \in Fin$
77	8	ad2antrr	$⊢ ((φ \land (i \in M \land k \in P)) \land l \in N) \to Y \in (B^{(N \times O)})$
78	9	ad2antrr	$⊢ ((φ \land (i \in M \land k \in P)) \land l \in N) \to Z \in (B^{(O \times P)})$
79		simplrr	$⊢ ((φ \land (i \in M \land k \in P)) \land l \in N) \to k \in P$
80	13 1 40 73 74 75 76 77 78 24 79	mamufv	$⊢ ((φ \land (i \in M \land k \in P)) \land l \in N) \to l (Y I Z) k = \underset{j \in O}{\sum_{R}} ((l Y j) \cdot_{R} (j Z k))$
81	80	oveq2d	$⊢ ((φ \land (i \in M \land k \in P)) \land l \in N) \to (i X l) \cdot_{R} (l (Y I Z) k) = (i X l) \cdot_{R} (\underset{j \in O}{\sum_{R}}, ((l Y j) \cdot_{R} (j Z k)))$
82	42	anass1rs	$⊢ (((φ \land (i \in M \land k \in P)) \land l \in N) \land j \in O) \to (l Y j) \cdot_{R} (j Z k) \in B$
83		eqid	$⊢ (j \in O ⟼ (l Y j) \cdot_{R} (j Z k)) = (j \in O ⟼ (l Y j) \cdot_{R} (j Z k))$
84		ovexd	$⊢ (((φ \land (i \in M \land k \in P)) \land l \in N) \land j \in O) \to (l Y j) \cdot_{R} (j Z k) \in V$
85		fvexd	$⊢ ((φ \land (i \in M \land k \in P)) \land l \in N) \to 0_{R} \in V$
86	83 75 84 85	fsuppmptdm	$⊢ ((φ \land (i \in M \land k \in P)) \land l \in N) \to {finSupp}_{0_{R}} ((j \in O ⟼ (l Y j) \cdot_{R} (j Z k)))$
87	1 55 56 40 73 75 25 82 86	gsummulc2	$⊢ ((φ \land (i \in M \land k \in P)) \land l \in N) \to \underset{j \in O}{\sum_{R}} ((i X l) \cdot_{R} ((l Y j) \cdot_{R} (j Z k))) = (i X l) \cdot_{R} (\underset{j \in O}{\sum_{R}}, ((l Y j) \cdot_{R} (j Z k)))$
88	81 87	eqtr4d	$⊢ ((φ \land (i \in M \land k \in P)) \land l \in N) \to (i X l) \cdot_{R} (l (Y I Z) k) = \underset{j \in O}{\sum_{R}} ((i X l) \cdot_{R} ((l Y j) \cdot_{R} (j Z k)))$
89	88	mpteq2dva	$⊢ (φ \land (i \in M \land k \in P)) \to (l \in N ⟼ (i X l) \cdot_{R} (l (Y I Z) k)) = (l \in N ⟼ \underset{j \in O}{\sum_{R}} ((i X l) \cdot_{R} ((l Y j) \cdot_{R} (j Z k))))$
90	89	oveq2d	$⊢ (φ \land (i \in M \land k \in P)) \to \underset{l \in N}{\sum_{R}} ((i X l) \cdot_{R} (l (Y I Z) k)) = \underset{l \in N}{\sum_{R}} (\underset{j \in O}{\sum_{R}}, ((i X l) \cdot_{R} ((l Y j) \cdot_{R} (j Z k))))$
91	45 72 90	3eqtr4d	$⊢ (φ \land (i \in M \land k \in P)) \to \underset{j \in O}{\sum_{R}} ((i (X F Y) j) \cdot_{R} (j Z k)) = \underset{l \in N}{\sum_{R}} ((i X l) \cdot_{R} (l (Y I Z) k))$
92	2	adantr	$⊢ (φ \land (i \in M \land k \in P)) \to R \in Ring$
93	3	adantr	$⊢ (φ \land (i \in M \land k \in P)) \to M \in Fin$
94	6	adantr	$⊢ (φ \land (i \in M \land k \in P)) \to P \in Fin$
95	1 2 10 3 4 5 7 8	mamucl	$⊢ φ \to X F Y \in (B^{(M \times O)})$
96	95	adantr	$⊢ (φ \land (i \in M \land k \in P)) \to X F Y \in (B^{(M \times O)})$
97	9	adantr	$⊢ (φ \land (i \in M \land k \in P)) \to Z \in (B^{(O \times P)})$
98		simprl	$⊢ (φ \land (i \in M \land k \in P)) \to i \in M$
99		simprr	$⊢ (φ \land (i \in M \land k \in P)) \to k \in P$
100	11 1 40 92 93 17 94 96 97 98 99	mamufv	$⊢ (φ \land (i \in M \land k \in P)) \to i ((X F Y) G Z) k = \underset{j \in O}{\sum_{R}} ((i (X F Y) j) \cdot_{R} (j Z k))$
101	7	adantr	$⊢ (φ \land (i \in M \land k \in P)) \to X \in (B^{(M \times N)})$
102	1 2 13 4 5 6 8 9	mamucl	$⊢ φ \to Y I Z \in (B^{(N \times P)})$
103	102	adantr	$⊢ (φ \land (i \in M \land k \in P)) \to Y I Z \in (B^{(N \times P)})$
104	12 1 40 92 93 18 94 101 103 98 99	mamufv	$⊢ (φ \land (i \in M \land k \in P)) \to i (X H (Y I Z)) k = \underset{l \in N}{\sum_{R}} ((i X l) \cdot_{R} (l (Y I Z) k))$
105	91 100 104	3eqtr4d	$⊢ (φ \land (i \in M \land k \in P)) \to i ((X F Y) G Z) k = i (X H (Y I Z)) k$
106	105	ralrimivva	$⊢ φ \to \forall i \in M \forall k \in P i ((X F Y) G Z) k = i (X H (Y I Z)) k$
107	1 2 11 3 5 6 95 9	mamucl	$⊢ φ \to (X F Y) G Z \in (B^{(M \times P)})$
108		elmapi	$⊢ (X F Y) G Z \in (B^{(M \times P)}) \to ((X F Y) G Z) : M \times P ⟶ B$
109		ffn	$⊢ ((X F Y) G Z) : M \times P ⟶ B \to ((X F Y) G Z) Fn (M \times P)$
110	107 108 109	3syl	$⊢ φ \to ((X F Y) G Z) Fn (M \times P)$
111	1 2 12 3 4 6 7 102	mamucl	$⊢ φ \to X H (Y I Z) \in (B^{(M \times P)})$
112		elmapi	$⊢ X H (Y I Z) \in (B^{(M \times P)}) \to (X H (Y I Z)) : M \times P ⟶ B$
113		ffn	$⊢ (X H (Y I Z)) : M \times P ⟶ B \to (X H (Y I Z)) Fn (M \times P)$
114	111 112 113	3syl	$⊢ φ \to (X H (Y I Z)) Fn (M \times P)$
115		eqfnov2	$⊢ (((X F Y) G Z) Fn (M \times P) \land (X H (Y I Z)) Fn (M \times P)) \to ((X F Y) G Z = X H (Y I Z) \leftrightarrow \forall i \in M \forall k \in P i ((X F Y) G Z) k = i (X H (Y I Z)) k)$
116	110 114 115	syl2anc	$⊢ φ \to ((X F Y) G Z = X H (Y I Z) \leftrightarrow \forall i \in M \forall k \in P i ((X F Y) G Z) k = i (X H (Y I Z)) k)$
117	106 116	mpbird	$⊢ φ \to (X F Y) G Z = X H (Y I Z)$

Metamath Proof Explorer

Theorem mamuass

Proof