Metamath Proof Explorer

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=n∈V,r∈V⟼m∈BasenMatr⟼k∈n,l∈n⟼i∈n∖k,j∈n∖l⟼imj

Detailed syntax breakdown

Step Hyp Ref Expression
0 csubma classsubMat
1 vn setvarn
2 cvv classV
3 vr setvarr
4 vm setvarm
5 cbs classBase
6 1 cv setvarn
7 cmat classMat
8 3 cv setvarr
9 6 8 7 co classnMatr
10 9 5 cfv classBasenMatr
11 vk setvark
12 vl setvarl
13 vi setvari
14 11 cv setvark
15 14 csn classk
16 6 15 cdif classn∖k
17 vj setvarj
18 12 cv setvarl
19 18 csn classl
20 6 19 cdif classn∖l
21 13 cv setvari
22 4 cv setvarm
23 17 cv setvarj
24 21 23 22 co classimj
25 13 17 16 20 24 cmpo classi∈n∖k,j∈n∖l⟼imj
26 11 12 6 6 25 cmpo classk∈n,l∈n⟼i∈n∖k,j∈n∖l⟼imj
27 4 10 26 cmpt classm∈BasenMatr⟼k∈n,l∈n⟼i∈n∖k,j∈n∖l⟼imj
28 1 3 2 2 27 cmpo classn∈V,r∈V⟼m∈BasenMatr⟼k∈n,l∈n⟼i∈n∖k,j∈n∖l⟼imj
29 0 28 wceq wffsubMat=n∈V,r∈V⟼m∈BasenMatr⟼k∈n,l∈n⟼i∈n∖k,j∈n∖l⟼imj