submabas

Description: Any subset of the index set of a square matrix defines a submatrix of the matrix. (Contributed by AV, 1-Jan-2019)

	Ref	Expression
Hypotheses	submabas.a	\|- A = ( N Mat R )
	submabas.b	\|- B = ( Base ` A )
Assertion	submabas	\|- ( ( M e. B /\ D C_ N ) -> ( i e. D , j e. D \|-> ( i M j ) ) e. ( Base ` ( D Mat R ) ) )

Step	Hyp	Ref	Expression
1		submabas.a	\|- A = ( N Mat R )
2		submabas.b	\|- B = ( Base ` A )
3		eqid	\|- ( D Mat R ) = ( D Mat R )
4		eqid	\|- ( Base ` R ) = ( Base ` R )
5		eqid	\|- ( Base ` ( D Mat R ) ) = ( Base ` ( D Mat R ) )
6	1 2	matrcl	\|- ( M e. B -> ( N e. Fin /\ R e. _V ) )
7	6	simpld	\|- ( M e. B -> N e. Fin )
8		ssfi	\|- ( ( N e. Fin /\ D C_ N ) -> D e. Fin )
9	7 8	sylan	\|- ( ( M e. B /\ D C_ N ) -> D e. Fin )
10	6	simprd	\|- ( M e. B -> R e. _V )
11	10	adantr	\|- ( ( M e. B /\ D C_ N ) -> R e. _V )
12		ssel	\|- ( D C_ N -> ( i e. D -> i e. N ) )
13	12	adantl	\|- ( ( M e. B /\ D C_ N ) -> ( i e. D -> i e. N ) )
14	13	imp	\|- ( ( ( M e. B /\ D C_ N ) /\ i e. D ) -> i e. N )
15	14	3adant3	\|- ( ( ( M e. B /\ D C_ N ) /\ i e. D /\ j e. D ) -> i e. N )
16		ssel	\|- ( D C_ N -> ( j e. D -> j e. N ) )
17	16	adantl	\|- ( ( M e. B /\ D C_ N ) -> ( j e. D -> j e. N ) )
18	17	imp	\|- ( ( ( M e. B /\ D C_ N ) /\ j e. D ) -> j e. N )
19	18	3adant2	\|- ( ( ( M e. B /\ D C_ N ) /\ i e. D /\ j e. D ) -> j e. N )
20	2	eleq2i	\|- ( M e. B <-> M e. ( Base ` A ) )
21	20	biimpi	\|- ( M e. B -> M e. ( Base ` A ) )
22	21	adantr	\|- ( ( M e. B /\ D C_ N ) -> M e. ( Base ` A ) )
23	22	3ad2ant1	\|- ( ( ( M e. B /\ D C_ N ) /\ i e. D /\ j e. D ) -> M e. ( Base ` A ) )
24	1 4	matecl	\|- ( ( i e. N /\ j e. N /\ M e. ( Base ` A ) ) -> ( i M j ) e. ( Base ` R ) )
25	15 19 23 24	syl3anc	\|- ( ( ( M e. B /\ D C_ N ) /\ i e. D /\ j e. D ) -> ( i M j ) e. ( Base ` R ) )
26	3 4 5 9 11 25	matbas2d	\|- ( ( M e. B /\ D C_ N ) -> ( i e. D , j e. D \|-> ( i M j ) ) e. ( Base ` ( D Mat R ) ) )

Metamath Proof Explorer