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

Metamath Proof Explorer

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 ‘ 𝐴 ) )