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 ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
submabas.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
Assertion submabas ( ( 𝑀 ∈ 𝐵 ∧ 𝐷 ⊆ 𝑁 ) → ( 𝑖 ∈ 𝐷 , 𝑗 ∈ 𝐷 ↦ ( 𝑖 𝑀 𝑗 ) ) ∈ ( Base ‘ ( 𝐷 Mat 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 submabas.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 submabas.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
3 eqid ⊢ ( 𝐷 Mat 𝑅 ) = ( 𝐷 Mat 𝑅 )
4 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
5 eqid ⊢ ( Base ‘ ( 𝐷 Mat 𝑅 ) ) = ( Base ‘ ( 𝐷 Mat 𝑅 ) )
6 1 2 matrcl ⊢ ( 𝑀 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
7 6 simpld ⊢ ( 𝑀 ∈ 𝐵 → 𝑁 ∈ Fin )
8 ssfi ⊢ ( ( 𝑁 ∈ Fin ∧ 𝐷 ⊆ 𝑁 ) → 𝐷 ∈ Fin )
9 7 8 sylan ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐷 ⊆ 𝑁 ) → 𝐷 ∈ Fin )
10 6 simprd ⊢ ( 𝑀 ∈ 𝐵 → 𝑅 ∈ V )
11 10 adantr ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐷 ⊆ 𝑁 ) → 𝑅 ∈ V )
12 ssel ⊢ ( 𝐷 ⊆ 𝑁 → ( 𝑖 ∈ 𝐷 → 𝑖 ∈ 𝑁 ) )
13 12 adantl ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐷 ⊆ 𝑁 ) → ( 𝑖 ∈ 𝐷 → 𝑖 ∈ 𝑁 ) )
14 13 imp ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐷 ⊆ 𝑁 ) ∧ 𝑖 ∈ 𝐷 ) → 𝑖 ∈ 𝑁 )
15 14 3adant3 ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐷 ⊆ 𝑁 ) ∧ 𝑖 ∈ 𝐷 ∧ 𝑗 ∈ 𝐷 ) → 𝑖 ∈ 𝑁 )
16 ssel ⊢ ( 𝐷 ⊆ 𝑁 → ( 𝑗 ∈ 𝐷 → 𝑗 ∈ 𝑁 ) )
17 16 adantl ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐷 ⊆ 𝑁 ) → ( 𝑗 ∈ 𝐷 → 𝑗 ∈ 𝑁 ) )
18 17 imp ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐷 ⊆ 𝑁 ) ∧ 𝑗 ∈ 𝐷 ) → 𝑗 ∈ 𝑁 )
19 18 3adant2 ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐷 ⊆ 𝑁 ) ∧ 𝑖 ∈ 𝐷 ∧ 𝑗 ∈ 𝐷 ) → 𝑗 ∈ 𝑁 )
20 2 eleq2i ⊢ ( 𝑀 ∈ 𝐵 ↔ 𝑀 ∈ ( Base ‘ 𝐴 ) )
21 20 biimpi ⊢ ( 𝑀 ∈ 𝐵 → 𝑀 ∈ ( Base ‘ 𝐴 ) )
22 21 adantr ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐷 ⊆ 𝑁 ) → 𝑀 ∈ ( Base ‘ 𝐴 ) )
23 22 3ad2ant1 ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐷 ⊆ 𝑁 ) ∧ 𝑖 ∈ 𝐷 ∧ 𝑗 ∈ 𝐷 ) → 𝑀 ∈ ( Base ‘ 𝐴 ) )
24 1 4 matecl ⊢ ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ∧ 𝑀 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑖 𝑀 𝑗 ) ∈ ( Base ‘ 𝑅 ) )
25 15 19 23 24 syl3anc ⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐷 ⊆ 𝑁 ) ∧ 𝑖 ∈ 𝐷 ∧ 𝑗 ∈ 𝐷 ) → ( 𝑖 𝑀 𝑗 ) ∈ ( Base ‘ 𝑅 ) )
26 3 4 5 9 11 25 matbas2d ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐷 ⊆ 𝑁 ) → ( 𝑖 ∈ 𝐷 , 𝑗 ∈ 𝐷 ↦ ( 𝑖 𝑀 𝑗 ) ) ∈ ( Base ‘ ( 𝐷 Mat 𝑅 ) ) )