Definition df-mvmul 20347

Description: The operator which multiplies an M x N -matrix with an N-dimensional vector. (Contributed by AV, 23-Feb-2019.)

Assertion

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

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

Detailed syntax breakdown of Definition df-mvmul

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

This definition is referenced by:  mvmulfval  20348