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

Metamath Proof Explorer

Theorem mamudi

Description: Matrix multiplication distributes over addition on the left. (Contributed by Stefan O'Rear, 5-Sep-2015) (Proof shortened by AV, 23-Jul-2019)

Ref Expression
Hypotheses mamucl.b 
|- B = ( Base ` R )
mamucl.r 
|- ( ph -> R e. Ring )
mamudi.f 
|- F = ( R maMul <. M , N , O >. )
mamudi.m 
|- ( ph -> M e. Fin )
mamudi.n 
|- ( ph -> N e. Fin )
mamudi.o 
|- ( ph -> O e. Fin )
mamudi.p 
|- .+ = ( +g ` R )
mamudi.x 
|- ( ph -> X e. ( B ^m ( M X. N ) ) )
mamudi.y 
|- ( ph -> Y e. ( B ^m ( M X. N ) ) )
mamudi.z 
|- ( ph -> Z e. ( B ^m ( N X. O ) ) )
Assertion mamudi 
|- ( ph -> ( ( X oF .+ Y ) F Z ) = ( ( X F Z ) oF .+ ( Y F Z ) ) )

Proof

Step Hyp Ref Expression
1 mamucl.b 
 |-  B = ( Base ` R )
2 mamucl.r 
 |-  ( ph -> R e. Ring )
3 mamudi.f 
 |-  F = ( R maMul <. M , N , O >. )
4 mamudi.m 
 |-  ( ph -> M e. Fin )
5 mamudi.n 
 |-  ( ph -> N e. Fin )
6 mamudi.o 
 |-  ( ph -> O e. Fin )
7 mamudi.p 
 |-  .+ = ( +g ` R )
8 mamudi.x 
 |-  ( ph -> X e. ( B ^m ( M X. N ) ) )
9 mamudi.y 
 |-  ( ph -> Y e. ( B ^m ( M X. N ) ) )
10 mamudi.z 
 |-  ( ph -> Z e. ( B ^m ( N X. O ) ) )
11 ringcmn 
 |-  ( R e. Ring -> R e. CMnd )
12 2 11 syl 
 |-  ( ph -> R e. CMnd )
13 12 adantr 
 |-  ( ( ph /\ ( i e. M /\ k e. O ) ) -> R e. CMnd )
14 5 adantr 
 |-  ( ( ph /\ ( i e. M /\ k e. O ) ) -> N e. Fin )
15 2 ad2antrr 
 |-  ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> R e. Ring )
16 elmapi 
 |-  ( X e. ( B ^m ( M X. N ) ) -> X : ( M X. N ) --> B )
17 8 16 syl 
 |-  ( ph -> X : ( M X. N ) --> B )
18 17 ad2antrr 
 |-  ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> X : ( M X. N ) --> B )
19 simplrl 
 |-  ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> i e. M )
20 simpr 
 |-  ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> j e. N )
21 18 19 20 fovcdmd 
 |-  ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> ( i X j ) e. B )
22 elmapi 
 |-  ( Z e. ( B ^m ( N X. O ) ) -> Z : ( N X. O ) --> B )
23 10 22 syl 
 |-  ( ph -> Z : ( N X. O ) --> B )
24 23 ad2antrr 
 |-  ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> Z : ( N X. O ) --> B )
25 simplrr 
 |-  ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> k e. O )
26 24 20 25 fovcdmd 
 |-  ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> ( j Z k ) e. B )
27 eqid 
 |-  ( .r ` R ) = ( .r ` R )
28 1 27 ringcl 
 |-  ( ( R e. Ring /\ ( i X j ) e. B /\ ( j Z k ) e. B ) -> ( ( i X j ) ( .r ` R ) ( j Z k ) ) e. B )
29 15 21 26 28 syl3anc 
 |-  ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> ( ( i X j ) ( .r ` R ) ( j Z k ) ) e. B )
30 elmapi 
 |-  ( Y e. ( B ^m ( M X. N ) ) -> Y : ( M X. N ) --> B )
