Metamath Proof Explorer

Definition df-mamu

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)

Ref Expression
Assertion 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 gsum ( j e. n |-> ( ( i x j ) ( .r ` r ) ( j y k ) ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmmul 
 |-  maMul
1 vr 
 |-  r
2 cvv 
 |-  _V
3 vo 
 |-  o
4 c1st 
 |-  1st
5 3 cv 
 |-  o
6 5 4 cfv 
 |-  ( 1st ` o )
7 6 4 cfv 
 |-  ( 1st ` ( 1st ` o ) )
8 vm 
 |-  m
9 c2nd 
 |-  2nd
10 6 9 cfv 
 |-  ( 2nd ` ( 1st ` o ) )
11 vn 
 |-  n
12 5 9 cfv 
 |-  ( 2nd ` o )
13 vp 
 |-  p
14 vx 
 |-  x
15 cbs 
 |-  Base
16 1 cv 
 |-  r
17 16 15 cfv 
 |-  ( Base ` r )
18 cmap 
 |-  ^m
19 8 cv 
 |-  m
20 11 cv 
 |-  n
21 19 20 cxp 
 |-  ( m X. n )
22 17 21 18 co 
 |-  ( ( Base ` r ) ^m ( m X. n ) )
23 vy 
 |-  y
24 13 cv 
 |-  p
25 20 24 cxp 
 |-  ( n X. p )
26 17 25 18 co 
 |-  ( ( Base ` r ) ^m ( n X. p ) )
27 vi 
 |-  i
28 vk 
 |-  k
29 cgsu 
 |-  gsum
30 vj 
 |-  j
31 27 cv 
 |-  i
32 14 cv 
 |-  x
33 30 cv 
 |-  j
34 31 33 32 co 
 |-  ( i x j )
35 cmulr 
 |-  .r
36 16 35 cfv 
 |-  ( .r ` r )
37 23 cv 
 |-  y
38 28 cv 
 |-  k
39 33 38 37 co 
 |-  ( j y k )
40 34 39 36 co 
 |-  ( ( i x j ) ( .r ` r ) ( j y k ) )
41 30 20 40 cmpt 
 |-  ( j e. n |-> ( ( i x j ) ( .r ` r ) ( j y k ) ) )
42 16 41 29 co 
 |-  ( r gsum ( j e. n |-> ( ( i x j ) ( .r ` r ) ( j y k ) ) ) )
43 27 28 19 24 42 cmpo 
 |-  ( i e. m , k e. p |-> ( r gsum ( j e. n |-> ( ( i x j ) ( .r ` r ) ( j y k ) ) ) ) )
44 14 23 22 26 43 cmpo 
 |-  ( x e. ( ( Base ` r ) ^m ( m X. n ) ) , y e. ( ( Base ` r ) ^m ( n X. p ) ) |-> ( i e. m , k e. p |-> ( r gsum ( j e. n |-> ( ( i x j ) ( .r ` r ) ( j y k ) ) ) ) ) )
45 13 12 44 csb 
 |-  [_ ( 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 gsum ( j e. n |-> ( ( i x j ) ( .r ` r ) ( j y k ) ) ) ) ) )
46 11 10 45 csb 
 |-  [_ ( 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 gsum ( j e. n |-> ( ( i x j ) ( .r ` r ) ( j y k ) ) ) ) ) )
47 8 7 46 csb 
 |-  [_ ( 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 gsum ( j e. n |-> ( ( i x j ) ( .r ` r ) ( j y k ) ) ) ) ) )
48 1 3 2 2 47 cmpo 
 |-  ( 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 gsum ( j e. n |-> ( ( i x j ) ( .r ` r ) ( j y k ) ) ) ) ) ) )
49 0 48 wceq 
 |-  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 gsum ( j e. n |-> ( ( i x j ) ( .r ` r ) ( j y k ) ) ) ) ) ) )