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 ${⊢}\mathrm{minMatR1}=\left({n}\in \mathrm{V},{r}\in \mathrm{V}⟼\left({m}\in {\mathrm{Base}}_{\left({n}\mathrm{Mat}{r}\right)}⟼\left({k}\in {n},{l}\in {n}⟼\left({i}\in {n},{j}\in {n}⟼if\left({i}={k},if\left({j}={l},{1}_{{r}},{0}_{{r}}\right),{i}{m}{j}\right)\right)\right)\right)\right)$

Detailed syntax breakdown

Step Hyp Ref Expression
0 cminmar1 ${class}\mathrm{minMatR1}$
1 vn ${setvar}{n}$
2 cvv ${class}\mathrm{V}$
3 vr ${setvar}{r}$
4 vm ${setvar}{m}$
5 cbs ${class}\mathrm{Base}$
6 1 cv ${setvar}{n}$
7 cmat ${class}\mathrm{Mat}$
8 3 cv ${setvar}{r}$
9 6 8 7 co ${class}\left({n}\mathrm{Mat}{r}\right)$
10 9 5 cfv ${class}{\mathrm{Base}}_{\left({n}\mathrm{Mat}{r}\right)}$
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\left({j}={l},{1}_{{r}},{0}_{{r}}\right)$
26 4 cv ${setvar}{m}$
27 15 18 26 co ${class}\left({i}{m}{j}\right)$
28 17 25 27 cif ${class}if\left({i}={k},if\left({j}={l},{1}_{{r}},{0}_{{r}}\right),{i}{m}{j}\right)$
29 13 14 6 6 28 cmpo ${class}\left({i}\in {n},{j}\in {n}⟼if\left({i}={k},if\left({j}={l},{1}_{{r}},{0}_{{r}}\right),{i}{m}{j}\right)\right)$
30 11 12 6 6 29 cmpo ${class}\left({k}\in {n},{l}\in {n}⟼\left({i}\in {n},{j}\in {n}⟼if\left({i}={k},if\left({j}={l},{1}_{{r}},{0}_{{r}}\right),{i}{m}{j}\right)\right)\right)$
31 4 10 30 cmpt ${class}\left({m}\in {\mathrm{Base}}_{\left({n}\mathrm{Mat}{r}\right)}⟼\left({k}\in {n},{l}\in {n}⟼\left({i}\in {n},{j}\in {n}⟼if\left({i}={k},if\left({j}={l},{1}_{{r}},{0}_{{r}}\right),{i}{m}{j}\right)\right)\right)\right)$
32 1 3 2 2 31 cmpo ${class}\left({n}\in \mathrm{V},{r}\in \mathrm{V}⟼\left({m}\in {\mathrm{Base}}_{\left({n}\mathrm{Mat}{r}\right)}⟼\left({k}\in {n},{l}\in {n}⟼\left({i}\in {n},{j}\in {n}⟼if\left({i}={k},if\left({j}={l},{1}_{{r}},{0}_{{r}}\right),{i}{m}{j}\right)\right)\right)\right)\right)$
33 0 32 wceq ${wff}\mathrm{minMatR1}=\left({n}\in \mathrm{V},{r}\in \mathrm{V}⟼\left({m}\in {\mathrm{Base}}_{\left({n}\mathrm{Mat}{r}\right)}⟼\left({k}\in {n},{l}\in {n}⟼\left({i}\in {n},{j}\in {n}⟼if\left({i}={k},if\left({j}={l},{1}_{{r}},{0}_{{r}}\right),{i}{m}{j}\right)\right)\right)\right)\right)$