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=NMatR
submabas.b ⊢B=BaseA
Assertion submabas ⊢M∈B∧D⊆N→i∈D,j∈D⟼iMj∈BaseDMatR

Proof

Step Hyp Ref Expression
1 submabas.a ⊢A=NMatR
2 submabas.b ⊢B=BaseA
3 eqid ⊢DMatR=DMatR
4 eqid ⊢BaseR=BaseR
5 eqid ⊢BaseDMatR=BaseDMatR
6 1 2 matrcl ⊢M∈B→N∈Fin∧R∈V
7 6 simpld ⊢M∈B→N∈Fin
8 ssfi ⊢N∈Fin∧D⊆N→D∈Fin
9 7 8 sylan ⊢M∈B∧D⊆N→D∈Fin
10 6 simprd ⊢M∈B→R∈V
11 10 adantr ⊢M∈B∧D⊆N→R∈V
12 ssel ⊢D⊆N→i∈D→i∈N
13 12 adantl ⊢M∈B∧D⊆N→i∈D→i∈N
14 13 imp ⊢M∈B∧D⊆N∧i∈D→i∈N
15 14 3adant3 ⊢M∈B∧D⊆N∧i∈D∧j∈D→i∈N
16 ssel ⊢D⊆N→j∈D→j∈N
17 16 adantl ⊢M∈B∧D⊆N→j∈D→j∈N
18 17 imp ⊢M∈B∧D⊆N∧j∈D→j∈N
19 18 3adant2 ⊢M∈B∧D⊆N∧i∈D∧j∈D→j∈N
20 2 eleq2i ⊢M∈B↔M∈BaseA
21 20 biimpi ⊢M∈B→M∈BaseA
22 21 adantr ⊢M∈B∧D⊆N→M∈BaseA
23 22 3ad2ant1 ⊢M∈B∧D⊆N∧i∈D∧j∈D→M∈BaseA
24 1 4 matecl ⊢i∈N∧j∈N∧M∈BaseA→iMj∈BaseR
25 15 19 23 24 syl3anc ⊢M∈B∧D⊆N∧i∈D∧j∈D→iMj∈BaseR
26 3 4 5 9 11 25 matbas2d ⊢M∈B∧D⊆N→i∈D,j∈D⟼iMj∈BaseDMatR