MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-marepv Structured version   Unicode version

Definition df-marepv 18483
Description: Function replacing a column of a matrix by a vector. (Contributed by AV, 9-Feb-2019.) (Revised by AV, 26-Feb-2019.)
Assertion
Ref Expression
df-marepv  |- matRepV  =  ( n  e.  _V , 
r  e.  _V  |->  ( m  e.  ( Base `  ( n Mat  r ) ) ,  v  e.  ( ( Base `  r
)  ^m  n )  |->  ( k  e.  n  |->  ( i  e.  n ,  j  e.  n  |->  if ( j  =  k ,  ( v `
 i ) ,  ( i m j ) ) ) ) ) )
Distinct variable group:    i, j, k, m, n, r, v

Detailed syntax breakdown of Definition df-marepv
StepHypRef Expression
1 cmatrepV 18481 . 2  class matRepV
2 vn . . 3  setvar  n
3 vr . . 3  setvar  r
4 cvv 3070 . . 3  class  _V
5 vm . . . 4  setvar  m
6 vv . . . 4  setvar  v
72cv 1369 . . . . . 6  class  n
83cv 1369 . . . . . 6  class  r
9 cmat 18391 . . . . . 6  class Mat
107, 8, 9co 6192 . . . . 5  class  ( n Mat  r )
11 cbs 14278 . . . . 5  class  Base
1210, 11cfv 5518 . . . 4  class  ( Base `  ( n Mat  r ) )
138, 11cfv 5518 . . . . 5  class  ( Base `  r )
14 cmap 7316 . . . . 5  class  ^m
1513, 7, 14co 6192 . . . 4  class  ( (
Base `  r )  ^m  n )
16 vk . . . . 5  setvar  k
17 vi . . . . . 6  setvar  i
18 vj . . . . . 6  setvar  j
1918, 16weq 1696 . . . . . . 7  wff  j  =  k
2017cv 1369 . . . . . . . 8  class  i
216cv 1369 . . . . . . . 8  class  v
2220, 21cfv 5518 . . . . . . 7  class  ( v `
 i )
2318cv 1369 . . . . . . . 8  class  j
245cv 1369 . . . . . . . 8  class  m
2520, 23, 24co 6192 . . . . . . 7  class  ( i m j )
2619, 22, 25cif 3891 . . . . . 6  class  if ( j  =  k ,  ( v `  i
) ,  ( i m j ) )
2717, 18, 7, 7, 26cmpt2 6194 . . . . 5  class  ( i  e.  n ,  j  e.  n  |->  if ( j  =  k ,  ( v `  i
) ,  ( i m j ) ) )
2816, 7, 27cmpt 4450 . . . 4  class  ( k  e.  n  |->  ( i  e.  n ,  j  e.  n  |->  if ( j  =  k ,  ( v `  i
) ,  ( i m j ) ) ) )
295, 6, 12, 15, 28cmpt2 6194 . . 3  class  ( m  e.  ( Base `  (
n Mat  r ) ) ,  v  e.  ( ( Base `  r
)  ^m  n )  |->  ( k  e.  n  |->  ( i  e.  n ,  j  e.  n  |->  if ( j  =  k ,  ( v `
 i ) ,  ( i m j ) ) ) ) )
302, 3, 4, 4, 29cmpt2 6194 . 2  class  ( n  e.  _V ,  r  e.  _V  |->  ( m  e.  ( Base `  (
n Mat  r ) ) ,  v  e.  ( ( Base `  r
)  ^m  n )  |->  ( k  e.  n  |->  ( i  e.  n ,  j  e.  n  |->  if ( j  =  k ,  ( v `
 i ) ,  ( i m j ) ) ) ) ) )
311, 30wceq 1370 1  wff matRepV  =  ( n  e.  _V , 
r  e.  _V  |->  ( m  e.  ( Base `  ( n Mat  r ) ) ,  v  e.  ( ( Base `  r
)  ^m  n )  |->  ( k  e.  n  |->  ( i  e.  n ,  j  e.  n  |->  if ( j  =  k ,  ( v `
 i ) ,  ( i m j ) ) ) ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  marepvfval  18489
  Copyright terms: Public domain W3C validator