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 ∈ V ∧ I ∈ Fin → N I = Base F

Proof

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