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 = (1 \dots N) Mat R$
	submat1n.b	$⊢ B = {Base}_{A}$
Assertion	submatres	$⊢ (N \in ℕ \land M \in B) \to N {subMat}_{1} (M) N = {M ↾}_{((1 \dots N - 1) \times (1 \dots N - 1))}$

Proof

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

Metamath Proof Explorer

Theorem submatres

Proof