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

Definition df-lbs 18896
 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 18895 . 2 class LBasis
2 vw . . 3 setvar 𝑤
3 cvv 3173 . . 3 class V
4 vb . . . . . . . . . 10 setvar 𝑏
54cv 1474 . . . . . . . . 9 class 𝑏
6 vn . . . . . . . . . 10 setvar 𝑛
76cv 1474 . . . . . . . . 9 class 𝑛
85, 7cfv 5804 . . . . . . . 8 class (𝑛𝑏)
92cv 1474 . . . . . . . . 9 class 𝑤
10 cbs 15695 . . . . . . . . 9 class Base
119, 10cfv 5804 . . . . . . . 8 class (Base‘𝑤)
128, 11wceq 1475 . . . . . . 7 wff (𝑛𝑏) = (Base‘𝑤)
13 vy . . . . . . . . . . . . 13 setvar 𝑦
1413cv 1474 . . . . . . . . . . . 12 class 𝑦
15 vx . . . . . . . . . . . . 13 setvar 𝑥
1615cv 1474 . . . . . . . . . . . 12 class 𝑥
17 cvsca 15772 . . . . . . . . . . . . 13 class ·𝑠
189, 17cfv 5804 . . . . . . . . . . . 12 class ( ·𝑠𝑤)
1914, 16, 18co 6549 . . . . . . . . . . 11 class (𝑦( ·𝑠𝑤)𝑥)
2016csn 4125 . . . . . . . . . . . . 13 class {𝑥}
215, 20cdif 3537 . . . . . . . . . . . 12 class (𝑏 ∖ {𝑥})
2221, 7cfv 5804 . . . . . . . . . . 11 class (𝑛‘(𝑏 ∖ {𝑥}))
2319, 22wcel 1977 . . . . . . . . . 10 wff (𝑦( ·𝑠𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥}))
2423wn 3 . . . . . . . . 9 wff ¬ (𝑦( ·𝑠𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥}))
25 vs . . . . . . . . . . . 12 setvar 𝑠
2625cv 1474 . . . . . . . . . . 11 class 𝑠
2726, 10cfv 5804 . . . . . . . . . 10 class (Base‘𝑠)
28 c0g 15923 . . . . . . . . . . . 12 class 0g
2926, 28cfv 5804 . . . . . . . . . . 11 class (0g𝑠)
3029csn 4125 . . . . . . . . . 10 class {(0g𝑠)}
3127, 30cdif 3537 . . . . . . . . 9 class ((Base‘𝑠) ∖ {(0g𝑠)})
3224, 13, 31wral 2896 . . . . . . . 8 wff 𝑦 ∈ ((Base‘𝑠) ∖ {(0g𝑠)}) ¬ (𝑦( ·𝑠𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥}))
3332, 15, 5wral 2896 . . . . . . 7 wff 𝑥𝑏𝑦 ∈ ((Base‘𝑠) ∖ {(0g𝑠)}) ¬ (𝑦( ·𝑠𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥}))
3412, 33wa 383 . . . . . 6 wff ((𝑛𝑏) = (Base‘𝑤) ∧ ∀𝑥𝑏𝑦 ∈ ((Base‘𝑠) ∖ {(0g𝑠)}) ¬ (𝑦( ·𝑠𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})))
35 csca 15771 . . . . . . 7 class Scalar
369, 35cfv 5804 . . . . . 6 class (Scalar‘𝑤)
3734, 25, 36wsbc 3402 . . . . 5 wff [(Scalar‘𝑤) / 𝑠]((𝑛𝑏) = (Base‘𝑤) ∧ ∀𝑥𝑏𝑦 ∈ ((Base‘𝑠) ∖ {(0g𝑠)}) ¬ (𝑦( ·𝑠𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})))
38 clspn 18792 . . . . . 6 class LSpan
399, 38cfv 5804 . . . . 5 class (LSpan‘𝑤)
4037, 6, 39wsbc 3402 . . . 4 wff [(LSpan‘𝑤) / 𝑛][(Scalar‘𝑤) / 𝑠]((𝑛𝑏) = (Base‘𝑤) ∧ ∀𝑥𝑏𝑦 ∈ ((Base‘𝑠) ∖ {(0g𝑠)}) ¬ (𝑦( ·𝑠𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})))
4111cpw 4108 . . . 4 class 𝒫 (Base‘𝑤)
4240, 4, 41crab 2900 . . 3 class {𝑏 ∈ 𝒫 (Base‘𝑤) ∣ [(LSpan‘𝑤) / 𝑛][(Scalar‘𝑤) / 𝑠]((𝑛𝑏) = (Base‘𝑤) ∧ ∀𝑥𝑏𝑦 ∈ ((Base‘𝑠) ∖ {(0g𝑠)}) ¬ (𝑦( ·𝑠𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})))}
432, 3, 42cmpt 4643 . 2 class (𝑤 ∈ V ↦ {𝑏 ∈ 𝒫 (Base‘𝑤) ∣ [(LSpan‘𝑤) / 𝑛][(Scalar‘𝑤) / 𝑠]((𝑛𝑏) = (Base‘𝑤) ∧ ∀𝑥𝑏𝑦 ∈ ((Base‘𝑠) ∖ {(0g𝑠)}) ¬ (𝑦( ·𝑠𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})))})
441, 43wceq 1475 1 wff LBasis = (𝑤 ∈ V ↦ {𝑏 ∈ 𝒫 (Base‘𝑤) ∣ [(LSpan‘𝑤) / 𝑛][(Scalar‘𝑤) / 𝑠]((𝑛𝑏) = (Base‘𝑤) ∧ ∀𝑥𝑏𝑦 ∈ ((Base‘𝑠) ∖ {(0g𝑠)}) ¬ (𝑦( ·𝑠𝑤)𝑥) ∈ (𝑛‘(𝑏 ∖ {𝑥})))})
 Colors of variables: wff setvar class This definition is referenced by:  islbs  18897
 Copyright terms: Public domain W3C validator