# Metamath Proof Explorer

## Theorem matvsca2

Description: Scalar multiplication in the matrix ring is cell-wise. (Contributed by Stefan O'Rear, 5-Sep-2015)

Ref Expression
Hypotheses matvsca2.a ${⊢}{A}={N}\mathrm{Mat}{R}$
matvsca2.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
matvsca2.k ${⊢}{K}={\mathrm{Base}}_{{R}}$
matvsca2.v
matvsca2.t
matvsca2.c ${⊢}{C}={N}×{N}$
Assertion matvsca2

### Proof

Step Hyp Ref Expression
1 matvsca2.a ${⊢}{A}={N}\mathrm{Mat}{R}$
2 matvsca2.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
3 matvsca2.k ${⊢}{K}={\mathrm{Base}}_{{R}}$
4 matvsca2.v
5 matvsca2.t
6 matvsca2.c ${⊢}{C}={N}×{N}$
7 1 2 matrcl ${⊢}{Y}\in {B}\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)$
8 7 adantl ${⊢}\left({X}\in {K}\wedge {Y}\in {B}\right)\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)$
9 eqid ${⊢}{R}\mathrm{freeLMod}\left({N}×{N}\right)={R}\mathrm{freeLMod}\left({N}×{N}\right)$
10 1 9 matvsca ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)\to {\cdot }_{\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)}={\cdot }_{{A}}$
11 8 10 syl ${⊢}\left({X}\in {K}\wedge {Y}\in {B}\right)\to {\cdot }_{\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)}={\cdot }_{{A}}$
12 11 4 syl6eqr
13 12 oveqd
14 eqid ${⊢}{\mathrm{Base}}_{\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)}={\mathrm{Base}}_{\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)}$
15 8 simpld ${⊢}\left({X}\in {K}\wedge {Y}\in {B}\right)\to {N}\in \mathrm{Fin}$
16 xpfi ${⊢}\left({N}\in \mathrm{Fin}\wedge {N}\in \mathrm{Fin}\right)\to {N}×{N}\in \mathrm{Fin}$
17 15 15 16 syl2anc ${⊢}\left({X}\in {K}\wedge {Y}\in {B}\right)\to {N}×{N}\in \mathrm{Fin}$
18 simpl ${⊢}\left({X}\in {K}\wedge {Y}\in {B}\right)\to {X}\in {K}$
19 simpr ${⊢}\left({X}\in {K}\wedge {Y}\in {B}\right)\to {Y}\in {B}$
20 1 9 matbas ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)\to {\mathrm{Base}}_{\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)}={\mathrm{Base}}_{{A}}$
21 8 20 syl ${⊢}\left({X}\in {K}\wedge {Y}\in {B}\right)\to {\mathrm{Base}}_{\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)}={\mathrm{Base}}_{{A}}$
22 21 2 syl6eqr ${⊢}\left({X}\in {K}\wedge {Y}\in {B}\right)\to {\mathrm{Base}}_{\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)}={B}$
23 19 22 eleqtrrd ${⊢}\left({X}\in {K}\wedge {Y}\in {B}\right)\to {Y}\in {\mathrm{Base}}_{\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)}$
24 eqid ${⊢}{\cdot }_{\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)}={\cdot }_{\left({R}\mathrm{freeLMod}\left({N}×{N}\right)\right)}$
25 9 14 3 17 18 23 24 5 frlmvscafval
26 6 xpeq1i ${⊢}{C}×\left\{{X}\right\}=\left({N}×{N}\right)×\left\{{X}\right\}$
27 26 oveq1i
28 25 27 syl6eqr
29 13 28 eqtr3d