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

Metamath Proof Explorer

Theorem frlmfibas

Description: The base set of the finite free module as a set exponential. (Contributed by AV, 6-Dec-2018)

Ref Expression
Hypotheses frlmfibas.f 
|- F = ( R freeLMod I )
frlmfibas.n 
|- N = ( Base ` R )
Assertion frlmfibas 
|- ( ( R e. V /\ I e. Fin ) -> ( N ^m I ) = ( Base ` F ) )

Proof

Step Hyp Ref Expression
1 frlmfibas.f 
 |-  F = ( R freeLMod I )
2 frlmfibas.n 
 |-  N = ( Base ` R )
3 elmapi 
 |-  ( a e. ( N ^m I ) -> a : I --> N )
4 3 adantl 
 |-  ( ( I e. Fin /\ a e. ( N ^m I ) ) -> a : I --> N )
5 simpl 
 |-  ( ( I e. Fin /\ a e. ( N ^m I ) ) -> I e. Fin )
6 fvexd 
 |-  ( ( I e. Fin /\ a e. ( N ^m I ) ) -> ( 0g ` R ) e. _V )
7 4 5 6 fdmfifsupp 
 |-  ( ( I e. Fin /\ a e. ( N ^m I ) ) -> a finSupp ( 0g ` R ) )
8 7 ralrimiva 
 |-  ( I e. Fin -> A. a e. ( N ^m I ) a finSupp ( 0g ` R ) )
9 8 adantl 
 |-  ( ( R e. V /\ I e. Fin ) -> A. a e. ( N ^m I ) a finSupp ( 0g ` R ) )
10 rabid2 
 |-  ( ( N ^m I ) = { a e. ( N ^m I ) | a finSupp ( 0g ` R ) } <-> A. a e. ( N ^m I ) a finSupp ( 0g ` R ) )
11 9 10 sylibr 
 |-  ( ( R e. V /\ I e. Fin ) -> ( N ^m I ) = { a e. ( N ^m I ) | a finSupp ( 0g ` R ) } )
12 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
13 eqid 
 |-  { a e. ( N ^m I ) | a finSupp ( 0g ` R ) } = { a e. ( N ^m I ) | a finSupp ( 0g ` R ) }
14 1 2 12 13 frlmbas 
 |-  ( ( R e. V /\ I e. Fin ) -> { a e. ( N ^m I ) | a finSupp ( 0g ` R ) } = ( Base ` F ) )
15 11 14 eqtrd 
 |-  ( ( R e. V /\ I e. Fin ) -> ( N ^m I ) = ( Base ` F ) )