Definition df-subma 22604

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.)

Assertion

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

Distinct variable group:   𝑛,𝑟,𝑚,𝑖,𝑗,𝑘,𝑙

Detailed syntax breakdown of Definition df-subma

Step	Hyp	Ref	Expression
1		csubma 22603	. 2 class subMat
2		vn	. . 3 setvar 𝑛
3		vr	. . 3 setvar 𝑟
4		cvv 3488	. . 3 class V
5		vm	. . . 4 setvar 𝑚
6	2	cv 1536	. . . . . 6 class 𝑛
7	3	cv 1536	. . . . . 6 class 𝑟
8		cmat 22432	. . . . . 6 class Mat
9	6, 7, 8	co 7448	. . . . 5 class (𝑛 Mat 𝑟)
10		cbs 17258	. . . . 5 class Base
11	9, 10	cfv 6573	. . . 4 class (Base‘(𝑛 Mat 𝑟))
12		vk	. . . . 5 setvar 𝑘
13		vl	. . . . 5 setvar 𝑙
14		vi	. . . . . 6 setvar 𝑖
15		vj	. . . . . 6 setvar 𝑗
16	12	cv 1536	. . . . . . . 8 class 𝑘
17	16	csn 4648	. . . . . . 7 class {𝑘}
18	6, 17	cdif 3973	. . . . . 6 class (𝑛 ∖ {𝑘})
19	13	cv 1536	. . . . . . . 8 class 𝑙
20	19	csn 4648	. . . . . . 7 class {𝑙}
21	6, 20	cdif 3973	. . . . . 6 class (𝑛 ∖ {𝑙})
22	14	cv 1536	. . . . . . 7 class 𝑖
23	15	cv 1536	. . . . . . 7 class 𝑗
24	5	cv 1536	. . . . . . 7 class 𝑚
25	22, 23, 24	co 7448	. . . . . 6 class (𝑖𝑚𝑗)
26	14, 15, 18, 21, 25	cmpo 7450	. . . . 5 class (𝑖 ∈ (𝑛 ∖ {𝑘}), 𝑗 ∈ (𝑛 ∖ {𝑙}) ↦ (𝑖𝑚𝑗))
27	12, 13, 6, 6, 26	cmpo 7450	. . . 4 class (𝑘 ∈ 𝑛, 𝑙 ∈ 𝑛 ↦ (𝑖 ∈ (𝑛 ∖ {𝑘}), 𝑗 ∈ (𝑛 ∖ {𝑙}) ↦ (𝑖𝑚𝑗)))
28	5, 11, 27	cmpt 5249	. . 3 class (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑘 ∈ 𝑛, 𝑙 ∈ 𝑛 ↦ (𝑖 ∈ (𝑛 ∖ {𝑘}), 𝑗 ∈ (𝑛 ∖ {𝑙}) ↦ (𝑖𝑚𝑗))))
29	2, 3, 4, 4, 28	cmpo 7450	. 2 class (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑘 ∈ 𝑛, 𝑙 ∈ 𝑛 ↦ (𝑖 ∈ (𝑛 ∖ {𝑘}), 𝑗 ∈ (𝑛 ∖ {𝑙}) ↦ (𝑖𝑚𝑗)))))
30	1, 29	wceq 1537	1 wff subMat = (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑘 ∈ 𝑛, 𝑙 ∈ 𝑛 ↦ (𝑖 ∈ (𝑛 ∖ {𝑘}), 𝑗 ∈ (𝑛 ∖ {𝑙}) ↦ (𝑖𝑚𝑗)))))

This definition is referenced by:  submafval  22606