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 
|- A = ( N Mat R )
matbas2.k 
|- K = ( Base ` R )
Assertion matbas2 
|- ( ( N e. Fin /\ R e. V ) -> ( K ^m ( N X. N ) ) = ( Base ` A ) )

Proof

Step Hyp Ref Expression
1 matbas2.a 
 |-  A = ( N Mat R )
2 matbas2.k 
 |-  K = ( Base ` R )
3 xpfi 
 |-  ( ( N e. Fin /\ N e. Fin ) -> ( N X. N ) e. Fin )
4 3 anidms 
 |-  ( N e. Fin -> ( N X. N ) e. Fin )
5 4 anim1ci 
 |-  ( ( N e. Fin /\ R e. V ) -> ( R e. V /\ ( N X. N ) e. Fin ) )
6 eqid 
 |-  ( R freeLMod ( N X. N ) ) = ( R freeLMod ( N X. N ) )
7 6 2 frlmfibas 
 |-  ( ( R e. V /\ ( N X. N ) e. Fin ) -> ( K ^m ( N X. N ) ) = ( Base ` ( R freeLMod ( N X. N ) ) ) )
8 5 7 syl 
 |-  ( ( N e. Fin /\ R e. V ) -> ( K ^m ( N X. N ) ) = ( Base ` ( R freeLMod ( N X. N ) ) ) )
9 1 6 matbas 
 |-  ( ( N e. Fin /\ R e. V ) -> ( Base ` ( R freeLMod ( N X. N ) ) ) = ( Base ` A ) )
10 8 9 eqtrd 
 |-  ( ( N e. Fin /\ R e. V ) -> ( K ^m ( N X. N ) ) = ( Base ` A ) )