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