Definition df-subma

Description: Define the submatrices of a square matrix. A submatrix is obtained by deleting a row and a column of the original matrix. Since the indices of a matrix need not to be sequential integers, it does not matter that there may be gaps in the numbering of the indices for the submatrix. The determinants of such submatrices are called the "minors" of the original matrix. (Contributed by AV, 27-Dec-2018)

	Ref	Expression
Assertion	df-subma	⊢ subMat = ( 𝑛 ∈ V , 𝑟 ∈ V ↦ ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ↦ ( 𝑘 ∈ 𝑛 , 𝑙 ∈ 𝑛 ↦ ( 𝑖 ∈ ( 𝑛 ∖ { 𝑘 } ) , 𝑗 ∈ ( 𝑛 ∖ { 𝑙 } ) ↦ ( 𝑖 𝑚 𝑗 ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csubma	⊢ subMat
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	11	cv	⊢ 𝑘
15	14	csn	⊢ { 𝑘 }
16	6 15	cdif	⊢ ( 𝑛 ∖ { 𝑘 } )
17		vj	⊢ 𝑗
18	12	cv	⊢ 𝑙
19	18	csn	⊢ { 𝑙 }
20	6 19	cdif	⊢ ( 𝑛 ∖ { 𝑙 } )
21	13	cv	⊢ 𝑖
22	4	cv	⊢ 𝑚
23	17	cv	⊢ 𝑗
24	21 23 22	co	⊢ ( 𝑖 𝑚 𝑗 )
25	13 17 16 20 24	cmpo	⊢ ( 𝑖 ∈ ( 𝑛 ∖ { 𝑘 } ) , 𝑗 ∈ ( 𝑛 ∖ { 𝑙 } ) ↦ ( 𝑖 𝑚 𝑗 ) )
26	11 12 6 6 25	cmpo	⊢ ( 𝑘 ∈ 𝑛 , 𝑙 ∈ 𝑛 ↦ ( 𝑖 ∈ ( 𝑛 ∖ { 𝑘 } ) , 𝑗 ∈ ( 𝑛 ∖ { 𝑙 } ) ↦ ( 𝑖 𝑚 𝑗 ) ) )
27	4 10 26	cmpt	⊢ ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ↦ ( 𝑘 ∈ 𝑛 , 𝑙 ∈ 𝑛 ↦ ( 𝑖 ∈ ( 𝑛 ∖ { 𝑘 } ) , 𝑗 ∈ ( 𝑛 ∖ { 𝑙 } ) ↦ ( 𝑖 𝑚 𝑗 ) ) ) )
28	1 3 2 2 27	cmpo	⊢ ( 𝑛 ∈ V , 𝑟 ∈ V ↦ ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ↦ ( 𝑘 ∈ 𝑛 , 𝑙 ∈ 𝑛 ↦ ( 𝑖 ∈ ( 𝑛 ∖ { 𝑘 } ) , 𝑗 ∈ ( 𝑛 ∖ { 𝑙 } ) ↦ ( 𝑖 𝑚 𝑗 ) ) ) ) )
29	0 28	wceq	⊢ subMat = ( 𝑛 ∈ V , 𝑟 ∈ V ↦ ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ↦ ( 𝑘 ∈ 𝑛 , 𝑙 ∈ 𝑛 ↦ ( 𝑖 ∈ ( 𝑛 ∖ { 𝑘 } ) , 𝑗 ∈ ( 𝑛 ∖ { 𝑙 } ) ↦ ( 𝑖 𝑚 𝑗 ) ) ) ) )