Theorem lssset 18934

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.)

Hypotheses

Ref	Expression
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

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

Distinct variable groups:   .+ , s   x, s, B   V, s   a, b, s, x, W   .x. , s

Allowed substitution hints:   B( a, b)   .+ ( x, a, b)   S( x, s, a, b)   .x. ( x, a, b)   F( x, s, a, b)   V( x, a, b)   X( x, s, a, b)

Proof of Theorem lssset

Dummy variable w is distinct from all other variables.

Step	Hyp	Ref	Expression
1		lssset.s	. 2 |- S = ( LSubSp ` W )
2		elex 3212	. . 3 |- ( W e. X -> W e. _V )
3		fveq2 6191	. . . . . . . 8 |- ( w = W -> ( Base ` w ) = ( Base ` W ) )
4		lssset.v	. . . . . . . 8 |- V = ( Base ` W )
5	3, 4	syl6eqr 2674	. . . . . . 7 |- ( w = W -> ( Base ` w ) = V )
6	5	pweqd 4163	. . . . . 6 |- ( w = W -> ~P ( Base ` w ) = ~P V )
7	6	difeq1d 3727	. . . . 5 |- ( w = W -> ( ~P ( Base ` w ) \ { (/) } ) = ( ~P V \ { (/) } ) )
8		fveq2 6191	. . . . . . . . 9 |- ( w = W -> (Scalar ` w ) = (Scalar ` W ) )
9		lssset.f	. . . . . . . . 9 |- F = (Scalar ` W )
10	8, 9	syl6eqr 2674	. . . . . . . 8 |- ( w = W -> (Scalar ` w ) = F )
11	10	fveq2d 6195	. . . . . . 7 |- ( w = W -> ( Base ` (Scalar ` w ) ) = ( Base ` F ) )
12		lssset.b	. . . . . . 7 |- B = ( Base ` F )
13	11, 12	syl6eqr 2674	. . . . . 6 |- ( w = W -> ( Base ` (Scalar ` w ) ) = B )
14		fveq2 6191	. . . . . . . . . . . 12 |- ( w = W -> ( .s ` w ) = ( .s ` W ) )
15		lssset.t	. . . . . . . . . . . 12 |- .x. = ( .s ` W )
16	14, 15	syl6eqr 2674	. . . . . . . . . . 11 |- ( w = W -> ( .s ` w ) = .x. )
17	16	oveqd 6667	. . . . . . . . . 10 |- ( w = W -> ( x ( .s ` w ) a ) = ( x .x. a ) )
18	17	oveq1d 6665	. . . . . . . . 9 |- ( w = W -> ( ( x ( .s ` w ) a ) ( +g ` w ) b ) = ( ( x .x. a ) ( +g ` w ) b ) )
19		fveq2 6191	. . . . . . . . . . 11 |- ( w = W -> ( +g ` w ) = ( +g ` W ) )
20		lssset.p	. . . . . . . . . . 11 |- .+ = ( +g ` W )
21	19, 20	syl6eqr 2674	. . . . . . . . . 10 |- ( w = W -> ( +g ` w ) = .+ )
22	21	oveqd 6667	. . . . . . . . 9 |- ( w = W -> ( ( x .x. a ) ( +g ` w ) b ) = ( ( x .x. a ) .+ b ) )
23	18, 22	eqtrd 2656	. . . . . . . 8 |- ( w = W -> ( ( x ( .s ` w ) a ) ( +g ` w ) b ) = ( ( x .x. a ) .+ b ) )
24	23	eleq1d 2686	. . . . . . 7 |- ( w = W -> ( ( ( x ( .s ` w ) a ) ( +g ` w ) b ) e. s <-> ( ( x .x. a ) .+ b ) e. s ) )
25	24	2ralbidv 2989	. . . . . 6 |- ( 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	13, 25	raleqbidv 3152	. . . . 5 |- ( 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	7, 26	rabeqbidv 3195	. . . 4 |- ( 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 18933	. . . 4 |- 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		fvex 6201	. . . . . . . 8 |- ( Base ` W ) e. _V
30	4, 29	eqeltri 2697	. . . . . . 7 |- V e. _V
31	30	pwex 4848	. . . . . 6 |- ~P V e. _V
32		difexg 4808	. . . . . 6 |- ( ~P V e. _V -> ( ~P V \ { (/) } ) e. _V )
33	31, 32	ax-mp 5	. . . . 5 |- ( ~P V \ { (/) } ) e. _V
34	33	rabex 4813	. . . 4 |- { s e. ( ~P V \ { (/) } ) | A. x e. B A. a e. s A. b e. s ( ( x .x. a ) .+ b ) e. s } e. _V
35	27, 28, 34	fvmpt 6282	. . 3 |- ( 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 } )
36	2, 35	syl 17	. 2 |- ( 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 } )
37	1, 36	syl5eq 2668	1 |- ( 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 } )

Syntax hints:   -> wi 4   = wceq 1483   e. wcel 1990   A.wral 2912   {crab 2916   _Vcvv 3200   \ cdif 3571   (/)c0 3915   ~Pcpw 4158   {csn 4177   ` cfv 5888  (class class class)co 6650   Basecbs 15857   +g cplusg 15941  Scalarcsca 15944   .scvsca 15945   LSubSpclss 18932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-iota 5851  df-fun 5890  df-fv 5896  df-ov 6653  df-lss 18933

This theorem is referenced by:  islss  18935