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	⊢ 𝐴 = ( 𝑁 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		vscandxnmulrndx	⊢ ( ·𝑠 ‘ ndx ) ≠ ( .r ‘ ndx )
5	3 4	setsnid	⊢ ( ·𝑠 ‘ 𝐺 ) = ( ·𝑠 ‘ ( 𝐺 sSet ⟨ ( .r ‘ ndx ) , ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) ⟩ ) )
6		eqid	⊢ ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ )
7	1 2 6	matval	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → 𝐴 = ( 𝐺 sSet ⟨ ( .r ‘ ndx ) , ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) ⟩ ) )
8	7	fveq2d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ( ·𝑠 ‘ 𝐴 ) = ( ·𝑠 ‘ ( 𝐺 sSet ⟨ ( .r ‘ ndx ) , ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) ⟩ ) ) )
9	5 8	eqtr4id	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ( ·𝑠 ‘ 𝐺 ) = ( ·𝑠 ‘ 𝐴 ) )