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	⊢ 𝐴 = ( 𝑁 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		3re	⊢ 3 ∈ ℝ
5		3lt5	⊢ 3 < 5
6	4 5	gtneii	⊢ 5 ≠ 3
7		scandx	⊢ ( Scalar ‘ ndx ) = 5
8		mulrndx	⊢ ( .r ‘ ndx ) = 3
9	7 8	neeq12i	⊢ ( ( Scalar ‘ ndx ) ≠ ( .r ‘ ndx ) ↔ 5 ≠ 3 )
10	6 9	mpbir	⊢ ( Scalar ‘ ndx ) ≠ ( .r ‘ ndx )
11	3 10	setsnid	⊢ ( Scalar ‘ 𝐺 ) = ( Scalar ‘ ( 𝐺 sSet ⟨ ( .r ‘ ndx ) , ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) ⟩ ) )
12		eqid	⊢ ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ )
13	1 2 12	matval	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → 𝐴 = ( 𝐺 sSet ⟨ ( .r ‘ ndx ) , ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) ⟩ ) )
14	13	fveq2d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ( Scalar ‘ 𝐴 ) = ( Scalar ‘ ( 𝐺 sSet ⟨ ( .r ‘ ndx ) , ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) ⟩ ) ) )
15	11 14	eqtr4id	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ( Scalar ‘ 𝐺 ) = ( Scalar ‘ 𝐴 ) )