# 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 𝐾 = ( Base ‘ 𝑅 )
matvscl.a 𝐴 = ( 𝑁 Mat 𝑅 )
matvscl.b 𝐵 = ( Base ‘ 𝐴 )
matvscl.s · = ( ·𝑠𝐴 )
Assertion matvscl ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐶𝐾𝑋𝐵 ) ) → ( 𝐶 · 𝑋 ) ∈ 𝐵 )

### Proof

Step Hyp Ref Expression
1 matvscl.k 𝐾 = ( Base ‘ 𝑅 )
2 matvscl.a 𝐴 = ( 𝑁 Mat 𝑅 )
3 matvscl.b 𝐵 = ( Base ‘ 𝐴 )
4 matvscl.s · = ( ·𝑠𝐴 )
5 2 matlmod ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ LMod )
6 5 adantr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐶𝐾𝑋𝐵 ) ) → 𝐴 ∈ LMod )
7 2 matsca2 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑅 = ( Scalar ‘ 𝐴 ) )
8 7 fveq2d ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
9 1 8 syl5eq ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐾 = ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
10 9 eleq2d ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝐶𝐾𝐶 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ) )
11 10 biimpd ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝐶𝐾𝐶 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ) )
12 11 adantrd ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( 𝐶𝐾𝑋𝐵 ) → 𝐶 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ) )
13 12 imp ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐶𝐾𝑋𝐵 ) ) → 𝐶 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
14 simprr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐶𝐾𝑋𝐵 ) ) → 𝑋𝐵 )
15 eqid ( Scalar ‘ 𝐴 ) = ( Scalar ‘ 𝐴 )
16 eqid ( Base ‘ ( Scalar ‘ 𝐴 ) ) = ( Base ‘ ( Scalar ‘ 𝐴 ) )
17 3 15 4 16 lmodvscl ( ( 𝐴 ∈ LMod ∧ 𝐶 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∧ 𝑋𝐵 ) → ( 𝐶 · 𝑋 ) ∈ 𝐵 )
18 6 13 14 17 syl3anc ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐶𝐾𝑋𝐵 ) ) → ( 𝐶 · 𝑋 ) ∈ 𝐵 )