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 = (1 \dots N) Mat R$
	smatcl.b	$⊢ B = {Base}_{A}$
	smatcl.c	$⊢ C = {Base}_{((1 \dots N - 1) Mat R)}$
	smatcl.s	$⊢ S = K {subMat}_{1} (M) L$
	smatcl.n	$⊢ φ \to N \in ℕ$
	smatcl.k	$⊢ φ \to K \in (1 \dots N)$
	smatcl.l	$⊢ φ \to L \in (1 \dots N)$
	smatcl.m	$⊢ φ \to M \in B$
Assertion	smatcl	$⊢ φ \to S \in C$

Proof

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

Metamath Proof Explorer

Theorem smatcl

Proof