31 9 30 syl 
 |-  ( ph -> Y : ( M X. N ) --> B )
32 31 ad2antrr 
 |-  ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> Y : ( M X. N ) --> B )
33 32 19 20 fovcdmd 
 |-  ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> ( i Y j ) e. B )
34 1 27 ringcl 
 |-  ( ( R e. Ring /\ ( i Y j ) e. B /\ ( j Z k ) e. B ) -> ( ( i Y j ) ( .r ` R ) ( j Z k ) ) e. B )
35 15 33 26 34 syl3anc 
 |-  ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> ( ( i Y j ) ( .r ` R ) ( j Z k ) ) e. B )
36 eqid 
 |-  ( j e. N |-> ( ( i X j ) ( .r ` R ) ( j Z k ) ) ) = ( j e. N |-> ( ( i X j ) ( .r ` R ) ( j Z k ) ) )
37 eqid 
 |-  ( j e. N |-> ( ( i Y j ) ( .r ` R ) ( j Z k ) ) ) = ( j e. N |-> ( ( i Y j ) ( .r ` R ) ( j Z k ) ) )
38 1 7 13 14 29 35 36 37 gsummptfidmadd2 
 |-  ( ( ph /\ ( i e. M /\ k e. O ) ) -> ( R gsum ( ( j e. N |-> ( ( i X j ) ( .r ` R ) ( j Z k ) ) ) oF .+ ( j e. N |-> ( ( i Y j ) ( .r ` R ) ( j Z k ) ) ) ) ) = ( ( R gsum ( j e. N |-> ( ( i X j ) ( .r ` R ) ( j Z k ) ) ) ) .+ ( R gsum ( j e. N |-> ( ( i Y j ) ( .r ` R ) ( j Z k ) ) ) ) ) )
39 8 ad2antrr 
 |-  ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> X e. ( B ^m ( M X. N ) ) )
40 ffn 
 |-  ( X : ( M X. N ) --> B -> X Fn ( M X. N ) )
41 39 16 40 3syl 
 |-  ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> X Fn ( M X. N ) )
42 9 ad2antrr 
 |-  ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> Y e. ( B ^m ( M X. N ) ) )
43 ffn 
 |-  ( Y : ( M X. N ) --> B -> Y Fn ( M X. N ) )
44 42 30 43 3syl 
 |-  ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> Y Fn ( M X. N ) )
45 xpfi 
 |-  ( ( M e. Fin /\ N e. Fin ) -> ( M X. N ) e. Fin )
46 4 5 45 syl2anc 
 |-  ( ph -> ( M X. N ) e. Fin )
47 46 ad2antrr 
 |-  ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> ( M X. N ) e. Fin )
48 opelxpi 
 |-  ( ( i e. M /\ j e. N ) -> <. i , j >. e. ( M X. N ) )
49 48 adantlr 
 |-  ( ( ( i e. M /\ k e. O ) /\ j e. N ) -> <. i , j >. e. ( M X. N ) )
50 49 adantll 
 |-  ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> <. i , j >. e. ( M X. N ) )
51 fnfvof 
 |-  ( ( ( X Fn ( M X. N ) /\ Y Fn ( M X. N ) ) /\ ( ( M X. N ) e. Fin /\ <. i , j >. e. ( M X. N ) ) ) -> ( ( X oF .+ Y ) ` <. i , j >. ) = ( ( X ` <. i , j >. ) .+ ( Y ` <. i , j >. ) ) )
52 41 44 47 50 51 syl22anc 
 |-  ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> ( ( X oF .+ Y ) ` <. i , j >. ) = ( ( X ` <. i , j >. ) .+ ( Y ` <. i , j >. ) ) )
53 df-ov 
 |-  ( i ( X oF .+ Y ) j ) = ( ( X oF .+ Y ) ` <. i , j >. )
54 df-ov 
 |-  ( i X j ) = ( X ` <. i , j >. )
