Metamath Proof Explorer

Theorem frlmbasmap

Description: Elements of the free module are set functions. (Contributed by Stefan O'Rear, 3-Feb-2015) (Proof shortened by AV, 21-Jul-2019)

Ref Expression
Hypotheses frlmval.f ⊢ F = R freeLMod I
frlmbasmap.n ⊢ N = Base R
frlmbasmap.b ⊢ B = Base F
Assertion frlmbasmap ⊢ I ∈ W ∧ X ∈ B → X ∈ N I

Proof

Step Hyp Ref Expression
1 frlmval.f ⊢ F = R freeLMod I
2 frlmbasmap.n ⊢ N = Base R
3 frlmbasmap.b ⊢ B = Base F
4 simpr ⊢ I ∈ W ∧ X ∈ B → X ∈ B
5 1 3 frlmrcl ⊢ X ∈ B → R ∈ V
6 simpl ⊢ I ∈ W ∧ X ∈ B → I ∈ W
7 eqid ⊢ 0 R = 0 R
8 1 2 7 3 frlmelbas ⊢ R ∈ V ∧ I ∈ W → X ∈ B ↔ X ∈ N I ∧ finSupp 0 R⁡ X
9 5 6 8 syl2an2 ⊢ I ∈ W ∧ X ∈ B → X ∈ B ↔ X ∈ N I ∧ finSupp 0 R⁡ X
10 4 9 mpbid ⊢ I ∈ W ∧ X ∈ B → X ∈ N I ∧ finSupp 0 R⁡ X
11 10 simpld ⊢ I ∈ W ∧ X ∈ B → X ∈ N I