# 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 = ( Base ` R )`
matvscl.a
`|- A = ( N Mat R )`
matvscl.b
`|- B = ( Base ` A )`
matvscl.s
`|- .x. = ( .s ` A )`
Assertion matvscl
`|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( C e. K /\ X e. B ) ) -> ( C .x. X ) e. B )`

### Proof

Step Hyp Ref Expression
1 matvscl.k
` |-  K = ( Base ` R )`
2 matvscl.a
` |-  A = ( N Mat R )`
3 matvscl.b
` |-  B = ( Base ` A )`
4 matvscl.s
` |-  .x. = ( .s ` A )`
5 2 matlmod
` |-  ( ( N e. Fin /\ R e. Ring ) -> A e. LMod )`
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( C e. K /\ X e. B ) ) -> A e. LMod )`
7 2 matsca2
` |-  ( ( N e. Fin /\ R e. Ring ) -> R = ( Scalar ` A ) )`
8 7 fveq2d
` |-  ( ( N e. Fin /\ R e. Ring ) -> ( Base ` R ) = ( Base ` ( Scalar ` A ) ) )`
9 1 8 syl5eq
` |-  ( ( N e. Fin /\ R e. Ring ) -> K = ( Base ` ( Scalar ` A ) ) )`
10 9 eleq2d
` |-  ( ( N e. Fin /\ R e. Ring ) -> ( C e. K <-> C e. ( Base ` ( Scalar ` A ) ) ) )`
11 10 biimpd
` |-  ( ( N e. Fin /\ R e. Ring ) -> ( C e. K -> C e. ( Base ` ( Scalar ` A ) ) ) )`
` |-  ( ( N e. Fin /\ R e. Ring ) -> ( ( C e. K /\ X e. B ) -> C e. ( Base ` ( Scalar ` A ) ) ) )`
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( C e. K /\ X e. B ) ) -> C e. ( Base ` ( Scalar ` A ) ) )`
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( C e. K /\ X e. B ) ) -> X e. B )`
` |-  ( Scalar ` A ) = ( Scalar ` A )`
` |-  ( Base ` ( Scalar ` A ) ) = ( Base ` ( Scalar ` A ) )`
` |-  ( ( A e. LMod /\ C e. ( Base ` ( Scalar ` A ) ) /\ X e. B ) -> ( C .x. X ) e. B )`
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( C e. K /\ X e. B ) ) -> ( C .x. X ) e. B )`