Metamath Proof Explorer


Theorem 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 ) ) )

Proof

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 ) ) )