Metamath Proof Explorer


Theorem 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
|- ( ph -> R e. Ring )
mamuass.m
|- ( ph -> M e. Fin )
mamuass.n
|- ( ph -> N e. Fin )
mamuass.o
|- ( ph -> O e. Fin )
mamuass.p
|- ( ph -> P e. Fin )
mamuass.x
|- ( ph -> X e. ( B ^m ( M X. N ) ) )
mamuass.y
|- ( ph -> Y e. ( B ^m ( N X. O ) ) )
mamuass.z
|- ( ph -> Z e. ( B ^m ( O X. 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
|- ( ph -> ( ( X F Y ) G Z ) = ( X H ( Y I Z ) ) )

Proof

Step Hyp Ref Expression
1 mamucl.b
 |-  B = ( Base ` R )
2 mamucl.r
 |-  ( ph -> R e. Ring )
3 mamuass.m
 |-  ( ph -> M e. Fin )
4 mamuass.n
 |-  ( ph -> N e. Fin )
5 mamuass.o
 |-  ( ph -> O e. Fin )
6 mamuass.p
 |-  ( ph -> P e. Fin )
7 mamuass.x
 |-  ( ph -> X e. ( B ^m ( M X. N ) ) )
8 mamuass.y
 |-  ( ph -> Y e. ( B ^m ( N X. O ) ) )
9 mamuass.z
 |-  ( ph -> Z e. ( B ^m ( O X. 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
 |-  ( ph -> R e. CMnd )
15 14 adantr
 |-  ( ( ph /\ ( i e. M /\ k e. P ) ) -> R e. CMnd )
16 5 adantr
 |-  ( ( ph /\ ( i e. M /\ k e. P ) ) -> O e. Fin )
17 4 adantr
 |-  ( ( ph /\ ( i e. M /\ k e. P ) ) -> N e. Fin )
18 eqid
 |-  ( .r ` R ) = ( .r ` R )
19 2 ad2antrr
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ ( j e. O /\ l e. N ) ) -> R e. Ring )
20 elmapi
 |-  ( X e. ( B ^m ( M X. N ) ) -> X : ( M X. N ) --> B )
21 7 20 syl
 |-  ( ph -> X : ( M X. N ) --> B )
22 21 ad2antrr
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ l e. N ) -> X : ( M X. N ) --> B )
23 simplrl
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ l e. N ) -> i e. M )
24 simpr
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ l e. N ) -> l e. N )
25 22 23 24 fovcdmd
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ l e. N ) -> ( i X l ) e. B )
26 25 adantrl
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ ( j e. O /\ l e. N ) ) -> ( i X l ) e. B )
27 elmapi
 |-  ( Y e. ( B ^m ( N X. O ) ) -> Y : ( N X. O ) --> B )
28 8 27 syl
 |-  ( ph -> Y : ( N X. O ) --> B )
29 28 ad2antrr
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ ( j e. O /\ l e. N ) ) -> Y : ( N X. O ) --> B )
30 simprr
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ ( j e. O /\ l e. N ) ) -> l e. N )
31 simprl
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ ( j e. O /\ l e. N ) ) -> j e. O )
32 29 30 31 fovcdmd
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ ( j e. O /\ l e. N ) ) -> ( l Y j ) e. B )
33 elmapi
 |-  ( Z e. ( B ^m ( O X. P ) ) -> Z : ( O X. P ) --> B )
34 9 33 syl
 |-  ( ph -> Z : ( O X. P ) --> B )
35 34 ad2antrr
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. O ) -> Z : ( O X. P ) --> B )
36 simpr
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. O ) -> j e. O )
37 simplrr
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. O ) -> k e. P )
38 35 36 37 fovcdmd
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. O ) -> ( j Z k ) e. B )
39 38 adantrr
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ ( j e. O /\ l e. N ) ) -> ( j Z k ) e. B )
40 1 18 19 32 39 ringcld
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ ( j e. O /\ l e. N ) ) -> ( ( l Y j ) ( .r ` R ) ( j Z k ) ) e. B )
41 1 18 19 26 40 ringcld
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ ( j e. O /\ l e. N ) ) -> ( ( i X l ) ( .r ` R ) ( ( l Y j ) ( .r ` R ) ( j Z k ) ) ) e. B )
42 1 15 16 17 41 gsumcom3fi
 |-  ( ( ph /\ ( i e. M /\ k e. P ) ) -> ( R gsum ( j e. O |-> ( R gsum ( l e. N |-> ( ( i X l ) ( .r ` R ) ( ( l Y j ) ( .r ` R ) ( j Z k ) ) ) ) ) ) ) = ( R gsum ( l e. N |-> ( R gsum ( j e. O |-> ( ( i X l ) ( .r ` R ) ( ( l Y j ) ( .r ` R ) ( j Z k ) ) ) ) ) ) ) )
