MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  islbs Structured version   Visualization version   GIF version

Theorem islbs 19278
Description: The predicate "𝐵 is a basis for the left module or vector space 𝑊". 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.)
Hypotheses
Ref Expression
islbs.v 𝑉 = (Base‘𝑊)
islbs.f 𝐹 = (Scalar‘𝑊)
islbs.s · = ( ·𝑠𝑊)
islbs.k 𝐾 = (Base‘𝐹)
islbs.j 𝐽 = (LBasis‘𝑊)
islbs.n 𝑁 = (LSpan‘𝑊)
islbs.z 0 = (0g𝐹)
Assertion
Ref Expression
islbs (𝑊𝑋 → (𝐵𝐽 ↔ (𝐵𝑉 ∧ (𝑁𝐵) = 𝑉 ∧ ∀𝑥𝐵𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥})))))
Distinct variable groups:   𝑥,𝑦,𝐵   𝑦,𝐾   𝑥,𝑁,𝑦   𝑥,𝑊,𝑦   𝑥,𝐹,𝑦   𝑦, 0
Allowed substitution hints:   · (𝑥,𝑦)   𝐽(𝑥,𝑦)   𝐾(𝑥)   𝑉(𝑥,𝑦)   𝑋(𝑥,𝑦)   0 (𝑥)

