Definition df-minmar1 21692

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

Step	Hyp	Ref	Expression
1		cminmar1 21690	. 2 class minMatR1
2		vn	. . 3 setvar 𝑛
3		vr	. . 3 setvar 𝑟
4		cvv 3422	. . 3 class V
5		vm	. . . 4 setvar 𝑚
6	2	cv 1538	. . . . . 6 class 𝑛
7	3	cv 1538	. . . . . 6 class 𝑟
8		cmat 21464	. . . . . 6 class Mat
9	6, 7, 8	co 7255	. . . . 5 class (𝑛 Mat 𝑟)
10		cbs 16840	. . . . 5 class Base
11	9, 10	cfv 6418	. . . 4 class (Base‘(𝑛 Mat 𝑟))
12		vk	. . . . 5 setvar 𝑘
13		vl	. . . . 5 setvar 𝑙
14		vi	. . . . . 6 setvar 𝑖
15		vj	. . . . . 6 setvar 𝑗
16	14, 12	weq 1967	. . . . . . 7 wff 𝑖 = 𝑘
17	15, 13	weq 1967	. . . . . . . 8 wff 𝑗 = 𝑙
18		cur 19652	. . . . . . . . 9 class 1r
19	7, 18	cfv 6418	. . . . . . . 8 class (1r‘𝑟)
20		c0g 17067	. . . . . . . . 9 class 0g
21	7, 20	cfv 6418	. . . . . . . 8 class (0g‘𝑟)
22	17, 19, 21	cif 4456	. . . . . . 7 class if(𝑗 = 𝑙, (1r‘𝑟), (0g‘𝑟))
23	14	cv 1538	. . . . . . . 8 class 𝑖
24	15	cv 1538	. . . . . . . 8 class 𝑗
25	5	cv 1538	. . . . . . . 8 class 𝑚
26	23, 24, 25	co 7255	. . . . . . 7 class (𝑖𝑚𝑗)
27	16, 22, 26	cif 4456	. . . . . 6 class if(𝑖 = 𝑘, if(𝑗 = 𝑙, (1r‘𝑟), (0g‘𝑟)), (𝑖𝑚𝑗))
28	14, 15, 6, 6, 27	cmpo 7257	. . . . 5 class (𝑖 ∈ 𝑛, 𝑗 ∈ 𝑛 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, (1r‘𝑟), (0g‘𝑟)), (𝑖𝑚𝑗)))
29	12, 13, 6, 6, 28	cmpo 7257	. . . 4 class (𝑘 ∈ 𝑛, 𝑙 ∈ 𝑛 ↦ (𝑖 ∈ 𝑛, 𝑗 ∈ 𝑛 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, (1r‘𝑟), (0g‘𝑟)), (𝑖𝑚𝑗))))
30	5, 11, 29	cmpt 5153	. . 3 class (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑘 ∈ 𝑛, 𝑙 ∈ 𝑛 ↦ (𝑖 ∈ 𝑛, 𝑗 ∈ 𝑛 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, (1r‘𝑟), (0g‘𝑟)), (𝑖𝑚𝑗)))))
31	2, 3, 4, 4, 30	cmpo 7257	. 2 class (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑘 ∈ 𝑛, 𝑙 ∈ 𝑛 ↦ (𝑖 ∈ 𝑛, 𝑗 ∈ 𝑛 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, (1r‘𝑟), (0g‘𝑟)), (𝑖𝑚𝑗))))))
32	1, 31	wceq 1539	1 wff minMatR1 = (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑘 ∈ 𝑛, 𝑙 ∈ 𝑛 ↦ (𝑖 ∈ 𝑛, 𝑗 ∈ 𝑛 ↦ if(𝑖 = 𝑘, if(𝑗 = 𝑙, (1r‘𝑟), (0g‘𝑟)), (𝑖𝑚𝑗))))))

This definition is referenced by:  minmar1fval  21703