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

Metamath Proof Explorer

Theorem mamudir

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