# Metamath Proof Explorer

## Theorem matlmod

Description: The matrix ring is a linear structure. (Contributed by Stefan O'Rear, 4-Sep-2015)

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

### Proof

Step Hyp Ref Expression
1 matlmod.a ${⊢}{A}={N}\mathrm{Mat}{R}$
2 sqxpexg ${⊢}{N}\in \mathrm{Fin}\to {N}×{N}\in \mathrm{V}$
3 eqid ${⊢}{R}\mathrm{freeLMod}\left({N}×{N}\right)={R}\mathrm{freeLMod}\left({N}×{N}\right)$
4 3 frlmlmod ${⊢}\left({R}\in \mathrm{Ring}\wedge {N}×{N}\in \mathrm{V}\right)\to {R}\mathrm{freeLMod}\left({N}×{N}\right)\in \mathrm{LMod}$
5 4 ancoms ${⊢}\left({N}×{N}\in \mathrm{V}\wedge {R}\in \mathrm{Ring}\right)\to {R}\mathrm{freeLMod}\left({N}×{N}\right)\in \mathrm{LMod}$
6 2 5 sylan ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {R}\mathrm{freeLMod}\left({N}×{N}\right)\in \mathrm{LMod}$
7 eqidd ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {\mathrm{Base}}_{\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)}={\mathrm{Base}}_{\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)}$
8 1 3 matbas ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {\mathrm{Base}}_{\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)}={\mathrm{Base}}_{{A}}$
9 1 3 matplusg ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {+}_{\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)}={+}_{{A}}$
10 9 oveqdr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)}\wedge {y}\in {\mathrm{Base}}_{\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)}\right)\right)\to {x}{+}_{\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)}{y}={x}{+}_{{A}}{y}$
11 eqidd ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to \mathrm{Scalar}\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)=\mathrm{Scalar}\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)$
12 1 3 matsca ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to \mathrm{Scalar}\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)=\mathrm{Scalar}\left({A}\right)$
13 eqid ${⊢}{\mathrm{Base}}_{\mathrm{Scalar}\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)}$
14 1 3 matvsca ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {\cdot }_{\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)}={\cdot }_{{A}}$
15 14 oveqdr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)}\wedge {y}\in {\mathrm{Base}}_{\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)}\right)\right)\to {x}{\cdot }_{\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)}{y}={x}{\cdot }_{{A}}{y}$
16 7 8 10 11 12 13 15 lmodpropd ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to \left({R}\mathrm{freeLMod}\left({N}×{N}\right)\in \mathrm{LMod}↔{A}\in \mathrm{LMod}\right)$
17 6 16 mpbid ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {A}\in \mathrm{LMod}$