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

Metamath Proof Explorer

Definition df-lss

Description: Define the set of linear subspaces of a left module or left vector space: a linear subspace of a left module or left vector space is a non-empty subset of the base set of the left module/vector space with a closure condition on vector addition and scalar multiplication. (Contributed by NM, 8-Dec-2013)

Ref Expression
Assertion df-lss 
|- LSubSp = ( w e. _V |-> { s e. ( ~P ( Base ` w ) \ { (/) } ) | A. x e. ( Base ` ( Scalar ` w ) ) A. a e. s A. b e. s ( ( x ( .s ` w ) a ) ( +g ` w ) b ) e. s } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 clss 
 |-  LSubSp
1 vw 
 |-  w
2 cvv 
 |-  _V
3 vs 
 |-  s
4 cbs 
 |-  Base
5 1 cv 
 |-  w
6 5 4 cfv 
 |-  ( Base ` w )
7 6 cpw 
 |-  ~P ( Base ` w )
8 c0 
 |-  (/)
9 8 csn 
 |-  { (/) }
10 7 9 cdif 
 |-  ( ~P ( Base ` w ) \ { (/) } )
11 vx 
 |-  x
12 csca 
 |-  Scalar
13 5 12 cfv 
 |-  ( Scalar ` w )
14 13 4 cfv 
 |-  ( Base ` ( Scalar ` w ) )
15 va 
 |-  a
16 3 cv 
 |-  s
17 vb 
 |-  b
18 11 cv 
 |-  x
19 cvsca 
 |-  .s
20 5 19 cfv 
 |-  ( .s ` w )
21 15 cv 
 |-  a
22 18 21 20 co 
 |-  ( x ( .s ` w ) a )
23 cplusg 
 |-  +g
24 5 23 cfv 
 |-  ( +g ` w )
25 17 cv 
 |-  b
26 22 25 24 co 
 |-  ( ( x ( .s ` w ) a ) ( +g ` w ) b )
27 26 16 wcel 
 |-  ( ( x ( .s ` w ) a ) ( +g ` w ) b ) e. s
28 27 17 16 wral 
 |-  A. b e. s ( ( x ( .s ` w ) a ) ( +g ` w ) b ) e. s
29 28 15 16 wral 
 |-  A. a e. s A. b e. s ( ( x ( .s ` w ) a ) ( +g ` w ) b ) e. s
30 29 11 14 wral 
 |-  A. x e. ( Base ` ( Scalar ` w ) ) A. a e. s A. b e. s ( ( x ( .s ` w ) a ) ( +g ` w ) b ) e. s
31 30 3 10 crab 
 |-  { s e. ( ~P ( Base ` w ) \ { (/) } ) | A. x e. ( Base ` ( Scalar ` w ) ) A. a e. s A. b e. s ( ( x ( .s ` w ) a ) ( +g ` w ) b ) e. s }
32 1 2 31 cmpt 
 |-  ( w e. _V |-> { s e. ( ~P ( Base ` w ) \ { (/) } ) | A. x e. ( Base ` ( Scalar ` w ) ) A. a e. s A. b e. s ( ( x ( .s ` w ) a ) ( +g ` w ) b ) e. s } )
33 0 32 wceq 
 |-  LSubSp = ( w e. _V |-> { s e. ( ~P ( Base ` w ) \ { (/) } ) | A. x e. ( Base ` ( Scalar ` w ) ) A. a e. s A. b e. s ( ( x ( .s ` w ) a ) ( +g ` w ) b ) e. s } )