Definition df-mamu 20190

Description: The operator which multiplies an m x n matrix with an n x p matrix, see also the definition in [Lang] p. 504. Note that it is not generally possible to recover the dimensions from the matrix, since all n x 0 and all 0 x n matrices are represented by the empty set. (Contributed by Stefan O'Rear, 4-Sep-2015.)

Assertion

Ref	Expression
df-mamu	|- maMul = ( r e. _V , o e. _V |-> [_ ( 1st ` ( 1st ` o ) ) / m ]_ [_ ( 2nd ` ( 1st ` o ) ) / n ]_ [_ ( 2nd ` o ) / p ]_ ( x e. ( ( Base ` r ) ^m ( m X. n ) ) , y e. ( ( Base ` r ) ^m ( n X. p ) ) |-> ( i e. m , k e. p |-> ( r gsumg ( j e. n |-> ( ( i x j ) ( .r ` r ) ( j y k ) ) ) ) ) ) )

Distinct variable group:   i, j, k, m, n, o, p, r, x, y

Detailed syntax breakdown of Definition df-mamu

Step	Hyp	Ref	Expression
1		cmmul 20189	. 2 class maMul
2		vr	. . 3 setvar r
3		vo	. . 3 setvar o
4		cvv 3200	. . 3 class _V
5		vm	. . . 4 setvar m
6	3	cv 1482	. . . . . 6 class o
7		c1st 7166	. . . . . 6 class 1st
8	6, 7	cfv 5888	. . . . 5 class ( 1st ` o )
9	8, 7	cfv 5888	. . . 4 class ( 1st ` ( 1st ` o ) )
10		vn	. . . . 5 setvar n
11		c2nd 7167	. . . . . 6 class 2nd
12	8, 11	cfv 5888	. . . . 5 class ( 2nd ` ( 1st ` o ) )
13		vp	. . . . . 6 setvar p
14	6, 11	cfv 5888	. . . . . 6 class ( 2nd ` o )
15		vx	. . . . . . 7 setvar x
16		vy	. . . . . . 7 setvar y
17	2	cv 1482	. . . . . . . . 9 class r
18		cbs 15857	. . . . . . . . 9 class Base
19	17, 18	cfv 5888	. . . . . . . 8 class ( Base ` r )
20	5	cv 1482	. . . . . . . . 9 class m
21	10	cv 1482	. . . . . . . . 9 class n
22	20, 21	cxp 5112	. . . . . . . 8 class ( m X. n )
23		cmap 7857	. . . . . . . 8 class ^m
24	19, 22, 23	co 6650	. . . . . . 7 class ( ( Base ` r ) ^m ( m X. n ) )
25	13	cv 1482	. . . . . . . . 9 class p
26	21, 25	cxp 5112	. . . . . . . 8 class ( n X. p )
27	19, 26, 23	co 6650	. . . . . . 7 class ( ( Base ` r ) ^m ( n X. p ) )
28		vi	. . . . . . . 8 setvar i
29		vk	. . . . . . . 8 setvar k
30		vj	. . . . . . . . . 10 setvar j
31	28	cv 1482	. . . . . . . . . . . 12 class i
32	30	cv 1482	. . . . . . . . . . . 12 class j
33	15	cv 1482	. . . . . . . . . . . 12 class x
34	31, 32, 33	co 6650	. . . . . . . . . . 11 class ( i x j )
35	29	cv 1482	. . . . . . . . . . . 12 class k
36	16	cv 1482	. . . . . . . . . . . 12 class y
37	32, 35, 36	co 6650	. . . . . . . . . . 11 class ( j y k )
38		cmulr 15942	. . . . . . . . . . . 12 class .r
39	17, 38	cfv 5888	. . . . . . . . . . 11 class ( .r ` r )
40	34, 37, 39	co 6650	. . . . . . . . . 10 class ( ( i x j ) ( .r ` r ) ( j y k ) )
41	30, 21, 40	cmpt 4729	. . . . . . . . 9 class ( j e. n |-> ( ( i x j ) ( .r ` r ) ( j y k ) ) )
42		cgsu 16101	. . . . . . . . 9 class gsumg
43	17, 41, 42	co 6650	. . . . . . . 8 class ( r gsumg ( j e. n |-> ( ( i x j ) ( .r ` r ) ( j y k ) ) ) )
44	28, 29, 20, 25, 43	cmpt2 6652	. . . . . . 7 class ( i e. m , k e. p |-> ( r gsumg ( j e. n |-> ( ( i x j ) ( .r ` r ) ( j y k ) ) ) ) )
45	15, 16, 24, 27, 44	cmpt2 6652	. . . . . 6 class ( x e. ( ( Base ` r ) ^m ( m X. n ) ) , y e. ( ( Base ` r ) ^m ( n X. p ) ) |-> ( i e. m , k e. p |-> ( r gsumg ( j e. n |-> ( ( i x j ) ( .r ` r ) ( j y k ) ) ) ) ) )
46	13, 14, 45	csb 3533	. . . . 5 class [_ ( 2nd ` o ) / p ]_ ( x e. ( ( Base ` r ) ^m ( m X. n ) ) , y e. ( ( Base ` r ) ^m ( n X. p ) ) |-> ( i e. m , k e. p |-> ( r gsumg ( j e. n |-> ( ( i x j ) ( .r ` r ) ( j y k ) ) ) ) ) )
47	10, 12, 46	csb 3533	. . . 4 class [_ ( 2nd ` ( 1st ` o ) ) / n ]_ [_ ( 2nd ` o ) / p ]_ ( x e. ( ( Base ` r ) ^m ( m X. n ) ) , y e. ( ( Base ` r ) ^m ( n X. p ) ) |-> ( i e. m , k e. p |-> ( r gsumg ( j e. n |-> ( ( i x j ) ( .r ` r ) ( j y k ) ) ) ) ) )
48	5, 9, 47	csb 3533	. . 3 class [_ ( 1st ` ( 1st ` o ) ) / m ]_ [_ ( 2nd ` ( 1st ` o ) ) / n ]_ [_ ( 2nd ` o ) / p ]_ ( x e. ( ( Base ` r ) ^m ( m X. n ) ) , y e. ( ( Base ` r ) ^m ( n X. p ) ) |-> ( i e. m , k e. p |-> ( r gsumg ( j e. n |-> ( ( i x j ) ( .r ` r ) ( j y k ) ) ) ) ) )
49	2, 3, 4, 4, 48	cmpt2 6652	. 2 class ( r e. _V , o e. _V |-> [_ ( 1st ` ( 1st ` o ) ) / m ]_ [_ ( 2nd ` ( 1st ` o ) ) / n ]_ [_ ( 2nd ` o ) / p ]_ ( x e. ( ( Base ` r ) ^m ( m X. n ) ) , y e. ( ( Base ` r ) ^m ( n X. p ) ) |-> ( i e. m , k e. p |-> ( r gsumg ( j e. n |-> ( ( i x j ) ( .r ` r ) ( j y k ) ) ) ) ) ) )
50	1, 49	wceq 1483	1 wff maMul = ( r e. _V , o e. _V |-> [_ ( 1st ` ( 1st ` o ) ) / m ]_ [_ ( 2nd ` ( 1st ` o ) ) / n ]_ [_ ( 2nd ` o ) / p ]_ ( x e. ( ( Base ` r ) ^m ( m X. n ) ) , y e. ( ( Base ` r ) ^m ( n X. p ) ) |-> ( i e. m , k e. p |-> ( r gsumg ( j e. n |-> ( ( i x j ) ( .r ` r ) ( j y k ) ) ) ) ) ) )

This definition is referenced by:  mamufval  20191