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

Theorem islbs 20537
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 3463 . . . 4 (𝑊𝑋𝑊 ∈ V)
2 islbs.j . . . . 5 𝐽 = (LBasis‘𝑊)
3 fveq2 6842 . . . . . . . . 9 (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊))
4 islbs.v . . . . . . . . 9 𝑉 = (Base‘𝑊)
53, 4eqtr4di 2794 . . . . . . . 8 (𝑤 = 𝑊 → (Base‘𝑤) = 𝑉)
65pweqd 4577 . . . . . . 7 (𝑤 = 𝑊 → 𝒫 (Base‘𝑤) = 𝒫 𝑉)
7 fvexd 6857 . . . . . . . 8 (𝑤 = 𝑊 → (LSpan‘𝑤) ∈ V)
8 fveq2 6842 . . . . . . . . 9 (𝑤 = 𝑊 → (LSpan‘𝑤) = (LSpan‘𝑊))
9 islbs.n . . . . . . . . 9 𝑁 = (LSpan‘𝑊)
108, 9eqtr4di 2794 . . . . . . . 8 (𝑤 = 𝑊 → (LSpan‘𝑤) = 𝑁)
11 fvexd 6857 . . . . . . . . 9 ((𝑤 = 𝑊𝑛 = 𝑁) → (Scalar‘𝑤) ∈ V)
12 fveq2 6842 . . . . . . . . . . 11 (𝑤 = 𝑊 → (Scalar‘𝑤) = (Scalar‘𝑊))
1312adantr 481 . . . . . . . . . 10 ((𝑤 = 𝑊𝑛 = 𝑁) → (Scalar‘𝑤) = (Scalar‘𝑊))
14 islbs.f . . . . . . . . . 10 𝐹 = (Scalar‘𝑊)
1513, 14eqtr4di 2794 . . . . . . . . 9 ((𝑤 = 𝑊𝑛 = 𝑁) → (Scalar‘𝑤) = 𝐹)
16 simplr 767 . . . . . . . . . . . 12 (((𝑤 = 𝑊𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → 𝑛 = 𝑁)
1716fveq1d 6844 . . . . . . . . . . 11 (((𝑤 = 𝑊𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (𝑛𝑏) = (𝑁𝑏))
185ad2antrr 724 . . . . . . . . . . 11 (((𝑤 = 𝑊𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (Base‘𝑤) = 𝑉)
1917, 18eqeq12d 2752 . . . . . . . . . 10 (((𝑤 = 𝑊𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → ((𝑛𝑏) = (Base‘𝑤) ↔ (𝑁𝑏) = 𝑉))
20 simpr 485 . . . . . . . . . . . . . . 15 (((𝑤 = 𝑊𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → 𝑓 = 𝐹)
2120fveq2d 6846 . . . . . . . . . . . . . 14 (((𝑤 = 𝑊𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (Base‘𝑓) = (Base‘𝐹))
22 islbs.k . . . . . . . . . . . . . 14 𝐾 = (Base‘𝐹)
2321, 22eqtr4di 2794 . . . . . . . . . . . . 13 (((𝑤 = 𝑊𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (Base‘𝑓) = 𝐾)
2420fveq2d 6846 . . . . . . . . . . . . . . 15 (((𝑤 = 𝑊𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (0g𝑓) = (0g𝐹))
25 islbs.z . . . . . . . . . . . . . . 15 0 = (0g𝐹)
2624, 25eqtr4di 2794 . . . . . . . . . . . . . 14 (((𝑤 = 𝑊𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (0g𝑓) = 0 )
2726sneqd 4598 . . . . . . . . . . . . 13 (((𝑤 = 𝑊𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → {(0g𝑓)} = { 0 })
2823, 27difeq12d 4083 . . . . . . . . . . . 12 (((𝑤 = 𝑊𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → ((Base‘𝑓) ∖ {(0g𝑓)}) = (𝐾 ∖ { 0 }))
29 fveq2 6842 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑊 → ( ·𝑠𝑤) = ( ·𝑠𝑊))
30 islbs.s . . . . . . . . . . . . . . . . 17 · = ( ·𝑠𝑊)
3129, 30eqtr4di 2794 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑊 → ( ·𝑠𝑤) = · )
3231ad2antrr 724 . . . . . . . . . . . . . . 15 (((𝑤 = 𝑊𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → ( ·𝑠𝑤) = · )
3332oveqd 7374 . . . . . . . . . . . . . 14 (((𝑤 = 𝑊𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (𝑦( ·𝑠𝑤)𝑥) = (𝑦 · 𝑥))
3416fveq1d 6844 . . . . . . . . . . . . . 14 (((𝑤 = 𝑊𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (𝑛‘(𝑏 ∖ {𝑥})) = (𝑁‘(𝑏 ∖ {𝑥})))
3533, 34eleq12d 2832 . . . . . . . . . . . . 13 (((𝑤 = 𝑊𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → ((𝑦( ·𝑠𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})) ↔ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥}))))
3635notbid 317 . . . . . . . . . . . 12 (((𝑤 = 𝑊𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (¬ (𝑦( ·𝑠𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})) ↔ ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥}))))
3728, 36raleqbidv 3319 . . . . . . . . . . 11 (((𝑤 = 𝑊𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (∀𝑦 ∈ ((Base‘𝑓) ∖ {(0g𝑓)}) ¬ (𝑦( ·𝑠𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})) ↔ ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥}))))
3837ralbidv 3174 . . . . . . . . . 10 (((𝑤 = 𝑊𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (∀𝑥𝑏𝑦 ∈ ((Base‘𝑓) ∖ {(0g𝑓)}) ¬ (𝑦( ·𝑠𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})) ↔ ∀𝑥𝑏𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥}))))
3919, 38anbi12d 631 . . . . . . . . 9 (((𝑤 = 𝑊𝑛 = 𝑁) ∧ 𝑓 = 𝐹) → (((𝑛𝑏) = (Base‘𝑤) ∧ ∀𝑥𝑏𝑦 ∈ ((Base‘𝑓) ∖ {(0g𝑓)}) ¬ (𝑦( ·𝑠𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥}))) ↔ ((𝑁𝑏) = 𝑉 ∧ ∀𝑥𝑏𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))))
4011, 15, 39sbcied2 3786 . . . . . . . 8 ((𝑤 = 𝑊𝑛 = 𝑁) → ([(Scalar‘𝑤) / 𝑓]((𝑛𝑏) = (Base‘𝑤) ∧ ∀𝑥𝑏𝑦 ∈ ((Base‘𝑓) ∖ {(0g𝑓)}) ¬ (𝑦( ·𝑠𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥}))) ↔ ((𝑁𝑏) = 𝑉 ∧ ∀𝑥𝑏𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))))
417, 10, 40sbcied2 3786 . . . . . . 7 (𝑤 = 𝑊 → ([(LSpan‘𝑤) / 𝑛][(Scalar‘𝑤) / 𝑓]((𝑛𝑏) = (Base‘𝑤) ∧ ∀𝑥𝑏𝑦 ∈ ((Base‘𝑓) ∖ {(0g𝑓)}) ¬ (𝑦( ·𝑠𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥}))) ↔ ((𝑁𝑏) = 𝑉 ∧ ∀𝑥𝑏𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))))
426, 41rabeqbidv 3424 . . . . . 6 (𝑤 = 𝑊 → {𝑏 ∈ 𝒫 (Base‘𝑤) ∣ [(LSpan‘𝑤) / 𝑛][(Scalar‘𝑤) / 𝑓]((𝑛𝑏) = (Base‘𝑤) ∧ ∀𝑥𝑏𝑦 ∈ ((Base‘𝑓) ∖ {(0g𝑓)}) ¬ (𝑦( ·𝑠𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})))} = {𝑏 ∈ 𝒫 𝑉 ∣ ((𝑁𝑏) = 𝑉 ∧ ∀𝑥𝑏𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))})
43 df-lbs 20536 . . . . . 6 LBasis = (𝑤 ∈ V ↦ {𝑏 ∈ 𝒫 (Base‘𝑤) ∣ [(LSpan‘𝑤) / 𝑛][(Scalar‘𝑤) / 𝑓]((𝑛𝑏) = (Base‘𝑤) ∧ ∀𝑥𝑏𝑦 ∈ ((Base‘𝑓) ∖ {(0g𝑓)}) ¬ (𝑦( ·𝑠𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})))})
444fvexi 6856 . . . . . . . 8 𝑉 ∈ V
4544pwex 5335 . . . . . . 7 𝒫 𝑉 ∈ V
4645rabex 5289 . . . . . 6 {𝑏 ∈ 𝒫 𝑉 ∣ ((𝑁𝑏) = 𝑉 ∧ ∀𝑥𝑏𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))} ∈ V
4742, 43, 46fvmpt 6948 . . . . 5 (𝑊 ∈ V → (LBasis‘𝑊) = {𝑏 ∈ 𝒫 𝑉 ∣ ((𝑁𝑏) = 𝑉 ∧ ∀𝑥𝑏𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))})
482, 47eqtrid 2788 . . . 4 (𝑊 ∈ V → 𝐽 = {𝑏 ∈ 𝒫 𝑉 ∣ ((𝑁𝑏) = 𝑉 ∧ ∀𝑥𝑏𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))})
491, 48syl 17 . . 3 (𝑊𝑋𝐽 = {𝑏 ∈ 𝒫 𝑉 ∣ ((𝑁𝑏) = 𝑉 ∧ ∀𝑥𝑏𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))})
5049eleq2d 2823 . 2 (𝑊𝑋 → (𝐵𝐽𝐵 ∈ {𝑏 ∈ 𝒫 𝑉 ∣ ((𝑁𝑏) = 𝑉 ∧ ∀𝑥𝑏𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))}))
5144elpw2 5302 . . . 4 (𝐵 ∈ 𝒫 𝑉𝐵𝑉)
5251anbi1i 624 . . 3 ((𝐵 ∈ 𝒫 𝑉 ∧ ((𝑁𝐵) = 𝑉 ∧ ∀𝑥𝐵𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥})))) ↔ (𝐵𝑉 ∧ ((𝑁𝐵) = 𝑉 ∧ ∀𝑥𝐵𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥})))))
53 fveqeq2 6851 . . . . 5 (𝑏 = 𝐵 → ((𝑁𝑏) = 𝑉 ↔ (𝑁𝐵) = 𝑉))
54 difeq1 4075 . . . . . . . . . 10 (𝑏 = 𝐵 → (𝑏 ∖ {𝑥}) = (𝐵 ∖ {𝑥}))
5554fveq2d 6846 . . . . . . . . 9 (𝑏 = 𝐵 → (𝑁‘(𝑏 ∖ {𝑥})) = (𝑁‘(𝐵 ∖ {𝑥})))
5655eleq2d 2823 . . . . . . . 8 (𝑏 = 𝐵 → ((𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})) ↔ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥}))))
5756notbid 317 . . . . . . 7 (𝑏 = 𝐵 → (¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})) ↔ ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥}))))
5857ralbidv 3174 . . . . . 6 (𝑏 = 𝐵 → (∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})) ↔ ∀𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥}))))
5958raleqbi1dv 3307 . . . . 5 (𝑏 = 𝐵 → (∀𝑥𝑏𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})) ↔ ∀𝑥𝐵𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥}))))
6053, 59anbi12d 631 . . . 4 (𝑏 = 𝐵 → (((𝑁𝑏) = 𝑉 ∧ ∀𝑥𝑏𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥}))) ↔ ((𝑁𝐵) = 𝑉 ∧ ∀𝑥𝐵𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥})))))
6160elrab 3645 . . 3 (𝐵 ∈ {𝑏 ∈ 𝒫 𝑉 ∣ ((𝑁𝑏) = 𝑉 ∧ ∀𝑥𝑏𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))} ↔ (𝐵 ∈ 𝒫 𝑉 ∧ ((𝑁𝐵) = 𝑉 ∧ ∀𝑥𝐵𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥})))))
62 3anass 1095 . . 3 ((𝐵𝑉 ∧ (𝑁𝐵) = 𝑉 ∧ ∀𝑥𝐵𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥}))) ↔ (𝐵𝑉 ∧ ((𝑁𝐵) = 𝑉 ∧ ∀𝑥𝐵𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥})))))
6352, 61, 623bitr4i 302 . 2 (𝐵 ∈ {𝑏 ∈ 𝒫 𝑉 ∣ ((𝑁𝑏) = 𝑉 ∧ ∀𝑥𝑏𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝑏 ∖ {𝑥})))} ↔ (𝐵𝑉 ∧ (𝑁𝐵) = 𝑉 ∧ ∀𝑥𝐵𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥}))))
6450, 63bitrdi 286 1 (𝑊𝑋 → (𝐵𝐽 ↔ (𝐵𝑉 ∧ (𝑁𝐵) = 𝑉 ∧ ∀𝑥𝐵𝑦 ∈ (𝐾 ∖ { 0 }) ¬ (𝑦 · 𝑥) ∈ (𝑁‘(𝐵 ∖ {𝑥})))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wcel 2106  wral 3064  {crab 3407  Vcvv 3445  [wsbc 3739  cdif 3907  wss 3910  𝒫 cpw 4560  {csn 4586  cfv 6496  (class class class)co 7357  Basecbs 17083  Scalarcsca 17136   ·𝑠 cvsca 17137  0gc0g 17321  LSpanclspn 20432  LBasisclbs 20535
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-sbc 3740  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-iota 6448  df-fun 6498  df-fv 6504  df-ov 7360  df-lbs 20536
This theorem is referenced by:  lbsss  20538  lbssp  20540  lbsind  20541  lbspropd  20560  islbs2  20615  frlmlbs  21203  islbs4  21238
  Copyright terms: Public domain W3C validator