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 = n ∈ V , r ∈ V ⟼ m ∈ Base n Mat r ⟼ k ∈ n , l ∈ n ⟼ i ∈ n , j ∈ n ⟼ if i = k if j = l 1 r 0 r i m j

Detailed syntax breakdown

Step Hyp Ref Expression
0 cminmar1 class minMatR1
1 vn setvar n
2 cvv class V
3 vr setvar r
4 vm setvar m
5 cbs class Base
6 1 cv setvar n
7 cmat class Mat
8 3 cv setvar r
9 6 8 7 co class n Mat r
10 9 5 cfv class Base n Mat r
11 vk setvar k
12 vl setvar l
13 vi setvar i
14 vj setvar j
15 13 cv setvar i
16 11 cv setvar k
17 15 16 wceq wff i = k
18 14 cv setvar j
19 12 cv setvar l
20 18 19 wceq wff j = l
21 cur class 1 r
22 8 21 cfv class 1 r
23 c0g class 0 𝑔
24 8 23 cfv class 0 r
25 20 22 24 cif class if j = l 1 r 0 r
26 4 cv setvar m
27 15 18 26 co class i m j
28 17 25 27 cif class if i = k if j = l 1 r 0 r i m j
29 13 14 6 6 28 cmpo class i ∈ n , j ∈ n ⟼ if i = k if j = l 1 r 0 r i m j
30 11 12 6 6 29 cmpo class k ∈ n , l ∈ n ⟼ i ∈ n , j ∈ n ⟼ if i = k if j = l 1 r 0 r i m j
31 4 10 30 cmpt class m ∈ Base n Mat r ⟼ k ∈ n , l ∈ n ⟼ i ∈ n , j ∈ n ⟼ if i = k if j = l 1 r 0 r i m j
32 1 3 2 2 31 cmpo class n ∈ V , r ∈ V ⟼ m ∈ Base n Mat r ⟼ k ∈ n , l ∈ n ⟼ i ∈ n , j ∈ n ⟼ if i = k if j = l 1 r 0 r i m j
33 0 32 wceq wff minMatR1 = n ∈ V , r ∈ V ⟼ m ∈ Base n Mat r ⟼ k ∈ n , l ∈ n ⟼ i ∈ n , j ∈ n ⟼ if i = k if j = l 1 r 0 r i m j