# Metamath Proof Explorer

## Theorem matsca

Description: The matrix ring has the same scalars 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 matsca ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in {V}\right)\to \mathrm{Scalar}\left({G}\right)=\mathrm{Scalar}\left({A}\right)$

### 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 eqid ${⊢}{R}\mathrm{maMul}⟨{N},{N},{N}⟩={R}\mathrm{maMul}⟨{N},{N},{N}⟩$
4 1 2 3 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}⟩⟩$
5 4 fveq2d ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in {V}\right)\to \mathrm{Scalar}\left({A}\right)=\mathrm{Scalar}\left({G}\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{R}\mathrm{maMul}⟨{N},{N},{N}⟩⟩\right)$
6 scaid ${⊢}\mathrm{Scalar}=\mathrm{Slot}\mathrm{Scalar}\left(\mathrm{ndx}\right)$
7 3re ${⊢}3\in ℝ$
8 3lt5 ${⊢}3<5$
9 7 8 gtneii ${⊢}5\ne 3$
10 scandx ${⊢}\mathrm{Scalar}\left(\mathrm{ndx}\right)=5$
11 mulrndx ${⊢}{\cdot }_{\mathrm{ndx}}=3$
12 10 11 neeq12i ${⊢}\mathrm{Scalar}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}↔5\ne 3$
13 9 12 mpbir ${⊢}\mathrm{Scalar}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}$
14 6 13 setsnid ${⊢}\mathrm{Scalar}\left({G}\right)=\mathrm{Scalar}\left({G}\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{R}\mathrm{maMul}⟨{N},{N},{N}⟩⟩\right)$
15 5 14 syl6reqr ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in {V}\right)\to \mathrm{Scalar}\left({G}\right)=\mathrm{Scalar}\left({A}\right)$