# Metamath Proof Explorer

## Theorem matsca2

Description: The scalars of the matrix ring are the underlying ring. (Contributed by Stefan O'Rear, 5-Sep-2015)

Ref Expression
Hypothesis matsca2.a ${⊢}{A}={N}\mathrm{Mat}{R}$
Assertion matsca2 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in {V}\right)\to {R}=\mathrm{Scalar}\left({A}\right)$

### Proof

Step Hyp Ref Expression
1 matsca2.a ${⊢}{A}={N}\mathrm{Mat}{R}$
2 xpfi ${⊢}\left({N}\in \mathrm{Fin}\wedge {N}\in \mathrm{Fin}\right)\to {N}×{N}\in \mathrm{Fin}$
3 2 anidms ${⊢}{N}\in \mathrm{Fin}\to {N}×{N}\in \mathrm{Fin}$
4 eqid ${⊢}{R}\mathrm{freeLMod}\left({N}×{N}\right)={R}\mathrm{freeLMod}\left({N}×{N}\right)$
5 4 frlmsca ${⊢}\left({R}\in {V}\wedge {N}×{N}\in \mathrm{Fin}\right)\to {R}=\mathrm{Scalar}\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)$
6 5 ancoms ${⊢}\left({N}×{N}\in \mathrm{Fin}\wedge {R}\in {V}\right)\to {R}=\mathrm{Scalar}\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)$
7 3 6 sylan ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in {V}\right)\to {R}=\mathrm{Scalar}\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)$
8 1 4 matsca ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in {V}\right)\to \mathrm{Scalar}\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)=\mathrm{Scalar}\left({A}\right)$
9 7 8 eqtrd ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in {V}\right)\to {R}=\mathrm{Scalar}\left({A}\right)$