Proof of Theorem islbs
Dummy variables 𝑏 𝑓 𝑛 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elex 3352 . . . 4 (𝑊𝑋𝑊 ∈ V)
2 islbs.j . . . . 5 𝐽 = (LBasis‘𝑊)
3 fveq2 6352 . . . . . . . . 9 (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊))
4 islbs.v . . . . . . . . 9 𝑉 = (Base‘𝑊)
53, 4syl6eqr 2812 . . . . . . . 8 (𝑤 = 𝑊 → (Base‘𝑤) = 𝑉)
65pweqd 4307 . . . . . . 7 (𝑤 = 𝑊 → 𝒫 (Base‘𝑤) = 𝒫 𝑉)
7 fvexd 6364 . . . . . . . 8 (𝑤 = 𝑊 → (LSpan‘𝑤) ∈ V)
8 fveq2 6352 . . . . . . . . 9 (𝑤 = 𝑊 → (LSpan‘𝑤) = (LSpan‘𝑊))
9 islbs.n . . . . . . . . 9 𝑁 = (LSpan‘𝑊)
108, 9syl6eqr 2812 . . . . . . . 8 (𝑤 = 𝑊 → (LSpan‘𝑤) = 𝑁)
11 fvexd 6364 . . . . . . . . 9 ((𝑤 = 𝑊𝑛 = 𝑁) → (Scalar‘𝑤) ∈ V)
12 fveq2 6352 . . . . . . . . . . 11 (𝑤 = 𝑊 → (Scalar‘𝑤) = (Scalar‘𝑊))
1312adantr 472 . . . . . . . . . 10 ((𝑤 = 𝑊𝑛 = 𝑁) → (Scalar‘𝑤) = (Scalar‘𝑊))
14 islbs.f . . . . . . . . . 10 𝐹 = (Scalar‘𝑊)
1513, 14syl6eqr 2812 . . . . . . . . 9 ((𝑤 = 𝑊𝑛 = 𝑁) → (Scalar‘𝑤) = 𝐹)
16 simplr 809 . . . . . . . . . . . 12 (((𝑤 = 𝑊𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → 𝑛 = 𝑁)
1716fveq1d 6354 . . . . . . . . . . 11 (((𝑤 = 𝑊𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (𝑛𝑏) = (𝑁𝑏))
185ad2antrr 764 . . . . . . . . . . 11 (((𝑤 = 𝑊𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (Base‘𝑤) = 𝑉)
1917, 18eqeq12d 2775 . . . . . . . . . 10 (((𝑤 = 𝑊𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → ((𝑛𝑏) = (Base‘𝑤) ↔ (𝑁𝑏) = 𝑉))
20 simpr 479 . . . . . . . . . . . . . . 15 (((𝑤 = 𝑊𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → 𝑓 = 𝐹)
2120fveq2d 6356 . . . . . . . . . . . . . 14 (((𝑤 = 𝑊𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (Base‘𝑓) = (Base‘𝐹))
22 islbs.k . . . . . . . . . . . . . 14 𝐾 = (Base‘𝐹)
2321, 22syl6eqr 2812 . . . . . . . . . . . . 13 (((𝑤 = 𝑊𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (Base‘𝑓) = 𝐾)
2420fveq2d 6356 . . . . . . . . . . . . . . 15 (((𝑤 = 𝑊𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (0g𝑓) = (0g𝐹))
25 islbs.z . . . . . . . . . . . . . . 15 0 = (0g𝐹)
2624, 25syl6eqr 2812 . . . . . . . . . . . . . 14 (((𝑤 = 𝑊𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (0g𝑓) = 0 )
2726sneqd 4333 . . . . . . . . . . . . 13 (((𝑤 = 𝑊𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → {(0g𝑓)} = { 0 })
2823, 27difeq12d 3872 . . . . . . . . . . . 12 (((𝑤 = 𝑊𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → ((Base‘𝑓) ∖ {(0g𝑓)}) = (𝐾 ∖ { 0 }))
29 fveq2 6352 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑊 → ( ·𝑠𝑤) = ( ·𝑠𝑊))
30 islbs.s . . . . . . . . . . . . . . . . 17 · = ( ·𝑠𝑊)
3129, 30syl6eqr 2812 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑊 → ( ·𝑠𝑤) = · )
3231ad2antrr 764 . . . . . . . . . . . . . . 15 (((𝑤 = 𝑊𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → ( ·𝑠𝑤) = · )
3332oveqd 6830 . . . . . . . . . . . . . 14 (((𝑤 = 𝑊𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (𝑦( ·𝑠𝑤)𝑥) = (𝑦 · 𝑥))
3416fveq1d 6354 . . . . . . . . . . . . . 14 (((𝑤 = 𝑊𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (𝑛‘(𝑏 ∖ {𝑥})) = (𝑁‘(𝑏 ∖ {𝑥})))
3533, 34eleq12d 2833 . . . . . . . . . . . . 13 (((𝑤 = 𝑊𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → ((𝑦( ·𝑠𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})) ↔ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥}))))
3635notbid 307 . . . . . . . . . . . 12 (((𝑤 = 𝑊𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (¬ (𝑦( ·𝑠𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})) ↔ ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥}))))
3728, 36raleqbidv 3291 . . . . . . . . . . 11 (((𝑤 = 𝑊𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (∀𝑦 ∈ ((Base‘𝑓) ∖ {(0g𝑓)}) ¬ (𝑦( ·𝑠𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})) ↔ ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥}))))
3837ralbidv 3124 . . . . . . . . . 10 (((𝑤 = 𝑊𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (∀𝑥𝑏𝑦 ∈ ((Base‘𝑓) ∖ {(0g𝑓)}) ¬ (𝑦( ·𝑠𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})) ↔ ∀𝑥𝑏𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥}))))
3919, 38anbi12d 749 . . . . . . . . 9 (((𝑤 = 𝑊𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (((𝑛𝑏) = (Base‘𝑤) ∧ ∀𝑥𝑏𝑦 ∈ ((Base‘𝑓) ∖ {(0g𝑓)}) ¬ (𝑦( ·𝑠𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥}))) ↔ ((𝑁𝑏) = 𝑉 ∧ ∀𝑥𝑏𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))))
4011, 15, 39sbcied2 3614 . . . . . . . 8 ((𝑤 = 𝑊𝑛 = 𝑁) → ([(Scalar‘𝑤) / 𝑓]((𝑛𝑏) = (Base‘𝑤) ∧ ∀𝑥𝑏𝑦 ∈ ((Base‘𝑓) ∖ {(0g𝑓)}) ¬ (𝑦( ·𝑠𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥}))) ↔ ((𝑁𝑏) = 𝑉 ∧ ∀𝑥𝑏𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))))
417, 10, 40sbcied2 3614 . . . . . . 7 (𝑤 = 𝑊 → ([(LSpan‘𝑤) / 𝑛][(Scalar‘𝑤) / 𝑓]((𝑛𝑏) = (Base‘𝑤) ∧ ∀𝑥𝑏𝑦 ∈ ((Base‘𝑓) ∖ {(0g𝑓)}) ¬ (𝑦( ·𝑠𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥}))) ↔ ((𝑁𝑏) = 𝑉 ∧ ∀𝑥𝑏𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))))
426, 41rabeqbidv 3335 . . . . . 6 (𝑤 = 𝑊 → {𝑏 ∈ 𝒫 (Base‘𝑤) ∣ [(LSpan‘𝑤) / 𝑛][(Scalar‘𝑤) / 𝑓]((𝑛𝑏) = (Base‘𝑤) ∧ ∀𝑥𝑏𝑦 ∈ ((Base‘𝑓) ∖ {(0g𝑓)}) ¬ (𝑦( ·𝑠𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})))} = {𝑏 ∈ 𝒫 𝑉 ∣ ((𝑁𝑏) = 𝑉 ∧ ∀𝑥𝑏𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))})
43 df-lbs 19277 . . . . . 6 LBasis = (𝑤 ∈ V ↦ {𝑏 ∈ 𝒫 (Base‘𝑤) ∣ [(LSpan‘𝑤) / 𝑛][(Scalar‘𝑤) / 𝑓]((𝑛𝑏) = (Base‘𝑤) ∧ ∀𝑥𝑏𝑦 ∈ ((Base‘𝑓) ∖ {(0g𝑓)}) ¬ (𝑦( ·𝑠𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})))})
44 fvex 6362 . . . . . . . . 9 (Base‘𝑊) ∈ V
454, 44eqeltri 2835 . . . . . . . 8 𝑉 ∈ V
4645pwex 4997 . . . . . . 7 𝒫 𝑉 ∈ V
4746rabex 4964 . . . . . 6 {𝑏 ∈ 𝒫 𝑉 ∣ ((𝑁𝑏) = 𝑉 ∧ ∀𝑥𝑏𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))} ∈ V
4842, 43, 47fvmpt 6444 . . . . 5 (𝑊 ∈ V → (LBasis‘𝑊) = {𝑏 ∈ 𝒫 𝑉 ∣ ((𝑁𝑏) = 𝑉 ∧ ∀𝑥𝑏𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))})
492, 48syl5eq 2806 . . . 4 (𝑊 ∈ V → 𝐽 = {𝑏 ∈ 𝒫 𝑉 ∣ ((𝑁𝑏) = 𝑉 ∧ ∀𝑥𝑏𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))})
501, 49syl 17 . . 3 (𝑊𝑋𝐽 = {𝑏 ∈ 𝒫 𝑉 ∣ ((𝑁𝑏) = 𝑉 ∧ ∀𝑥𝑏𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))})
5150eleq2d 2825 . 2 (𝑊𝑋 → (𝐵𝐽𝐵 ∈ {𝑏 ∈ 𝒫 𝑉 ∣ ((𝑁𝑏) = 𝑉 ∧ ∀𝑥𝑏𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))}))
5245elpw2 4977 . . . 4 (𝐵 ∈ 𝒫 𝑉𝐵𝑉)
5352anbi1i 733 . . 3 ((𝐵 ∈ 𝒫 𝑉 ∧ ((𝑁𝐵) = 𝑉 ∧ ∀𝑥𝐵𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥})))) ↔ (𝐵𝑉 ∧ ((𝑁𝐵) = 𝑉 ∧ ∀𝑥𝐵𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥})))))
54 fveq2 6352 . . . . . 6 (𝑏 = 𝐵 → (𝑁𝑏) = (𝑁𝐵))
5554eqeq1d 2762 . . . . 5 (𝑏 = 𝐵 → ((𝑁𝑏) = 𝑉 ↔ (𝑁𝐵) = 𝑉))
56 difeq1 3864 . . . . . . . . . 10 (𝑏 = 𝐵 → (𝑏 ∖ {𝑥}) = (𝐵 ∖ {𝑥}))
5756fveq2d 6356 . . . . . . . . 9 (𝑏 = 𝐵 → (𝑁‘(𝑏 ∖ {𝑥})) = (𝑁‘(𝐵 ∖ {𝑥})))
5857eleq2d 2825 . . . . . . . 8 (𝑏 = 𝐵 → ((𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})) ↔ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥}))))
5958notbid 307 . . . . . . 7 (𝑏 = 𝐵 → (¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})) ↔ ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥}))))
6059ralbidv 3124 . . . . . 6 (𝑏 = 𝐵 → (∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})) ↔ ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥}))))
6160raleqbi1dv 3285 . . . . 5 (𝑏 = 𝐵 → (∀𝑥𝑏𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})) ↔ ∀𝑥𝐵𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥}))))
6255, 61anbi12d 749 . . . 4 (𝑏 = 𝐵 → (((𝑁𝑏) = 𝑉 ∧ ∀𝑥𝑏𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥}))) ↔ ((𝑁𝐵) = 𝑉 ∧ ∀𝑥𝐵𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥})))))
6362elrab 3504 . . 3 (𝐵 ∈ {𝑏 ∈ 𝒫 𝑉 ∣ ((𝑁𝑏) = 𝑉 ∧ ∀𝑥𝑏𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))} ↔ (𝐵 ∈ 𝒫 𝑉 ∧ ((𝑁𝐵) = 𝑉 ∧ ∀𝑥𝐵𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥})))))
64 3anass 1081 . . 3 ((𝐵𝑉 ∧ (𝑁𝐵) = 𝑉 ∧ ∀𝑥𝐵𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥}))) ↔ (𝐵𝑉 ∧ ((𝑁𝐵) = 𝑉 ∧ ∀𝑥𝐵𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥})))))
6553, 63, 643bitr4i 292 . 2 (𝐵 ∈ {𝑏 ∈ 𝒫 𝑉 ∣ ((𝑁𝑏) = 𝑉 ∧ ∀𝑥𝑏𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))} ↔ (𝐵𝑉 ∧ (𝑁𝐵) = 𝑉 ∧ ∀𝑥𝐵𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥}))))
6651, 65syl6bb 276 1 (𝑊𝑋 → (𝐵𝐽 ↔ (𝐵𝑉 ∧ (𝑁𝐵) = 𝑉 ∧ ∀𝑥𝐵𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥})))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  w3a 1072   = wceq 1632  wcel 2139  wral 3050  {crab 3054  Vcvv 3340  [wsbc 3576  cdif 3712  wss 3715  𝒫 cpw 4302  {csn 4321  cfv 6049  (class class class)co 6813  Basecbs 16059  Scalarcsca 16146   ·𝑠 cvsca 16147  0gc0g 16302  LSpanclspn 19173  LBasisclbs 19276
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-iota 6012  df-fun 6051  df-fv 6057  df-ov 6816  df-lbs 19277
This theorem is referenced by:  lbsss  19279  lbssp  19281  lbsind  19282  lbspropd  19301  islbs2  19356  frlmlbs  20338  islbs4  20373
  Copyright terms: Public domain W3C validator