Metamath Proof Explorer

Theorem islindf2

Description: Property of an independent family of vectors with prior constrained domain and codomain. (Contributed by Stefan O'Rear, 26-Feb-2015)

Ref Expression
Hypotheses islindf.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
islindf.v ⊢ · = ( ·𝑠 ‘ 𝑊 )
islindf.k ⊢ 𝐾 = ( LSpan ‘ 𝑊 )
islindf.s ⊢ 𝑆 = ( Scalar ‘ 𝑊 )
islindf.n ⊢ 𝑁 = ( Base ‘ 𝑆 )
islindf.z ⊢ 0 = ( 0g ‘ 𝑆 )
Assertion islindf2 ( ( 𝑊 ∈ 𝑌 ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( 𝐹 LIndF 𝑊 ↔ ∀ 𝑥 ∈ 𝐼 ∀ 𝑘 ∈ ( 𝑁 ∖ { 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 simp1 ⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → 𝑊 ∈ 𝑌 )
8 simp3 ⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → 𝐹 : 𝐼 ⟶ 𝐵 )
9 simp2 ⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → 𝐼 ∈ 𝑋 )
10 8 9 fexd ⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → 𝐹 ∈ V )
11 1 2 3 4 5 6 islindf ⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐹 ∈ V ) → ( 𝐹 LIndF 𝑊 ↔ ( 𝐹 : dom 𝐹 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ) ) )
12 7 10 11 syl2anc ⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( 𝐹 LIndF 𝑊 ↔ ( 𝐹 : dom 𝐹 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ) ) )
13 ffdm ⊢ ( 𝐹 : 𝐼 ⟶ 𝐵 → ( 𝐹 : dom 𝐹 ⟶ 𝐵 ∧ dom 𝐹 ⊆ 𝐼 ) )
14 13 simpld ⊢ ( 𝐹 : 𝐼 ⟶ 𝐵 → 𝐹 : dom 𝐹 ⟶ 𝐵 )
15 14 3ad2ant3 ⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → 𝐹 : dom 𝐹 ⟶ 𝐵 )
16 15 biantrurd ⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ↔ ( 𝐹 : dom 𝐹 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ) ) )
17 fdm ⊢ ( 𝐹 : 𝐼 ⟶ 𝐵 → dom 𝐹 = 𝐼 )
18 17 3ad2ant3 ⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → dom 𝐹 = 𝐼 )
19 18 difeq1d ⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( dom 𝐹 ∖ { 𝑥 } ) = ( 𝐼 ∖ { 𝑥 } ) )
20 19 imaeq2d ⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) = ( 𝐹 “ ( 𝐼 ∖ { 𝑥 } ) ) )
21 20 fveq2d ⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( 𝐾 ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) = ( 𝐾 ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑥 } ) ) ) )
22 21 eleq2d ⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( ( 𝑘 · ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ↔ ( 𝑘 · ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )
23 22 notbid ⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( ¬ ( 𝑘 · ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ↔ ¬ ( 𝑘 · ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )
24 23 ralbidv ⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ↔ ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )
25 18 24 raleqbidv ⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ↔ ∀ 𝑥 ∈ 𝐼 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )
26 12 16 25 3bitr2d ⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐼 ∈ 𝑋 ∧ 𝐹 : 𝐼 ⟶ 𝐵 ) → ( 𝐹 LIndF 𝑊 ↔ ∀ 𝑥 ∈ 𝐼 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( 𝐼 ∖ { 𝑥 } ) ) ) ) )