Metamath Proof Explorer

Theorem islinds2

Description: Expanded property of an independent set of vectors. (Contributed by Stefan O'Rear, 24-Feb-2015)

Ref Expression
Hypotheses islindf.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
islindf.v ⊢ · = ( ·𝑠 ‘ 𝑊 )
islindf.k ⊢ 𝐾 = ( LSpan ‘ 𝑊 )
islindf.s ⊢ 𝑆 = ( Scalar ‘ 𝑊 )
islindf.n ⊢ 𝑁 = ( Base ‘ 𝑆 )
islindf.z ⊢ 0 = ( 0g ‘ 𝑆 )
Assertion islinds2 ( 𝑊 ∈ 𝑌 → ( 𝐹 ∈ ( LIndS ‘ 𝑊 ) ↔ ( 𝐹 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · 𝑥 ) ∈ ( 𝐾 ‘ ( 𝐹 ∖ { 𝑥 } ) ) ) ) )

Proof

Step Hyp Ref Expression
1 islindf.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
2 islindf.v ⊢ · = ( ·𝑠 ‘ 𝑊 )
3 islindf.k ⊢ 𝐾 = ( LSpan ‘ 𝑊 )
4 islindf.s ⊢ 𝑆 = ( Scalar ‘ 𝑊 )
5 islindf.n ⊢ 𝑁 = ( Base ‘ 𝑆 )
6 islindf.z ⊢ 0 = ( 0g ‘ 𝑆 )
7 1 islinds ⊢ ( 𝑊 ∈ 𝑌 → ( 𝐹 ∈ ( LIndS ‘ 𝑊 ) ↔ ( 𝐹 ⊆ 𝐵 ∧ ( I ↾ 𝐹 ) LIndF 𝑊 ) ) )
8 1 fvexi ⊢ 𝐵 ∈ V
9 8 ssex ⊢ ( 𝐹 ⊆ 𝐵 → 𝐹 ∈ V )
10 9 adantl ⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐹 ⊆ 𝐵 ) → 𝐹 ∈ V )
11 resiexg ⊢ ( 𝐹 ∈ V → ( I ↾ 𝐹 ) ∈ V )
12 10 11 syl ⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐹 ⊆ 𝐵 ) → ( I ↾ 𝐹 ) ∈ V )
13 1 2 3 4 5 6 islindf ⊢ ( ( 𝑊 ∈ 𝑌 ∧ ( I ↾ 𝐹 ) ∈ V ) → ( ( I ↾ 𝐹 ) LIndF 𝑊 ↔ ( ( I ↾ 𝐹 ) : dom ( I ↾ 𝐹 ) ⟶ 𝐵 ∧ ∀ 𝑥 ∈ dom ( I ↾ 𝐹 ) ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( ( I ↾ 𝐹 ) ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( ( I ↾ 𝐹 ) “ ( dom ( I ↾ 𝐹 ) ∖ { 𝑥 } ) ) ) ) ) )
14 12 13 syldan ⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐹 ⊆ 𝐵 ) → ( ( I ↾ 𝐹 ) LIndF 𝑊 ↔ ( ( I ↾ 𝐹 ) : dom ( I ↾ 𝐹 ) ⟶ 𝐵 ∧ ∀ 𝑥 ∈ dom ( I ↾ 𝐹 ) ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( ( I ↾ 𝐹 ) ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( ( I ↾ 𝐹 ) “ ( dom ( I ↾ 𝐹 ) ∖ { 𝑥 } ) ) ) ) ) )
15 14 pm5.32da ⊢ ( 𝑊 ∈ 𝑌 → ( ( 𝐹 ⊆ 𝐵 ∧ ( I ↾ 𝐹 ) LIndF 𝑊 ) ↔ ( 𝐹 ⊆ 𝐵 ∧ ( ( I ↾ 𝐹 ) : dom ( I ↾ 𝐹 ) ⟶ 𝐵 ∧ ∀ 𝑥 ∈ dom ( I ↾ 𝐹 ) ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( ( I ↾ 𝐹 ) ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( ( I ↾ 𝐹 ) “ ( dom ( I ↾ 𝐹 ) ∖ { 𝑥 } ) ) ) ) ) ) )
16 dmresi ⊢ dom ( I ↾ 𝐹 ) = 𝐹
17 16 raleqi ⊢ ( ∀ 𝑥 ∈ dom ( I ↾ 𝐹 ) ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( ( I ↾ 𝐹 ) ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( ( I ↾ 𝐹 ) “ ( dom ( I ↾ 𝐹 ) ∖ { 𝑥 } ) ) ) ↔ ∀ 𝑥 ∈ 𝐹 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( ( I ↾ 𝐹 ) ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( ( I ↾ 𝐹 ) “ ( dom ( I ↾ 𝐹 ) ∖ { 𝑥 } ) ) ) )
18 fvresi ⊢ ( 𝑥 ∈ 𝐹 → ( ( I ↾ 𝐹 ) ‘ 𝑥 ) = 𝑥 )
19 18 oveq2d ⊢ ( 𝑥 ∈ 𝐹 → ( 𝑘 · ( ( I ↾ 𝐹 ) ‘ 𝑥 ) ) = ( 𝑘 · 𝑥 ) )
20 16 difeq1i ⊢ ( dom ( I ↾ 𝐹 ) ∖ { 𝑥 } ) = ( 𝐹 ∖ { 𝑥 } )
21 20 imaeq2i ⊢ ( ( I ↾ 𝐹 ) “ ( dom ( I ↾ 𝐹 ) ∖ { 𝑥 } ) ) = ( ( I ↾ 𝐹 ) “ ( 𝐹 ∖ { 𝑥 } ) )
22 difss ⊢ ( 𝐹 ∖ { 𝑥 } ) ⊆ 𝐹
23 resiima ⊢ ( ( 𝐹 ∖ { 𝑥 } ) ⊆ 𝐹 → ( ( I ↾ 𝐹 ) “ ( 𝐹 ∖ { 𝑥 } ) ) = ( 𝐹 ∖ { 𝑥 } ) )
24 22 23 ax-mp ⊢ ( ( I ↾ 𝐹 ) “ ( 𝐹 ∖ { 𝑥 } ) ) = ( 𝐹 ∖ { 𝑥 } )
25 21 24 eqtri ⊢ ( ( I ↾ 𝐹 ) “ ( dom ( I ↾ 𝐹 ) ∖ { 𝑥 } ) ) = ( 𝐹 ∖ { 𝑥 } )
26 25 fveq2i ⊢ ( 𝐾 ‘ ( ( I ↾ 𝐹 ) “ ( dom ( I ↾ 𝐹 ) ∖ { 𝑥 } ) ) ) = ( 𝐾 ‘ ( 𝐹 ∖ { 𝑥 } ) )
27 26 a1i ⊢ ( 𝑥 ∈ 𝐹 → ( 𝐾 ‘ ( ( I ↾ 𝐹 ) “ ( dom ( I ↾ 𝐹 ) ∖ { 𝑥 } ) ) ) = ( 𝐾 ‘ ( 𝐹 ∖ { 𝑥 } ) ) )
28 19 27 eleq12d ⊢ ( 𝑥 ∈ 𝐹 → ( ( 𝑘 · ( ( I ↾ 𝐹 ) ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( ( I ↾ 𝐹 ) “ ( dom ( I ↾ 𝐹 ) ∖ { 𝑥 } ) ) ) ↔ ( 𝑘 · 𝑥 ) ∈ ( 𝐾 ‘ ( 𝐹 ∖ { 𝑥 } ) ) ) )
29 28 notbid ⊢ ( 𝑥 ∈ 𝐹 → ( ¬ ( 𝑘 · ( ( I ↾ 𝐹 ) ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( ( I ↾ 𝐹 ) “ ( dom ( I ↾ 𝐹 ) ∖ { 𝑥 } ) ) ) ↔ ¬ ( 𝑘 · 𝑥 ) ∈ ( 𝐾 ‘ ( 𝐹 ∖ { 𝑥 } ) ) ) )
30 29 ralbidv ⊢ ( 𝑥 ∈ 𝐹 → ( ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( ( I ↾ 𝐹 ) ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( ( I ↾ 𝐹 ) “ ( dom ( I ↾ 𝐹 ) ∖ { 𝑥 } ) ) ) ↔ ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · 𝑥 ) ∈ ( 𝐾 ‘ ( 𝐹 ∖ { 𝑥 } ) ) ) )
31 30 ralbiia ⊢ ( ∀ 𝑥 ∈ 𝐹 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( ( I ↾ 𝐹 ) ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( ( I ↾ 𝐹 ) “ ( dom ( I ↾ 𝐹 ) ∖ { 𝑥 } ) ) ) ↔ ∀ 𝑥 ∈ 𝐹 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · 𝑥 ) ∈ ( 𝐾 ‘ ( 𝐹 ∖ { 𝑥 } ) ) )
32 17 31 bitri ⊢ ( ∀ 𝑥 ∈ dom ( I ↾ 𝐹 ) ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( ( I ↾ 𝐹 ) ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( ( I ↾ 𝐹 ) “ ( dom ( I ↾ 𝐹 ) ∖ { 𝑥 } ) ) ) ↔ ∀ 𝑥 ∈ 𝐹 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · 𝑥 ) ∈ ( 𝐾 ‘ ( 𝐹 ∖ { 𝑥 } ) ) )
33 32 anbi2i ⊢ ( ( ( I ↾ 𝐹 ) : dom ( I ↾ 𝐹 ) ⟶ 𝐵 ∧ ∀ 𝑥 ∈ dom ( I ↾ 𝐹 ) ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( ( I ↾ 𝐹 ) ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( ( I ↾ 𝐹 ) “ ( dom ( I ↾ 𝐹 ) ∖ { 𝑥 } ) ) ) ) ↔ ( ( I ↾ 𝐹 ) : dom ( I ↾ 𝐹 ) ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · 𝑥 ) ∈ ( 𝐾 ‘ ( 𝐹 ∖ { 𝑥 } ) ) ) )
34 f1oi ⊢ ( I ↾ 𝐹 ) : 𝐹 –1-1-onto→ 𝐹
35 f1of ⊢ ( ( I ↾ 𝐹 ) : 𝐹 –1-1-onto→ 𝐹 → ( I ↾ 𝐹 ) : 𝐹 ⟶ 𝐹 )
36 34 35 ax-mp ⊢ ( I ↾ 𝐹 ) : 𝐹 ⟶ 𝐹
37 16 feq2i ⊢ ( ( I ↾ 𝐹 ) : dom ( I ↾ 𝐹 ) ⟶ 𝐹 ↔ ( I ↾ 𝐹 ) : 𝐹 ⟶ 𝐹 )
38 36 37 mpbir ⊢ ( I ↾ 𝐹 ) : dom ( I ↾ 𝐹 ) ⟶ 𝐹
39 fss ⊢ ( ( ( I ↾ 𝐹 ) : dom ( I ↾ 𝐹 ) ⟶ 𝐹 ∧ 𝐹 ⊆ 𝐵 ) → ( I ↾ 𝐹 ) : dom ( I ↾ 𝐹 ) ⟶ 𝐵 )
40 38 39 mpan ⊢ ( 𝐹 ⊆ 𝐵 → ( I ↾ 𝐹 ) : dom ( I ↾ 𝐹 ) ⟶ 𝐵 )
41 40 biantrurd ⊢ ( 𝐹 ⊆ 𝐵 → ( ∀ 𝑥 ∈ 𝐹 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · 𝑥 ) ∈ ( 𝐾 ‘ ( 𝐹 ∖ { 𝑥 } ) ) ↔ ( ( I ↾ 𝐹 ) : dom ( I ↾ 𝐹 ) ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · 𝑥 ) ∈ ( 𝐾 ‘ ( 𝐹 ∖ { 𝑥 } ) ) ) ) )
42 33 41 bitr4id ⊢ ( 𝐹 ⊆ 𝐵 → ( ( ( I ↾ 𝐹 ) : dom ( I ↾ 𝐹 ) ⟶ 𝐵 ∧ ∀ 𝑥 ∈ dom ( I ↾ 𝐹 ) ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( ( I ↾ 𝐹 ) ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( ( I ↾ 𝐹 ) “ ( dom ( I ↾ 𝐹 ) ∖ { 𝑥 } ) ) ) ) ↔ ∀ 𝑥 ∈ 𝐹 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · 𝑥 ) ∈ ( 𝐾 ‘ ( 𝐹 ∖ { 𝑥 } ) ) ) )
43 42 pm5.32i ⊢ ( ( 𝐹 ⊆ 𝐵 ∧ ( ( I ↾ 𝐹 ) : dom ( I ↾ 𝐹 ) ⟶ 𝐵 ∧ ∀ 𝑥 ∈ dom ( I ↾ 𝐹 ) ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( ( I ↾ 𝐹 ) ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( ( I ↾ 𝐹 ) “ ( dom ( I ↾ 𝐹 ) ∖ { 𝑥 } ) ) ) ) ) ↔ ( 𝐹 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · 𝑥 ) ∈ ( 𝐾 ‘ ( 𝐹 ∖ { 𝑥 } ) ) ) )
44 43 a1i ⊢ ( 𝑊 ∈ 𝑌 → ( ( 𝐹 ⊆ 𝐵 ∧ ( ( I ↾ 𝐹 ) : dom ( I ↾ 𝐹 ) ⟶ 𝐵 ∧ ∀ 𝑥 ∈ dom ( I ↾ 𝐹 ) ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( ( I ↾ 𝐹 ) ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( ( I ↾ 𝐹 ) “ ( dom ( I ↾ 𝐹 ) ∖ { 𝑥 } ) ) ) ) ) ↔ ( 𝐹 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · 𝑥 ) ∈ ( 𝐾 ‘ ( 𝐹 ∖ { 𝑥 } ) ) ) ) )
45 7 15 44 3bitrd ⊢ ( 𝑊 ∈ 𝑌 → ( 𝐹 ∈ ( LIndS ‘ 𝑊 ) ↔ ( 𝐹 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · 𝑥 ) ∈ ( 𝐾 ‘ ( 𝐹 ∖ { 𝑥 } ) ) ) ) )