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

Metamath Proof Explorer

Theorem matbas2

Description: The base set of the matrix ring as a set exponential. (Contributed by Stefan O'Rear, 5-Sep-2015) (Proof shortened by AV, 16-Dec-2018)

Ref Expression
Hypotheses matbas2.a ⊢ A = N Mat R
matbas2.k ⊢ K = Base R
Assertion matbas2 ⊢ N ∈ Fin ∧ R ∈ V → K N × N = Base A

Proof

Step Hyp Ref Expression
1 matbas2.a ⊢ A = N Mat R
2 matbas2.k ⊢ K = Base R
3 xpfi ⊢ N ∈ Fin ∧ N ∈ Fin → N × N ∈ Fin
4 3 anidms ⊢ N ∈ Fin → N × N ∈ Fin
5 4 anim1ci ⊢ N ∈ Fin ∧ R ∈ V → R ∈ V ∧ N × N ∈ Fin
6 eqid ⊢ R freeLMod N × N = R freeLMod N × N
7 6 2 frlmfibas ⊢ R ∈ V ∧ N × N ∈ Fin → K N × N = Base R freeLMod N × N
8 5 7 syl ⊢ N ∈ Fin ∧ R ∈ V → K N × N = Base R freeLMod N × N
9 1 6 matbas ⊢ N ∈ Fin ∧ R ∈ V → Base R freeLMod N × N = Base A
10 8 9 eqtrd ⊢ N ∈ Fin ∧ R ∈ V → K N × N = Base A