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

Definition df-lbs 15844
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 15843 . 2  class LBasis
2 vw . . 3  set  w
3 cvv 2801 . . 3  class  _V
4 vb . . . . . . . . . 10  set  b
54cv 1631 . . . . . . . . 9  class  b
6 vn . . . . . . . . . 10  set  n
76cv 1631 . . . . . . . . 9  class  n
85, 7cfv 5271 . . . . . . . 8  class  ( n `
 b )
92cv 1631 . . . . . . . . 9  class  w
10 cbs 13164 . . . . . . . . 9  class  Base
119, 10cfv 5271 . . . . . . . 8  class  ( Base `  w )
128, 11wceq 1632 . . . . . . 7  wff  ( n `
 b )  =  ( Base `  w
)
13 vy . . . . . . . . . . . . 13  set  y
1413cv 1631 . . . . . . . . . . . 12  class  y
15 vx . . . . . . . . . . . . 13  set  x
1615cv 1631 . . . . . . . . . . . 12  class  x
17 cvsca 13228 . . . . . . . . . . . . 13  class  .s
189, 17cfv 5271 . . . . . . . . . . . 12  class  ( .s
`  w )
1914, 16, 18co 5874 . . . . . . . . . . 11  class  ( y ( .s `  w
) x )
2016csn 3653 . . . . . . . . . . . . 13  class  { x }
215, 20cdif 3162 . . . . . . . . . . . 12  class  ( b 
\  { x }
)
2221, 7cfv 5271 . . . . . . . . . . 11  class  ( n `
 ( b  \  { x } ) )
2319, 22wcel 1696 . . . . . . . . . 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  set  s
2625cv 1631 . . . . . . . . . . 11  class  s
2726, 10cfv 5271 . . . . . . . . . 10  class  ( Base `  s )
28 c0g 13416 . . . . . . . . . . . 12  class  0g
2926, 28cfv 5271 . . . . . . . . . . 11  class  ( 0g
`  s )
3029csn 3653 . . . . . . . . . 10  class  { ( 0g `  s ) }
3127, 30cdif 3162 . . . . . . . . 9  class  ( (
Base `  s )  \  { ( 0g `  s ) } )
3224, 13, 31wral 2556 . . . . . . . 8  wff  A. y  e.  ( ( Base `  s
)  \  { ( 0g `  s ) } )  -.  ( y ( .s `  w
) x )  e.  ( n `  (
b  \  { x } ) )
3332, 15, 5wral 2556 . . . . . . 7  wff  A. x  e.  b  A. y  e.  ( ( Base `  s
)  \  { ( 0g `  s ) } )  -.  ( y ( .s `  w
) x )  e.  ( n `  (
b  \  { x } ) )
3412, 33wa 358 . . . . . 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 13227 . . . . . . 7  class Scalar
369, 35cfv 5271 . . . . . 6  class  (Scalar `  w )
3734, 25, 36wsbc 3004 . . . . 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 15744 . . . . . 6  class  LSpan
399, 38cfv 5271 . . . . 5  class  ( LSpan `  w )
4037, 6, 39wsbc 3004 . . . 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 3638 . . . 4  class  ~P ( Base `  w )
4240, 4, 41crab 2560 . . 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 4093 . 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 1632 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 set class
This definition is referenced by:  islbs  15845
  Copyright terms: Public domain W3C validator