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

Proof

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

Metamath Proof Explorer

Theorem submat1n

Proof