# Metamath Proof Explorer

## Theorem submatres

Description: Special case where the submatrix is a restriction of the initial matrix, and no renumbering occurs. (Contributed by Thierry Arnoux, 26-Aug-2020)

Ref Expression
Hypotheses submat1n.a ${⊢}{A}=\left(1\dots {N}\right)\mathrm{Mat}{R}$
submat1n.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
Assertion submatres ${⊢}\left({N}\in ℕ\wedge {M}\in {B}\right)\to {N}{\mathrm{subMat}}_{1}\left({M}\right){N}={{M}↾}_{\left(\left(1\dots {N}-1\right)×\left(1\dots {N}-1\right)\right)}$

### Proof

Step Hyp Ref Expression
1 submat1n.a ${⊢}{A}=\left(1\dots {N}\right)\mathrm{Mat}{R}$
2 submat1n.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
3 1 2 submat1n ${⊢}\left({N}\in ℕ\wedge {M}\in {B}\right)\to {N}{\mathrm{subMat}}_{1}\left({M}\right){N}={N}\left(\left(1\dots {N}\right)\mathrm{subMat}{R}\right)\left({M}\right){N}$
4 simpr ${⊢}\left({N}\in ℕ\wedge {M}\in {B}\right)\to {M}\in {B}$
5 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
6 5 eleq2i ${⊢}{N}\in ℕ↔{N}\in {ℤ}_{\ge 1}$
7 6 biimpi ${⊢}{N}\in ℕ\to {N}\in {ℤ}_{\ge 1}$
8 eluzfz2 ${⊢}{N}\in {ℤ}_{\ge 1}\to {N}\in \left(1\dots {N}\right)$
9 7 8 syl ${⊢}{N}\in ℕ\to {N}\in \left(1\dots {N}\right)$
10 9 adantr ${⊢}\left({N}\in ℕ\wedge {M}\in {B}\right)\to {N}\in \left(1\dots {N}\right)$
11 eqid ${⊢}\left(1\dots {N}\right)\mathrm{subMat}{R}=\left(1\dots {N}\right)\mathrm{subMat}{R}$
12 1 11 2 submaval ${⊢}\left({M}\in {B}\wedge {N}\in \left(1\dots {N}\right)\wedge {N}\in \left(1\dots {N}\right)\right)\to {N}\left(\left(1\dots {N}\right)\mathrm{subMat}{R}\right)\left({M}\right){N}=\left({i}\in \left(\left(1\dots {N}\right)\setminus \left\{{N}\right\}\right),{j}\in \left(\left(1\dots {N}\right)\setminus \left\{{N}\right\}\right)⟼{i}{M}{j}\right)$
13 4 10 10 12 syl3anc ${⊢}\left({N}\in ℕ\wedge {M}\in {B}\right)\to {N}\left(\left(1\dots {N}\right)\mathrm{subMat}{R}\right)\left({M}\right){N}=\left({i}\in \left(\left(1\dots {N}\right)\setminus \left\{{N}\right\}\right),{j}\in \left(\left(1\dots {N}\right)\setminus \left\{{N}\right\}\right)⟼{i}{M}{j}\right)$
14 fzdif2 ${⊢}{N}\in {ℤ}_{\ge 1}\to \left(1\dots {N}\right)\setminus \left\{{N}\right\}=\left(1\dots {N}-1\right)$
15 7 14 syl ${⊢}{N}\in ℕ\to \left(1\dots {N}\right)\setminus \left\{{N}\right\}=\left(1\dots {N}-1\right)$
16 difss ${⊢}\left(1\dots {N}\right)\setminus \left\{{N}\right\}\subseteq \left(1\dots {N}\right)$
17 15 16 eqsstrrdi ${⊢}{N}\in ℕ\to \left(1\dots {N}-1\right)\subseteq \left(1\dots {N}\right)$
18 17 adantr ${⊢}\left({N}\in ℕ\wedge {M}\in {B}\right)\to \left(1\dots {N}-1\right)\subseteq \left(1\dots {N}\right)$
19 resmpo ${⊢}\left(\left(1\dots {N}-1\right)\subseteq \left(1\dots {N}\right)\wedge \left(1\dots {N}-1\right)\subseteq \left(1\dots {N}\right)\right)\to {\left({i}\in \left(1\dots {N}\right),{j}\in \left(1\dots {N}\right)⟼{i}{M}{j}\right)↾}_{\left(\left(1\dots {N}-1\right)×\left(1\dots {N}-1\right)\right)}=\left({i}\in \left(1\dots {N}-1\right),{j}\in \left(1\dots {N}-1\right)⟼{i}{M}{j}\right)$
20 18 18 19 syl2anc ${⊢}\left({N}\in ℕ\wedge {M}\in {B}\right)\to {\left({i}\in \left(1\dots {N}\right),{j}\in \left(1\dots {N}\right)⟼{i}{M}{j}\right)↾}_{\left(\left(1\dots {N}-1\right)×\left(1\dots {N}-1\right)\right)}=\left({i}\in \left(1\dots {N}-1\right),{j}\in \left(1\dots {N}-1\right)⟼{i}{M}{j}\right)$
21 1 2 matmpo ${⊢}{M}\in {B}\to {M}=\left({i}\in \left(1\dots {N}\right),{j}\in \left(1\dots {N}\right)⟼{i}{M}{j}\right)$
22 21 reseq1d ${⊢}{M}\in {B}\to {{M}↾}_{\left(\left(1\dots {N}-1\right)×\left(1\dots {N}-1\right)\right)}={\left({i}\in \left(1\dots {N}\right),{j}\in \left(1\dots {N}\right)⟼{i}{M}{j}\right)↾}_{\left(\left(1\dots {N}-1\right)×\left(1\dots {N}-1\right)\right)}$
23 22 adantl ${⊢}\left({N}\in ℕ\wedge {M}\in {B}\right)\to {{M}↾}_{\left(\left(1\dots {N}-1\right)×\left(1\dots {N}-1\right)\right)}={\left({i}\in \left(1\dots {N}\right),{j}\in \left(1\dots {N}\right)⟼{i}{M}{j}\right)↾}_{\left(\left(1\dots {N}-1\right)×\left(1\dots {N}-1\right)\right)}$
24 15 adantr ${⊢}\left({N}\in ℕ\wedge {M}\in {B}\right)\to \left(1\dots {N}\right)\setminus \left\{{N}\right\}=\left(1\dots {N}-1\right)$
25 eqidd ${⊢}\left({N}\in ℕ\wedge {M}\in {B}\right)\to {i}{M}{j}={i}{M}{j}$
26 24 24 25 mpoeq123dv ${⊢}\left({N}\in ℕ\wedge {M}\in {B}\right)\to \left({i}\in \left(\left(1\dots {N}\right)\setminus \left\{{N}\right\}\right),{j}\in \left(\left(1\dots {N}\right)\setminus \left\{{N}\right\}\right)⟼{i}{M}{j}\right)=\left({i}\in \left(1\dots {N}-1\right),{j}\in \left(1\dots {N}-1\right)⟼{i}{M}{j}\right)$
27 20 23 26 3eqtr4rd ${⊢}\left({N}\in ℕ\wedge {M}\in {B}\right)\to \left({i}\in \left(\left(1\dots {N}\right)\setminus \left\{{N}\right\}\right),{j}\in \left(\left(1\dots {N}\right)\setminus \left\{{N}\right\}\right)⟼{i}{M}{j}\right)={{M}↾}_{\left(\left(1\dots {N}-1\right)×\left(1\dots {N}-1\right)\right)}$
28 3 13 27 3eqtrd ${⊢}\left({N}\in ℕ\wedge {M}\in {B}\right)\to {N}{\mathrm{subMat}}_{1}\left({M}\right){N}={{M}↾}_{\left(\left(1\dots {N}-1\right)×\left(1\dots {N}-1\right)\right)}$