43 2 ad2antrr
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. O ) -> R e. Ring )
44 3 ad2antrr
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. O ) -> M e. Fin )
45 4 ad2antrr
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. O ) -> N e. Fin )
46 5 ad2antrr
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. O ) -> O e. Fin )
47 7 ad2antrr
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. O ) -> X e. ( B ^m ( M X. N ) ) )
48 8 ad2antrr
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. O ) -> Y e. ( B ^m ( N X. O ) ) )
49 simplrl
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. O ) -> i e. M )
50 10 1 18 43 44 45 46 47 48 49 36 mamufv
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. O ) -> ( i ( X F Y ) j ) = ( R gsum ( l e. N |-> ( ( i X l ) ( .r ` R ) ( l Y j ) ) ) ) )
51 50 oveq1d
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. O ) -> ( ( i ( X F Y ) j ) ( .r ` R ) ( j Z k ) ) = ( ( R gsum ( l e. N |-> ( ( i X l ) ( .r ` R ) ( l Y j ) ) ) ) ( .r ` R ) ( j Z k ) ) )
52 eqid
 |-  ( 0g ` R ) = ( 0g ` R )
53 1 18 19 26 32 ringcld
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ ( j e. O /\ l e. N ) ) -> ( ( i X l ) ( .r ` R ) ( l Y j ) ) e. B )
54 53 anassrs
 |-  ( ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. O ) /\ l e. N ) -> ( ( i X l ) ( .r ` R ) ( l Y j ) ) e. B )
55 eqid
 |-  ( l e. N |-> ( ( i X l ) ( .r ` R ) ( l Y j ) ) ) = ( l e. N |-> ( ( i X l ) ( .r ` R ) ( l Y j ) ) )
56 ovexd
 |-  ( ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. O ) /\ l e. N ) -> ( ( i X l ) ( .r ` R ) ( l Y j ) ) e. _V )
57 fvexd
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. O ) -> ( 0g ` R ) e. _V )
58 55 45 56 57 fsuppmptdm
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. O ) -> ( l e. N |-> ( ( i X l ) ( .r ` R ) ( l Y j ) ) ) finSupp ( 0g ` R ) )
59 1 52 18 43 45 38 54 58 gsummulc1
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. O ) -> ( R gsum ( l e. N |-> ( ( ( i X l ) ( .r ` R ) ( l Y j ) ) ( .r ` R ) ( j Z k ) ) ) ) = ( ( R gsum ( l e. N |-> ( ( i X l ) ( .r ` R ) ( l Y j ) ) ) ) ( .r ` R ) ( j Z k ) ) )
60 1 18 ringass
 |-  ( ( R e. Ring /\ ( ( i X l ) e. B /\ ( l Y j ) e. B /\ ( j Z k ) e. B ) ) -> ( ( ( i X l ) ( .r ` R ) ( l Y j ) ) ( .r ` R ) ( j Z k ) ) = ( ( i X l ) ( .r ` R ) ( ( l Y j ) ( .r ` R ) ( j Z k ) ) ) )
61 19 26 32 39 60 syl13anc
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ ( j e. O /\ l e. N ) ) -> ( ( ( i X l ) ( .r ` R ) ( l Y j ) ) ( .r ` R ) ( j Z k ) ) = ( ( i X l ) ( .r ` R ) ( ( l Y j ) ( .r ` R ) ( j Z k ) ) ) )
62 61 anassrs
 |-  ( ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. O ) /\ l e. N ) -> ( ( ( i X l ) ( .r ` R ) ( l Y j ) ) ( .r ` R ) ( j Z k ) ) = ( ( i X l ) ( .r ` R ) ( ( l Y j ) ( .r ` R ) ( j Z k ) ) ) )
63 62 mpteq2dva
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. O ) -> ( l e. N |-> ( ( ( i X l ) ( .r ` R ) ( l Y j ) ) ( .r ` R ) ( j Z k ) ) ) = ( l e. N |-> ( ( i X l ) ( .r ` R ) ( ( l Y j ) ( .r ` R ) ( j Z k ) ) ) ) )
64 63 oveq2d
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. O ) -> ( R gsum ( l e. N |-> ( ( ( i X l ) ( .r ` R ) ( l Y j ) ) ( .r ` R ) ( j Z k ) ) ) ) = ( R gsum ( l e. N |-> ( ( i X l ) ( .r ` R ) ( ( l Y j ) ( .r ` R ) ( j Z k ) ) ) ) ) )
65 51 59 64 3eqtr2d
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. O ) -> ( ( i ( X F Y ) j ) ( .r ` R ) ( j Z k ) ) = ( R gsum ( l e. N |-> ( ( i X l ) ( .r ` R ) ( ( l Y j ) ( .r ` R ) ( j Z k ) ) ) ) ) )
66 65 mpteq2dva
 |-  ( ( ph /\ ( i e. M /\ k e. P ) ) -> ( j e. O |-> ( ( i ( X F Y ) j ) ( .r ` R ) ( j Z k ) ) ) = ( j e. O |-> ( R gsum ( l e. N |-> ( ( i X l ) ( .r ` R ) ( ( l Y j ) ( .r ` R ) ( j Z k ) ) ) ) ) ) )
