Metamath Proof Explorer

Definition df-marrep

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)

Ref Expression
Assertion 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 ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmarrep 
 |-  matRRep
1 vn 
 |-  n
2 cvv 
 |-  _V
3 vr 
 |-  r
4 vm 
 |-  m
5 cbs 
 |-  Base
6 1 cv 
 |-  n
7 cmat 
 |-  Mat
8 3 cv 
 |-  r
9 6 8 7 co 
 |-  ( n Mat r )
10 9 5 cfv 
 |-  ( Base ` ( n Mat r ) )
11 vs 
 |-  s
12 8 5 cfv 
 |-  ( Base ` r )
13 vk 
 |-  k
14 vl 
 |-  l
15 vi 
 |-  i
16 vj 
 |-  j
17 15 cv 
 |-  i
18 13 cv 
 |-  k
19 17 18 wceq 
 |-  i = k
20 16 cv 
 |-  j
21 14 cv 
 |-  l
22 20 21 wceq 
 |-  j = l
23 11 cv 
 |-  s
24 c0g 
 |-  0g
25 8 24 cfv 
 |-  ( 0g ` r )
26 22 23 25 cif 
 |-  if ( j = l , s , ( 0g ` r ) )
27 4 cv 
 |-  m
28 17 20 27 co 
 |-  ( i m j )
29 19 26 28 cif 
 |-  if ( i = k , if ( j = l , s , ( 0g ` r ) ) , ( i m j ) )
30 15 16 6 6 29 cmpo 
 |-  ( i e. n , j e. n |-> if ( i = k , if ( j = l , s , ( 0g ` r ) ) , ( i m j ) ) )
31 13 14 6 6 30 cmpo 
 |-  ( k e. n , l e. n |-> ( i e. n , j e. n |-> if ( i = k , if ( j = l , s , ( 0g ` r ) ) , ( i m j ) ) ) )
32 4 11 10 12 31 cmpo 
 |-  ( 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 ) ) ) ) )
33 1 3 2 2 32 cmpo 
 |-  ( 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 ) ) ) ) ) )
34 0 33 wceq 
 |-  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 ) ) ) ) ) )