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

Definition df-marrep 20121
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.)
Assertion
Ref Expression
df-marrep matRRep = (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)), 𝑠 ∈ (Base‘𝑟) ↦ (𝑘𝑛, 𝑙𝑛 ↦ (𝑖𝑛, 𝑗𝑛 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 𝑠, (0g𝑟)), (𝑖𝑚𝑗))))))
Distinct variable group:   𝑛,𝑟,𝑚,𝑖,𝑗,𝑘,𝑙,𝑠

Detailed syntax breakdown of Definition df-marrep
StepHypRef Expression
1 cmarrep 20119 . 2 class matRRep
2 vn . . 3 setvar 𝑛
3 vr . . 3 setvar 𝑟
4 cvv 3168 . . 3 class V
5 vm . . . 4 setvar 𝑚
6 vs . . . 4 setvar 𝑠
72cv 1473 . . . . . 6 class 𝑛
83cv 1473 . . . . . 6 class 𝑟
9 cmat 19970 . . . . . 6 class Mat
107, 8, 9co 6523 . . . . 5 class (𝑛 Mat 𝑟)
11 cbs 15637 . . . . 5 class Base
1210, 11cfv 5786 . . . 4 class (Base‘(𝑛 Mat 𝑟))
138, 11cfv 5786 . . . 4 class (Base‘𝑟)
14 vk . . . . 5 setvar 𝑘
15 vl . . . . 5 setvar 𝑙
16 vi . . . . . 6 setvar 𝑖
17 vj . . . . . 6 setvar 𝑗
1816, 14weq 1859 . . . . . . 7 wff 𝑖 = 𝑘
1917, 15weq 1859 . . . . . . . 8 wff 𝑗 = 𝑙
206cv 1473 . . . . . . . 8 class 𝑠
21 c0g 15865 . . . . . . . . 9 class 0g
228, 21cfv 5786 . . . . . . . 8 class (0g𝑟)
2319, 20, 22cif 4031 . . . . . . 7 class if(𝑗 = 𝑙, 𝑠, (0g𝑟))
2416cv 1473 . . . . . . . 8 class 𝑖
2517cv 1473 . . . . . . . 8 class 𝑗
265cv 1473 . . . . . . . 8 class 𝑚
2724, 25, 26co 6523 . . . . . . 7 class (𝑖𝑚𝑗)
2818, 23, 27cif 4031 . . . . . 6 class if(𝑖 = 𝑘, if(𝑗 = 𝑙, 𝑠, (0g𝑟)), (𝑖𝑚𝑗))
2916, 17, 7, 7, 28cmpt2 6525 . . . . 5 class (𝑖𝑛, 𝑗𝑛 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 𝑠, (0g𝑟)), (𝑖𝑚𝑗)))
3014, 15, 7, 7, 29cmpt2 6525 . . . 4 class (𝑘𝑛, 𝑙𝑛 ↦ (𝑖𝑛, 𝑗𝑛 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 𝑠, (0g𝑟)), (𝑖𝑚𝑗))))
315, 6, 12, 13, 30cmpt2 6525 . . 3 class (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)), 𝑠 ∈ (Base‘𝑟) ↦ (𝑘𝑛, 𝑙𝑛 ↦ (𝑖𝑛, 𝑗𝑛 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 𝑠, (0g𝑟)), (𝑖𝑚𝑗)))))
322, 3, 4, 4, 31cmpt2 6525 . 2 class (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)), 𝑠 ∈ (Base‘𝑟) ↦ (𝑘𝑛, 𝑙𝑛 ↦ (𝑖𝑛, 𝑗𝑛 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 𝑠, (0g𝑟)), (𝑖𝑚𝑗))))))
331, 32wceq 1474 1 wff matRRep = (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)), 𝑠 ∈ (Base‘𝑟) ↦ (𝑘𝑛, 𝑙𝑛 ↦ (𝑖𝑛, 𝑗𝑛 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, 𝑠, (0g𝑟)), (𝑖𝑚𝑗))))))
Colors of variables: wff setvar class
This definition is referenced by:  marrepfval  20123
  Copyright terms: Public domain W3C validator