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=BaseR
matvscl.a ⊢A=NMatR
matvscl.b ⊢B=BaseA
matvscl.s ⊢·˙=⋅A
Assertion matvscl ⊢N∈Fin∧R∈Ring∧C∈K∧X∈B→C·˙X∈B

Proof

Step Hyp Ref Expression
1 matvscl.k ⊢K=BaseR
2 matvscl.a ⊢A=NMatR
3 matvscl.b ⊢B=BaseA
4 matvscl.s ⊢·˙=⋅A
5 2 matlmod ⊢N∈Fin∧R∈Ring→A∈LMod
6 5 adantr ⊢N∈Fin∧R∈Ring∧C∈K∧X∈B→A∈LMod
7 2 matsca2 ⊢N∈Fin∧R∈Ring→R=Scalar⁡A
8 7 fveq2d ⊢N∈Fin∧R∈Ring→BaseR=BaseScalar⁡A
9 1 8 eqtrid ⊢N∈Fin∧R∈Ring→K=BaseScalar⁡A
10 9 eleq2d ⊢N∈Fin∧R∈Ring→C∈K↔C∈BaseScalar⁡A
11 10 biimpd ⊢N∈Fin∧R∈Ring→C∈K→C∈BaseScalar⁡A
12 11 adantrd ⊢N∈Fin∧R∈Ring→C∈K∧X∈B→C∈BaseScalar⁡A
13 12 imp ⊢N∈Fin∧R∈Ring∧C∈K∧X∈B→C∈BaseScalar⁡A
14 simprr ⊢N∈Fin∧R∈Ring∧C∈K∧X∈B→X∈B
15 eqid ⊢Scalar⁡A=Scalar⁡A
16 eqid ⊢BaseScalar⁡A=BaseScalar⁡A
17 3 15 4 16 lmodvscl ⊢A∈LMod∧C∈BaseScalar⁡A∧X∈B→C·˙X∈B
18 6 13 14 17 syl3anc ⊢N∈Fin∧R∈Ring∧C∈K∧X∈B→C·˙X∈B