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

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 𝑊 ) ) )