mavmulass

Description: Associativity of the multiplication of two NxN matrices with an N-dimensional vector. (Contributed by AV, 9-Feb-2019) (Revised by AV, 25-Feb-2019) (Proof shortened by AV, 22-Jul-2019)

	Ref	Expression
Hypotheses	1mavmul.a	\|- A = ( N Mat R )
	1mavmul.b	\|- B = ( Base ` R )
	1mavmul.t	\|- .x. = ( R maVecMul <. N , N >. )
	1mavmul.r	\|- ( ph -> R e. Ring )
	1mavmul.n	\|- ( ph -> N e. Fin )
	1mavmul.y	\|- ( ph -> Y e. ( B ^m N ) )
	mavmulass.m	\|- .X. = ( R maMul <. N , N , N >. )
	mavmulass.x	\|- ( ph -> X e. ( Base ` A ) )
	mavmulass.z	\|- ( ph -> Z e. ( Base ` A ) )
Assertion	mavmulass	\|- ( ph -> ( ( X .X. Z ) .x. Y ) = ( X .x. ( Z .x. Y ) ) )

Proof

Step	Hyp	Ref	Expression
1		1mavmul.a	\|- A = ( N Mat R )
2		1mavmul.b	\|- B = ( Base ` R )
3		1mavmul.t	\|- .x. = ( R maVecMul <. N , N >. )
4		1mavmul.r	\|- ( ph -> R e. Ring )
5		1mavmul.n	\|- ( ph -> N e. Fin )
6		1mavmul.y	\|- ( ph -> Y e. ( B ^m N ) )
7		mavmulass.m	\|- .X. = ( R maMul <. N , N , N >. )
8		mavmulass.x	\|- ( ph -> X e. ( Base ` A ) )
9		mavmulass.z	\|- ( ph -> Z e. ( Base ` A ) )
10		eqid	\|- ( .r ` R ) = ( .r ` R )
11	1 2	matbas2	\|- ( ( N e. Fin /\ R e. Ring ) -> ( B ^m ( N X. N ) ) = ( Base ` A ) )
12	5 4 11	syl2anc	\|- ( ph -> ( B ^m ( N X. N ) ) = ( Base ` A ) )
13	8 12	eleqtrrd	\|- ( ph -> X e. ( B ^m ( N X. N ) ) )
14	9 12	eleqtrrd	\|- ( ph -> Z e. ( B ^m ( N X. N ) ) )
15	2 4 7 5 5 5 13 14	mamucl	\|- ( ph -> ( X .X. Z ) e. ( B ^m ( N X. N ) ) )
16	15 12	eleqtrd	\|- ( ph -> ( X .X. Z ) e. ( Base ` A ) )
17	1 3 2 10 4 5 16 6	mavmulcl	\|- ( ph -> ( ( X .X. Z ) .x. Y ) e. ( B ^m N ) )
18		elmapi	\|- ( ( ( X .X. Z ) .x. Y ) e. ( B ^m N ) -> ( ( X .X. Z ) .x. Y ) : N --> B )
19		ffn	\|- ( ( ( X .X. Z ) .x. Y ) : N --> B -> ( ( X .X. Z ) .x. Y ) Fn N )
20	17 18 19	3syl	\|- ( ph -> ( ( X .X. Z ) .x. Y ) Fn N )
21	1 3 2 10 4 5 9 6	mavmulcl	\|- ( ph -> ( Z .x. Y ) e. ( B ^m N ) )
22	1 3 2 10 4 5 8 21	mavmulcl	\|- ( ph -> ( X .x. ( Z .x. Y ) ) e. ( B ^m N ) )
23		elmapi	\|- ( ( X .x. ( Z .x. Y ) ) e. ( B ^m N ) -> ( X .x. ( Z .x. Y ) ) : N --> B )
24		ffn	\|- ( ( X .x. ( Z .x. Y ) ) : N --> B -> ( X .x. ( Z .x. Y ) ) Fn N )
25	22 23 24	3syl	\|- ( ph -> ( X .x. ( Z .x. Y ) ) Fn N )
26		ringcmn	\|- ( R e. Ring -> R e. CMnd )
27	4 26	syl	\|- ( ph -> R e. CMnd )
28	27	adantr	\|- ( ( ph /\ i e. N ) -> R e. CMnd )
29	5	adantr	\|- ( ( ph /\ i e. N ) -> N e. Fin )
30	4	ad2antrr	\|- ( ( ( ph /\ i e. N ) /\ ( j e. N /\ k e. N ) ) -> R e. Ring )
31		elmapi	\|- ( X e. ( B ^m ( N X. N ) ) -> X : ( N X. N ) --> B )
32	13 31	syl	\|- ( ph -> X : ( N X. N ) --> B )
33	32	ad2antrr	\|- ( ( ( ph /\ i e. N ) /\ ( j e. N /\ k e. N ) ) -> X : ( N X. N ) --> B )
34		simplr	\|- ( ( ( ph /\ i e. N ) /\ ( j e. N /\ k e. N ) ) -> i e. N )
35		simprr	\|- ( ( ( ph /\ i e. N ) /\ ( j e. N /\ k e. N ) ) -> k e. N )
36	33 34 35	fovrnd	\|- ( ( ( ph /\ i e. N ) /\ ( j e. N /\ k e. N ) ) -> ( i X k ) e. B )
37		elmapi	\|- ( Z e. ( B ^m ( N X. N ) ) -> Z : ( N X. N ) --> B )
38	14 37	syl	\|- ( ph -> Z : ( N X. N ) --> B )
39	38	ad2antrr	\|- ( ( ( ph /\ i e. N ) /\ ( j e. N /\ k e. N ) ) -> Z : ( N X. N ) --> B )
40		simprl	\|- ( ( ( ph /\ i e. N ) /\ ( j e. N /\ k e. N ) ) -> j e. N )
41	39 35 40	fovrnd	\|- ( ( ( ph /\ i e. N ) /\ ( j e. N /\ k e. N ) ) -> ( k Z j ) e. B )
42		elmapi	\|- ( Y e. ( B ^m N ) -> Y : N --> B )
43		ffvelrn	\|- ( ( Y : N --> B /\ j e. N ) -> ( Y ` j ) e. B )
44	43	ex	\|- ( Y : N --> B -> ( j e. N -> ( Y ` j ) e. B ) )
45	6 42 44	3syl	\|- ( ph -> ( j e. N -> ( Y ` j ) e. B ) )
46	45	imp	\|- ( ( ph /\ j e. N ) -> ( Y ` j ) e. B )
47	46	ad2ant2r	\|- ( ( ( ph /\ i e. N ) /\ ( j e. N /\ k e. N ) ) -> ( Y ` j ) e. B )
48	2 10	ringcl	\|- ( ( R e. Ring /\ ( k Z j ) e. B /\ ( Y ` j ) e. B ) -> ( ( k Z j ) ( .r ` R ) ( Y ` j ) ) e. B )
49	30 41 47 48	syl3anc	\|- ( ( ( ph /\ i e. N ) /\ ( j e. N /\ k e. N ) ) -> ( ( k Z j ) ( .r ` R ) ( Y ` j ) ) e. B )
50	2 10	ringcl	\|- ( ( R e. Ring /\ ( i X k ) e. B /\ ( ( k Z j ) ( .r ` R ) ( Y ` j ) ) e. B ) -> ( ( i X k ) ( .r ` R ) ( ( k Z j ) ( .r ` R ) ( Y ` j ) ) ) e. B )
51	30 36 49 50	syl3anc	\|- ( ( ( ph /\ i e. N ) /\ ( j e. N /\ k e. N ) ) -> ( ( i X k ) ( .r ` R ) ( ( k Z j ) ( .r ` R ) ( Y ` j ) ) ) e. B )
52	2 28 29 29 51	gsumcom3fi	\|- ( ( ph /\ i e. N ) -> ( R gsum ( j e. N \|-> ( R gsum ( k e. N \|-> ( ( i X k ) ( .r ` R ) ( ( k Z j ) ( .r ` R ) ( Y ` j ) ) ) ) ) ) ) = ( R gsum ( k e. N \|-> ( R gsum ( j e. N \|-> ( ( i X k ) ( .r ` R ) ( ( k Z j ) ( .r ` R ) ( Y ` j ) ) ) ) ) ) ) )
53	4	ad2antrr	\|- ( ( ( ph /\ i e. N ) /\ j e. N ) -> R e. Ring )
54	5	ad2antrr	\|- ( ( ( ph /\ i e. N ) /\ j e. N ) -> N e. Fin )
55	13	ad2antrr	\|- ( ( ( ph /\ i e. N ) /\ j e. N ) -> X e. ( B ^m ( N X. N ) ) )
56	14	ad2antrr	\|- ( ( ( ph /\ i e. N ) /\ j e. N ) -> Z e. ( B ^m ( N X. N ) ) )
57		simplr	\|- ( ( ( ph /\ i e. N ) /\ j e. N ) -> i e. N )
58		simpr	\|- ( ( ( ph /\ i e. N ) /\ j e. N ) -> j e. N )
59	7 2 10 53 54 54 54 55 56 57 58	mamufv	\|- ( ( ( ph /\ i e. N ) /\ j e. N ) -> ( i ( X .X. Z ) j ) = ( R gsum ( k e. N \|-> ( ( i X k ) ( .r ` R ) ( k Z j ) ) ) ) )
60	59	oveq1d	\|- ( ( ( ph /\ i e. N ) /\ j e. N ) -> ( ( i ( X .X. Z ) j ) ( .r ` R ) ( Y ` j ) ) = ( ( R gsum ( k e. N \|-> ( ( i X k ) ( .r ` R ) ( k Z j ) ) ) ) ( .r ` R ) ( Y ` j ) ) )
61		eqid	\|- ( 0g ` R ) = ( 0g ` R )
62		eqid	\|- ( +g ` R ) = ( +g ` R )
63	46	adantlr	\|- ( ( ( ph /\ i e. N ) /\ j e. N ) -> ( Y ` j ) e. B )
64	4	adantr	\|- ( ( ph /\ i e. N ) -> R e. Ring )
65	64	ad2antrr	\|- ( ( ( ( ph /\ i e. N ) /\ j e. N ) /\ k e. N ) -> R e. Ring )
66	32	ad2antrr	\|- ( ( ( ph /\ i e. N ) /\ k e. N ) -> X : ( N X. N ) --> B )
67		simplr	\|- ( ( ( ph /\ i e. N ) /\ k e. N ) -> i e. N )
68		simpr	\|- ( ( ( ph /\ i e. N ) /\ k e. N ) -> k e. N )
69	66 67 68	fovrnd	\|- ( ( ( ph /\ i e. N ) /\ k e. N ) -> ( i X k ) e. B )
70	69	adantlr	\|- ( ( ( ( ph /\ i e. N ) /\ j e. N ) /\ k e. N ) -> ( i X k ) e. B )
71	38	adantr	\|- ( ( ph /\ i e. N ) -> Z : ( N X. N ) --> B )
72	71	ad2antrr	\|- ( ( ( ( ph /\ i e. N ) /\ j e. N ) /\ k e. N ) -> Z : ( N X. N ) --> B )
73		simpr	\|- ( ( ( ( ph /\ i e. N ) /\ j e. N ) /\ k e. N ) -> k e. N )
74		simplr	\|- ( ( ( ( ph /\ i e. N ) /\ j e. N ) /\ k e. N ) -> j e. N )
75	72 73 74	fovrnd	\|- ( ( ( ( ph /\ i e. N ) /\ j e. N ) /\ k e. N ) -> ( k Z j ) e. B )
76	2 10	ringcl	\|- ( ( R e. Ring /\ ( i X k ) e. B /\ ( k Z j ) e. B ) -> ( ( i X k ) ( .r ` R ) ( k Z j ) ) e. B )
77	65 70 75 76	syl3anc	\|- ( ( ( ( ph /\ i e. N ) /\ j e. N ) /\ k e. N ) -> ( ( i X k ) ( .r ` R ) ( k Z j ) ) e. B )
78		eqid	\|- ( k e. N \|-> ( ( i X k ) ( .r ` R ) ( k Z j ) ) ) = ( k e. N \|-> ( ( i X k ) ( .r ` R ) ( k Z j ) ) )
79		ovexd	\|- ( ( ( ( ph /\ i e. N ) /\ j e. N ) /\ k e. N ) -> ( ( i X k ) ( .r ` R ) ( k Z j ) ) e. _V )
80		fvexd	\|- ( ( ( ph /\ i e. N ) /\ j e. N ) -> ( 0g ` R ) e. _V )
81	78 54 79 80	fsuppmptdm	\|- ( ( ( ph /\ i e. N ) /\ j e. N ) -> ( k e. N \|-> ( ( i X k ) ( .r ` R ) ( k Z j ) ) ) finSupp ( 0g ` R ) )
82	2 61 62 10 53 54 63 77 81	gsummulc1	\|- ( ( ( ph /\ i e. N ) /\ j e. N ) -> ( R gsum ( k e. N \|-> ( ( ( i X k ) ( .r ` R ) ( k Z j ) ) ( .r ` R ) ( Y ` j ) ) ) ) = ( ( R gsum ( k e. N \|-> ( ( i X k ) ( .r ` R ) ( k Z j ) ) ) ) ( .r ` R ) ( Y ` j ) ) )
83	2 10	ringass	\|- ( ( R e. Ring /\ ( ( i X k ) e. B /\ ( k Z j ) e. B /\ ( Y ` j ) e. B ) ) -> ( ( ( i X k ) ( .r ` R ) ( k Z j ) ) ( .r ` R ) ( Y ` j ) ) = ( ( i X k ) ( .r ` R ) ( ( k Z j ) ( .r ` R ) ( Y ` j ) ) ) )
84	30 36 41 47 83	syl13anc	\|- ( ( ( ph /\ i e. N ) /\ ( j e. N /\ k e. N ) ) -> ( ( ( i X k ) ( .r ` R ) ( k Z j ) ) ( .r ` R ) ( Y ` j ) ) = ( ( i X k ) ( .r ` R ) ( ( k Z j ) ( .r ` R ) ( Y ` j ) ) ) )
85	84	anassrs	\|- ( ( ( ( ph /\ i e. N ) /\ j e. N ) /\ k e. N ) -> ( ( ( i X k ) ( .r ` R ) ( k Z j ) ) ( .r ` R ) ( Y ` j ) ) = ( ( i X k ) ( .r ` R ) ( ( k Z j ) ( .r ` R ) ( Y ` j ) ) ) )
86	85	mpteq2dva	\|- ( ( ( ph /\ i e. N ) /\ j e. N ) -> ( k e. N \|-> ( ( ( i X k ) ( .r ` R ) ( k Z j ) ) ( .r ` R ) ( Y ` j ) ) ) = ( k e. N \|-> ( ( i X k ) ( .r ` R ) ( ( k Z j ) ( .r ` R ) ( Y ` j ) ) ) ) )
87	86	oveq2d	\|- ( ( ( ph /\ i e. N ) /\ j e. N ) -> ( R gsum ( k e. N \|-> ( ( ( i X k ) ( .r ` R ) ( k Z j ) ) ( .r ` R ) ( Y ` j ) ) ) ) = ( R gsum ( k e. N \|-> ( ( i X k ) ( .r ` R ) ( ( k Z j ) ( .r ` R ) ( Y ` j ) ) ) ) ) )
88	60 82 87	3eqtr2d	\|- ( ( ( ph /\ i e. N ) /\ j e. N ) -> ( ( i ( X .X. Z ) j ) ( .r ` R ) ( Y ` j ) ) = ( R gsum ( k e. N \|-> ( ( i X k ) ( .r ` R ) ( ( k Z j ) ( .r ` R ) ( Y ` j ) ) ) ) ) )
89	88	mpteq2dva	\|- ( ( ph /\ i e. N ) -> ( j e. N \|-> ( ( i ( X .X. Z ) j ) ( .r ` R ) ( Y ` j ) ) ) = ( j e. N \|-> ( R gsum ( k e. N \|-> ( ( i X k ) ( .r ` R ) ( ( k Z j ) ( .r ` R ) ( Y ` j ) ) ) ) ) ) )
90	89	oveq2d	\|- ( ( ph /\ i e. N ) -> ( R gsum ( j e. N \|-> ( ( i ( X .X. Z ) j ) ( .r ` R ) ( Y ` j ) ) ) ) = ( R gsum ( j e. N \|-> ( R gsum ( k e. N \|-> ( ( i X k ) ( .r ` R ) ( ( k Z j ) ( .r ` R ) ( Y ` j ) ) ) ) ) ) ) )
91	4	ad2antrr	\|- ( ( ( ph /\ i e. N ) /\ k e. N ) -> R e. Ring )
92	5	ad2antrr	\|- ( ( ( ph /\ i e. N ) /\ k e. N ) -> N e. Fin )
93	9	ad2antrr	\|- ( ( ( ph /\ i e. N ) /\ k e. N ) -> Z e. ( Base ` A ) )
94	6	ad2antrr	\|- ( ( ( ph /\ i e. N ) /\ k e. N ) -> Y e. ( B ^m N ) )
95	1 3 2 10 91 92 93 94 68	mavmulfv	\|- ( ( ( ph /\ i e. N ) /\ k e. N ) -> ( ( Z .x. Y ) ` k ) = ( R gsum ( j e. N \|-> ( ( k Z j ) ( .r ` R ) ( Y ` j ) ) ) ) )
96	95	oveq2d	\|- ( ( ( ph /\ i e. N ) /\ k e. N ) -> ( ( i X k ) ( .r ` R ) ( ( Z .x. Y ) ` k ) ) = ( ( i X k ) ( .r ` R ) ( R gsum ( j e. N \|-> ( ( k Z j ) ( .r ` R ) ( Y ` j ) ) ) ) ) )
97	64	ad2antrr	\|- ( ( ( ( ph /\ i e. N ) /\ k e. N ) /\ j e. N ) -> R e. Ring )
98	71	ad2antrr	\|- ( ( ( ( ph /\ i e. N ) /\ k e. N ) /\ j e. N ) -> Z : ( N X. N ) --> B )
99		simplr	\|- ( ( ( ( ph /\ i e. N ) /\ k e. N ) /\ j e. N ) -> k e. N )
100		simpr	\|- ( ( ( ( ph /\ i e. N ) /\ k e. N ) /\ j e. N ) -> j e. N )
101	98 99 100	fovrnd	\|- ( ( ( ( ph /\ i e. N ) /\ k e. N ) /\ j e. N ) -> ( k Z j ) e. B )
102	45	ad2antrr	\|- ( ( ( ph /\ i e. N ) /\ k e. N ) -> ( j e. N -> ( Y ` j ) e. B ) )
103	102	imp	\|- ( ( ( ( ph /\ i e. N ) /\ k e. N ) /\ j e. N ) -> ( Y ` j ) e. B )
104	97 101 103 48	syl3anc	\|- ( ( ( ( ph /\ i e. N ) /\ k e. N ) /\ j e. N ) -> ( ( k Z j ) ( .r ` R ) ( Y ` j ) ) e. B )
105		eqid	\|- ( j e. N \|-> ( ( k Z j ) ( .r ` R ) ( Y ` j ) ) ) = ( j e. N \|-> ( ( k Z j ) ( .r ` R ) ( Y ` j ) ) )
106		ovexd	\|- ( ( ( ( ph /\ i e. N ) /\ k e. N ) /\ j e. N ) -> ( ( k Z j ) ( .r ` R ) ( Y ` j ) ) e. _V )
107		fvexd	\|- ( ( ( ph /\ i e. N ) /\ k e. N ) -> ( 0g ` R ) e. _V )
108	105 92 106 107	fsuppmptdm	\|- ( ( ( ph /\ i e. N ) /\ k e. N ) -> ( j e. N \|-> ( ( k Z j ) ( .r ` R ) ( Y ` j ) ) ) finSupp ( 0g ` R ) )
109	2 61 62 10 91 92 69 104 108	gsummulc2	\|- ( ( ( ph /\ i e. N ) /\ k e. N ) -> ( R gsum ( j e. N \|-> ( ( i X k ) ( .r ` R ) ( ( k Z j ) ( .r ` R ) ( Y ` j ) ) ) ) ) = ( ( i X k ) ( .r ` R ) ( R gsum ( j e. N \|-> ( ( k Z j ) ( .r ` R ) ( Y ` j ) ) ) ) ) )
110	96 109	eqtr4d	\|- ( ( ( ph /\ i e. N ) /\ k e. N ) -> ( ( i X k ) ( .r ` R ) ( ( Z .x. Y ) ` k ) ) = ( R gsum ( j e. N \|-> ( ( i X k ) ( .r ` R ) ( ( k Z j ) ( .r ` R ) ( Y ` j ) ) ) ) ) )
111	110	mpteq2dva	\|- ( ( ph /\ i e. N ) -> ( k e. N \|-> ( ( i X k ) ( .r ` R ) ( ( Z .x. Y ) ` k ) ) ) = ( k e. N \|-> ( R gsum ( j e. N \|-> ( ( i X k ) ( .r ` R ) ( ( k Z j ) ( .r ` R ) ( Y ` j ) ) ) ) ) ) )
112	111	oveq2d	\|- ( ( ph /\ i e. N ) -> ( R gsum ( k e. N \|-> ( ( i X k ) ( .r ` R ) ( ( Z .x. Y ) ` k ) ) ) ) = ( R gsum ( k e. N \|-> ( R gsum ( j e. N \|-> ( ( i X k ) ( .r ` R ) ( ( k Z j ) ( .r ` R ) ( Y ` j ) ) ) ) ) ) ) )
113	52 90 112	3eqtr4d	\|- ( ( ph /\ i e. N ) -> ( R gsum ( j e. N \|-> ( ( i ( X .X. Z ) j ) ( .r ` R ) ( Y ` j ) ) ) ) = ( R gsum ( k e. N \|-> ( ( i X k ) ( .r ` R ) ( ( Z .x. Y ) ` k ) ) ) ) )
114	16	adantr	\|- ( ( ph /\ i e. N ) -> ( X .X. Z ) e. ( Base ` A ) )
115	6	adantr	\|- ( ( ph /\ i e. N ) -> Y e. ( B ^m N ) )
116		simpr	\|- ( ( ph /\ i e. N ) -> i e. N )
117	1 3 2 10 64 29 114 115 116	mavmulfv	\|- ( ( ph /\ i e. N ) -> ( ( ( X .X. Z ) .x. Y ) ` i ) = ( R gsum ( j e. N \|-> ( ( i ( X .X. Z ) j ) ( .r ` R ) ( Y ` j ) ) ) ) )
118	8	adantr	\|- ( ( ph /\ i e. N ) -> X e. ( Base ` A ) )
119	21	adantr	\|- ( ( ph /\ i e. N ) -> ( Z .x. Y ) e. ( B ^m N ) )
120	1 3 2 10 64 29 118 119 116	mavmulfv	\|- ( ( ph /\ i e. N ) -> ( ( X .x. ( Z .x. Y ) ) ` i ) = ( R gsum ( k e. N \|-> ( ( i X k ) ( .r ` R ) ( ( Z .x. Y ) ` k ) ) ) ) )
121	113 117 120	3eqtr4d	\|- ( ( ph /\ i e. N ) -> ( ( ( X .X. Z ) .x. Y ) ` i ) = ( ( X .x. ( Z .x. Y ) ) ` i ) )
122	20 25 121	eqfnfvd	\|- ( ph -> ( ( X .X. Z ) .x. Y ) = ( X .x. ( Z .x. Y ) ) )

Metamath Proof Explorer

Theorem mavmulass

Proof