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=RfreeLModI
frlmfibas.n ⊢N=BaseR
Assertion frlmfibas ⊢R∈V∧I∈Fin→NI=BaseF

Proof

Step Hyp Ref Expression
1 frlmfibas.f ⊢F=RfreeLModI
2 frlmfibas.n ⊢N=BaseR
3 elmapi ⊢a∈NI→a:I⟶N
4 3 adantl ⊢I∈Fin∧a∈NI→a:I⟶N
5 simpl ⊢I∈Fin∧a∈NI→I∈Fin
6 fvexd ⊢I∈Fin∧a∈NI→0R∈V
7 4 5 6 fdmfifsupp ⊢I∈Fin∧a∈NI→finSupp0R⁡a
8 7 ralrimiva ⊢I∈Fin→∀a∈NIfinSupp0R⁡a
9 8 adantl ⊢R∈V∧I∈Fin→∀a∈NIfinSupp0R⁡a
10 rabid2 ⊢NI=a∈NI|finSupp0R⁡a↔∀a∈NIfinSupp0R⁡a
11 9 10 sylibr ⊢R∈V∧I∈Fin→NI=a∈NI|finSupp0R⁡a
12 eqid ⊢0R=0R
13 eqid ⊢a∈NI|finSupp0R⁡a=a∈NI|finSupp0R⁡a
14 1 2 12 13 frlmbas ⊢R∈V∧I∈Fin→a∈NI|finSupp0R⁡a=BaseF
15 11 14 eqtrd ⊢R∈V∧I∈Fin→NI=BaseF