Theorem psubclsetN 30418

Description: The set of closed projective subspaces in a Hilbert lattice. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.)

Hypotheses

Ref	Expression
psubclset.a	|- A = ( Atoms ` K )
psubclset.p	|- ._|_ = ( _|_ P ` K )
psubclset.c	|- C = ( PSubCl ` K )

Assertion

Ref	Expression
psubclsetN	|- ( K e. B -> C = { s | ( s C_ A /\ ( ._|_ ` ( ._|_ ` s ) ) = s ) } )

Distinct variable groups:   A, s   K, s

Allowed substitution hints:   B( s)   C( s)   ._|_ ( s)

Proof of Theorem psubclsetN

Dummy variable k is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 2924	. 2 |- ( K e. B -> K e. _V )
2		psubclset.c	. . 3 |- C = ( PSubCl ` K )
3		fveq2 5687	. . . . . . . 8 |- ( k = K -> ( Atoms ` k ) = ( Atoms ` K ) )
4		psubclset.a	. . . . . . . 8 |- A = ( Atoms ` K )
5	3, 4	syl6eqr 2454	. . . . . . 7 |- ( k = K -> ( Atoms ` k ) = A )
6	5	sseq2d 3336	. . . . . 6 |- ( k = K -> ( s C_ ( Atoms ` k ) <-> s C_ A ) )
7		fveq2 5687	. . . . . . . . 9 |- ( k = K -> ( _|_ P ` k ) = ( _|_ P ` K ) )
8		psubclset.p	. . . . . . . . 9 |- ._|_ = ( _|_ P ` K )
9	7, 8	syl6eqr 2454	. . . . . . . 8 |- ( k = K -> ( _|_ P ` k ) = ._|_ )
10	9	fveq1d 5689	. . . . . . . 8 |- ( k = K -> ( ( _|_ P ` k ) ` s ) = ( ._|_ ` s ) )
11	9, 10	fveq12d 5693	. . . . . . 7 |- ( k = K -> ( ( _|_ P ` k ) ` ( ( _|_ P ` k ) ` s ) ) = ( ._|_ ` ( ._|_ ` s ) ) )
12	11	eqeq1d 2412	. . . . . 6 |- ( k = K -> ( ( ( _|_ P ` k ) ` ( ( _|_ P ` k ) ` s ) ) = s <-> ( ._|_ ` ( ._|_ ` s ) ) = s ) )
13	6, 12	anbi12d 692	. . . . 5 |- ( k = K -> ( ( s C_ ( Atoms ` k ) /\ ( ( _|_ P ` k ) ` ( ( _|_ P ` k ) ` s ) ) = s ) <-> ( s C_ A /\ ( ._|_ ` ( ._|_ ` s ) ) = s ) ) )
14	13	abbidv 2518	. . . 4 |- ( k = K -> { s | ( s C_ ( Atoms ` k ) /\ ( ( _|_ P ` k ) ` ( ( _|_ P ` k ) ` s ) ) = s ) } = { s | ( s C_ A /\ ( ._|_ ` ( ._|_ ` s ) ) = s ) } )
15		df-psubclN 30417	. . . 4 |- PSubCl = ( k e. _V |-> { s | ( s C_ ( Atoms ` k ) /\ ( ( _|_ P ` k ) ` ( ( _|_ P ` k ) ` s ) ) = s ) } )
16		fvex 5701	. . . . . . 7 |- ( Atoms ` K ) e. _V
17	4, 16	eqeltri 2474	. . . . . 6 |- A e. _V
18	17	pwex 4342	. . . . 5 |- ~P A e. _V
19		df-pw 3761	. . . . . . . . 9 |- ~P A = { s | s C_ A }
20	19	abeq2i 2511	. . . . . . . 8 |- ( s e. ~P A <-> s C_ A )
21	20	anbi1i 677	. . . . . . 7 |- ( ( s e. ~P A /\ ( ._|_ ` ( ._|_ ` s ) ) = s ) <-> ( s C_ A /\ ( ._|_ ` ( ._|_ ` s ) ) = s ) )
22	21	abbii 2516	. . . . . 6 |- { s | ( s e. ~P A /\ ( ._|_ ` ( ._|_ ` s ) ) = s ) } = { s | ( s C_ A /\ ( ._|_ ` ( ._|_ ` s ) ) = s ) }
23		ssab2 3387	. . . . . 6 |- { s | ( s e. ~P A /\ ( ._|_ ` ( ._|_ ` s ) ) = s ) } C_ ~P A
24	22, 23	eqsstr3i 3339	. . . . 5 |- { s | ( s C_ A /\ ( ._|_ ` ( ._|_ ` s ) ) = s ) } C_ ~P A
25	18, 24	ssexi 4308	. . . 4 |- { s | ( s C_ A /\ ( ._|_ ` ( ._|_ ` s ) ) = s ) } e. _V
26	14, 15, 25	fvmpt 5765	. . 3 |- ( K e. _V -> ( PSubCl ` K ) = { s | ( s C_ A /\ ( ._|_ ` ( ._|_ ` s ) ) = s ) } )
27	2, 26	syl5eq 2448	. 2 |- ( K e. _V -> C = { s | ( s C_ A /\ ( ._|_ ` ( ._|_ ` s ) ) = s ) } )
28	1, 27	syl 16	1 |- ( K e. B -> C = { s | ( s C_ A /\ ( ._|_ ` ( ._|_ ` s ) ) = s ) } )

Syntax hints:   -> wi 4   /\ wa 359   = wceq 1649   e. wcel 1721   {cab 2390   _Vcvv 2916   C_ wss 3280   ~Pcpw 3759   ` cfv 5413   Atomscatm 29746   _|_ PcpolN 30384   PSubClcpscN 30416

This theorem is referenced by:  ispsubclN  30419

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-sbc 3122  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-opab 4227  df-mpt 4228  df-id 4458  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-iota 5377  df-fun 5415  df-fv 5421  df-psubclN 30417