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

Definition df-minmar1 20369
Description: Define the matrices whose determinants are the minors of a square matrix. In contrast to the standard definition of minors, a row is replaced by 0's and one 1 instead of deleting the column and row (e.g., definition in [Lang] p. 515). By this, the determinant of such a matrix is equal to the minor determined in the standard way (as determinant of a submatrix, see df-subma 20311- note that the matrix is transposed compared with the submatrix defined in df-subma 20311, but this does not matter because the determinants are the same, see mdettpos 20345). Such matrices are used in the definition of an adjunct of a square matrix, see df-madu 20368. (Contributed by AV, 27-Dec-2018.)
Assertion
Ref Expression
df-minmar1 minMatR1 = (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑘𝑛, 𝑙𝑛 ↦ (𝑖𝑛, 𝑗𝑛 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, (1r𝑟), (0g𝑟)), (𝑖𝑚𝑗))))))
Distinct variable group:   𝑛,𝑟,𝑚,𝑖,𝑗,𝑘,𝑙

Detailed syntax breakdown of Definition df-minmar1
StepHypRef Expression
1 cminmar1 20367 . 2 class minMatR1
2 vn . . 3 setvar 𝑛
3 vr . . 3 setvar 𝑟
4 cvv 3189 . . 3 class V
5 vm . . . 4 setvar 𝑚
62cv 1479 . . . . . 6 class 𝑛
73cv 1479 . . . . . 6 class 𝑟
8 cmat 20141 . . . . . 6 class Mat
96, 7, 8co 6610 . . . . 5 class (𝑛 Mat 𝑟)
10 cbs 15788 . . . . 5 class Base
119, 10cfv 5852 . . . 4 class (Base‘(𝑛 Mat 𝑟))
12 vk . . . . 5 setvar 𝑘
13 vl . . . . 5 setvar 𝑙
14 vi . . . . . 6 setvar 𝑖
15 vj . . . . . 6 setvar 𝑗
1614, 12weq 1871 . . . . . . 7 wff 𝑖 = 𝑘
1715, 13weq 1871 . . . . . . . 8 wff 𝑗 = 𝑙
18 cur 18429 . . . . . . . . 9 class 1r
197, 18cfv 5852 . . . . . . . 8 class (1r𝑟)
20 c0g 16028 . . . . . . . . 9 class 0g
217, 20cfv 5852 . . . . . . . 8 class (0g𝑟)
2217, 19, 21cif 4063 . . . . . . 7 class if(𝑗 = 𝑙, (1r𝑟), (0g𝑟))
2314cv 1479 . . . . . . . 8 class 𝑖
2415cv 1479 . . . . . . . 8 class 𝑗
255cv 1479 . . . . . . . 8 class 𝑚
2623, 24, 25co 6610 . . . . . . 7 class (𝑖𝑚𝑗)
2716, 22, 26cif 4063 . . . . . 6 class if(𝑖 = 𝑘, if(𝑗 = 𝑙, (1r𝑟), (0g𝑟)), (𝑖𝑚𝑗))
2814, 15, 6, 6, 27cmpt2 6612 . . . . 5 class (𝑖𝑛, 𝑗𝑛 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, (1r𝑟), (0g𝑟)), (𝑖𝑚𝑗)))
2912, 13, 6, 6, 28cmpt2 6612 . . . 4 class (𝑘𝑛, 𝑙𝑛 ↦ (𝑖𝑛, 𝑗𝑛 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, (1r𝑟), (0g𝑟)), (𝑖𝑚𝑗))))
305, 11, 29cmpt 4678 . . 3 class (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑘𝑛, 𝑙𝑛 ↦ (𝑖𝑛, 𝑗𝑛 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, (1r𝑟), (0g𝑟)), (𝑖𝑚𝑗)))))
312, 3, 4, 4, 30cmpt2 6612 . 2 class (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑘𝑛, 𝑙𝑛 ↦ (𝑖𝑛, 𝑗𝑛 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, (1r𝑟), (0g𝑟)), (𝑖𝑚𝑗))))))
321, 31wceq 1480 1 wff minMatR1 = (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑘𝑛, 𝑙𝑛 ↦ (𝑖𝑛, 𝑗𝑛 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, (1r𝑟), (0g𝑟)), (𝑖𝑚𝑗))))))
Colors of variables: wff setvar class
This definition is referenced by:  minmar1fval  20380
  Copyright terms: Public domain W3C validator