Metamath Proof Explorer

Theorem islindf

Description: Property of an independent family 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 islindf ( ( 𝑊 ∈ 𝑌 ∧ 𝐹 ∈ 𝑋 ) → ( 𝐹 LIndF 𝑊 ↔ ( 𝐹 : dom 𝐹 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ) ) )

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 feq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 : dom 𝑓 ⟶ ( Base ‘ 𝑤 ) ↔ 𝐹 : dom 𝑓 ⟶ ( Base ‘ 𝑤 ) ) )
8 7 adantr ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝑊 ) → ( 𝑓 : dom 𝑓 ⟶ ( Base ‘ 𝑤 ) ↔ 𝐹 : dom 𝑓 ⟶ ( Base ‘ 𝑤 ) ) )
9 dmeq ⊢ ( 𝑓 = 𝐹 → dom 𝑓 = dom 𝐹 )
10 9 adantr ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝑊 ) → dom 𝑓 = dom 𝐹 )
11 fveq2 ⊢ ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = ( Base ‘ 𝑊 ) )
12 11 1 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = 𝐵 )
13 12 adantl ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝑊 ) → ( Base ‘ 𝑤 ) = 𝐵 )
14 10 13 feq23d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝑊 ) → ( 𝐹 : dom 𝑓 ⟶ ( Base ‘ 𝑤 ) ↔ 𝐹 : dom 𝐹 ⟶ 𝐵 ) )
15 8 14 bitrd ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝑊 ) → ( 𝑓 : dom 𝑓 ⟶ ( Base ‘ 𝑤 ) ↔ 𝐹 : dom 𝐹 ⟶ 𝐵 ) )
16 fvex ⊢ ( Scalar ‘ 𝑤 ) ∈ V
17 fveq2 ⊢ ( 𝑠 = ( Scalar ‘ 𝑤 ) → ( Base ‘ 𝑠 ) = ( Base ‘ ( Scalar ‘ 𝑤 ) ) )
18 fveq2 ⊢ ( 𝑠 = ( Scalar ‘ 𝑤 ) → ( 0g ‘ 𝑠 ) = ( 0g ‘ ( Scalar ‘ 𝑤 ) ) )
19 18 sneqd ⊢ ( 𝑠 = ( Scalar ‘ 𝑤 ) → { ( 0g ‘ 𝑠 ) } = { ( 0g ‘ ( Scalar ‘ 𝑤 ) ) } )
20 17 19 difeq12d ⊢ ( 𝑠 = ( Scalar ‘ 𝑤 ) → ( ( Base ‘ 𝑠 ) ∖ { ( 0g ‘ 𝑠 ) } ) = ( ( Base ‘ ( Scalar ‘ 𝑤 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑤 ) ) } ) )
21 20 raleqdv ⊢ ( 𝑠 = ( Scalar ‘ 𝑤 ) → ( ∀ 𝑘 ∈ ( ( Base ‘ 𝑠 ) ∖ { ( 0g ‘ 𝑠 ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑤 ) ( 𝑓 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑓 “ ( dom 𝑓 ∖ { 𝑥 } ) ) ) ↔ ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑤 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑤 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑤 ) ( 𝑓 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑓 “ ( dom 𝑓 ∖ { 𝑥 } ) ) ) ) )
22 21 ralbidv ⊢ ( 𝑠 = ( Scalar ‘ 𝑤 ) → ( ∀ 𝑥 ∈ dom 𝑓 ∀ 𝑘 ∈ ( ( Base ‘ 𝑠 ) ∖ { ( 0g ‘ 𝑠 ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑤 ) ( 𝑓 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑓 “ ( dom 𝑓 ∖ { 𝑥 } ) ) ) ↔ ∀ 𝑥 ∈ dom 𝑓 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑤 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑤 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑤 ) ( 𝑓 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑓 “ ( dom 𝑓 ∖ { 𝑥 } ) ) ) ) )
23 16 22 sbcie ⊢ ( [ ( Scalar ‘ 𝑤 ) / 𝑠 ] ∀ 𝑥 ∈ dom 𝑓 ∀ 𝑘 ∈ ( ( Base ‘ 𝑠 ) ∖ { ( 0g ‘ 𝑠 ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑤 ) ( 𝑓 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑓 “ ( dom 𝑓 ∖ { 𝑥 } ) ) ) ↔ ∀ 𝑥 ∈ dom 𝑓 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑤 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑤 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑤 ) ( 𝑓 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑓 “ ( dom 𝑓 ∖ { 𝑥 } ) ) ) )
24 fveq2 ⊢ ( 𝑤 = 𝑊 → ( Scalar ‘ 𝑤 ) = ( Scalar ‘ 𝑊 ) )
25 24 4 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( Scalar ‘ 𝑤 ) = 𝑆 )
26 25 fveq2d ⊢ ( 𝑤 = 𝑊 → ( Base ‘ ( Scalar ‘ 𝑤 ) ) = ( Base ‘ 𝑆 ) )
27 26 5 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( Base ‘ ( Scalar ‘ 𝑤 ) ) = 𝑁 )
28 25 fveq2d ⊢ ( 𝑤 = 𝑊 → ( 0g ‘ ( Scalar ‘ 𝑤 ) ) = ( 0g ‘ 𝑆 ) )
29 28 6 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( 0g ‘ ( Scalar ‘ 𝑤 ) ) = 0 )
30 29 sneqd ⊢ ( 𝑤 = 𝑊 → { ( 0g ‘ ( Scalar ‘ 𝑤 ) ) } = { 0 } )
31 27 30 difeq12d ⊢ ( 𝑤 = 𝑊 → ( ( Base ‘ ( Scalar ‘ 𝑤 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑤 ) ) } ) = ( 𝑁 ∖ { 0 } ) )
32 31 adantl ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝑊 ) → ( ( Base ‘ ( Scalar ‘ 𝑤 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑤 ) ) } ) = ( 𝑁 ∖ { 0 } ) )
33 fveq2 ⊢ ( 𝑤 = 𝑊 → ( ·𝑠 ‘ 𝑤 ) = ( ·𝑠 ‘ 𝑊 ) )
34 33 2 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( ·𝑠 ‘ 𝑤 ) = · )
35 34 adantl ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝑊 ) → ( ·𝑠 ‘ 𝑤 ) = · )
36 eqidd ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝑊 ) → 𝑘 = 𝑘 )
37 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
38 37 adantr ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝑊 ) → ( 𝑓 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
39 35 36 38 oveq123d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝑊 ) → ( 𝑘 ( ·𝑠 ‘ 𝑤 ) ( 𝑓 ‘ 𝑥 ) ) = ( 𝑘 · ( 𝐹 ‘ 𝑥 ) ) )
40 fveq2 ⊢ ( 𝑤 = 𝑊 → ( LSpan ‘ 𝑤 ) = ( LSpan ‘ 𝑊 ) )
41 40 3 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( LSpan ‘ 𝑤 ) = 𝐾 )
42 41 adantl ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝑊 ) → ( LSpan ‘ 𝑤 ) = 𝐾 )
43 imaeq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 “ ( dom 𝑓 ∖ { 𝑥 } ) ) = ( 𝐹 “ ( dom 𝑓 ∖ { 𝑥 } ) ) )
44 9 difeq1d ⊢ ( 𝑓 = 𝐹 → ( dom 𝑓 ∖ { 𝑥 } ) = ( dom 𝐹 ∖ { 𝑥 } ) )
45 44 imaeq2d ⊢ ( 𝑓 = 𝐹 → ( 𝐹 “ ( dom 𝑓 ∖ { 𝑥 } ) ) = ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) )
46 43 45 eqtrd ⊢ ( 𝑓 = 𝐹 → ( 𝑓 “ ( dom 𝑓 ∖ { 𝑥 } ) ) = ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) )
47 46 adantr ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝑊 ) → ( 𝑓 “ ( dom 𝑓 ∖ { 𝑥 } ) ) = ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) )
48 42 47 fveq12d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝑊 ) → ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑓 “ ( dom 𝑓 ∖ { 𝑥 } ) ) ) = ( 𝐾 ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) )
49 39 48 eleq12d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝑊 ) → ( ( 𝑘 ( ·𝑠 ‘ 𝑤 ) ( 𝑓 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑓 “ ( dom 𝑓 ∖ { 𝑥 } ) ) ) ↔ ( 𝑘 · ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ) )
50 49 notbid ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝑊 ) → ( ¬ ( 𝑘 ( ·𝑠 ‘ 𝑤 ) ( 𝑓 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑓 “ ( dom 𝑓 ∖ { 𝑥 } ) ) ) ↔ ¬ ( 𝑘 · ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ) )
51 32 50 raleqbidv ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝑊 ) → ( ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑤 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑤 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑤 ) ( 𝑓 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑓 “ ( dom 𝑓 ∖ { 𝑥 } ) ) ) ↔ ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ) )
52 10 51 raleqbidv ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝑊 ) → ( ∀ 𝑥 ∈ dom 𝑓 ∀ 𝑘 ∈ ( ( Base ‘ ( Scalar ‘ 𝑤 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑤 ) ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑤 ) ( 𝑓 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑓 “ ( dom 𝑓 ∖ { 𝑥 } ) ) ) ↔ ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ) )
53 23 52 syl5bb ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝑊 ) → ( [ ( Scalar ‘ 𝑤 ) / 𝑠 ] ∀ 𝑥 ∈ dom 𝑓 ∀ 𝑘 ∈ ( ( Base ‘ 𝑠 ) ∖ { ( 0g ‘ 𝑠 ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑤 ) ( 𝑓 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑓 “ ( dom 𝑓 ∖ { 𝑥 } ) ) ) ↔ ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ) )
54 15 53 anbi12d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑤 = 𝑊 ) → ( ( 𝑓 : dom 𝑓 ⟶ ( Base ‘ 𝑤 ) ∧ [ ( Scalar ‘ 𝑤 ) / 𝑠 ] ∀ 𝑥 ∈ dom 𝑓 ∀ 𝑘 ∈ ( ( Base ‘ 𝑠 ) ∖ { ( 0g ‘ 𝑠 ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑤 ) ( 𝑓 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑓 “ ( dom 𝑓 ∖ { 𝑥 } ) ) ) ) ↔ ( 𝐹 : dom 𝐹 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ) ) )
55 df-lindf ⊢ LIndF = { ⟨ 𝑓 , 𝑤 ⟩ ∣ ( 𝑓 : dom 𝑓 ⟶ ( Base ‘ 𝑤 ) ∧ [ ( Scalar ‘ 𝑤 ) / 𝑠 ] ∀ 𝑥 ∈ dom 𝑓 ∀ 𝑘 ∈ ( ( Base ‘ 𝑠 ) ∖ { ( 0g ‘ 𝑠 ) } ) ¬ ( 𝑘 ( ·𝑠 ‘ 𝑤 ) ( 𝑓 ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ 𝑤 ) ‘ ( 𝑓 “ ( dom 𝑓 ∖ { 𝑥 } ) ) ) ) }
56 54 55 brabga ⊢ ( ( 𝐹 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌 ) → ( 𝐹 LIndF 𝑊 ↔ ( 𝐹 : dom 𝐹 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ) ) )
57 56 ancoms ⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐹 ∈ 𝑋 ) → ( 𝐹 LIndF 𝑊 ↔ ( 𝐹 : dom 𝐹 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑘 ∈ ( 𝑁 ∖ { 0 } ) ¬ ( 𝑘 · ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐾 ‘ ( 𝐹 “ ( dom 𝐹 ∖ { 𝑥 } ) ) ) ) ) )