This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem matvsca

Description: The matrix ring has the same scalar multiplication as its underlying linear structure. (Contributed by Stefan O'Rear, 4-Sep-2015) (Proof shortened by AV, 12-Nov-2024)

Ref Expression
Hypotheses matbas.a ⊢ A = N Mat R
matbas.g ⊢ G = R freeLMod N × N
Assertion matvsca ⊢ N ∈ Fin ∧ R ∈ V → ⋅ G = ⋅ A

Proof

Step Hyp Ref Expression
1 matbas.a ⊢ A = N Mat R
2 matbas.g ⊢ G = R freeLMod N × N
3 vscaid ⊢ ⋅ 𝑠 = Slot ⋅ ndx
4 vscandxnmulrndx ⊢ ⋅ ndx ≠ ⋅ ndx
5 3 4 setsnid ⊢ ⋅ G = ⋅ G sSet ⋅ ndx R maMul N N N
6 eqid ⊢ R maMul N N N = R maMul N N N
7 1 2 6 matval ⊢ N ∈ Fin ∧ R ∈ V → A = G sSet ⋅ ndx R maMul N N N
8 7 fveq2d ⊢ N ∈ Fin ∧ R ∈ V → ⋅ A = ⋅ G sSet ⋅ ndx R maMul N N N
9 5 8 eqtr4id ⊢ N ∈ Fin ∧ R ∈ V → ⋅ G = ⋅ A