Metamath Proof Explorer

Theorem smatcl

Description: Closure of the square submatrix: if M is a square matrix of dimension N with indices in ( 1 ... N ) , then a submatrix of M is of dimension ( N - 1 ) . (Contributed by Thierry Arnoux, 19-Aug-2020)

Ref Expression
Hypotheses smatcl.a ${⊢}{A}=\left(1\dots {N}\right)\mathrm{Mat}{R}$
smatcl.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
smatcl.c ${⊢}{C}={\mathrm{Base}}_{\left(\left(1\dots {N}-1\right)\mathrm{Mat}{R}\right)}$
smatcl.s ${⊢}{S}={K}{\mathrm{subMat}}_{1}\left({M}\right){L}$
smatcl.n ${⊢}{\phi }\to {N}\in ℕ$
smatcl.k ${⊢}{\phi }\to {K}\in \left(1\dots {N}\right)$
smatcl.l ${⊢}{\phi }\to {L}\in \left(1\dots {N}\right)$
smatcl.m ${⊢}{\phi }\to {M}\in {B}$
Assertion smatcl ${⊢}{\phi }\to {S}\in {C}$

Proof

Step Hyp Ref Expression
1 smatcl.a ${⊢}{A}=\left(1\dots {N}\right)\mathrm{Mat}{R}$
2 smatcl.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
3 smatcl.c ${⊢}{C}={\mathrm{Base}}_{\left(\left(1\dots {N}-1\right)\mathrm{Mat}{R}\right)}$
4 smatcl.s ${⊢}{S}={K}{\mathrm{subMat}}_{1}\left({M}\right){L}$
5 smatcl.n ${⊢}{\phi }\to {N}\in ℕ$
6 smatcl.k ${⊢}{\phi }\to {K}\in \left(1\dots {N}\right)$
7 smatcl.l ${⊢}{\phi }\to {L}\in \left(1\dots {N}\right)$
8 smatcl.m ${⊢}{\phi }\to {M}\in {B}$
9 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
10 1 9 2 matbas2i ${⊢}{M}\in {B}\to {M}\in \left({{\mathrm{Base}}_{{R}}}^{\left(\left(1\dots {N}\right)×\left(1\dots {N}\right)\right)}\right)$
11 8 10 syl ${⊢}{\phi }\to {M}\in \left({{\mathrm{Base}}_{{R}}}^{\left(\left(1\dots {N}\right)×\left(1\dots {N}\right)\right)}\right)$
12 4 5 5 6 7 11 smatrcl ${⊢}{\phi }\to {S}\in \left({{\mathrm{Base}}_{{R}}}^{\left(\left(1\dots {N}-1\right)×\left(1\dots {N}-1\right)\right)}\right)$
13 fzfi ${⊢}\left(1\dots {N}-1\right)\in \mathrm{Fin}$
14 1 2 matrcl ${⊢}{M}\in {B}\to \left(\left(1\dots {N}\right)\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)$
15 14 simprd ${⊢}{M}\in {B}\to {R}\in \mathrm{V}$
16 8 15 syl ${⊢}{\phi }\to {R}\in \mathrm{V}$
17 eqid ${⊢}\left(1\dots {N}-1\right)\mathrm{Mat}{R}=\left(1\dots {N}-1\right)\mathrm{Mat}{R}$
18 17 9 matbas2 ${⊢}\left(\left(1\dots {N}-1\right)\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)\to {{\mathrm{Base}}_{{R}}}^{\left(\left(1\dots {N}-1\right)×\left(1\dots {N}-1\right)\right)}={\mathrm{Base}}_{\left(\left(1\dots {N}-1\right)\mathrm{Mat}{R}\right)}$
19 13 16 18 sylancr ${⊢}{\phi }\to {{\mathrm{Base}}_{{R}}}^{\left(\left(1\dots {N}-1\right)×\left(1\dots {N}-1\right)\right)}={\mathrm{Base}}_{\left(\left(1\dots {N}-1\right)\mathrm{Mat}{R}\right)}$
20 19 eleq2d ${⊢}{\phi }\to \left({S}\in \left({{\mathrm{Base}}_{{R}}}^{\left(\left(1\dots {N}-1\right)×\left(1\dots {N}-1\right)\right)}\right)↔{S}\in {\mathrm{Base}}_{\left(\left(1\dots {N}-1\right)\mathrm{Mat}{R}\right)}\right)$
21 12 20 mpbid ${⊢}{\phi }\to {S}\in {\mathrm{Base}}_{\left(\left(1\dots {N}-1\right)\mathrm{Mat}{R}\right)}$
22 21 3 eleqtrrdi ${⊢}{\phi }\to {S}\in {C}$