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

Definition df-lbs 18842
Description: Define the set of bases to a left module or left vector space. (Contributed by Mario Carneiro, 24-Jun-2014.)
Assertion
Ref Expression
df-lbs LBasis = (𝑤 ∈ V ↦ {𝑏 ∈ 𝒫 (Base‘𝑤) ∣ [(LSpan‘𝑤) / 𝑛][(Scalar‘𝑤) / 𝑠]((𝑛𝑏) = (Base‘𝑤) ∧ ∀𝑥𝑏𝑦 ∈ ((Base‘𝑠) ∖ {(0g𝑠)}) ¬ (𝑦( ·𝑠𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})))})
Distinct variable group:   𝑛,𝑏,𝑠,𝑤,𝑥,𝑦

Detailed syntax breakdown of Definition df-lbs
StepHypRef Expression
1 clbs 18841 . 2 class LBasis
2 vw . . 3 setvar 𝑤
3 cvv 3172 . . 3 class V
4 vb . . . . . . . . . 10 setvar 𝑏
54cv 1473 . . . . . . . . 9 class 𝑏
6 vn . . . . . . . . . 10 setvar 𝑛
76cv 1473 . . . . . . . . 9 class 𝑛
85, 7cfv 5790 . . . . . . . 8 class (𝑛𝑏)
92cv 1473 . . . . . . . . 9 class 𝑤
10 cbs 15641 . . . . . . . . 9 class Base
119, 10cfv 5790 . . . . . . . 8 class (Base‘𝑤)
128, 11wceq 1474 . . . . . . 7 wff (𝑛𝑏) = (Base‘𝑤)
13 vy . . . . . . . . . . . . 13 setvar 𝑦
1413cv 1473 . . . . . . . . . . . 12 class 𝑦
15 vx . . . . . . . . . . . . 13 setvar 𝑥
1615cv 1473 . . . . . . . . . . . 12 class 𝑥
17 cvsca 15718 . . . . . . . . . . . . 13 class ·𝑠
189, 17cfv 5790 . . . . . . . . . . . 12 class ( ·𝑠𝑤)
1914, 16, 18co 6527 . . . . . . . . . . 11 class (𝑦( ·𝑠𝑤)𝑥)
2016csn 4124 . . . . . . . . . . . . 13 class {𝑥}
215, 20cdif 3536 . . . . . . . . . . . 12 class (𝑏 ∖ {𝑥})
2221, 7cfv 5790 . . . . . . . . . . 11 class (𝑛‘(𝑏 ∖ {𝑥}))
2319, 22wcel 1976 . . . . . . . . . 10 wff (𝑦( ·𝑠𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥}))
2423wn 3 . . . . . . . . 9 wff ¬ (𝑦( ·𝑠𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥}))
25 vs . . . . . . . . . . . 12 setvar 𝑠
2625cv 1473 . . . . . . . . . . 11 class 𝑠
2726, 10cfv 5790 . . . . . . . . . 10 class (Base‘𝑠)
28 c0g 15869 . . . . . . . . . . . 12 class 0g
2926, 28cfv 5790 . . . . . . . . . . 11 class (0g𝑠)
3029csn 4124 . . . . . . . . . 10 class {(0g𝑠)}
3127, 30cdif 3536 . . . . . . . . 9 class ((Base‘𝑠) ∖ {(0g𝑠)})
3224, 13, 31wral 2895 . . . . . . . 8 wff 𝑦 ∈ ((Base‘𝑠) ∖ {(0g𝑠)}) ¬ (𝑦( ·𝑠𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥}))
3332, 15, 5wral 2895 . . . . . . 7 wff 𝑥𝑏𝑦 ∈ ((Base‘𝑠) ∖ {(0g𝑠)}) ¬ (𝑦( ·𝑠𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥}))
3412, 33wa 382 . . . . . 6 wff ((𝑛𝑏) = (Base‘𝑤) ∧ ∀𝑥𝑏𝑦 ∈ ((Base‘𝑠) ∖ {(0g𝑠)}) ¬ (𝑦( ·𝑠𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})))
35 csca 15717 . . . . . . 7 class Scalar
369, 35cfv 5790 . . . . . 6 class (Scalar‘𝑤)
3734, 25, 36wsbc 3401 . . . . 5 wff [(Scalar‘𝑤) / 𝑠]((𝑛𝑏) = (Base‘𝑤) ∧ ∀𝑥𝑏𝑦 ∈ ((Base‘𝑠) ∖ {(0g𝑠)}) ¬ (𝑦( ·𝑠𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})))
38 clspn 18738 . . . . . 6 class LSpan
399, 38cfv 5790 . . . . 5 class (LSpan‘𝑤)
4037, 6, 39wsbc 3401 . . . 4 wff [(LSpan‘𝑤) / 𝑛][(Scalar‘𝑤) / 𝑠]((𝑛𝑏) = (Base‘𝑤) ∧ ∀𝑥𝑏𝑦 ∈ ((Base‘𝑠) ∖ {(0g𝑠)}) ¬ (𝑦( ·𝑠𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})))
4111cpw 4107 . . . 4 class 𝒫 (Base‘𝑤)
4240, 4, 41crab 2899 . . 3 class {𝑏 ∈ 𝒫 (Base‘𝑤) ∣ [(LSpan‘𝑤) / 𝑛][(Scalar‘𝑤) / 𝑠]((𝑛𝑏) = (Base‘𝑤) ∧ ∀𝑥𝑏𝑦 ∈ ((Base‘𝑠) ∖ {(0g𝑠)}) ¬ (𝑦( ·𝑠𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})))}
432, 3, 42cmpt 4637 . 2 class (𝑤 ∈ V ↦ {𝑏 ∈ 𝒫 (Base‘𝑤) ∣ [(LSpan‘𝑤) / 𝑛][(Scalar‘𝑤) / 𝑠]((𝑛𝑏) = (Base‘𝑤) ∧ ∀𝑥𝑏𝑦 ∈ ((Base‘𝑠) ∖ {(0g𝑠)}) ¬ (𝑦( ·𝑠𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})))})
441, 43wceq 1474 1 wff LBasis = (𝑤 ∈ V ↦ {𝑏 ∈ 𝒫 (Base‘𝑤) ∣ [(LSpan‘𝑤) / 𝑛][(Scalar‘𝑤) / 𝑠]((𝑛𝑏) = (Base‘𝑤) ∧ ∀𝑥𝑏𝑦 ∈ ((Base‘𝑠) ∖ {(0g𝑠)}) ¬ (𝑦( ·𝑠𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})))})
Colors of variables: wff setvar class
This definition is referenced by:  islbs  18843
  Copyright terms: Public domain W3C validator