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	birani	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐷 ⊆ 𝑁 ) → 𝑀 ∈ ( Base ‘ 𝐴 ) )
22	21	3ad2ant1	⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐷 ⊆ 𝑁 ) ∧ 𝑖 ∈ 𝐷 ∧ 𝑗 ∈ 𝐷 ) → 𝑀 ∈ ( Base ‘ 𝐴 ) )
23	1 4	matecl	⊢ ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ∧ 𝑀 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑖 𝑀 𝑗 ) ∈ ( Base ‘ 𝑅 ) )
24	15 19 22 23	syl3anc	⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ 𝐷 ⊆ 𝑁 ) ∧ 𝑖 ∈ 𝐷 ∧ 𝑗 ∈ 𝐷 ) → ( 𝑖 𝑀 𝑗 ) ∈ ( Base ‘ 𝑅 ) )
25	3 4 5 9 11 24	matbas2d	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐷 ⊆ 𝑁 ) → ( 𝑖 ∈ 𝐷 , 𝑗 ∈ 𝐷 ↦ ( 𝑖 𝑀 𝑗 ) ) ∈ ( Base ‘ ( 𝐷 Mat 𝑅 ) ) )