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