This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem frlmelbas

Description: Membership in the base set of the free module. (Contributed by Stefan O'Rear, 1-Feb-2015) (Revised by AV, 23-Jun-2019)

Ref Expression
Hypotheses frlmval.f ⊢ F = R freeLMod I
frlmelbas.n ⊢ N = Base R
frlmelbas.z ⊢ 0 ˙ = 0 R
frlmelbas.b ⊢ B = Base F
Assertion frlmelbas ⊢ R ∈ V ∧ I ∈ W → X ∈ B ↔ X ∈ N I ∧ finSupp 0 ˙⁡ X

Proof

Step Hyp Ref Expression
1 frlmval.f ⊢ F = R freeLMod I
2 frlmelbas.n ⊢ N = Base R
3 frlmelbas.z ⊢ 0 ˙ = 0 R
4 frlmelbas.b ⊢ B = Base F
5 eqid ⊢ k ∈ N I | finSupp 0 ˙⁡ k = k ∈ N I | finSupp 0 ˙⁡ k
6 1 2 3 5 frlmbas ⊢ R ∈ V ∧ I ∈ W → k ∈ N I | finSupp 0 ˙⁡ k = Base F
7 4 6 eqtr4id ⊢ R ∈ V ∧ I ∈ W → B = k ∈ N I | finSupp 0 ˙⁡ k
8 7 eleq2d ⊢ R ∈ V ∧ I ∈ W → X ∈ B ↔ X ∈ k ∈ N I | finSupp 0 ˙⁡ k
9 breq1 ⊢ k = X → finSupp 0 ˙⁡ k ↔ finSupp 0 ˙⁡ X
10 9 elrab ⊢ X ∈ k ∈ N I | finSupp 0 ˙⁡ k ↔ X ∈ N I ∧ finSupp 0 ˙⁡ X
11 8 10 bitrdi ⊢ R ∈ V ∧ I ∈ W → X ∈ B ↔ X ∈ N I ∧ finSupp 0 ˙⁡ X