Theorem 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	⊢ 𝐴 = ( ( 1 ... 𝑁 ) Mat 𝑅 )
	smatcl.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	smatcl.c	⊢ 𝐶 = ( Base ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) )
	smatcl.s	⊢ 𝑆 = ( 𝐾 ( subMat1 ‘ 𝑀 ) 𝐿 )
	smatcl.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	smatcl.k	⊢ ( 𝜑 → 𝐾 ∈ ( 1 ... 𝑁 ) )
	smatcl.l	⊢ ( 𝜑 → 𝐿 ∈ ( 1 ... 𝑁 ) )
	smatcl.m	⊢ ( 𝜑 → 𝑀 ∈ 𝐵 )
Assertion	smatcl	⊢ ( 𝜑 → 𝑆 ∈ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		smatcl.a	⊢ 𝐴 = ( ( 1 ... 𝑁 ) Mat 𝑅 )
2		smatcl.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		smatcl.c	⊢ 𝐶 = ( Base ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) )
4		smatcl.s	⊢ 𝑆 = ( 𝐾 ( subMat1 ‘ 𝑀 ) 𝐿 )
5		smatcl.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
6		smatcl.k	⊢ ( 𝜑 → 𝐾 ∈ ( 1 ... 𝑁 ) )
7		smatcl.l	⊢ ( 𝜑 → 𝐿 ∈ ( 1 ... 𝑁 ) )
8		smatcl.m	⊢ ( 𝜑 → 𝑀 ∈ 𝐵 )
9		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
10	1 9 2	matbas2i	⊢ ( 𝑀 ∈ 𝐵 → 𝑀 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ( 1 ... 𝑁 ) × ( 1 ... 𝑁 ) ) ) )
11	8 10	syl	⊢ ( 𝜑 → 𝑀 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ( 1 ... 𝑁 ) × ( 1 ... 𝑁 ) ) ) )
12	4 5 5 6 7 11	smatrcl	⊢ ( 𝜑 → 𝑆 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ( 1 ... ( 𝑁 − 1 ) ) × ( 1 ... ( 𝑁 − 1 ) ) ) ) )
13		fzfi	⊢ ( 1 ... ( 𝑁 − 1 ) ) ∈ Fin
14	1 2	matrcl	⊢ ( 𝑀 ∈ 𝐵 → ( ( 1 ... 𝑁 ) ∈ Fin ∧ 𝑅 ∈ V ) )
15	14	simprd	⊢ ( 𝑀 ∈ 𝐵 → 𝑅 ∈ V )
16	8 15	syl	⊢ ( 𝜑 → 𝑅 ∈ V )
17		eqid	⊢ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) = ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 )
18	17 9	matbas2	⊢ ( ( ( 1 ... ( 𝑁 − 1 ) ) ∈ Fin ∧ 𝑅 ∈ V ) → ( ( Base ‘ 𝑅 ) ↑m ( ( 1 ... ( 𝑁 − 1 ) ) × ( 1 ... ( 𝑁 − 1 ) ) ) ) = ( Base ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) )
19	13 16 18	sylancr	⊢ ( 𝜑 → ( ( Base ‘ 𝑅 ) ↑m ( ( 1 ... ( 𝑁 − 1 ) ) × ( 1 ... ( 𝑁 − 1 ) ) ) ) = ( Base ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) )
20	19	eleq2d	⊢ ( 𝜑 → ( 𝑆 ∈ ( ( Base ‘ 𝑅 ) ↑m ( ( 1 ... ( 𝑁 − 1 ) ) × ( 1 ... ( 𝑁 − 1 ) ) ) ) ↔ 𝑆 ∈ ( Base ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) ) )
21	12 20	mpbid	⊢ ( 𝜑 → 𝑆 ∈ ( Base ‘ ( ( 1 ... ( 𝑁 − 1 ) ) Mat 𝑅 ) ) )
22	21 3	eleqtrrdi	⊢ ( 𝜑 → 𝑆 ∈ 𝐶 )