# Metamath Proof Explorer

## Definition df-minmar1

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 - note that the matrix is transposed compared with the submatrix defined in df-subma , but this does not matter because the determinants are the same, see mdettpos ). Such matrices are used in the definition of an adjunct of a square matrix, see df-madu . (Contributed by AV, 27-Dec-2018)

Ref Expression
Assertion df-minmar1 minMatR1 = ( 𝑛 ∈ V , 𝑟 ∈ V ↦ ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ↦ ( 𝑘𝑛 , 𝑙𝑛 ↦ ( 𝑖𝑛 , 𝑗𝑛 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , ( 1r𝑟 ) , ( 0g𝑟 ) ) , ( 𝑖 𝑚 𝑗 ) ) ) ) ) )

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cminmar1 minMatR1
1 vn 𝑛
2 cvv V
3 vr 𝑟
4 vm 𝑚
5 cbs Base
6 1 cv 𝑛
7 cmat Mat
8 3 cv 𝑟
9 6 8 7 co ( 𝑛 Mat 𝑟 )
10 9 5 cfv ( Base ‘ ( 𝑛 Mat 𝑟 ) )
11 vk 𝑘
12 vl 𝑙
13 vi 𝑖
14 vj 𝑗
15 13 cv 𝑖
16 11 cv 𝑘
17 15 16 wceq 𝑖 = 𝑘
18 14 cv 𝑗
19 12 cv 𝑙
20 18 19 wceq 𝑗 = 𝑙
21 cur 1r
22 8 21 cfv ( 1r𝑟 )
23 c0g 0g
24 8 23 cfv ( 0g𝑟 )
25 20 22 24 cif if ( 𝑗 = 𝑙 , ( 1r𝑟 ) , ( 0g𝑟 ) )
26 4 cv 𝑚
27 15 18 26 co ( 𝑖 𝑚 𝑗 )
28 17 25 27 cif if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , ( 1r𝑟 ) , ( 0g𝑟 ) ) , ( 𝑖 𝑚 𝑗 ) )
29 13 14 6 6 28 cmpo ( 𝑖𝑛 , 𝑗𝑛 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , ( 1r𝑟 ) , ( 0g𝑟 ) ) , ( 𝑖 𝑚 𝑗 ) ) )
30 11 12 6 6 29 cmpo ( 𝑘𝑛 , 𝑙𝑛 ↦ ( 𝑖𝑛 , 𝑗𝑛 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , ( 1r𝑟 ) , ( 0g𝑟 ) ) , ( 𝑖 𝑚 𝑗 ) ) ) )
31 4 10 30 cmpt ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ↦ ( 𝑘𝑛 , 𝑙𝑛 ↦ ( 𝑖𝑛 , 𝑗𝑛 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , ( 1r𝑟 ) , ( 0g𝑟 ) ) , ( 𝑖 𝑚 𝑗 ) ) ) ) )
32 1 3 2 2 31 cmpo ( 𝑛 ∈ V , 𝑟 ∈ V ↦ ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ↦ ( 𝑘𝑛 , 𝑙𝑛 ↦ ( 𝑖𝑛 , 𝑗𝑛 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , ( 1r𝑟 ) , ( 0g𝑟 ) ) , ( 𝑖 𝑚 𝑗 ) ) ) ) ) )
33 0 32 wceq minMatR1 = ( 𝑛 ∈ V , 𝑟 ∈ V ↦ ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ↦ ( 𝑘𝑛 , 𝑙𝑛 ↦ ( 𝑖𝑛 , 𝑗𝑛 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , ( 1r𝑟 ) , ( 0g𝑟 ) ) , ( 𝑖 𝑚 𝑗 ) ) ) ) ) )