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