Metamath Proof Explorer


Theorem islbs

Description: The predicate " B is a basis for the left module or vector space W ". A subset of the base set is a basis if zero is not in the set, it spans the set, and no nonzero multiple of an element of the basis is in the span of the rest of the family. (Contributed by Mario Carneiro, 24-Jun-2014) (Revised by Mario Carneiro, 14-Jan-2015)

Ref Expression
Hypotheses islbs.v 𝑉 = ( Base ‘ 𝑊 )
islbs.f 𝐹 = ( Scalar ‘ 𝑊 )
islbs.s · = ( ·𝑠𝑊 )
islbs.k 𝐾 = ( Base ‘ 𝐹 )
islbs.j 𝐽 = ( LBasis ‘ 𝑊 )
islbs.n 𝑁 = ( LSpan ‘ 𝑊 )
islbs.z 0 = ( 0g𝐹 )
Assertion islbs ( 𝑊𝑋 → ( 𝐵𝐽 ↔ ( 𝐵𝑉 ∧ ( 𝑁𝐵 ) = 𝑉 ∧ ∀ 𝑥𝐵𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) )

Proof

Step Hyp Ref Expression
1 islbs.v 𝑉 = ( Base ‘ 𝑊 )
2 islbs.f 𝐹 = ( Scalar ‘ 𝑊 )
3 islbs.s · = ( ·𝑠𝑊 )
4 islbs.k 𝐾 = ( Base ‘ 𝐹 )
5 islbs.j 𝐽 = ( LBasis ‘ 𝑊 )
6 islbs.n 𝑁 = ( LSpan ‘ 𝑊 )
7 islbs.z 0 = ( 0g𝐹 )
8 elex ( 𝑊𝑋𝑊 ∈ V )
9 fveq2 ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = ( Base ‘ 𝑊 ) )
10 9 1 eqtr4di ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = 𝑉 )
11 10 pweqd ( 𝑤 = 𝑊 → 𝒫 ( Base ‘ 𝑤 ) = 𝒫 𝑉 )
12 fvexd ( 𝑤 = 𝑊 → ( LSpan ‘ 𝑤 ) ∈ V )
13 fveq2 ( 𝑤 = 𝑊 → ( LSpan ‘ 𝑤 ) = ( LSpan ‘ 𝑊 ) )
14 13 6 eqtr4di ( 𝑤 = 𝑊 → ( LSpan ‘ 𝑤 ) = 𝑁 )
15 fvexd ( ( 𝑤 = 𝑊𝑛 = 𝑁 ) → ( Scalar ‘ 𝑤 ) ∈ V )
16 fveq2 ( 𝑤 = 𝑊 → ( Scalar ‘ 𝑤 ) = ( Scalar ‘ 𝑊 ) )
17 16 adantr ( ( 𝑤 = 𝑊𝑛 = 𝑁 ) → ( Scalar ‘ 𝑤 ) = ( Scalar ‘ 𝑊 ) )
18 17 2 eqtr4di ( ( 𝑤 = 𝑊𝑛 = 𝑁 ) → ( Scalar ‘ 𝑤 ) = 𝐹 )
19 simplr ( ( ( 𝑤 = 𝑊𝑛 = 𝑁 ) ∧ 𝑓 = 𝐹 ) → 𝑛 = 𝑁 )
20 19 fveq1d ( ( ( 𝑤 = 𝑊𝑛 = 𝑁 ) ∧ 𝑓 = 𝐹 ) → ( 𝑛𝑏 ) = ( 𝑁𝑏 ) )
21 10 ad2antrr ( ( ( 𝑤 = 𝑊𝑛 = 𝑁 ) ∧ 𝑓 = 𝐹 ) → ( Base ‘ 𝑤 ) = 𝑉 )
22 20 21 eqeq12d ( ( ( 𝑤 = 𝑊𝑛 = 𝑁 ) ∧ 𝑓 = 𝐹 ) → ( ( 𝑛𝑏 ) = ( Base ‘ 𝑤 ) ↔ ( 𝑁𝑏 ) = 𝑉 ) )
23 simpr ( ( ( 𝑤 = 𝑊𝑛 = 𝑁 ) ∧ 𝑓 = 𝐹 ) → 𝑓 = 𝐹 )
24 23 fveq2d ( ( ( 𝑤 = 𝑊𝑛 = 𝑁 ) ∧ 𝑓 = 𝐹 ) → ( Base ‘ 𝑓 ) = ( Base ‘ 𝐹 ) )
25 24 4 eqtr4di ( ( ( 𝑤 = 𝑊𝑛 = 𝑁 ) ∧ 𝑓 = 𝐹 ) → ( Base ‘ 𝑓 ) = 𝐾 )
26 23 fveq2d ( ( ( 𝑤 = 𝑊𝑛 = 𝑁 ) ∧ 𝑓 = 𝐹 ) → ( 0g𝑓 ) = ( 0g𝐹 ) )
27 26 7 eqtr4di ( ( ( 𝑤 = 𝑊𝑛 = 𝑁 ) ∧ 𝑓 = 𝐹 ) → ( 0g𝑓 ) = 0 )
28 27 sneqd ( ( ( 𝑤 = 𝑊𝑛 = 𝑁 ) ∧ 𝑓 = 𝐹 ) → { ( 0g𝑓 ) } = { 0 } )
29 25 28 difeq12d ( ( ( 𝑤 = 𝑊𝑛 = 𝑁 ) ∧ 𝑓 = 𝐹 ) → ( ( Base ‘ 𝑓 ) ∖ { ( 0g𝑓 ) } ) = ( 𝐾 ∖ { 0 } ) )
30 fveq2 ( 𝑤 = 𝑊 → ( ·𝑠𝑤 ) = ( ·𝑠𝑊 ) )
31 30 3 eqtr4di ( 𝑤 = 𝑊 → ( ·𝑠𝑤 ) = · )
32 31 ad2antrr ( ( ( 𝑤 = 𝑊𝑛 = 𝑁 ) ∧ 𝑓 = 𝐹 ) → ( ·𝑠𝑤 ) = · )
33 32 oveqd ( ( ( 𝑤 = 𝑊𝑛 = 𝑁 ) ∧ 𝑓 = 𝐹 ) → ( 𝑦 ( ·𝑠𝑤 ) 𝑥 ) = ( 𝑦 · 𝑥 ) )
34 19 fveq1d ( ( ( 𝑤 = 𝑊𝑛 = 𝑁 ) ∧ 𝑓 = 𝐹 ) → ( 𝑛 ‘ ( 𝑏 ∖ { 𝑥 } ) ) = ( 𝑁 ‘ ( 𝑏 ∖ { 𝑥 } ) ) )
35 33 34 eleq12d ( ( ( 𝑤 = 𝑊𝑛 = 𝑁 ) ∧ 𝑓 = 𝐹 ) → ( ( 𝑦 ( ·𝑠𝑤 ) 𝑥 ) ∈ ( 𝑛 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ↔ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ) )
36 35 notbid ( ( ( 𝑤 = 𝑊𝑛 = 𝑁 ) ∧ 𝑓 = 𝐹 ) → ( ¬ ( 𝑦 ( ·𝑠𝑤 ) 𝑥 ) ∈ ( 𝑛 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ↔ ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ) )
37 29 36 raleqbidv ( ( ( 𝑤 = 𝑊𝑛 = 𝑁 ) ∧ 𝑓 = 𝐹 ) → ( ∀ 𝑦 ∈ ( ( Base ‘ 𝑓 ) ∖ { ( 0g𝑓 ) } ) ¬ ( 𝑦 ( ·𝑠𝑤 ) 𝑥 ) ∈ ( 𝑛 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ↔ ∀ 𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ) )
38 37 ralbidv ( ( ( 𝑤 = 𝑊𝑛 = 𝑁 ) ∧ 𝑓 = 𝐹 ) → ( ∀ 𝑥𝑏𝑦 ∈ ( ( Base ‘ 𝑓 ) ∖ { ( 0g𝑓 ) } ) ¬ ( 𝑦 ( ·𝑠𝑤 ) 𝑥 ) ∈ ( 𝑛 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ↔ ∀ 𝑥𝑏𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ) )
39 22 38 anbi12d ( ( ( 𝑤 = 𝑊𝑛 = 𝑁 ) ∧ 𝑓 = 𝐹 ) → ( ( ( 𝑛𝑏 ) = ( Base ‘ 𝑤 ) ∧ ∀ 𝑥𝑏𝑦 ∈ ( ( Base ‘ 𝑓 ) ∖ { ( 0g𝑓 ) } ) ¬ ( 𝑦 ( ·𝑠𝑤 ) 𝑥 ) ∈ ( 𝑛 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ) ↔ ( ( 𝑁𝑏 ) = 𝑉 ∧ ∀ 𝑥𝑏𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ) ) )
40 15 18 39 sbcied2 ( ( 𝑤 = 𝑊𝑛 = 𝑁 ) → ( [ ( Scalar ‘ 𝑤 ) / 𝑓 ] ( ( 𝑛𝑏 ) = ( Base ‘ 𝑤 ) ∧ ∀ 𝑥𝑏𝑦 ∈ ( ( Base ‘ 𝑓 ) ∖ { ( 0g𝑓 ) } ) ¬ ( 𝑦 ( ·𝑠𝑤 ) 𝑥 ) ∈ ( 𝑛 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ) ↔ ( ( 𝑁𝑏 ) = 𝑉 ∧ ∀ 𝑥𝑏𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ) ) )
41 12 14 40 sbcied2 ( 𝑤 = 𝑊 → ( [ ( LSpan ‘ 𝑤 ) / 𝑛 ] [ ( Scalar ‘ 𝑤 ) / 𝑓 ] ( ( 𝑛𝑏 ) = ( Base ‘ 𝑤 ) ∧ ∀ 𝑥𝑏𝑦 ∈ ( ( Base ‘ 𝑓 ) ∖ { ( 0g𝑓 ) } ) ¬ ( 𝑦 ( ·𝑠𝑤 ) 𝑥 ) ∈ ( 𝑛 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ) ↔ ( ( 𝑁𝑏 ) = 𝑉 ∧ ∀ 𝑥𝑏𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ) ) )
42 11 41 rabeqbidv ( 𝑤 = 𝑊 → { 𝑏 ∈ 𝒫 ( Base ‘ 𝑤 ) ∣ [ ( LSpan ‘ 𝑤 ) / 𝑛 ] [ ( Scalar ‘ 𝑤 ) / 𝑓 ] ( ( 𝑛𝑏 ) = ( Base ‘ 𝑤 ) ∧ ∀ 𝑥𝑏𝑦 ∈ ( ( Base ‘ 𝑓 ) ∖ { ( 0g𝑓 ) } ) ¬ ( 𝑦 ( ·𝑠𝑤 ) 𝑥 ) ∈ ( 𝑛 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ) } = { 𝑏 ∈ 𝒫 𝑉 ∣ ( ( 𝑁𝑏 ) = 𝑉 ∧ ∀ 𝑥𝑏𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ) } )
43 df-lbs LBasis = ( 𝑤 ∈ V ↦ { 𝑏 ∈ 𝒫 ( Base ‘ 𝑤 ) ∣ [ ( LSpan ‘ 𝑤 ) / 𝑛 ] [ ( Scalar ‘ 𝑤 ) / 𝑓 ] ( ( 𝑛𝑏 ) = ( Base ‘ 𝑤 ) ∧ ∀ 𝑥𝑏𝑦 ∈ ( ( Base ‘ 𝑓 ) ∖ { ( 0g𝑓 ) } ) ¬ ( 𝑦 ( ·𝑠𝑤 ) 𝑥 ) ∈ ( 𝑛 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ) } )
44 1 fvexi 𝑉 ∈ V
45 44 pwex 𝒫 𝑉 ∈ V
46 45 rabex { 𝑏 ∈ 𝒫 𝑉 ∣ ( ( 𝑁𝑏 ) = 𝑉 ∧ ∀ 𝑥𝑏𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ) } ∈ V
47 42 43 46 fvmpt ( 𝑊 ∈ V → ( LBasis ‘ 𝑊 ) = { 𝑏 ∈ 𝒫 𝑉 ∣ ( ( 𝑁𝑏 ) = 𝑉 ∧ ∀ 𝑥𝑏𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ) } )
48 5 47 syl5eq ( 𝑊 ∈ V → 𝐽 = { 𝑏 ∈ 𝒫 𝑉 ∣ ( ( 𝑁𝑏 ) = 𝑉 ∧ ∀ 𝑥𝑏𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ) } )
49 8 48 syl ( 𝑊𝑋𝐽 = { 𝑏 ∈ 𝒫 𝑉 ∣ ( ( 𝑁𝑏 ) = 𝑉 ∧ ∀ 𝑥𝑏𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ) } )
50 49 eleq2d ( 𝑊𝑋 → ( 𝐵𝐽𝐵 ∈ { 𝑏 ∈ 𝒫 𝑉 ∣ ( ( 𝑁𝑏 ) = 𝑉 ∧ ∀ 𝑥𝑏𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ) } ) )
51 44 elpw2 ( 𝐵 ∈ 𝒫 𝑉𝐵𝑉 )
52 51 anbi1i ( ( 𝐵 ∈ 𝒫 𝑉 ∧ ( ( 𝑁𝐵 ) = 𝑉 ∧ ∀ 𝑥𝐵𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) ↔ ( 𝐵𝑉 ∧ ( ( 𝑁𝐵 ) = 𝑉 ∧ ∀ 𝑥𝐵𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) )
53 fveqeq2 ( 𝑏 = 𝐵 → ( ( 𝑁𝑏 ) = 𝑉 ↔ ( 𝑁𝐵 ) = 𝑉 ) )
54 difeq1 ( 𝑏 = 𝐵 → ( 𝑏 ∖ { 𝑥 } ) = ( 𝐵 ∖ { 𝑥 } ) )
55 54 fveq2d ( 𝑏 = 𝐵 → ( 𝑁 ‘ ( 𝑏 ∖ { 𝑥 } ) ) = ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) )
56 55 eleq2d ( 𝑏 = 𝐵 → ( ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ↔ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) )
57 56 notbid ( 𝑏 = 𝐵 → ( ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ↔ ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) )
58 57 ralbidv ( 𝑏 = 𝐵 → ( ∀ 𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ↔ ∀ 𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) )
59 58 raleqbi1dv ( 𝑏 = 𝐵 → ( ∀ 𝑥𝑏𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ↔ ∀ 𝑥𝐵𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) )
60 53 59 anbi12d ( 𝑏 = 𝐵 → ( ( ( 𝑁𝑏 ) = 𝑉 ∧ ∀ 𝑥𝑏𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ) ↔ ( ( 𝑁𝐵 ) = 𝑉 ∧ ∀ 𝑥𝐵𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) )
61 60 elrab ( 𝐵 ∈ { 𝑏 ∈ 𝒫 𝑉 ∣ ( ( 𝑁𝑏 ) = 𝑉 ∧ ∀ 𝑥𝑏𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ) } ↔ ( 𝐵 ∈ 𝒫 𝑉 ∧ ( ( 𝑁𝐵 ) = 𝑉 ∧ ∀ 𝑥𝐵𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) )
62 3anass ( ( 𝐵𝑉 ∧ ( 𝑁𝐵 ) = 𝑉 ∧ ∀ 𝑥𝐵𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ↔ ( 𝐵𝑉 ∧ ( ( 𝑁𝐵 ) = 𝑉 ∧ ∀ 𝑥𝐵𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) )
63 52 61 62 3bitr4i ( 𝐵 ∈ { 𝑏 ∈ 𝒫 𝑉 ∣ ( ( 𝑁𝑏 ) = 𝑉 ∧ ∀ 𝑥𝑏𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝑏 ∖ { 𝑥 } ) ) ) } ↔ ( 𝐵𝑉 ∧ ( 𝑁𝐵 ) = 𝑉 ∧ ∀ 𝑥𝐵𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) )
64 50 63 bitrdi ( 𝑊𝑋 → ( 𝐵𝐽 ↔ ( 𝐵𝑉 ∧ ( 𝑁𝐵 ) = 𝑉 ∧ ∀ 𝑥𝐵𝑦 ∈ ( 𝐾 ∖ { 0 } ) ¬ ( 𝑦 · 𝑥 ) ∈ ( 𝑁 ‘ ( 𝐵 ∖ { 𝑥 } ) ) ) ) )