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

Definition df-marrep 18466
Description: Define the matrices whose k-th row is replaced by 0's and an arbitrary element of the underlying ring at the l-th column. (Contributed by AV, 12-Feb-2019.)
Assertion
Ref Expression
df-marrep  |- matRRep  =  ( n  e.  _V , 
r  e.  _V  |->  ( m  e.  ( Base `  ( n Mat  r ) ) ,  s  e.  ( Base `  r
)  |->  ( k  e.  n ,  l  e.  n  |->  ( i  e.  n ,  j  e.  n  |->  if ( i  =  k ,  if ( j  =  l ,  s ,  ( 0g `  r ) ) ,  ( i m j ) ) ) ) ) )
Distinct variable group:    n, r, m, i, j, k, l, s

Detailed syntax breakdown of Definition df-marrep
StepHypRef Expression
1 cmarrep 18464 . 2  class matRRep
2 vn . . 3  setvar  n
3 vr . . 3  setvar  r
4 cvv 3054 . . 3  class  _V
5 vm . . . 4  setvar  m
6 vs . . . 4  setvar  s
72cv 1369 . . . . . 6  class  n
83cv 1369 . . . . . 6  class  r
9 cmat 18375 . . . . . 6  class Mat
107, 8, 9co 6176 . . . . 5  class  ( n Mat  r )
11 cbs 14262 . . . . 5  class  Base
1210, 11cfv 5502 . . . 4  class  ( Base `  ( n Mat  r ) )
138, 11cfv 5502 . . . 4  class  ( Base `  r )
14 vk . . . . 5  setvar  k
15 vl . . . . 5  setvar  l
16 vi . . . . . 6  setvar  i
17 vj . . . . . 6  setvar  j
1816, 14weq 1696 . . . . . . 7  wff  i  =  k
1917, 15weq 1696 . . . . . . . 8  wff  j  =  l
206cv 1369 . . . . . . . 8  class  s
21 c0g 14466 . . . . . . . . 9  class  0g
228, 21cfv 5502 . . . . . . . 8  class  ( 0g
`  r )
2319, 20, 22cif 3875 . . . . . . 7  class  if ( j  =  l ,  s ,  ( 0g
`  r ) )
2416cv 1369 . . . . . . . 8  class  i
2517cv 1369 . . . . . . . 8  class  j
265cv 1369 . . . . . . . 8  class  m
2724, 25, 26co 6176 . . . . . . 7  class  ( i m j )
2818, 23, 27cif 3875 . . . . . 6  class  if ( i  =  k ,  if ( j  =  l ,  s ,  ( 0g `  r
) ) ,  ( i m j ) )
2916, 17, 7, 7, 28cmpt2 6178 . . . . 5  class  ( i  e.  n ,  j  e.  n  |->  if ( i  =  k ,  if ( j  =  l ,  s ,  ( 0g `  r
) ) ,  ( i m j ) ) )
3014, 15, 7, 7, 29cmpt2 6178 . . . 4  class  ( k  e.  n ,  l  e.  n  |->  ( i  e.  n ,  j  e.  n  |->  if ( i  =  k ,  if ( j  =  l ,  s ,  ( 0g `  r
) ) ,  ( i m j ) ) ) )
315, 6, 12, 13, 30cmpt2 6178 . . 3  class  ( m  e.  ( Base `  (
n Mat  r ) ) ,  s  e.  (
Base `  r )  |->  ( k  e.  n ,  l  e.  n  |->  ( i  e.  n ,  j  e.  n  |->  if ( i  =  k ,  if ( j  =  l ,  s ,  ( 0g
`  r ) ) ,  ( i m j ) ) ) ) )
322, 3, 4, 4, 31cmpt2 6178 . 2  class  ( n  e.  _V ,  r  e.  _V  |->  ( m  e.  ( Base `  (
n Mat  r ) ) ,  s  e.  (
Base `  r )  |->  ( k  e.  n ,  l  e.  n  |->  ( i  e.  n ,  j  e.  n  |->  if ( i  =  k ,  if ( j  =  l ,  s ,  ( 0g
`  r ) ) ,  ( i m j ) ) ) ) ) )
331, 32wceq 1370 1  wff matRRep  =  ( n  e.  _V , 
r  e.  _V  |->  ( m  e.  ( Base `  ( n Mat  r ) ) ,  s  e.  ( Base `  r
)  |->  ( k  e.  n ,  l  e.  n  |->  ( i  e.  n ,  j  e.  n  |->  if ( i  =  k ,  if ( j  =  l ,  s ,  ( 0g `  r ) ) ,  ( i m j ) ) ) ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  marrepfval  18468
  Copyright terms: Public domain W3C validator