55 df-ov 
 |-  ( i Y j ) = ( Y ` <. i , j >. )
56 54 55 oveq12i 
 |-  ( ( i X j ) .+ ( i Y j ) ) = ( ( X ` <. i , j >. ) .+ ( Y ` <. i , j >. ) )
57 52 53 56 3eqtr4g 
 |-  ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> ( i ( X oF .+ Y ) j ) = ( ( i X j ) .+ ( i Y j ) ) )
58 57 oveq1d 
 |-  ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> ( ( i ( X oF .+ Y ) j ) ( .r ` R ) ( j Z k ) ) = ( ( ( i X j ) .+ ( i Y j ) ) ( .r ` R ) ( j Z k ) ) )
59 1 7 27 ringdir 
 |-  ( ( R e. Ring /\ ( ( i X j ) e. B /\ ( i Y j ) e. B /\ ( j Z k ) e. B ) ) -> ( ( ( i X j ) .+ ( i Y j ) ) ( .r ` R ) ( j Z k ) ) = ( ( ( i X j ) ( .r ` R ) ( j Z k ) ) .+ ( ( i Y j ) ( .r ` R ) ( j Z k ) ) ) )
60 15 21 33 26 59 syl13anc 
 |-  ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> ( ( ( i X j ) .+ ( i Y j ) ) ( .r ` R ) ( j Z k ) ) = ( ( ( i X j ) ( .r ` R ) ( j Z k ) ) .+ ( ( i Y j ) ( .r ` R ) ( j Z k ) ) ) )
61 58 60 eqtrd 
 |-  ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> ( ( i ( X oF .+ Y ) j ) ( .r ` R ) ( j Z k ) ) = ( ( ( i X j ) ( .r ` R ) ( j Z k ) ) .+ ( ( i Y j ) ( .r ` R ) ( j Z k ) ) ) )
62 61 mpteq2dva 
 |-  ( ( ph /\ ( i e. M /\ k e. O ) ) -> ( j e. N |-> ( ( i ( X oF .+ Y ) j ) ( .r ` R ) ( j Z k ) ) ) = ( j e. N |-> ( ( ( i X j ) ( .r ` R ) ( j Z k ) ) .+ ( ( i Y j ) ( .r ` R ) ( j Z k ) ) ) ) )
63 eqidd 
 |-  ( ( ph /\ ( i e. M /\ k e. O ) ) -> ( j e. N |-> ( ( i X j ) ( .r ` R ) ( j Z k ) ) ) = ( j e. N |-> ( ( i X j ) ( .r ` R ) ( j Z k ) ) ) )
64 eqidd 
 |-  ( ( ph /\ ( i e. M /\ k e. O ) ) -> ( j e. N |-> ( ( i Y j ) ( .r ` R ) ( j Z k ) ) ) = ( j e. N |-> ( ( i Y j ) ( .r ` R ) ( j Z k ) ) ) )
65 14 29 35 63 64 offval2 
 |-  ( ( ph /\ ( i e. M /\ k e. O ) ) -> ( ( j e. N |-> ( ( i X j ) ( .r ` R ) ( j Z k ) ) ) oF .+ ( j e. N |-> ( ( i Y j ) ( .r ` R ) ( j Z k ) ) ) ) = ( j e. N |-> ( ( ( i X j ) ( .r ` R ) ( j Z k ) ) .+ ( ( i Y j ) ( .r ` R ) ( j Z k ) ) ) ) )
66 62 65 eqtr4d 
 |-  ( ( ph /\ ( i e. M /\ k e. O ) ) -> ( j e. N |-> ( ( i ( X oF .+ Y ) j ) ( .r ` R ) ( j Z k ) ) ) = ( ( j e. N |-> ( ( i X j ) ( .r ` R ) ( j Z k ) ) ) oF .+ ( j e. N |-> ( ( i Y j ) ( .r ` R ) ( j Z k ) ) ) ) )
