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

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) (Proof shortened by AV, 12-Nov-2024)

Ref Expression
Hypotheses matbas.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
matbas.g ⊢ 𝐺 = ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) )
Assertion matsca ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ( Scalar ‘ 𝐺 ) = ( Scalar ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 matbas.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 matbas.g ⊢ 𝐺 = ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) )
3 scaid ⊢ Scalar = Slot ( Scalar ‘ ndx )
4 scandxnmulrndx ⊢ ( Scalar ‘ ndx ) ≠ ( .r ‘ ndx )
5 3 4 setsnid ⊢ ( Scalar ‘ 𝐺 ) = ( Scalar ‘ ( 𝐺 sSet ⟨ ( .r ‘ ndx ) , ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) ⟩ ) )
6 eqid ⊢ ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ )
7 1 2 6 matval ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → 𝐴 = ( 𝐺 sSet ⟨ ( .r ‘ ndx ) , ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) ⟩ ) )
8 7 fveq2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ( Scalar ‘ 𝐴 ) = ( Scalar ‘ ( 𝐺 sSet ⟨ ( .r ‘ ndx ) , ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) ⟩ ) ) )
9 5 8 eqtr4id ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ( Scalar ‘ 𝐺 ) = ( Scalar ‘ 𝐴 ) )