# Metamath Proof Explorer

## Theorem matbas

Description: The matrix ring has the same base set as its underlying group. (Contributed by Stefan O'Rear, 4-Sep-2015)

Ref Expression
Hypotheses matbas.a ${⊢}{A}={N}\mathrm{Mat}{R}$
matbas.g ${⊢}{G}={R}\mathrm{freeLMod}\left({N}×{N}\right)$
Assertion matbas ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in {V}\right)\to {\mathrm{Base}}_{{G}}={\mathrm{Base}}_{{A}}$

### Proof

Step Hyp Ref Expression
1 matbas.a ${⊢}{A}={N}\mathrm{Mat}{R}$
2 matbas.g ${⊢}{G}={R}\mathrm{freeLMod}\left({N}×{N}\right)$
3 baseid ${⊢}\mathrm{Base}=\mathrm{Slot}{\mathrm{Base}}_{\mathrm{ndx}}$
4 basendxnmulrndx ${⊢}{\mathrm{Base}}_{\mathrm{ndx}}\ne {\cdot }_{\mathrm{ndx}}$
5 3 4 setsnid ${⊢}{\mathrm{Base}}_{{G}}={\mathrm{Base}}_{\left({G}\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{R}\mathrm{maMul}⟨{N},{N},{N}⟩⟩\right)}$
6 eqid ${⊢}{R}\mathrm{maMul}⟨{N},{N},{N}⟩={R}\mathrm{maMul}⟨{N},{N},{N}⟩$
7 1 2 6 matval ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in {V}\right)\to {A}={G}\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{R}\mathrm{maMul}⟨{N},{N},{N}⟩⟩$
8 7 fveq2d ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in {V}\right)\to {\mathrm{Base}}_{{A}}={\mathrm{Base}}_{\left({G}\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{R}\mathrm{maMul}⟨{N},{N},{N}⟩⟩\right)}$
9 5 8 eqtr4id ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in {V}\right)\to {\mathrm{Base}}_{{G}}={\mathrm{Base}}_{{A}}$