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

Metamath Proof Explorer

Theorem matbas2

Description: The base set of the matrix ring as a set exponential. (Contributed by Stefan O'Rear, 5-Sep-2015) (Proof shortened by AV, 16-Dec-2018)

Ref Expression
Hypotheses matbas2.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
matbas2.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
Assertion matbas2 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ( 𝐾 ↑m ( 𝑁 × 𝑁 ) ) = ( Base ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 matbas2.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 matbas2.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
3 xpfi ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ) → ( 𝑁 × 𝑁 ) ∈ Fin )
4 3 anidms ⊢ ( 𝑁 ∈ Fin → ( 𝑁 × 𝑁 ) ∈ Fin )
5 4 anim1ci ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 ∈ 𝑉 ∧ ( 𝑁 × 𝑁 ) ∈ Fin ) )
6 eqid ⊢ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) = ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) )
7 6 2 frlmfibas ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑁 × 𝑁 ) ∈ Fin ) → ( 𝐾 ↑m ( 𝑁 × 𝑁 ) ) = ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) )
8 5 7 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ( 𝐾 ↑m ( 𝑁 × 𝑁 ) ) = ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) )
9 1 6 matbas ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( Base ‘ 𝐴 ) )
10 8 9 eqtrd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ( 𝐾 ↑m ( 𝑁 × 𝑁 ) ) = ( Base ‘ 𝐴 ) )