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 ‘ 𝑟 ) ) , ( 𝑖 𝑚 𝑗 ) ) ) ) ) )