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