Theorem matbas2i

Description: A matrix is a function. (Contributed by Stefan O'Rear, 11-Sep-2015)

	Ref	Expression
Hypotheses	matbas2.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	matbas2.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	matbas2i.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
Assertion	matbas2i	⊢ ( 𝑀 ∈ 𝐵 → 𝑀 ∈ ( 𝐾 ↑m ( 𝑁 × 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		matbas2.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		matbas2.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
3		matbas2i.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
4		id	⊢ ( 𝑀 ∈ 𝐵 → 𝑀 ∈ 𝐵 )
5	4 3	eleqtrdi	⊢ ( 𝑀 ∈ 𝐵 → 𝑀 ∈ ( Base ‘ 𝐴 ) )
6	1 3	matrcl	⊢ ( 𝑀 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
7	1 2	matbas2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) → ( 𝐾 ↑m ( 𝑁 × 𝑁 ) ) = ( Base ‘ 𝐴 ) )
8	6 7	syl	⊢ ( 𝑀 ∈ 𝐵 → ( 𝐾 ↑m ( 𝑁 × 𝑁 ) ) = ( Base ‘ 𝐴 ) )
9	5 8	eleqtrrd	⊢ ( 𝑀 ∈ 𝐵 → 𝑀 ∈ ( 𝐾 ↑m ( 𝑁 × 𝑁 ) ) )