67 66 oveq2d
 |-  ( ( ph /\ ( i e. M /\ k e. P ) ) -> ( R gsum ( j e. O |-> ( ( i ( X F Y ) j ) ( .r ` R ) ( j Z k ) ) ) ) = ( R gsum ( j e. O |-> ( R gsum ( l e. N |-> ( ( i X l ) ( .r ` R ) ( ( l Y j ) ( .r ` R ) ( j Z k ) ) ) ) ) ) ) )
68 2 ad2antrr
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ l e. N ) -> R e. Ring )
69 4 ad2antrr
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ l e. N ) -> N e. Fin )
70 5 ad2antrr
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ l e. N ) -> O e. Fin )
71 6 ad2antrr
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ l e. N ) -> P e. Fin )
72 8 ad2antrr
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ l e. N ) -> Y e. ( B ^m ( N X. O ) ) )
73 9 ad2antrr
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ l e. N ) -> Z e. ( B ^m ( O X. P ) ) )
74 simplrr
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ l e. N ) -> k e. P )
75 13 1 18 68 69 70 71 72 73 24 74 mamufv
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ l e. N ) -> ( l ( Y I Z ) k ) = ( R gsum ( j e. O |-> ( ( l Y j ) ( .r ` R ) ( j Z k ) ) ) ) )
76 75 oveq2d
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ l e. N ) -> ( ( i X l ) ( .r ` R ) ( l ( Y I Z ) k ) ) = ( ( i X l ) ( .r ` R ) ( R gsum ( j e. O |-> ( ( l Y j ) ( .r ` R ) ( j Z k ) ) ) ) ) )
77 40 anass1rs
 |-  ( ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ l e. N ) /\ j e. O ) -> ( ( l Y j ) ( .r ` R ) ( j Z k ) ) e. B )
78 eqid
 |-  ( j e. O |-> ( ( l Y j ) ( .r ` R ) ( j Z k ) ) ) = ( j e. O |-> ( ( l Y j ) ( .r ` R ) ( j Z k ) ) )
79 ovexd
 |-  ( ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ l e. N ) /\ j e. O ) -> ( ( l Y j ) ( .r ` R ) ( j Z k ) ) e. _V )
80 fvexd
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ l e. N ) -> ( 0g ` R ) e. _V )
81 78 70 79 80 fsuppmptdm
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ l e. N ) -> ( j e. O |-> ( ( l Y j ) ( .r ` R ) ( j Z k ) ) ) finSupp ( 0g ` R ) )
82 1 52 18 68 70 25 77 81 gsummulc2
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ l e. N ) -> ( R gsum ( j e. O |-> ( ( i X l ) ( .r ` R ) ( ( l Y j ) ( .r ` R ) ( j Z k ) ) ) ) ) = ( ( i X l ) ( .r ` R ) ( R gsum ( j e. O |-> ( ( l Y j ) ( .r ` R ) ( j Z k ) ) ) ) ) )
83 76 82 eqtr4d
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ l e. N ) -> ( ( i X l ) ( .r ` R ) ( l ( Y I Z ) k ) ) = ( R gsum ( j e. O |-> ( ( i X l ) ( .r ` R ) ( ( l Y j ) ( .r ` R ) ( j Z k ) ) ) ) ) )
84 83 mpteq2dva
 |-  ( ( ph /\ ( i e. M /\ k e. P ) ) -> ( l e. N |-> ( ( i X l ) ( .r ` R ) ( l ( Y I Z ) k ) ) ) = ( l e. N |-> ( R gsum ( j e. O |-> ( ( i X l ) ( .r ` R ) ( ( l Y j ) ( .r ` R ) ( j Z k ) ) ) ) ) ) )
