# Metamath Proof Explorer

## Theorem submat1n

Description: One case where the submatrix with integer indices, subMat1 , and the general submatrix subMat , agree. (Contributed by Thierry Arnoux, 22-Aug-2020)

Ref Expression
Hypotheses submat1n.a ${⊢}{A}=\left(1\dots {N}\right)\mathrm{Mat}{R}$
submat1n.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
Assertion 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}$

### 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 fzdif2 ${⊢}{N}\in {ℤ}_{\ge 1}\to \left(1\dots {N}\right)\setminus \left\{{N}\right\}=\left(1\dots {N}-1\right)$
4 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
5 3 4 eleq2s ${⊢}{N}\in ℕ\to \left(1\dots {N}\right)\setminus \left\{{N}\right\}=\left(1\dots {N}-1\right)$
6 5 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)$
7 6 adantr ${⊢}\left(\left({N}\in ℕ\wedge {M}\in {B}\right)\wedge {i}\in \left(\left(1\dots {N}\right)\setminus \left\{{N}\right\}\right)\right)\to \left(1\dots {N}\right)\setminus \left\{{N}\right\}=\left(1\dots {N}-1\right)$
8 eqid ${⊢}{N}{\mathrm{subMat}}_{1}\left({M}\right){N}={N}{\mathrm{subMat}}_{1}\left({M}\right){N}$
9 elfz1end ${⊢}{N}\in ℕ↔{N}\in \left(1\dots {N}\right)$
10 9 biimpi ${⊢}{N}\in ℕ\to {N}\in \left(1\dots {N}\right)$
11 10 adantr ${⊢}\left({N}\in ℕ\wedge {M}\in {B}\right)\to {N}\in \left(1\dots {N}\right)$
12 11 9 sylibr ${⊢}\left({N}\in ℕ\wedge {M}\in {B}\right)\to {N}\in ℕ$
13 12 adantr ${⊢}\left(\left({N}\in ℕ\wedge {M}\in {B}\right)\wedge \left({i}\in \left(\left(1\dots {N}\right)\setminus \left\{{N}\right\}\right)\wedge {j}\in \left(\left(1\dots {N}\right)\setminus \left\{{N}\right\}\right)\right)\right)\to {N}\in ℕ$
14 13 10 syl ${⊢}\left(\left({N}\in ℕ\wedge {M}\in {B}\right)\wedge \left({i}\in \left(\left(1\dots {N}\right)\setminus \left\{{N}\right\}\right)\wedge {j}\in \left(\left(1\dots {N}\right)\setminus \left\{{N}\right\}\right)\right)\right)\to {N}\in \left(1\dots {N}\right)$
15 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
16 1 15 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)$
17 16 ad2antlr ${⊢}\left(\left({N}\in ℕ\wedge {M}\in {B}\right)\wedge \left({i}\in \left(\left(1\dots {N}\right)\setminus \left\{{N}\right\}\right)\wedge {j}\in \left(\left(1\dots {N}\right)\setminus \left\{{N}\right\}\right)\right)\right)\to {M}\in \left({{\mathrm{Base}}_{{R}}}^{\left(\left(1\dots {N}\right)×\left(1\dots {N}\right)\right)}\right)$
18 simprl ${⊢}\left(\left({N}\in ℕ\wedge {M}\in {B}\right)\wedge \left({i}\in \left(\left(1\dots {N}\right)\setminus \left\{{N}\right\}\right)\wedge {j}\in \left(\left(1\dots {N}\right)\setminus \left\{{N}\right\}\right)\right)\right)\to {i}\in \left(\left(1\dots {N}\right)\setminus \left\{{N}\right\}\right)$
19 nnz ${⊢}{N}\in ℕ\to {N}\in ℤ$
20 fzoval ${⊢}{N}\in ℤ\to \left(1..^{N}\right)=\left(1\dots {N}-1\right)$
21 19 20 syl ${⊢}{N}\in ℕ\to \left(1..^{N}\right)=\left(1\dots {N}-1\right)$
22 21 5 eqtr4d ${⊢}{N}\in ℕ\to \left(1..^{N}\right)=\left(1\dots {N}\right)\setminus \left\{{N}\right\}$
23 13 22 syl ${⊢}\left(\left({N}\in ℕ\wedge {M}\in {B}\right)\wedge \left({i}\in \left(\left(1\dots {N}\right)\setminus \left\{{N}\right\}\right)\wedge {j}\in \left(\left(1\dots {N}\right)\setminus \left\{{N}\right\}\right)\right)\right)\to \left(1..^{N}\right)=\left(1\dots {N}\right)\setminus \left\{{N}\right\}$
24 18 23 eleqtrrd ${⊢}\left(\left({N}\in ℕ\wedge {M}\in {B}\right)\wedge \left({i}\in \left(\left(1\dots {N}\right)\setminus \left\{{N}\right\}\right)\wedge {j}\in \left(\left(1\dots {N}\right)\setminus \left\{{N}\right\}\right)\right)\right)\to {i}\in \left(1..^{N}\right)$
25 simprr ${⊢}\left(\left({N}\in ℕ\wedge {M}\in {B}\right)\wedge \left({i}\in \left(\left(1\dots {N}\right)\setminus \left\{{N}\right\}\right)\wedge {j}\in \left(\left(1\dots {N}\right)\setminus \left\{{N}\right\}\right)\right)\right)\to {j}\in \left(\left(1\dots {N}\right)\setminus \left\{{N}\right\}\right)$
26 25 23 eleqtrrd ${⊢}\left(\left({N}\in ℕ\wedge {M}\in {B}\right)\wedge \left({i}\in \left(\left(1\dots {N}\right)\setminus \left\{{N}\right\}\right)\wedge {j}\in \left(\left(1\dots {N}\right)\setminus \left\{{N}\right\}\right)\right)\right)\to {j}\in \left(1..^{N}\right)$
27 8 13 13 14 14 17 24 26 smattl ${⊢}\left(\left({N}\in ℕ\wedge {M}\in {B}\right)\wedge \left({i}\in \left(\left(1\dots {N}\right)\setminus \left\{{N}\right\}\right)\wedge {j}\in \left(\left(1\dots {N}\right)\setminus \left\{{N}\right\}\right)\right)\right)\to {i}\left({N}{\mathrm{subMat}}_{1}\left({M}\right){N}\right){j}={i}{M}{j}$
28 27 eqcomd ${⊢}\left(\left({N}\in ℕ\wedge {M}\in {B}\right)\wedge \left({i}\in \left(\left(1\dots {N}\right)\setminus \left\{{N}\right\}\right)\wedge {j}\in \left(\left(1\dots {N}\right)\setminus \left\{{N}\right\}\right)\right)\right)\to {i}{M}{j}={i}\left({N}{\mathrm{subMat}}_{1}\left({M}\right){N}\right){j}$
29 6 7 28 mpoeq123dva ${⊢}\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}\left({N}{\mathrm{subMat}}_{1}\left({M}\right){N}\right){j}\right)$
30 simpr ${⊢}\left({N}\in ℕ\wedge {M}\in {B}\right)\to {M}\in {B}$
31 eqid ${⊢}\left(1\dots {N}\right)\mathrm{subMat}{R}=\left(1\dots {N}\right)\mathrm{subMat}{R}$
32 1 31 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)$
33 30 11 11 32 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)$
34 eqid ${⊢}{\mathrm{Base}}_{\left(\left(1\dots {N}-1\right)\mathrm{Mat}{R}\right)}={\mathrm{Base}}_{\left(\left(1\dots {N}-1\right)\mathrm{Mat}{R}\right)}$
35 1 2 34 8 12 11 11 30 smatcl ${⊢}\left({N}\in ℕ\wedge {M}\in {B}\right)\to {N}{\mathrm{subMat}}_{1}\left({M}\right){N}\in {\mathrm{Base}}_{\left(\left(1\dots {N}-1\right)\mathrm{Mat}{R}\right)}$
36 eqid ${⊢}\left(1\dots {N}-1\right)\mathrm{Mat}{R}=\left(1\dots {N}-1\right)\mathrm{Mat}{R}$
37 36 34 matmpo ${⊢}{N}{\mathrm{subMat}}_{1}\left({M}\right){N}\in {\mathrm{Base}}_{\left(\left(1\dots {N}-1\right)\mathrm{Mat}{R}\right)}\to {N}{\mathrm{subMat}}_{1}\left({M}\right){N}=\left({i}\in \left(1\dots {N}-1\right),{j}\in \left(1\dots {N}-1\right)⟼{i}\left({N}{\mathrm{subMat}}_{1}\left({M}\right){N}\right){j}\right)$
38 35 37 syl ${⊢}\left({N}\in ℕ\wedge {M}\in {B}\right)\to {N}{\mathrm{subMat}}_{1}\left({M}\right){N}=\left({i}\in \left(1\dots {N}-1\right),{j}\in \left(1\dots {N}-1\right)⟼{i}\left({N}{\mathrm{subMat}}_{1}\left({M}\right){N}\right){j}\right)$
39 29 33 38 3eqtr4rd ${⊢}\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}$