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

Definition df-lbs 17156
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  =  ( w  e.  _V  |->  { b  e.  ~P ( Base `  w )  | 
[. ( LSpan `  w
)  /  n ]. [. (Scalar `  w )  /  s ]. (
( n `  b
)  =  ( Base `  w )  /\  A. x  e.  b  A. y  e.  ( ( Base `  s )  \  { ( 0g `  s ) } )  -.  ( y ( .s `  w ) x )  e.  ( n `  ( b 
\  { x }
) ) ) } )
Distinct variable group:    n, b, s, w, x, y

Detailed syntax breakdown of Definition df-lbs
StepHypRef Expression
1 clbs 17155 . 2  class LBasis
2 vw . . 3  setvar  w
3 cvv 2972 . . 3  class  _V
4 vb . . . . . . . . . 10  setvar  b
54cv 1368 . . . . . . . . 9  class  b
6 vn . . . . . . . . . 10  setvar  n
76cv 1368 . . . . . . . . 9  class  n
85, 7cfv 5418 . . . . . . . 8  class  ( n `
 b )
92cv 1368 . . . . . . . . 9  class  w
10 cbs 14174 . . . . . . . . 9  class  Base
119, 10cfv 5418 . . . . . . . 8  class  ( Base `  w )
128, 11wceq 1369 . . . . . . 7  wff  ( n `
 b )  =  ( Base `  w
)
13 vy . . . . . . . . . . . . 13  setvar  y
1413cv 1368 . . . . . . . . . . . 12  class  y
15 vx . . . . . . . . . . . . 13  setvar  x
1615cv 1368 . . . . . . . . . . . 12  class  x
17 cvsca 14242 . . . . . . . . . . . . 13  class  .s
189, 17cfv 5418 . . . . . . . . . . . 12  class  ( .s
`  w )
1914, 16, 18co 6091 . . . . . . . . . . 11  class  ( y ( .s `  w
) x )
2016csn 3877 . . . . . . . . . . . . 13  class  { x }
215, 20cdif 3325 . . . . . . . . . . . 12  class  ( b 
\  { x }
)
2221, 7cfv 5418 . . . . . . . . . . 11  class  ( n `
 ( b  \  { x } ) )
2319, 22wcel 1756 . . . . . . . . . 10  wff  ( y ( .s `  w
) x )  e.  ( n `  (
b  \  { x } ) )
2423wn 3 . . . . . . . . 9  wff  -.  (
y ( .s `  w ) x )  e.  ( n `  ( b  \  {
x } ) )
25 vs . . . . . . . . . . . 12  setvar  s
2625cv 1368 . . . . . . . . . . 11  class  s
2726, 10cfv 5418 . . . . . . . . . 10  class  ( Base `  s )
28 c0g 14378 . . . . . . . . . . . 12  class  0g
2926, 28cfv 5418 . . . . . . . . . . 11  class  ( 0g
`  s )
3029csn 3877 . . . . . . . . . 10  class  { ( 0g `  s ) }
3127, 30cdif 3325 . . . . . . . . 9  class  ( (
Base `  s )  \  { ( 0g `  s ) } )
3224, 13, 31wral 2715 . . . . . . . 8  wff  A. y  e.  ( ( Base `  s
)  \  { ( 0g `  s ) } )  -.  ( y ( .s `  w
) x )  e.  ( n `  (
b  \  { x } ) )
3332, 15, 5wral 2715 . . . . . . 7  wff  A. x  e.  b  A. y  e.  ( ( Base `  s
)  \  { ( 0g `  s ) } )  -.  ( y ( .s `  w
) x )  e.  ( n `  (
b  \  { x } ) )
3412, 33wa 369 . . . . . 6  wff  ( ( n `  b )  =  ( Base `  w
)  /\  A. x  e.  b  A. y  e.  ( ( Base `  s
)  \  { ( 0g `  s ) } )  -.  ( y ( .s `  w
) x )  e.  ( n `  (
b  \  { x } ) ) )
35 csca 14241 . . . . . . 7  class Scalar
369, 35cfv 5418 . . . . . 6  class  (Scalar `  w )
3734, 25, 36wsbc 3186 . . . . 5  wff  [. (Scalar `  w )  /  s ]. ( ( n `  b )  =  (
Base `  w )  /\  A. x  e.  b 
A. y  e.  ( ( Base `  s
)  \  { ( 0g `  s ) } )  -.  ( y ( .s `  w
) x )  e.  ( n `  (
b  \  { x } ) ) )
38 clspn 17052 . . . . . 6  class  LSpan
399, 38cfv 5418 . . . . 5  class  ( LSpan `  w )
4037, 6, 39wsbc 3186 . . . 4  wff  [. ( LSpan `  w )  /  n ]. [. (Scalar `  w )  /  s ]. ( ( n `  b )  =  (
Base `  w )  /\  A. x  e.  b 
A. y  e.  ( ( Base `  s
)  \  { ( 0g `  s ) } )  -.  ( y ( .s `  w
) x )  e.  ( n `  (
b  \  { x } ) ) )
4111cpw 3860 . . . 4  class  ~P ( Base `  w )
4240, 4, 41crab 2719 . . 3  class  { b  e.  ~P ( Base `  w )  |  [. ( LSpan `  w )  /  n ]. [. (Scalar `  w )  /  s ]. ( ( n `  b )  =  (
Base `  w )  /\  A. x  e.  b 
A. y  e.  ( ( Base `  s
)  \  { ( 0g `  s ) } )  -.  ( y ( .s `  w
) x )  e.  ( n `  (
b  \  { x } ) ) ) }
432, 3, 42cmpt 4350 . 2  class  ( w  e.  _V  |->  { b  e.  ~P ( Base `  w )  |  [. ( LSpan `  w )  /  n ]. [. (Scalar `  w )  /  s ]. ( ( n `  b )  =  (
Base `  w )  /\  A. x  e.  b 
A. y  e.  ( ( Base `  s
)  \  { ( 0g `  s ) } )  -.  ( y ( .s `  w
) x )  e.  ( n `  (
b  \  { x } ) ) ) } )
441, 43wceq 1369 1  wff LBasis  =  ( w  e.  _V  |->  { b  e.  ~P ( Base `  w )  | 
[. ( LSpan `  w
)  /  n ]. [. (Scalar `  w )  /  s ]. (
( n `  b
)  =  ( Base `  w )  /\  A. x  e.  b  A. y  e.  ( ( Base `  s )  \  { ( 0g `  s ) } )  -.  ( y ( .s `  w ) x )  e.  ( n `  ( b 
\  { x }
) ) ) } )
Colors of variables: wff setvar class
This definition is referenced by:  islbs  17157
  Copyright terms: Public domain W3C validator