# 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}\mathrm{Mat}{R}$
matbas2.k ${⊢}{K}={\mathrm{Base}}_{{R}}$
Assertion matbas2 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in {V}\right)\to {{K}}^{\left({N}×{N}\right)}={\mathrm{Base}}_{{A}}$

### Proof

Step Hyp Ref Expression
1 matbas2.a ${⊢}{A}={N}\mathrm{Mat}{R}$
2 matbas2.k ${⊢}{K}={\mathrm{Base}}_{{R}}$
3 xpfi ${⊢}\left({N}\in \mathrm{Fin}\wedge {N}\in \mathrm{Fin}\right)\to {N}×{N}\in \mathrm{Fin}$
4 3 anidms ${⊢}{N}\in \mathrm{Fin}\to {N}×{N}\in \mathrm{Fin}$
5 4 anim1ci ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in {V}\right)\to \left({R}\in {V}\wedge {N}×{N}\in \mathrm{Fin}\right)$
6 eqid ${⊢}{R}\mathrm{freeLMod}\left({N}×{N}\right)={R}\mathrm{freeLMod}\left({N}×{N}\right)$
7 6 2 frlmfibas ${⊢}\left({R}\in {V}\wedge {N}×{N}\in \mathrm{Fin}\right)\to {{K}}^{\left({N}×{N}\right)}={\mathrm{Base}}_{\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)}$
8 5 7 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in {V}\right)\to {{K}}^{\left({N}×{N}\right)}={\mathrm{Base}}_{\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)}$
9 1 6 matbas ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in {V}\right)\to {\mathrm{Base}}_{\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)}={\mathrm{Base}}_{{A}}$
10 8 9 eqtrd ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in {V}\right)\to {{K}}^{\left({N}×{N}\right)}={\mathrm{Base}}_{{A}}$