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 ∈ V , r ∈ V ⟼ m ∈ Base n Mat r , v ∈ Base r n ⟼ k ∈ n ⟼ i ∈ n , j ∈ n ⟼ if j = k v ⁡ i i m j

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmatrepV class matRepV
1 vn setvar n
2 cvv class V
3 vr setvar r
4 vm setvar m
5 cbs class Base
6 1 cv setvar n
7 cmat class Mat
8 3 cv setvar r
9 6 8 7 co class n Mat r
10 9 5 cfv class Base n Mat r
11 vv setvar v
12 8 5 cfv class Base r
13 cmap class ↑ 𝑚
14 12 6 13 co class Base r n
15 vk setvar k
16 vi setvar i
17 vj setvar j
18 17 cv setvar j
19 15 cv setvar k
20 18 19 wceq wff j = k
21 11 cv setvar v
22 16 cv setvar i
23 22 21 cfv class v ⁡ i
24 4 cv setvar m
25 22 18 24 co class i m j
26 20 23 25 cif class if j = k v ⁡ i i m j
27 16 17 6 6 26 cmpo class i ∈ n , j ∈ n ⟼ if j = k v ⁡ i i m j
28 15 6 27 cmpt class k ∈ n ⟼ i ∈ n , j ∈ n ⟼ if j = k v ⁡ i i m j
29 4 11 10 14 28 cmpo class m ∈ Base n Mat r , v ∈ Base r n ⟼ k ∈ n ⟼ i ∈ n , j ∈ n ⟼ if j = k v ⁡ i i m j
30 1 3 2 2 29 cmpo class n ∈ V , r ∈ V ⟼ m ∈ Base n Mat r , v ∈ Base r n ⟼ k ∈ n ⟼ i ∈ n , j ∈ n ⟼ if j = k v ⁡ i i m j
31 0 30 wceq wff matRepV = n ∈ V , r ∈ V ⟼ m ∈ Base n Mat r , v ∈ Base r n ⟼ k ∈ n ⟼ i ∈ n , j ∈ n ⟼ if j = k v ⁡ i i m j