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