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

Metamath Proof Explorer

Theorem matbas2i

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

Ref Expression
Hypotheses matbas2.a ⊢ A = N Mat R
matbas2.k ⊢ K = Base R
matbas2i.b ⊢ B = Base A
Assertion matbas2i ⊢ M ∈ B → M ∈ K N × N

Proof

Step Hyp Ref Expression
1 matbas2.a ⊢ A = N Mat R
2 matbas2.k ⊢ K = Base R
3 matbas2i.b ⊢ B = Base A
4 id ⊢ M ∈ B → M ∈ B
5 4 3 eleqtrdi ⊢ M ∈ B → M ∈ Base A
6 1 3 matrcl ⊢ M ∈ B → N ∈ Fin ∧ R ∈ V
7 1 2 matbas2 ⊢ N ∈ Fin ∧ R ∈ V → K N × N = Base A
8 6 7 syl ⊢ M ∈ B → K N × N = Base A
9 5 8 eleqtrrd ⊢ M ∈ B → M ∈ K N × N