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	2	ringcmnd	$⊢ φ \to R \in CMnd$
15	14	adantr	$⊢ (φ \land (i \in M \land k \in P)) \to R \in CMnd$
16	5	adantr	$⊢ (φ \land (i \in M \land k \in P)) \to O \in Fin$
17	4	adantr	$⊢ (φ \land (i \in M \land k \in P)) \to N \in Fin$
18		eqid	$⊢ \cdot_{R} = \cdot_{R}$
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	fovcdmd	$⊢ ((φ \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	fovcdmd	$⊢ ((φ \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	fovcdmd	$⊢ ((φ \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	1 18 19 32 39	ringcld	$⊢ ((φ \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$
41	1 18 19 26 40	ringcld	$⊢ ((φ \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$
42	1 15 16 17 41	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))))$
43	2	ad2antrr	$⊢ ((φ \land (i \in M \land k \in P)) \land j \in O) \to R \in Ring$
44	3	ad2antrr	$⊢ ((φ \land (i \in M \land k \in P)) \land j \in O) \to M \in Fin$
45	4	ad2antrr	$⊢ ((φ \land (i \in M \land k \in P)) \land j \in O) \to N \in Fin$
46	5	ad2antrr	$⊢ ((φ \land (i \in M \land k \in P)) \land j \in O) \to O \in Fin$
47	7	ad2antrr	$⊢ ((φ \land (i \in M \land k \in P)) \land j \in O) \to X \in (B^{(M \times N)})$
48	8	ad2antrr	$⊢ ((φ \land (i \in M \land k \in P)) \land j \in O) \to Y \in (B^{(N \times O)})$
49		simplrl	$⊢ ((φ \land (i \in M \land k \in P)) \land j \in O) \to i \in M$
50	10 1 18 43 44 45 46 47 48 49 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))$
51	50	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)$
52		eqid	$⊢ 0_{R} = 0_{R}$
53	1 18 19 26 32	ringcld	$⊢ ((φ \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$
54	53	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$
55		eqid	$⊢ (l \in N ⟼ (i X l) \cdot_{R} (l Y j)) = (l \in N ⟼ (i X l) \cdot_{R} (l Y j))$
56		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$
57		fvexd	$⊢ ((φ \land (i \in M \land k \in P)) \land j \in O) \to 0_{R} \in V$
58	55 45 56 57	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)))$
59	1 52 18 43 45 38 54 58	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)$
60	1 18	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))$
61	19 26 32 39 60	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))$
62	61	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))$
63	62	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)))$
64	63	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)))$
65	51 59 64	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)))$
66	65	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))))$
67	66	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))))$
68	2	ad2antrr	$⊢ ((φ \land (i \in M \land k \in P)) \land l \in N) \to R \in Ring$
69	4	ad2antrr	$⊢ ((φ \land (i \in M \land k \in P)) \land l \in N) \to N \in Fin$
70	5	ad2antrr	$⊢ ((φ \land (i \in M \land k \in P)) \land l \in N) \to O \in Fin$
71	6	ad2antrr	$⊢ ((φ \land (i \in M \land k \in P)) \land l \in N) \to P \in Fin$
72	8	ad2antrr	$⊢ ((φ \land (i \in M \land k \in P)) \land l \in N) \to Y \in (B^{(N \times O)})$
73	9	ad2antrr	$⊢ ((φ \land (i \in M \land k \in P)) \land l \in N) \to Z \in (B^{(O \times P)})$
74		simplrr	$⊢ ((φ \land (i \in M \land k \in P)) \land l \in N) \to k \in P$
75	13 1 18 68 69 70 71 72 73 24 74	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))$
76	75	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)))$
77	40	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$
78		eqid	$⊢ (j \in O ⟼ (l Y j) \cdot_{R} (j Z k)) = (j \in O ⟼ (l Y j) \cdot_{R} (j Z k))$
79		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$
80		fvexd	$⊢ ((φ \land (i \in M \land k \in P)) \land l \in N) \to 0_{R} \in V$
81	78 70 79 80	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)))$
82	1 52 18 68 70 25 77 81	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)))$
83	76 82	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)))$
84	83	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))))$
85	84	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))))$
86	42 67 85	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))$
87	2	adantr	$⊢ (φ \land (i \in M \land k \in P)) \to R \in Ring$
88	3	adantr	$⊢ (φ \land (i \in M \land k \in P)) \to M \in Fin$
89	6	adantr	$⊢ (φ \land (i \in M \land k \in P)) \to P \in Fin$
90	1 2 10 3 4 5 7 8	mamucl	$⊢ φ \to X F Y \in (B^{(M \times O)})$
91	90	adantr	$⊢ (φ \land (i \in M \land k \in P)) \to X F Y \in (B^{(M \times O)})$
92	9	adantr	$⊢ (φ \land (i \in M \land k \in P)) \to Z \in (B^{(O \times P)})$
93		simprl	$⊢ (φ \land (i \in M \land k \in P)) \to i \in M$
94		simprr	$⊢ (φ \land (i \in M \land k \in P)) \to k \in P$
95	11 1 18 87 88 16 89 91 92 93 94	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))$
96	7	adantr	$⊢ (φ \land (i \in M \land k \in P)) \to X \in (B^{(M \times N)})$
97	1 2 13 4 5 6 8 9	mamucl	$⊢ φ \to Y I Z \in (B^{(N \times P)})$
98	97	adantr	$⊢ (φ \land (i \in M \land k \in P)) \to Y I Z \in (B^{(N \times P)})$
99	12 1 18 87 88 17 89 96 98 93 94	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))$
100	86 95 99	3eqtr4d	$⊢ (φ \land (i \in M \land k \in P)) \to i ((X F Y) G Z) k = i (X H (Y I Z)) k$
101	100	ralrimivva	$⊢ φ \to \forall i \in M \forall k \in P i ((X F Y) G Z) k = i (X H (Y I Z)) k$
102	1 2 11 3 5 6 90 9	mamucl	$⊢ φ \to (X F Y) G Z \in (B^{(M \times P)})$
103		elmapi	$⊢ (X F Y) G Z \in (B^{(M \times P)}) \to ((X F Y) G Z) : M \times P ⟶ B$
104		ffn	$⊢ ((X F Y) G Z) : M \times P ⟶ B \to ((X F Y) G Z) Fn (M \times P)$
105	102 103 104	3syl	$⊢ φ \to ((X F Y) G Z) Fn (M \times P)$
106	1 2 12 3 4 6 7 97	mamucl	$⊢ φ \to X H (Y I Z) \in (B^{(M \times P)})$
107		elmapi	$⊢ X H (Y I Z) \in (B^{(M \times P)}) \to (X H (Y I Z)) : M \times P ⟶ B$
108		ffn	$⊢ (X H (Y I Z)) : M \times P ⟶ B \to (X H (Y I Z)) Fn (M \times P)$
109	106 107 108	3syl	$⊢ φ \to (X H (Y I Z)) Fn (M \times P)$
110		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)$
111	105 109 110	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)$
112	101 111	mpbird	$⊢ φ \to (X F Y) G Z = X H (Y I Z)$

Metamath Proof Explorer

Theorem mamuass

Proof