Theorem matsca2

Description: The scalars of the matrix ring are the underlying ring. (Contributed by Stefan O'Rear, 5-Sep-2015)

	Ref	Expression
Hypothesis	matsca2.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
Assertion	matsca2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → 𝑅 = ( Scalar ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		matsca2.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		xpfi	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ) → ( 𝑁 × 𝑁 ) ∈ Fin )
3	2	anidms	⊢ ( 𝑁 ∈ Fin → ( 𝑁 × 𝑁 ) ∈ Fin )
4		eqid	⊢ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) = ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) )
5	4	frlmsca	⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑁 × 𝑁 ) ∈ Fin ) → 𝑅 = ( Scalar ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) )
6	5	ancoms	⊢ ( ( ( 𝑁 × 𝑁 ) ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → 𝑅 = ( Scalar ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) )
7	3 6	sylan	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → 𝑅 = ( Scalar ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) )
8	1 4	matsca	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ( Scalar ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( Scalar ‘ 𝐴 ) )
9	7 8	eqtrd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → 𝑅 = ( Scalar ‘ 𝐴 ) )