67 66 oveq2d 
 |-  ( ( ph /\ ( i e. M /\ k e. O ) ) -> ( R gsum ( j e. N |-> ( ( i ( X oF .+ Y ) j ) ( .r ` R ) ( j Z k ) ) ) ) = ( R gsum ( ( j e. N |-> ( ( i X j ) ( .r ` R ) ( j Z k ) ) ) oF .+ ( j e. N |-> ( ( i Y j ) ( .r ` R ) ( j Z k ) ) ) ) ) )
68 2 adantr 
 |-  ( ( ph /\ ( i e. M /\ k e. O ) ) -> R e. Ring )
69 4 adantr 
 |-  ( ( ph /\ ( i e. M /\ k e. O ) ) -> M e. Fin )
70 6 adantr 
 |-  ( ( ph /\ ( i e. M /\ k e. O ) ) -> O e. Fin )
71 8 adantr 
 |-  ( ( ph /\ ( i e. M /\ k e. O ) ) -> X e. ( B ^m ( M X. N ) ) )
72 10 adantr 
 |-  ( ( ph /\ ( i e. M /\ k e. O ) ) -> Z e. ( B ^m ( N X. O ) ) )
73 simprl 
 |-  ( ( ph /\ ( i e. M /\ k e. O ) ) -> i e. M )
74 simprr 
 |-  ( ( ph /\ ( i e. M /\ k e. O ) ) -> k e. O )
75 3 1 27 68 69 14 70 71 72 73 74 mamufv 
 |-  ( ( ph /\ ( i e. M /\ k e. O ) ) -> ( i ( X F Z ) k ) = ( R gsum ( j e. N |-> ( ( i X j ) ( .r ` R ) ( j Z k ) ) ) ) )
76 9 adantr 
 |-  ( ( ph /\ ( i e. M /\ k e. O ) ) -> Y e. ( B ^m ( M X. N ) ) )
77 3 1 27 68 69 14 70 76 72 73 74 mamufv 
 |-  ( ( ph /\ ( i e. M /\ k e. O ) ) -> ( i ( Y F Z ) k ) = ( R gsum ( j e. N |-> ( ( i Y j ) ( .r ` R ) ( j Z k ) ) ) ) )
78 75 77 oveq12d 
 |-  ( ( ph /\ ( i e. M /\ k e. O ) ) -> ( ( i ( X F Z ) k ) .+ ( i ( Y F Z ) k ) ) = ( ( R gsum ( j e. N |-> ( ( i X j ) ( .r ` R ) ( j Z k ) ) ) ) .+ ( R gsum ( j e. N |-> ( ( i Y j ) ( .r ` R ) ( j Z k ) ) ) ) ) )
79 38 67 78 3eqtr4d 
 |-  ( ( ph /\ ( i e. M /\ k e. O ) ) -> ( R gsum ( j e. N |-> ( ( i ( X oF .+ Y ) j ) ( .r ` R ) ( j Z k ) ) ) ) = ( ( i ( X F Z ) k ) .+ ( i ( Y F Z ) k ) ) )
80 ringmnd 
 |-  ( R e. Ring -> R e. Mnd )
81 2 80 syl 
 |-  ( ph -> R e. Mnd )
82 1 7 mndvcl 
 |-  ( ( R e. Mnd /\ X e. ( B ^m ( M X. N ) ) /\ Y e. ( B ^m ( M X. N ) ) ) -> ( X oF .+ Y ) e. ( B ^m ( M X. N ) ) )
83 81 8 9 82 syl3anc 
 |-  ( ph -> ( X oF .+ Y ) e. ( B ^m ( M X. N ) ) )
84 83 adantr 
 |-  ( ( ph /\ ( i e. M /\ k e. O ) ) -> ( X oF .+ Y ) e. ( B ^m ( M X. N ) ) )
