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 𝐵 = ( Base ‘ 𝑊 )
Assertion islinds ( 𝑊𝑉 → ( 𝑋 ∈ ( LIndS ‘ 𝑊 ) ↔ ( 𝑋𝐵 ∧ ( I ↾ 𝑋 ) LIndF 𝑊 ) ) )

Proof

Step Hyp Ref Expression
1 islinds.b 𝐵 = ( Base ‘ 𝑊 )
2 elex ( 𝑊𝑉𝑊 ∈ V )
3 fveq2 ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = ( Base ‘ 𝑊 ) )
4 3 pweqd ( 𝑤 = 𝑊 → 𝒫 ( Base ‘ 𝑤 ) = 𝒫 ( Base ‘ 𝑊 ) )
5 breq2 ( 𝑤 = 𝑊 → ( ( I ↾ 𝑠 ) LIndF 𝑤 ↔ ( I ↾ 𝑠 ) LIndF 𝑊 ) )
6 4 5 rabeqbidv ( 𝑤 = 𝑊 → { 𝑠 ∈ 𝒫 ( Base ‘ 𝑤 ) ∣ ( I ↾ 𝑠 ) LIndF 𝑤 } = { 𝑠 ∈ 𝒫 ( Base ‘ 𝑊 ) ∣ ( I ↾ 𝑠 ) LIndF 𝑊 } )
7 df-linds LIndS = ( 𝑤 ∈ V ↦ { 𝑠 ∈ 𝒫 ( Base ‘ 𝑤 ) ∣ ( I ↾ 𝑠 ) LIndF 𝑤 } )
8 fvex ( Base ‘ 𝑊 ) ∈ V
9 8 pwex 𝒫 ( Base ‘ 𝑊 ) ∈ V
10 9 rabex { 𝑠 ∈ 𝒫 ( Base ‘ 𝑊 ) ∣ ( I ↾ 𝑠 ) LIndF 𝑊 } ∈ V
11 6 7 10 fvmpt ( 𝑊 ∈ V → ( LIndS ‘ 𝑊 ) = { 𝑠 ∈ 𝒫 ( Base ‘ 𝑊 ) ∣ ( I ↾ 𝑠 ) LIndF 𝑊 } )
12 2 11 syl ( 𝑊𝑉 → ( LIndS ‘ 𝑊 ) = { 𝑠 ∈ 𝒫 ( Base ‘ 𝑊 ) ∣ ( I ↾ 𝑠 ) LIndF 𝑊 } )
13 12 eleq2d ( 𝑊𝑉 → ( 𝑋 ∈ ( LIndS ‘ 𝑊 ) ↔ 𝑋 ∈ { 𝑠 ∈ 𝒫 ( Base ‘ 𝑊 ) ∣ ( I ↾ 𝑠 ) LIndF 𝑊 } ) )
14 reseq2 ( 𝑠 = 𝑋 → ( I ↾ 𝑠 ) = ( I ↾ 𝑋 ) )
15 14 breq1d ( 𝑠 = 𝑋 → ( ( I ↾ 𝑠 ) LIndF 𝑊 ↔ ( I ↾ 𝑋 ) LIndF 𝑊 ) )
16 15 elrab ( 𝑋 ∈ { 𝑠 ∈ 𝒫 ( Base ‘ 𝑊 ) ∣ ( I ↾ 𝑠 ) LIndF 𝑊 } ↔ ( 𝑋 ∈ 𝒫 ( Base ‘ 𝑊 ) ∧ ( I ↾ 𝑋 ) LIndF 𝑊 ) )
17 13 16 bitrdi ( 𝑊𝑉 → ( 𝑋 ∈ ( LIndS ‘ 𝑊 ) ↔ ( 𝑋 ∈ 𝒫 ( Base ‘ 𝑊 ) ∧ ( I ↾ 𝑋 ) LIndF 𝑊 ) ) )
18 8 elpw2 ( 𝑋 ∈ 𝒫 ( Base ‘ 𝑊 ) ↔ 𝑋 ⊆ ( Base ‘ 𝑊 ) )
19 1 sseq2i ( 𝑋𝐵𝑋 ⊆ ( Base ‘ 𝑊 ) )
20 18 19 bitr4i ( 𝑋 ∈ 𝒫 ( Base ‘ 𝑊 ) ↔ 𝑋𝐵 )
21 20 anbi1i ( ( 𝑋 ∈ 𝒫 ( Base ‘ 𝑊 ) ∧ ( I ↾ 𝑋 ) LIndF 𝑊 ) ↔ ( 𝑋𝐵 ∧ ( I ↾ 𝑋 ) LIndF 𝑊 ) )
22 17 21 bitrdi ( 𝑊𝑉 → ( 𝑋 ∈ ( LIndS ‘ 𝑊 ) ↔ ( 𝑋𝐵 ∧ ( I ↾ 𝑋 ) LIndF 𝑊 ) ) )