Definition df-smat

Description: Define a function generating submatrices of an integer-indexed matrix. The function maps an index in ( ( 1 ... M ) X. ( 1 ... N ) ) into a new index in ( ( 1 ... ( M - 1 ) ) X. ( 1 ... ( N - 1 ) ) ) . A submatrix is obtained by deleting a row and a column of the original matrix. Because this function re-indexes the matrix, the resulting submatrix still has the same index set for rows and columns, and its determinent is defined, unlike the current df-subma . (Contributed by Thierry Arnoux, 18-Aug-2020)

	Ref	Expression
Assertion	df-smat	⊢ subMat1 = ( 𝑚 ∈ V ↦ ( 𝑘 ∈ ℕ , 𝑙 ∈ ℕ ↦ ( 𝑚 ∘ ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝑘 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝑙 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csmat	⊢ subMat1
1		vm	⊢ 𝑚
2		cvv	⊢ V
3		vk	⊢ 𝑘
4		cn	⊢ ℕ
5		vl	⊢ 𝑙
6	1	cv	⊢ 𝑚
7		vi	⊢ 𝑖
8		vj	⊢ 𝑗
9	7	cv	⊢ 𝑖
10		clt	⊢ <
11	3	cv	⊢ 𝑘
12	9 11 10	wbr	⊢ 𝑖 < 𝑘
13		caddc	⊢ +
14		c1	⊢ 1
15	9 14 13	co	⊢ ( 𝑖 + 1 )
16	12 9 15	cif	⊢ if ( 𝑖 < 𝑘 , 𝑖 , ( 𝑖 + 1 ) )
17	8	cv	⊢ 𝑗
18	5	cv	⊢ 𝑙
19	17 18 10	wbr	⊢ 𝑗 < 𝑙
20	17 14 13	co	⊢ ( 𝑗 + 1 )
21	19 17 20	cif	⊢ if ( 𝑗 < 𝑙 , 𝑗 , ( 𝑗 + 1 ) )
22	16 21	cop	⊢ ⟨ if ( 𝑖 < 𝑘 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝑙 , 𝑗 , ( 𝑗 + 1 ) ) ⟩
23	7 8 4 4 22	cmpo	⊢ ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝑘 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝑙 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ )
24	6 23	ccom	⊢ ( 𝑚 ∘ ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝑘 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝑙 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) )
25	3 5 4 4 24	cmpo	⊢ ( 𝑘 ∈ ℕ , 𝑙 ∈ ℕ ↦ ( 𝑚 ∘ ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝑘 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝑙 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) ) )
26	1 2 25	cmpt	⊢ ( 𝑚 ∈ V ↦ ( 𝑘 ∈ ℕ , 𝑙 ∈ ℕ ↦ ( 𝑚 ∘ ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝑘 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝑙 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) ) ) )
27	0 26	wceq	⊢ subMat1 = ( 𝑚 ∈ V ↦ ( 𝑘 ∈ ℕ , 𝑙 ∈ ℕ ↦ ( 𝑚 ∘ ( 𝑖 ∈ ℕ , 𝑗 ∈ ℕ ↦ ⟨ if ( 𝑖 < 𝑘 , 𝑖 , ( 𝑖 + 1 ) ) , if ( 𝑗 < 𝑙 , 𝑗 , ( 𝑗 + 1 ) ) ⟩ ) ) ) )