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