This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 ) ) )