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