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

Metamath Proof Explorer

Theorem islss

Description: The predicate "is a subspace" (of a left module or left vector space). (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 8-Jan-2015)

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 islss 
|- ( U e. S <-> ( U C_ V /\ U =/= (/) /\ A. x e. B A. a e. U A. b e. U ( ( x .x. a ) .+ b ) e. U ) )

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 elfvex 
 |-  ( U e. ( LSubSp ` W ) -> W e. _V )
8 7 6 eleq2s 
 |-  ( U e. S -> W e. _V )
9 fvprc 
 |-  ( -. W e. _V -> ( Base ` W ) = (/) )
10 3 9 eqtrid 
 |-  ( -. W e. _V -> V = (/) )
11 10 sseq2d 
 |-  ( -. W e. _V -> ( U C_ V <-> U C_ (/) ) )
12 11 biimpcd 
 |-  ( U C_ V -> ( -. W e. _V -> U C_ (/) ) )
13 ss0 
 |-  ( U C_ (/) -> U = (/) )
14 12 13 syl6 
 |-  ( U C_ V -> ( -. W e. _V -> U = (/) ) )
15 14 necon1ad 
 |-  ( U C_ V -> ( U =/= (/) -> W e. _V ) )
16 15 imp 
 |-  ( ( U C_ V /\ U =/= (/) ) -> W e. _V )
17 16 3adant3 
 |-  ( ( U C_ V /\ U =/= (/) /\ A. x e. B A. a e. U A. b e. U ( ( x .x. a ) .+ b ) e. U ) -> W e. _V )
18 1 2 3 4 5 6 lssset 
 |-  ( W e. _V -> S = { s e. ( ~P V \ { (/) } ) | A. x e. B A. a e. s A. b e. s ( ( x .x. a ) .+ b ) e. s } )
19 18 eleq2d 
 |-  ( W e. _V -> ( U e. S <-> U e. { s e. ( ~P V \ { (/) } ) | A. x e. B A. a e. s A. b e. s ( ( x .x. a ) .+ b ) e. s } ) )
20 eldifsn 
 |-  ( U e. ( ~P V \ { (/) } ) <-> ( U e. ~P V /\ U =/= (/) ) )
21 3 fvexi 
 |-  V e. _V
22 21 elpw2 
 |-  ( U e. ~P V <-> U C_ V )
23 22 anbi1i 
 |-  ( ( U e. ~P V /\ U =/= (/) ) <-> ( U C_ V /\ U =/= (/) ) )
24 20 23 bitri 
 |-  ( U e. ( ~P V \ { (/) } ) <-> ( U C_ V /\ U =/= (/) ) )
25 24 anbi1i 
 |-  ( ( U e. ( ~P V \ { (/) } ) /\ A. x e. B A. a e. U A. b e. U ( ( x .x. a ) .+ b ) e. U ) <-> ( ( U C_ V /\ U =/= (/) ) /\ A. x e. B A. a e. U A. b e. U ( ( x .x. a ) .+ b ) e. U ) )
26 eleq2 
 |-  ( s = U -> ( ( ( x .x. a ) .+ b ) e. s <-> ( ( x .x. a ) .+ b ) e. U ) )
27 26 raleqbi1dv 
 |-  ( s = U -> ( A. b e. s ( ( x .x. a ) .+ b ) e. s <-> A. b e. U ( ( x .x. a ) .+ b ) e. U ) )
28 27 raleqbi1dv 
 |-  ( s = U -> ( A. a e. s A. b e. s ( ( x .x. a ) .+ b ) e. s <-> A. a e. U A. b e. U ( ( x .x. a ) .+ b ) e. U ) )
29 28 ralbidv 
 |-  ( s = U -> ( A. x e. B A. a e. s A. b e. s ( ( x .x. a ) .+ b ) e. s <-> A. x e. B A. a e. U A. b e. U ( ( x .x. a ) .+ b ) e. U ) )
30 29 elrab 
 |-  ( U e. { s e. ( ~P V \ { (/) } ) | A. x e. B A. a e. s A. b e. s ( ( x .x. a ) .+ b ) e. s } <-> ( U e. ( ~P V \ { (/) } ) /\ A. x e. B A. a e. U A. b e. U ( ( x .x. a ) .+ b ) e. U ) )
31 df-3an 
 |-  ( ( U C_ V /\ U =/= (/) /\ A. x e. B A. a e. U A. b e. U ( ( x .x. a ) .+ b ) e. U ) <-> ( ( U C_ V /\ U =/= (/) ) /\ A. x e. B A. a e. U A. b e. U ( ( x .x. a ) .+ b ) e. U ) )
32 25 30 31 3bitr4i 
 |-  ( U e. { s e. ( ~P V \ { (/) } ) | A. x e. B A. a e. s A. b e. s ( ( x .x. a ) .+ b ) e. s } <-> ( U C_ V /\ U =/= (/) /\ A. x e. B A. a e. U A. b e. U ( ( x .x. a ) .+ b ) e. U ) )
33 19 32 bitrdi 
 |-  ( W e. _V -> ( U e. S <-> ( U C_ V /\ U =/= (/) /\ A. x e. B A. a e. U A. b e. U ( ( x .x. a ) .+ b ) e. U ) ) )
34 8 17 33 pm5.21nii 
 |-  ( U e. S <-> ( U C_ V /\ U =/= (/) /\ A. x e. B A. a e. U A. b e. U ( ( x .x. a ) .+ b ) e. U ) )