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

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

Detailed syntax breakdown of Definition df-marepv
StepHypRef Expression
1 cmatrepV 20581 . 2 class matRepV
2 vn . . 3 setvar 𝑛
3 vr . . 3 setvar 𝑟
4 cvv 3351 . . 3 class V
5 vm . . . 4 setvar 𝑚
6 vv . . . 4 setvar 𝑣
72cv 1630 . . . . . 6 class 𝑛
83cv 1630 . . . . . 6 class 𝑟
9 cmat 20430 . . . . . 6 class Mat
107, 8, 9co 6793 . . . . 5 class (𝑛 Mat 𝑟)
11 cbs 16064 . . . . 5 class Base
1210, 11cfv 6031 . . . 4 class (Base‘(𝑛 Mat 𝑟))
138, 11cfv 6031 . . . . 5 class (Base‘𝑟)
14 cmap 8009 . . . . 5 class 𝑚
1513, 7, 14co 6793 . . . 4 class ((Base‘𝑟) ↑𝑚 𝑛)
16 vk . . . . 5 setvar 𝑘
17 vi . . . . . 6 setvar 𝑖
18 vj . . . . . 6 setvar 𝑗
1918, 16weq 2043 . . . . . . 7 wff 𝑗 = 𝑘
2017cv 1630 . . . . . . . 8 class 𝑖
216cv 1630 . . . . . . . 8 class 𝑣
2220, 21cfv 6031 . . . . . . 7 class (𝑣𝑖)
2318cv 1630 . . . . . . . 8 class 𝑗
245cv 1630 . . . . . . . 8 class 𝑚
2520, 23, 24co 6793 . . . . . . 7 class (𝑖𝑚𝑗)
2619, 22, 25cif 4225 . . . . . 6 class if(𝑗 = 𝑘, (𝑣𝑖), (𝑖𝑚𝑗))
2717, 18, 7, 7, 26cmpt2 6795 . . . . 5 class (𝑖𝑛, 𝑗𝑛 ↦ if(𝑗 = 𝑘, (𝑣𝑖), (𝑖𝑚𝑗)))
2816, 7, 27cmpt 4863 . . . 4 class (𝑘𝑛 ↦ (𝑖𝑛, 𝑗𝑛 ↦ if(𝑗 = 𝑘, (𝑣𝑖), (𝑖𝑚𝑗))))
295, 6, 12, 15, 28cmpt2 6795 . . 3 class (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)), 𝑣 ∈ ((Base‘𝑟) ↑𝑚 𝑛) ↦ (𝑘𝑛 ↦ (𝑖𝑛, 𝑗𝑛 ↦ if(𝑗 = 𝑘, (𝑣𝑖), (𝑖𝑚𝑗)))))
302, 3, 4, 4, 29cmpt2 6795 . 2 class (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)), 𝑣 ∈ ((Base‘𝑟) ↑𝑚 𝑛) ↦ (𝑘𝑛 ↦ (𝑖𝑛, 𝑗𝑛 ↦ if(𝑗 = 𝑘, (𝑣𝑖), (𝑖𝑚𝑗))))))
311, 30wceq 1631 1 wff matRepV = (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)), 𝑣 ∈ ((Base‘𝑟) ↑𝑚 𝑛) ↦ (𝑘𝑛 ↦ (𝑖𝑛, 𝑗𝑛 ↦ if(𝑗 = 𝑘, (𝑣𝑖), (𝑖𝑚𝑗))))))
Colors of variables: wff setvar class
This definition is referenced by:  marepvfval  20589
  Copyright terms: Public domain W3C validator