# Metamath Proof Explorer

## Theorem matvsca

Description: The matrix ring has the same scalar multiplication as its underlying linear structure. (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 matvsca ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in {V}\right)\to {\cdot }_{{G}}={\cdot }_{{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 vscaid ${⊢}{\cdot }_{𝑠}=\mathrm{Slot}{\cdot }_{\mathrm{ndx}}$
4 vscandx ${⊢}{\cdot }_{\mathrm{ndx}}=6$
5 3re ${⊢}3\in ℝ$
6 3lt6 ${⊢}3<6$
7 5 6 gtneii ${⊢}6\ne 3$
8 mulrndx ${⊢}{\cdot }_{\mathrm{ndx}}=3$
9 7 8 neeqtrri ${⊢}6\ne {\cdot }_{\mathrm{ndx}}$
10 4 9 eqnetri ${⊢}{\cdot }_{\mathrm{ndx}}\ne {\cdot }_{\mathrm{ndx}}$
11 3 10 setsnid ${⊢}{\cdot }_{{G}}={\cdot }_{\left({G}\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{R}\mathrm{maMul}⟨{N},{N},{N}⟩⟩\right)}$
12 eqid ${⊢}{R}\mathrm{maMul}⟨{N},{N},{N}⟩={R}\mathrm{maMul}⟨{N},{N},{N}⟩$
13 1 2 12 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}⟩⟩$
14 13 fveq2d ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in {V}\right)\to {\cdot }_{{A}}={\cdot }_{\left({G}\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{R}\mathrm{maMul}⟨{N},{N},{N}⟩⟩\right)}$
15 11 14 eqtr4id ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in {V}\right)\to {\cdot }_{{G}}={\cdot }_{{A}}$