85 84 oveq2d
 |-  ( ( ph /\ ( i e. M /\ k e. P ) ) -> ( R gsum ( l e. N |-> ( ( i X l ) ( .r ` R ) ( l ( Y I Z ) k ) ) ) ) = ( R gsum ( l e. N |-> ( R gsum ( j e. O |-> ( ( i X l ) ( .r ` R ) ( ( l Y j ) ( .r ` R ) ( j Z k ) ) ) ) ) ) ) )
86 42 67 85 3eqtr4d
 |-  ( ( ph /\ ( i e. M /\ k e. P ) ) -> ( R gsum ( j e. O |-> ( ( i ( X F Y ) j ) ( .r ` R ) ( j Z k ) ) ) ) = ( R gsum ( l e. N |-> ( ( i X l ) ( .r ` R ) ( l ( Y I Z ) k ) ) ) ) )
87 2 adantr
 |-  ( ( ph /\ ( i e. M /\ k e. P ) ) -> R e. Ring )
88 3 adantr
 |-  ( ( ph /\ ( i e. M /\ k e. P ) ) -> M e. Fin )
89 6 adantr
 |-  ( ( ph /\ ( i e. M /\ k e. P ) ) -> P e. Fin )
90 1 2 10 3 4 5 7 8 mamucl
 |-  ( ph -> ( X F Y ) e. ( B ^m ( M X. O ) ) )
91 90 adantr
 |-  ( ( ph /\ ( i e. M /\ k e. P ) ) -> ( X F Y ) e. ( B ^m ( M X. O ) ) )
92 9 adantr
 |-  ( ( ph /\ ( i e. M /\ k e. P ) ) -> Z e. ( B ^m ( O X. P ) ) )
93 simprl
 |-  ( ( ph /\ ( i e. M /\ k e. P ) ) -> i e. M )
94 simprr
 |-  ( ( ph /\ ( i e. M /\ k e. P ) ) -> k e. P )
95 11 1 18 87 88 16 89 91 92 93 94 mamufv
 |-  ( ( ph /\ ( i e. M /\ k e. P ) ) -> ( i ( ( X F Y ) G Z ) k ) = ( R gsum ( j e. O |-> ( ( i ( X F Y ) j ) ( .r ` R ) ( j Z k ) ) ) ) )
96 7 adantr
 |-  ( ( ph /\ ( i e. M /\ k e. P ) ) -> X e. ( B ^m ( M X. N ) ) )
97 1 2 13 4 5 6 8 9 mamucl
 |-  ( ph -> ( Y I Z ) e. ( B ^m ( N X. P ) ) )
98 97 adantr
 |-  ( ( ph /\ ( i e. M /\ k e. P ) ) -> ( Y I Z ) e. ( B ^m ( N X. P ) ) )
99 12 1 18 87 88 17 89 96 98 93 94 mamufv
 |-  ( ( ph /\ ( i e. M /\ k e. P ) ) -> ( i ( X H ( Y I Z ) ) k ) = ( R gsum ( l e. N |-> ( ( i X l ) ( .r ` R ) ( l ( Y I Z ) k ) ) ) ) )
100 86 95 99 3eqtr4d
 |-  ( ( ph /\ ( i e. M /\ k e. P ) ) -> ( i ( ( X F Y ) G Z ) k ) = ( i ( X H ( Y I Z ) ) k ) )
101 100 ralrimivva
 |-  ( ph -> A. i e. M A. k e. 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
 |-  ( ph -> ( ( X F Y ) G Z ) e. ( B ^m ( M X. P ) ) )
103 elmapi
 |-  ( ( ( X F Y ) G Z ) e. ( B ^m ( M X. P ) ) -> ( ( X F Y ) G Z ) : ( M X. P ) --> B )
104 ffn
 |-  ( ( ( X F Y ) G Z ) : ( M X. P ) --> B -> ( ( X F Y ) G Z ) Fn ( M X. P ) )
105 102 103 104 3syl
 |-  ( ph -> ( ( X F Y ) G Z ) Fn ( M X. P ) )
106 1 2 12 3 4 6 7 97 mamucl
 |-  ( ph -> ( X H ( Y I Z ) ) e. ( B ^m ( M X. P ) ) )
107 elmapi
 |-  ( ( X H ( Y I Z ) ) e. ( B ^m ( M X. P ) ) -> ( X H ( Y I Z ) ) : ( M X. P ) --> B )
108 ffn
 |-  ( ( X H ( Y I Z ) ) : ( M X. P ) --> B -> ( X H ( Y I Z ) ) Fn ( M X. P ) )
109 106 107 108 3syl
 |-  ( ph -> ( X H ( Y I Z ) ) Fn ( M X. P ) )
110 eqfnov2
 |-  ( ( ( ( X F Y ) G Z ) Fn ( M X. P ) /\ ( X H ( Y I Z ) ) Fn ( M X. P ) ) -> ( ( ( X F Y ) G Z ) = ( X H ( Y I Z ) ) <-> A. i e. M A. k e. P ( i ( ( X F Y ) G Z ) k ) = ( i ( X H ( Y I Z ) ) k ) ) )
111 105 109 110 syl2anc
 |-  ( ph -> ( ( ( X F Y ) G Z ) = ( X H ( Y I Z ) ) <-> A. i e. M A. k e. P ( i ( ( X F Y ) G Z ) k ) = ( i ( X H ( Y I Z ) ) k ) ) )
112 101 111 mpbird
 |-  ( ph -> ( ( X F Y ) G Z ) = ( X H ( Y I Z ) ) )