85 3 1 27 68 69 14 70 84 72 73 74 mamufv 
 |-  ( ( ph /\ ( i e. M /\ k e. O ) ) -> ( i ( ( X oF .+ Y ) F Z ) k ) = ( R gsum ( j e. N |-> ( ( i ( X oF .+ Y ) j ) ( .r ` R ) ( j Z k ) ) ) ) )
86 1 2 3 4 5 6 8 10 mamucl 
 |-  ( ph -> ( X F Z ) e. ( B ^m ( M X. O ) ) )
87 elmapi 
 |-  ( ( X F Z ) e. ( B ^m ( M X. O ) ) -> ( X F Z ) : ( M X. O ) --> B )
88 ffn 
 |-  ( ( X F Z ) : ( M X. O ) --> B -> ( X F Z ) Fn ( M X. O ) )
89 86 87 88 3syl 
 |-  ( ph -> ( X F Z ) Fn ( M X. O ) )
90 89 adantr 
 |-  ( ( ph /\ ( i e. M /\ k e. O ) ) -> ( X F Z ) Fn ( M X. O ) )
91 1 2 3 4 5 6 9 10 mamucl 
 |-  ( ph -> ( Y F Z ) e. ( B ^m ( M X. O ) ) )
92 elmapi 
 |-  ( ( Y F Z ) e. ( B ^m ( M X. O ) ) -> ( Y F Z ) : ( M X. O ) --> B )
93 ffn 
 |-  ( ( Y F Z ) : ( M X. O ) --> B -> ( Y F Z ) Fn ( M X. O ) )
94 91 92 93 3syl 
 |-  ( ph -> ( Y F Z ) Fn ( M X. O ) )
95 94 adantr 
 |-  ( ( ph /\ ( i e. M /\ k e. O ) ) -> ( Y F Z ) Fn ( M X. O ) )
96 xpfi 
 |-  ( ( M e. Fin /\ O e. Fin ) -> ( M X. O ) e. Fin )
97 4 6 96 syl2anc 
 |-  ( ph -> ( M X. O ) e. Fin )
98 97 adantr 
 |-  ( ( ph /\ ( i e. M /\ k e. O ) ) -> ( M X. O ) e. Fin )
99 opelxpi 
 |-  ( ( i e. M /\ k e. O ) -> <. i , k >. e. ( M X. O ) )
100 99 adantl 
 |-  ( ( ph /\ ( i e. M /\ k e. O ) ) -> <. i , k >. e. ( M X. O ) )
101 fnfvof 
 |-  ( ( ( ( X F Z ) Fn ( M X. O ) /\ ( Y F Z ) Fn ( M X. O ) ) /\ ( ( M X. O ) e. Fin /\ <. i , k >. e. ( M X. O ) ) ) -> ( ( ( X F Z ) oF .+ ( Y F Z ) ) ` <. i , k >. ) = ( ( ( X F Z ) ` <. i , k >. ) .+ ( ( Y F Z ) ` <. i , k >. ) ) )
102 90 95 98 100 101 syl22anc 
 |-  ( ( ph /\ ( i e. M /\ k e. O ) ) -> ( ( ( X F Z ) oF .+ ( Y F Z ) ) ` <. i , k >. ) = ( ( ( X F Z ) ` <. i , k >. ) .+ ( ( Y F Z ) ` <. i , k >. ) ) )
103 df-ov 
 |-  ( i ( ( X F Z ) oF .+ ( Y F Z ) ) k ) = ( ( ( X F Z ) oF .+ ( Y F Z ) ) ` <. i , k >. )
104 df-ov 
 |-  ( i ( X F Z ) k ) = ( ( X F Z ) ` <. i , k >. )
105 df-ov 
 |-  ( i ( Y F Z ) k ) = ( ( Y F Z ) ` <. i , k >. )
106 104 105 oveq12i 
 |-  ( ( i ( X F Z ) k ) .+ ( i ( Y F Z ) k ) ) = ( ( ( X F Z ) ` <. i , k >. ) .+ ( ( Y F Z ) ` <. i , k >. ) )
107 102 103 106 3eqtr4g 
 |-  ( ( ph /\ ( i e. M /\ k e. O ) ) -> ( i ( ( X F Z ) oF .+ ( Y F Z ) ) k ) = ( ( i ( X F Z ) k ) .+ ( i ( Y F Z ) k ) ) )
108 79 85 107 3eqtr4d 
 |-  ( ( ph /\ ( i e. M /\ k e. O ) ) -> ( i ( ( X oF .+ Y ) F Z ) k ) = ( i ( ( X F Z ) oF .+ ( Y F Z ) ) k ) )
109 108 ralrimivva 
 |-  ( ph -> A. i e. M A. k e. O ( i ( ( X oF .+ Y ) F Z ) k ) = ( i ( ( X F Z ) oF .+ ( Y F Z ) ) k ) )
110 1 2 3 4 5 6 83 10 mamucl 
 |-  ( ph -> ( ( X oF .+ Y ) F Z ) e. ( B ^m ( M X. O ) ) )
111 elmapi 
 |-  ( ( ( X oF .+ Y ) F Z ) e. ( B ^m ( M X. O ) ) -> ( ( X oF .+ Y ) F Z ) : ( M X. O ) --> B )
112 ffn 
 |-  ( ( ( X oF .+ Y ) F Z ) : ( M X. O ) --> B -> ( ( X oF .+ Y ) F Z ) Fn ( M X. O ) )
113 110 111 112 3syl 
 |-  ( ph -> ( ( X oF .+ Y ) F Z ) Fn ( M X. O ) )
114 1 7 mndvcl 
 |-  ( ( R e. Mnd /\ ( X F Z ) e. ( B ^m ( M X. O ) ) /\ ( Y F Z ) e. ( B ^m ( M X. O ) ) ) -> ( ( X F Z ) oF .+ ( Y F Z ) ) e. ( B ^m ( M X. O ) ) )
115 81 86 91 114 syl3anc 
 |-  ( ph -> ( ( X F Z ) oF .+ ( Y F Z ) ) e. ( B ^m ( M X. O ) ) )
116 elmapi 
 |-  ( ( ( X F Z ) oF .+ ( Y F Z ) ) e. ( B ^m ( M X. O ) ) -> ( ( X F Z ) oF .+ ( Y F Z ) ) : ( M X. O ) --> B )
117 ffn 
 |-  ( ( ( X F Z ) oF .+ ( Y F Z ) ) : ( M X. O ) --> B -> ( ( X F Z ) oF .+ ( Y F Z ) ) Fn ( M X. O ) )
118 115 116 117 3syl 
 |-  ( ph -> ( ( X F Z ) oF .+ ( Y F Z ) ) Fn ( M X. O ) )
119 eqfnov2 
 |-  ( ( ( ( X oF .+ Y ) F Z ) Fn ( M X. O ) /\ ( ( X F Z ) oF .+ ( Y F Z ) ) Fn ( M X. O ) ) -> ( ( ( X oF .+ Y ) F Z ) = ( ( X F Z ) oF .+ ( Y F Z ) ) <-> A. i e. M A. k e. O ( i ( ( X oF .+ Y ) F Z ) k ) = ( i ( ( X F Z ) oF .+ ( Y F Z ) ) k ) ) )
120 113 118 119 syl2anc 
 |-  ( ph -> ( ( ( X oF .+ Y ) F Z ) = ( ( X F Z ) oF .+ ( Y F Z ) ) <-> A. i e. M A. k e. O ( i ( ( X oF .+ Y ) F Z ) k ) = ( i ( ( X F Z ) oF .+ ( Y F Z ) ) k ) ) )
121 109 120 mpbird 
 |-  ( ph -> ( ( X oF .+ Y ) F Z ) = ( ( X F Z ) oF .+ ( Y F Z ) ) )