This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ B ∧ D ⊆ N → i ∈ D , j ∈ D ⟼ i M j ∈ 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 ∈ 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 ∈ Base A
21 20 biimpi ⊢ M ∈ B → M ∈ Base A
22 21 adantr ⊢ M ∈ B ∧ D ⊆ N → M ∈ Base A
23 22 3ad2ant1 ⊢ M ∈ B ∧ D ⊆ N ∧ i ∈ D ∧ j ∈ D → M ∈ Base A
24 1 4 matecl ⊢ i ∈ N ∧ j ∈ N ∧ M ∈ Base A → i M j ∈ Base R
25 15 19 23 24 syl3anc ⊢ M ∈ B ∧ D ⊆ N ∧ i ∈ D ∧ j ∈ D → i M j ∈ Base R
26 3 4 5 9 11 25 matbas2d ⊢ M ∈ B ∧ D ⊆ N → i ∈ D , j ∈ D ⟼ i M j ∈ Base D Mat R