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)

Ref Expression
Hypotheses matbas.a 𝐴 = ( 𝑁 Mat 𝑅 )
matbas.g 𝐺 = ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) )
Assertion matvsca ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉 ) → ( ·𝑠𝐺 ) = ( ·𝑠𝐴 ) )

Proof

Step Hyp Ref Expression
1 matbas.a 𝐴 = ( 𝑁 Mat 𝑅 )
2 matbas.g 𝐺 = ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) )
3 vscaid ·𝑠 = Slot ( ·𝑠 ‘ ndx )
4 vscandx ( ·𝑠 ‘ ndx ) = 6
5 3re 3 ∈ ℝ
6 3lt6 3 < 6
7 5 6 gtneii 6 ≠ 3
8 mulrndx ( .r ‘ ndx ) = 3
9 7 8 neeqtrri 6 ≠ ( .r ‘ ndx )
10 4 9 eqnetri ( ·𝑠 ‘ ndx ) ≠ ( .r ‘ ndx )
11 3 10 setsnid ( ·𝑠𝐺 ) = ( ·𝑠 ‘ ( 𝐺 sSet ⟨ ( .r ‘ ndx ) , ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) ⟩ ) )
12 eqid ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ )
13 1 2 12 matval ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉 ) → 𝐴 = ( 𝐺 sSet ⟨ ( .r ‘ ndx ) , ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) ⟩ ) )
14 13 fveq2d ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉 ) → ( ·𝑠𝐴 ) = ( ·𝑠 ‘ ( 𝐺 sSet ⟨ ( .r ‘ ndx ) , ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) ⟩ ) ) )
15 11 14 eqtr4id ( ( 𝑁 ∈ Fin ∧ 𝑅𝑉 ) → ( ·𝑠𝐺 ) = ( ·𝑠𝐴 ) )