This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-lbs

Description: Define the set of bases to a left module or left vector space. (Contributed by Mario Carneiro, 24-Jun-2014)

Ref Expression
Assertion 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 } ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 clbs 
 |-  LBasis
1 vw 
 |-  w
2 cvv 
 |-  _V
3 vb 
 |-  b
4 cbs 
 |-  Base
5 1 cv 
 |-  w
6 5 4 cfv 
 |-  ( Base ` w )
7 6 cpw 
 |-  ~P ( Base ` w )
8 clspn 
 |-  LSpan
9 5 8 cfv 
 |-  ( LSpan ` w )
10 vn 
 |-  n
11 csca 
 |-  Scalar
12 5 11 cfv 
 |-  ( Scalar ` w )
13 vs 
 |-  s
14 10 cv 
 |-  n
15 3 cv 
 |-  b
16 15 14 cfv 
 |-  ( n ` b )
17 16 6 wceq 
 |-  ( n ` b ) = ( Base ` w )
18 vx 
 |-  x
19 vy 
 |-  y
20 13 cv 
 |-  s
21 20 4 cfv 
 |-  ( Base ` s )
22 c0g 
 |-  0g
23 20 22 cfv 
 |-  ( 0g ` s )
24 23 csn 
 |-  { ( 0g ` s ) }
25 21 24 cdif 
 |-  ( ( Base ` s ) \ { ( 0g ` s ) } )
26 19 cv 
 |-  y
27 cvsca 
 |-  .s
28 5 27 cfv 
 |-  ( .s ` w )
29 18 cv 
 |-  x
30 26 29 28 co 
 |-  ( y ( .s ` w ) x )
31 29 csn 
 |-  { x }
32 15 31 cdif 
 |-  ( b \ { x } )
33 32 14 cfv 
 |-  ( n ` ( b \ { x } ) )
34 30 33 wcel 
 |-  ( y ( .s ` w ) x ) e. ( n ` ( b \ { x } ) )
35 34 wn 
 |-  -. ( y ( .s ` w ) x ) e. ( n ` ( b \ { x } ) )
36 35 19 25 wral 
 |-  A. y e. ( ( Base ` s ) \ { ( 0g ` s ) } ) -. ( y ( .s ` w ) x ) e. ( n ` ( b \ { x } ) )
37 36 18 15 wral 
 |-  A. x e. b A. y e. ( ( Base ` s ) \ { ( 0g ` s ) } ) -. ( y ( .s ` w ) x ) e. ( n ` ( b \ { x } ) )
38 17 37 wa 
 |-  ( ( n ` b ) = ( Base ` w ) /\ A. x e. b A. y e. ( ( Base ` s ) \ { ( 0g ` s ) } ) -. ( y ( .s ` w ) x ) e. ( n ` ( b \ { x } ) ) )
39 38 13 12 wsbc 
 |-  [. ( 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 } ) ) )
40 39 10 9 wsbc 
 |-  [. ( 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 } ) ) )
41 40 3 7 crab 
 |-  { 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 } ) ) ) }
42 1 2 41 cmpt 
 |-  ( 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 } ) ) ) } )
43 0 42 wceq 
 |-  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 } ) ) ) } )