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 Mat R
matvsca2.b B = Base A
matvsca2.k K = Base R
matvsca2.v · ˙ = A
matvsca2.t × ˙ = R
matvsca2.c C = N × N
Assertion matvsca2 X K Y B X · ˙ Y = C × X × ˙ f Y

Proof

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