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	4	ringcmnd	\|- ( ph -> R e. CMnd )
27	26	adantr	\|- ( ( ph /\ i e. N ) -> R e. CMnd )
28	5	adantr	\|- ( ( ph /\ i e. N ) -> N e. Fin )
29	4	ad2antrr	\|- ( ( ( ph /\ i e. N ) /\ ( j e. N /\ k e. N ) ) -> R e. Ring )
30		elmapi	\|- ( X e. ( B ^m ( N X. N ) ) -> X : ( N X. N ) --> B )
31	13 30	syl	\|- ( ph -> X : ( N X. N ) --> B )
32	31	ad2antrr	\|- ( ( ( ph /\ i e. N ) /\ ( j e. N /\ k e. N ) ) -> X : ( N X. N ) --> B )
33		simplr	\|- ( ( ( ph /\ i e. N ) /\ ( j e. N /\ k e. N ) ) -> i e. N )
34		simprr	\|- ( ( ( ph /\ i e. N ) /\ ( j e. N /\ k e. N ) ) -> k e. N )
35	32 33 34	fovcdmd	\|- ( ( ( ph /\ i e. N ) /\ ( j e. N /\ k e. N ) ) -> ( i X k ) e. B )
36		elmapi	\|- ( Z e. ( B ^m ( N X. N ) ) -> Z : ( N X. N ) --> B )
37	14 36	syl	\|- ( ph -> Z : ( N X. N ) --> B )
38	37	ad2antrr	\|- ( ( ( ph /\ i e. N ) /\ ( j e. N /\ k e. N ) ) -> Z : ( N X. N ) --> B )
39		simprl	\|- ( ( ( ph /\ i e. N ) /\ ( j e. N /\ k e. N ) ) -> j e. N )
40	38 34 39	fovcdmd	\|- ( ( ( ph /\ i e. N ) /\ ( j e. N /\ k e. N ) ) -> ( k Z j ) e. B )
41		elmapi	\|- ( Y e. ( B ^m N ) -> Y : N --> B )
42		ffvelcdm	\|- ( ( Y : N --> B /\ j e. N ) -> ( Y ` j ) e. B )
43	42	ex	\|- ( Y : N --> B -> ( j e. N -> ( Y ` j ) e. B ) )
44	6 41 43	3syl	\|- ( ph -> ( j e. N -> ( Y ` j ) e. B ) )
45	44	imp	\|- ( ( ph /\ j e. N ) -> ( Y ` j ) e. B )
46	45	ad2ant2r	\|- ( ( ( ph /\ i e. N ) /\ ( j e. N /\ k e. N ) ) -> ( Y ` j ) e. B )
47	2 10 29 40 46	ringcld	\|- ( ( ( ph /\ i e. N ) /\ ( j e. N /\ k e. N ) ) -> ( ( k Z j ) ( .r ` R ) ( Y ` j ) ) e. B )
48	2 10 29 35 47	ringcld	\|- ( ( ( ph /\ i e. N ) /\ ( j e. N /\ k e. N ) ) -> ( ( i X k ) ( .r ` R ) ( ( k Z j ) ( .r ` R ) ( Y ` j ) ) ) e. B )
49	2 27 28 28 48	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 ) ) ) ) ) ) ) )
50	4	ad2antrr	\|- ( ( ( ph /\ i e. N ) /\ j e. N ) -> R e. Ring )
51	5	ad2antrr	\|- ( ( ( ph /\ i e. N ) /\ j e. N ) -> N e. Fin )
52	13	ad2antrr	\|- ( ( ( ph /\ i e. N ) /\ j e. N ) -> X e. ( B ^m ( N X. N ) ) )
53	14	ad2antrr	\|- ( ( ( ph /\ i e. N ) /\ j e. N ) -> Z e. ( B ^m ( N X. N ) ) )
54		simplr	\|- ( ( ( ph /\ i e. N ) /\ j e. N ) -> i e. N )
55		simpr	\|- ( ( ( ph /\ i e. N ) /\ j e. N ) -> j e. N )
56	7 2 10 50 51 51 51 52 53 54 55	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 ) ) ) ) )
57	56	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 ) ) )
58		eqid	\|- ( 0g ` R ) = ( 0g ` R )
59	45	adantlr	\|- ( ( ( ph /\ i e. N ) /\ j e. N ) -> ( Y ` j ) e. B )
60	4	adantr	\|- ( ( ph /\ i e. N ) -> R e. Ring )
61	60	ad2antrr	\|- ( ( ( ( ph /\ i e. N ) /\ j e. N ) /\ k e. N ) -> R e. Ring )
62	31	ad2antrr	\|- ( ( ( ph /\ i e. N ) /\ k e. N ) -> X : ( N X. N ) --> B )
63		simplr	\|- ( ( ( ph /\ i e. N ) /\ k e. N ) -> i e. N )
64		simpr	\|- ( ( ( ph /\ i e. N ) /\ k e. N ) -> k e. N )
65	62 63 64	fovcdmd	\|- ( ( ( ph /\ i e. N ) /\ k e. N ) -> ( i X k ) e. B )
66	65	adantlr	\|- ( ( ( ( ph /\ i e. N ) /\ j e. N ) /\ k e. N ) -> ( i X k ) e. B )
67	37	adantr	\|- ( ( ph /\ i e. N ) -> Z : ( N X. N ) --> B )
68	67	ad2antrr	\|- ( ( ( ( ph /\ i e. N ) /\ j e. N ) /\ k e. N ) -> Z : ( N X. N ) --> B )
69		simpr	\|- ( ( ( ( ph /\ i e. N ) /\ j e. N ) /\ k e. N ) -> k e. N )
70		simplr	\|- ( ( ( ( ph /\ i e. N ) /\ j e. N ) /\ k e. N ) -> j e. N )
71	68 69 70	fovcdmd	\|- ( ( ( ( ph /\ i e. N ) /\ j e. N ) /\ k e. N ) -> ( k Z j ) e. B )
72	2 10 61 66 71	ringcld	\|- ( ( ( ( ph /\ i e. N ) /\ j e. N ) /\ k e. N ) -> ( ( i X k ) ( .r ` R ) ( k Z j ) ) e. B )
73		eqid	\|- ( k e. N \|-> ( ( i X k ) ( .r ` R ) ( k Z j ) ) ) = ( k e. N \|-> ( ( i X k ) ( .r ` R ) ( k Z j ) ) )
74		ovexd	\|- ( ( ( ( ph /\ i e. N ) /\ j e. N ) /\ k e. N ) -> ( ( i X k ) ( .r ` R ) ( k Z j ) ) e. _V )
75		fvexd	\|- ( ( ( ph /\ i e. N ) /\ j e. N ) -> ( 0g ` R ) e. _V )
76	73 51 74 75	fsuppmptdm	\|- ( ( ( ph /\ i e. N ) /\ j e. N ) -> ( k e. N \|-> ( ( i X k ) ( .r ` R ) ( k Z j ) ) ) finSupp ( 0g ` R ) )
77	2 58 10 50 51 59 72 76	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 ) ) )
78	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 ) ) ) )
79	29 35 40 46 78	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 ) ) ) )
80	79	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 ) ) ) )
81	80	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 ) ) ) ) )
82	81	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 ) ) ) ) ) )
83	57 77 82	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 ) ) ) ) ) )
84	83	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 ) ) ) ) ) ) )
85	84	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 ) ) ) ) ) ) ) )
86	4	ad2antrr	\|- ( ( ( ph /\ i e. N ) /\ k e. N ) -> R e. Ring )
87	5	ad2antrr	\|- ( ( ( ph /\ i e. N ) /\ k e. N ) -> N e. Fin )
88	9	ad2antrr	\|- ( ( ( ph /\ i e. N ) /\ k e. N ) -> Z e. ( Base ` A ) )
89	6	ad2antrr	\|- ( ( ( ph /\ i e. N ) /\ k e. N ) -> Y e. ( B ^m N ) )
90	1 3 2 10 86 87 88 89 64	mavmulfv	\|- ( ( ( ph /\ i e. N ) /\ k e. N ) -> ( ( Z .x. Y ) ` k ) = ( R gsum ( j e. N \|-> ( ( k Z j ) ( .r ` R ) ( Y ` j ) ) ) ) )
91	90	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 ) ) ) ) ) )
92	60	ad2antrr	\|- ( ( ( ( ph /\ i e. N ) /\ k e. N ) /\ j e. N ) -> R e. Ring )
93	67	ad2antrr	\|- ( ( ( ( ph /\ i e. N ) /\ k e. N ) /\ j e. N ) -> Z : ( N X. N ) --> B )
94		simplr	\|- ( ( ( ( ph /\ i e. N ) /\ k e. N ) /\ j e. N ) -> k e. N )
95		simpr	\|- ( ( ( ( ph /\ i e. N ) /\ k e. N ) /\ j e. N ) -> j e. N )
96	93 94 95	fovcdmd	\|- ( ( ( ( ph /\ i e. N ) /\ k e. N ) /\ j e. N ) -> ( k Z j ) e. B )
97	44	ad2antrr	\|- ( ( ( ph /\ i e. N ) /\ k e. N ) -> ( j e. N -> ( Y ` j ) e. B ) )
98	97	imp	\|- ( ( ( ( ph /\ i e. N ) /\ k e. N ) /\ j e. N ) -> ( Y ` j ) e. B )
99	2 10 92 96 98	ringcld	\|- ( ( ( ( ph /\ i e. N ) /\ k e. N ) /\ j e. N ) -> ( ( k Z j ) ( .r ` R ) ( Y ` j ) ) e. B )
100		eqid	\|- ( j e. N \|-> ( ( k Z j ) ( .r ` R ) ( Y ` j ) ) ) = ( j e. N \|-> ( ( k Z j ) ( .r ` R ) ( Y ` j ) ) )
101		ovexd	\|- ( ( ( ( ph /\ i e. N ) /\ k e. N ) /\ j e. N ) -> ( ( k Z j ) ( .r ` R ) ( Y ` j ) ) e. _V )
102		fvexd	\|- ( ( ( ph /\ i e. N ) /\ k e. N ) -> ( 0g ` R ) e. _V )
103	100 87 101 102	fsuppmptdm	\|- ( ( ( ph /\ i e. N ) /\ k e. N ) -> ( j e. N \|-> ( ( k Z j ) ( .r ` R ) ( Y ` j ) ) ) finSupp ( 0g ` R ) )
104	2 58 10 86 87 65 99 103	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 ) ) ) ) ) )
105	91 104	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 ) ) ) ) ) )
106	105	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 ) ) ) ) ) ) )
107	106	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 ) ) ) ) ) ) ) )
108	49 85 107	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 ) ) ) ) )
109	16	adantr	\|- ( ( ph /\ i e. N ) -> ( X .X. Z ) e. ( Base ` A ) )
110	6	adantr	\|- ( ( ph /\ i e. N ) -> Y e. ( B ^m N ) )
111		simpr	\|- ( ( ph /\ i e. N ) -> i e. N )
112	1 3 2 10 60 28 109 110 111	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 ) ) ) ) )
113	8	adantr	\|- ( ( ph /\ i e. N ) -> X e. ( Base ` A ) )
114	21	adantr	\|- ( ( ph /\ i e. N ) -> ( Z .x. Y ) e. ( B ^m N ) )
115	1 3 2 10 60 28 113 114 111	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 ) ) ) ) )
116	108 112 115	3eqtr4d	\|- ( ( ph /\ i e. N ) -> ( ( ( X .X. Z ) .x. Y ) ` i ) = ( ( X .x. ( Z .x. Y ) ) ` i ) )
117	20 25 116	eqfnfvd	\|- ( ph -> ( ( X .X. Z ) .x. Y ) = ( X .x. ( Z .x. Y ) ) )

Metamath Proof Explorer

Theorem mavmulass

Proof