Metamath Proof Explorer

Theorem lssset

Description: The set of all (not necessarily closed) linear subspaces of a left module or left vector space. (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 15-Jul-2014)

Ref Expression
Hypotheses lssset.f 
|- F = ( Scalar ` W )
lssset.b 
|- B = ( Base ` F )
lssset.v 
|- V = ( Base ` W )
lssset.p 
|- .+ = ( +g ` W )
lssset.t 
|- .x. = ( .s ` W )
lssset.s 
|- S = ( LSubSp ` W )
Assertion lssset 
|- ( W e. X -> S = { s e. ( ~P V \ { (/) } ) | A. x e. B A. a e. s A. b e. s ( ( x .x. a ) .+ b ) e. s } )

Proof

Step Hyp Ref Expression
1 lssset.f 
 |-  F = ( Scalar ` W )
2 lssset.b 
 |-  B = ( Base ` F )
3 lssset.v 
 |-  V = ( Base ` W )
4 lssset.p 
 |-  .+ = ( +g ` W )
5 lssset.t 
 |-  .x. = ( .s ` W )
6 lssset.s 
 |-  S = ( LSubSp ` W )
7 elex 
 |-  ( W e. X -> W e. _V )
8 fveq2 
 |-  ( w = W -> ( Base ` w ) = ( Base ` W ) )
9 8 3 eqtr4di 
 |-  ( w = W -> ( Base ` w ) = V )
10 9 pweqd 
 |-  ( w = W -> ~P ( Base ` w ) = ~P V )
11 10 difeq1d 
 |-  ( w = W -> ( ~P ( Base ` w ) \ { (/) } ) = ( ~P V \ { (/) } ) )
12 fveq2 
 |-  ( w = W -> ( Scalar ` w ) = ( Scalar ` W ) )
13 12 1 eqtr4di 
 |-  ( w = W -> ( Scalar ` w ) = F )
14 13 fveq2d 
 |-  ( w = W -> ( Base ` ( Scalar ` w ) ) = ( Base ` F ) )
15 14 2 eqtr4di 
 |-  ( w = W -> ( Base ` ( Scalar ` w ) ) = B )
16 fveq2 
 |-  ( w = W -> ( .s ` w ) = ( .s ` W ) )
17 16 5 eqtr4di 
 |-  ( w = W -> ( .s ` w ) = .x. )
18 17 oveqd 
 |-  ( w = W -> ( x ( .s ` w ) a ) = ( x .x. a ) )
19 18 oveq1d 
 |-  ( w = W -> ( ( x ( .s ` w ) a ) ( +g ` w ) b ) = ( ( x .x. a ) ( +g ` w ) b ) )
20 fveq2 
 |-  ( w = W -> ( +g ` w ) = ( +g ` W ) )
21 20 4 eqtr4di 
 |-  ( w = W -> ( +g ` w ) = .+ )
22 21 oveqd 
 |-  ( w = W -> ( ( x .x. a ) ( +g ` w ) b ) = ( ( x .x. a ) .+ b ) )
23 19 22 eqtrd 
 |-  ( w = W -> ( ( x ( .s ` w ) a ) ( +g ` w ) b ) = ( ( x .x. a ) .+ b ) )
24 23 eleq1d 
 |-  ( w = W -> ( ( ( x ( .s ` w ) a ) ( +g ` w ) b ) e. s <-> ( ( x .x. a ) .+ b ) e. s ) )
25 24 2ralbidv 
 |-  ( w = W -> ( A. a e. s A. b e. s ( ( x ( .s ` w ) a ) ( +g ` w ) b ) e. s <-> A. a e. s A. b e. s ( ( x .x. a ) .+ b ) e. s ) )
26 15 25 raleqbidv 
 |-  ( w = W -> ( A. x e. ( Base ` ( Scalar ` w ) ) A. a e. s A. b e. s ( ( x ( .s ` w ) a ) ( +g ` w ) b ) e. s <-> A. x e. B A. a e. s A. b e. s ( ( x .x. a ) .+ b ) e. s ) )
27 11 26 rabeqbidv 
 |-  ( w = W -> { 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 } = { s e. ( ~P V \ { (/) } ) | A. x e. B A. a e. s A. b e. s ( ( x .x. a ) .+ b ) e. s } )
28 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 } )
29 3 fvexi 
 |-  V e. _V
30 29 pwex 
 |-  ~P V e. _V
31 30 difexi 
 |-  ( ~P V \ { (/) } ) e. _V
32 31 rabex 
 |-  { s e. ( ~P V \ { (/) } ) | A. x e. B A. a e. s A. b e. s ( ( x .x. a ) .+ b ) e. s } e. _V
33 27 28 32 fvmpt 
 |-  ( W e. _V -> ( LSubSp ` W ) = { s e. ( ~P V \ { (/) } ) | A. x e. B A. a e. s A. b e. s ( ( x .x. a ) .+ b ) e. s } )
34 7 33 syl 
 |-  ( W e. X -> ( LSubSp ` W ) = { s e. ( ~P V \ { (/) } ) | A. x e. B A. a e. s A. b e. s ( ( x .x. a ) .+ b ) e. s } )
35 6 34 syl5eq 
 |-  ( W e. X -> S = { s e. ( ~P V \ { (/) } ) | A. x e. B A. a e. s A. b e. s ( ( x .x. a ) .+ b ) e. s } )