Metamath Proof Explorer


Theorem matsca

Description: The matrix ring has the same scalars as its underlying linear structure. (Contributed by Stefan O'Rear, 4-Sep-2015)

Ref Expression
Hypotheses matbas.a A = N Mat R
matbas.g G = R freeLMod N × N
Assertion matsca N Fin R V Scalar G = Scalar A

Proof

Step Hyp Ref Expression
1 matbas.a A = N Mat R
2 matbas.g G = R freeLMod N × N
3 eqid R maMul N N N = R maMul N N N
4 1 2 3 matval N Fin R V A = G sSet ndx R maMul N N N
5 4 fveq2d N Fin R V Scalar A = Scalar G sSet ndx R maMul N N N
6 scaid Scalar = Slot Scalar ndx
7 3re 3
8 3lt5 3 < 5
9 7 8 gtneii 5 3
10 scandx Scalar ndx = 5
11 mulrndx ndx = 3
12 10 11 neeq12i Scalar ndx ndx 5 3
13 9 12 mpbir Scalar ndx ndx
14 6 13 setsnid Scalar G = Scalar G sSet ndx R maMul N N N
15 5 14 syl6reqr N Fin R V Scalar G = Scalar A