# Metamath Proof Explorer

## Theorem matvscl

Description: Closure of the scalar multiplication in the matrix ring. ( lmodvscl analog.) (Contributed by AV, 27-Nov-2019)

Ref Expression
Hypotheses matvscl.k ${⊢}{K}={\mathrm{Base}}_{{R}}$
matvscl.a ${⊢}{A}={N}\mathrm{Mat}{R}$
matvscl.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
matvscl.s
Assertion matvscl

### Proof

Step Hyp Ref Expression
1 matvscl.k ${⊢}{K}={\mathrm{Base}}_{{R}}$
2 matvscl.a ${⊢}{A}={N}\mathrm{Mat}{R}$
3 matvscl.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
4 matvscl.s
5 2 matlmod ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {A}\in \mathrm{LMod}$
6 5 adantr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({C}\in {K}\wedge {X}\in {B}\right)\right)\to {A}\in \mathrm{LMod}$
7 2 matsca2 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {R}=\mathrm{Scalar}\left({A}\right)$
8 7 fveq2d ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {\mathrm{Base}}_{{R}}={\mathrm{Base}}_{\mathrm{Scalar}\left({A}\right)}$
9 1 8 syl5eq ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {K}={\mathrm{Base}}_{\mathrm{Scalar}\left({A}\right)}$
10 9 eleq2d ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to \left({C}\in {K}↔{C}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({A}\right)}\right)$
11 10 biimpd ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to \left({C}\in {K}\to {C}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({A}\right)}\right)$
12 11 adantrd ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to \left(\left({C}\in {K}\wedge {X}\in {B}\right)\to {C}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({A}\right)}\right)$
13 12 imp ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({C}\in {K}\wedge {X}\in {B}\right)\right)\to {C}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({A}\right)}$
14 simprr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({C}\in {K}\wedge {X}\in {B}\right)\right)\to {X}\in {B}$
15 eqid ${⊢}\mathrm{Scalar}\left({A}\right)=\mathrm{Scalar}\left({A}\right)$
16 eqid ${⊢}{\mathrm{Base}}_{\mathrm{Scalar}\left({A}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({A}\right)}$
17 3 15 4 16 lmodvscl
18 6 13 14 17 syl3anc