Metamath Proof Explorer

Theorem islinds

Description: Property of an independent set of vectors in terms of an independent family. (Contributed by Stefan O'Rear, 24-Feb-2015)

Ref Expression
Hypothesis islinds.b ⊢ B = Base W
Assertion islinds ⊢ W ∈ V → X ∈ LIndS ⁡ W ↔ X ⊆ B ∧ I ↾ X LIndF W

Proof

Step Hyp Ref Expression
1 islinds.b ⊢ B = Base W
2 elex ⊢ W ∈ V → W ∈ V
3 fveq2 ⊢ w = W → Base w = Base W
4 3 pweqd ⊢ w = W → 𝒫 Base w = 𝒫 Base W
5 breq2 ⊢ w = W → I ↾ s LIndF w ↔ I ↾ s LIndF W
6 4 5 rabeqbidv ⊢ w = W → s ∈ 𝒫 Base w | I ↾ s LIndF w = s ∈ 𝒫 Base W | I ↾ s LIndF W
7 df-linds ⊢ LIndS = w ∈ V ⟼ s ∈ 𝒫 Base w | I ↾ s LIndF w
8 fvex ⊢ Base W ∈ V
9 8 pwex ⊢ 𝒫 Base W ∈ V
10 9 rabex ⊢ s ∈ 𝒫 Base W | I ↾ s LIndF W ∈ V
11 6 7 10 fvmpt ⊢ W ∈ V → LIndS ⁡ W = s ∈ 𝒫 Base W | I ↾ s LIndF W
12 2 11 syl ⊢ W ∈ V → LIndS ⁡ W = s ∈ 𝒫 Base W | I ↾ s LIndF W
13 12 eleq2d ⊢ W ∈ V → X ∈ LIndS ⁡ W ↔ X ∈ s ∈ 𝒫 Base W | I ↾ s LIndF W
14 reseq2 ⊢ s = X → I ↾ s = I ↾ X
15 14 breq1d ⊢ s = X → I ↾ s LIndF W ↔ I ↾ X LIndF W
16 15 elrab ⊢ X ∈ s ∈ 𝒫 Base W | I ↾ s LIndF W ↔ X ∈ 𝒫 Base W ∧ I ↾ X LIndF W
17 13 16 bitrdi ⊢ W ∈ V → X ∈ LIndS ⁡ W ↔ X ∈ 𝒫 Base W ∧ I ↾ X LIndF W
18 8 elpw2 ⊢ X ∈ 𝒫 Base W ↔ X ⊆ Base W
19 1 sseq2i ⊢ X ⊆ B ↔ X ⊆ Base W
20 18 19 bitr4i ⊢ X ∈ 𝒫 Base W ↔ X ⊆ B
21 20 anbi1i ⊢ X ∈ 𝒫 Base W ∧ I ↾ X LIndF W ↔ X ⊆ B ∧ I ↾ X LIndF W
22 17 21 bitrdi ⊢ W ∈ V → X ∈ LIndS ⁡ W ↔ X ⊆ B ∧ I ↾ X LIndF W