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

Definition df-marepv 21167
 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 = (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)), 𝑣 ∈ ((Base‘𝑟) ↑m 𝑛) ↦ (𝑘𝑛 ↦ (𝑖𝑛, 𝑗𝑛 ↦ if(𝑗 = 𝑘, (𝑣𝑖), (𝑖𝑚𝑗))))))
Distinct variable group:   𝑖,𝑗,𝑘,𝑚,𝑛,𝑟,𝑣

Detailed syntax breakdown of Definition df-marepv
StepHypRef Expression
1 cmatrepV 21165 . 2 class matRepV
2 vn . . 3 setvar 𝑛
3 vr . . 3 setvar 𝑟
4 cvv 3444 . . 3 class V
5 vm . . . 4 setvar 𝑚
6 vv . . . 4 setvar 𝑣
72cv 1537 . . . . . 6 class 𝑛
83cv 1537 . . . . . 6 class 𝑟
9 cmat 21015 . . . . . 6 class Mat
107, 8, 9co 7139 . . . . 5 class (𝑛 Mat 𝑟)
11 cbs 16478 . . . . 5 class Base
1210, 11cfv 6328 . . . 4 class (Base‘(𝑛 Mat 𝑟))
138, 11cfv 6328 . . . . 5 class (Base‘𝑟)
14 cmap 8393 . . . . 5 class m
1513, 7, 14co 7139 . . . 4 class ((Base‘𝑟) ↑m 𝑛)
16 vk . . . . 5 setvar 𝑘
17 vi . . . . . 6 setvar 𝑖
18 vj . . . . . 6 setvar 𝑗
1918, 16weq 1964 . . . . . . 7 wff 𝑗 = 𝑘
2017cv 1537 . . . . . . . 8 class 𝑖
216cv 1537 . . . . . . . 8 class 𝑣
2220, 21cfv 6328 . . . . . . 7 class (𝑣𝑖)
2318cv 1537 . . . . . . . 8 class 𝑗
245cv 1537 . . . . . . . 8 class 𝑚
2520, 23, 24co 7139 . . . . . . 7 class (𝑖𝑚𝑗)
2619, 22, 25cif 4428 . . . . . 6 class if(𝑗 = 𝑘, (𝑣𝑖), (𝑖𝑚𝑗))
2717, 18, 7, 7, 26cmpo 7141 . . . . 5 class (𝑖𝑛, 𝑗𝑛 ↦ if(𝑗 = 𝑘, (𝑣𝑖), (𝑖𝑚𝑗)))
2816, 7, 27cmpt 5113 . . . 4 class (𝑘𝑛 ↦ (𝑖𝑛, 𝑗𝑛 ↦ if(𝑗 = 𝑘, (𝑣𝑖), (𝑖𝑚𝑗))))
295, 6, 12, 15, 28cmpo 7141 . . 3 class (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)), 𝑣 ∈ ((Base‘𝑟) ↑m 𝑛) ↦ (𝑘𝑛 ↦ (𝑖𝑛, 𝑗𝑛 ↦ if(𝑗 = 𝑘, (𝑣𝑖), (𝑖𝑚𝑗)))))
302, 3, 4, 4, 29cmpo 7141 . 2 class (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)), 𝑣 ∈ ((Base‘𝑟) ↑m 𝑛) ↦ (𝑘𝑛 ↦ (𝑖𝑛, 𝑗𝑛 ↦ if(𝑗 = 𝑘, (𝑣𝑖), (𝑖𝑚𝑗))))))
311, 30wceq 1538 1 wff matRepV = (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)), 𝑣 ∈ ((Base‘𝑟) ↑m 𝑛) ↦ (𝑘𝑛 ↦ (𝑖𝑛, 𝑗𝑛 ↦ if(𝑗 = 𝑘, (𝑣𝑖), (𝑖𝑚𝑗))))))
 Colors of variables: wff setvar class This definition is referenced by:  marepvfval  21173
 Copyright terms: Public domain W3C validator