Metamath Proof Explorer

Definition df-marepv

Description: Function replacing a column of a matrix by a vector. (Contributed by AV, 9-Feb-2019) (Revised by AV, 26-Feb-2019)

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmatrepV 
 |-  matRepV
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 vv 
 |-  v
12 8 5 cfv 
 |-  ( Base ` r )
13 cmap 
 |-  ^m
14 12 6 13 co 
 |-  ( ( Base ` r ) ^m n )
15 vk 
 |-  k
16 vi 
 |-  i
17 vj 
 |-  j
18 17 cv 
 |-  j
19 15 cv 
 |-  k
20 18 19 wceq 
 |-  j = k
21 11 cv 
 |-  v
22 16 cv 
 |-  i
23 22 21 cfv 
 |-  ( v ` i )
24 4 cv 
 |-  m
25 22 18 24 co 
 |-  ( i m j )
26 20 23 25 cif 
 |-  if ( j = k , ( v ` i ) , ( i m j ) )
27 16 17 6 6 26 cmpo 
 |-  ( i e. n , j e. n |-> if ( j = k , ( v ` i ) , ( i m j ) ) )
28 15 6 27 cmpt 
 |-  ( k e. n |-> ( i e. n , j e. n |-> if ( j = k , ( v ` i ) , ( i m j ) ) ) )
29 4 11 10 14 28 cmpo 
 |-  ( 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 ) ) ) ) )
30 1 3 2 2 29 cmpo 
 |-  ( 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 ) ) ) ) ) )
31 0 30 wceq 
 |-  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 ) ) ) ) ) )