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 ... N ) Mat R )
	smatcl.b	\|- B = ( Base ` A )
	smatcl.c	\|- C = ( Base ` ( ( 1 ... ( N - 1 ) ) Mat R ) )
	smatcl.s	\|- S = ( K ( subMat1 ` M ) L )
	smatcl.n	\|- ( ph -> N e. NN )
	smatcl.k	\|- ( ph -> K e. ( 1 ... N ) )
	smatcl.l	\|- ( ph -> L e. ( 1 ... N ) )
	smatcl.m	\|- ( ph -> M e. B )
Assertion	smatcl	\|- ( ph -> S e. C )

Proof

Step	Hyp	Ref	Expression
1		smatcl.a	\|- A = ( ( 1 ... N ) Mat R )
2		smatcl.b	\|- B = ( Base ` A )
3		smatcl.c	\|- C = ( Base ` ( ( 1 ... ( N - 1 ) ) Mat R ) )
4		smatcl.s	\|- S = ( K ( subMat1 ` M ) L )
5		smatcl.n	\|- ( ph -> N e. NN )
6		smatcl.k	\|- ( ph -> K e. ( 1 ... N ) )
7		smatcl.l	\|- ( ph -> L e. ( 1 ... N ) )
8		smatcl.m	\|- ( ph -> M e. B )
9		eqid	\|- ( Base ` R ) = ( Base ` R )
10	1 9 2	matbas2i	\|- ( M e. B -> M e. ( ( Base ` R ) ^m ( ( 1 ... N ) X. ( 1 ... N ) ) ) )
11	8 10	syl	\|- ( ph -> M e. ( ( Base ` R ) ^m ( ( 1 ... N ) X. ( 1 ... N ) ) ) )
12	4 5 5 6 7 11	smatrcl	\|- ( ph -> S e. ( ( Base ` R ) ^m ( ( 1 ... ( N - 1 ) ) X. ( 1 ... ( N - 1 ) ) ) ) )
13		fzfi	\|- ( 1 ... ( N - 1 ) ) e. Fin
14	1 2	matrcl	\|- ( M e. B -> ( ( 1 ... N ) e. Fin /\ R e. _V ) )
15	14	simprd	\|- ( M e. B -> R e. _V )
16	8 15	syl	\|- ( ph -> R e. _V )
17		eqid	\|- ( ( 1 ... ( N - 1 ) ) Mat R ) = ( ( 1 ... ( N - 1 ) ) Mat R )
18	17 9	matbas2	\|- ( ( ( 1 ... ( N - 1 ) ) e. Fin /\ R e. _V ) -> ( ( Base ` R ) ^m ( ( 1 ... ( N - 1 ) ) X. ( 1 ... ( N - 1 ) ) ) ) = ( Base ` ( ( 1 ... ( N - 1 ) ) Mat R ) ) )
19	13 16 18	sylancr	\|- ( ph -> ( ( Base ` R ) ^m ( ( 1 ... ( N - 1 ) ) X. ( 1 ... ( N - 1 ) ) ) ) = ( Base ` ( ( 1 ... ( N - 1 ) ) Mat R ) ) )
20	19	eleq2d	\|- ( ph -> ( S e. ( ( Base ` R ) ^m ( ( 1 ... ( N - 1 ) ) X. ( 1 ... ( N - 1 ) ) ) ) <-> S e. ( Base ` ( ( 1 ... ( N - 1 ) ) Mat R ) ) ) )
21	12 20	mpbid	\|- ( ph -> S e. ( Base ` ( ( 1 ... ( N - 1 ) ) Mat R ) ) )
22	21 3	eleqtrrdi	\|- ( ph -> S e. C )

Metamath Proof Explorer

Theorem smatcl

Proof