Theorem thlle

Description: Ordering on the Hilbert lattice of closed subspaces. (Contributed by Mario Carneiro, 25-Oct-2015)

	Ref	Expression
Hypotheses	thlval.k	|- K = ( toHL ` W )
	thlbas.c	|- C = ( ClSubSp ` W )
	thlle.i	|- I = ( toInc ` C )
	thlle.l	|- .<_ = ( le ` I )
Assertion	thlle	|- .<_ = ( le ` K )

Proof

Step	Hyp	Ref	Expression
1		thlval.k	|- K = ( toHL ` W )
2		thlbas.c	|- C = ( ClSubSp ` W )
3		thlle.i	|- I = ( toInc ` C )
4		thlle.l	|- .<_ = ( le ` I )
5		pleid	|- le = Slot ( le ` ndx )
6		10re	|- ; 1 0 e. RR
7		1nn0	|- 1 e. NN0
8		0nn0	|- 0 e. NN0
9		1nn	|- 1 e. NN
10		0lt1	|- 0 < 1
11	7 8 9 10	declt	|- ; 1 0 < ; 1 1
12	6 11	ltneii	|- ; 1 0 =/= ; 1 1
13		plendx	|- ( le ` ndx ) = ; 1 0
14		ocndx	|- ( oc ` ndx ) = ; 1 1
15	13 14	neeq12i	|- ( ( le ` ndx ) =/= ( oc ` ndx ) <-> ; 1 0 =/= ; 1 1 )
16	12 15	mpbir	|- ( le ` ndx ) =/= ( oc ` ndx )
17	5 16	setsnid	|- ( le ` I ) = ( le ` ( I sSet <. ( oc ` ndx ) , ( ocv ` W ) >. ) )
18	4 17	eqtri	|- .<_ = ( le ` ( I sSet <. ( oc ` ndx ) , ( ocv ` W ) >. ) )
19		eqid	|- ( ocv ` W ) = ( ocv ` W )
20	1 2 3 19	thlval	|- ( W e. _V -> K = ( I sSet <. ( oc ` ndx ) , ( ocv ` W ) >. ) )
21	20	fveq2d	|- ( W e. _V -> ( le ` K ) = ( le ` ( I sSet <. ( oc ` ndx ) , ( ocv ` W ) >. ) ) )
22	18 21	eqtr4id	|- ( W e. _V -> .<_ = ( le ` K ) )
23	5	str0	|- (/) = ( le ` (/) )
24	2	fvexi	|- C e. _V
25	3	ipolerval	|- ( C e. _V -> { <. x , y >. | ( { x , y } C_ C /\ x C_ y ) } = ( le ` I ) )
26	24 25	ax-mp	|- { <. x , y >. | ( { x , y } C_ C /\ x C_ y ) } = ( le ` I )
27	4 26	eqtr4i	|- .<_ = { <. x , y >. | ( { x , y } C_ C /\ x C_ y ) }
28		opabn0	|- ( { <. x , y >. | ( { x , y } C_ C /\ x C_ y ) } =/= (/) <-> E. x E. y ( { x , y } C_ C /\ x C_ y ) )
29		vex	|- x e. _V
30		vex	|- y e. _V
31	29 30	prss	|- ( ( x e. C /\ y e. C ) <-> { x , y } C_ C )
32		elfvex	|- ( x e. ( ClSubSp ` W ) -> W e. _V )
33	32 2	eleq2s	|- ( x e. C -> W e. _V )
34	33	ad2antrr	|- ( ( ( x e. C /\ y e. C ) /\ x C_ y ) -> W e. _V )
35	31 34	sylanbr	|- ( ( { x , y } C_ C /\ x C_ y ) -> W e. _V )
36	35	exlimivv	|- ( E. x E. y ( { x , y } C_ C /\ x C_ y ) -> W e. _V )
37	28 36	sylbi	|- ( { <. x , y >. | ( { x , y } C_ C /\ x C_ y ) } =/= (/) -> W e. _V )
38	37	necon1bi	|- ( -. W e. _V -> { <. x , y >. | ( { x , y } C_ C /\ x C_ y ) } = (/) )
39	27 38	eqtrid	|- ( -. W e. _V -> .<_ = (/) )
40		fvprc	|- ( -. W e. _V -> ( toHL ` W ) = (/) )
41	1 40	eqtrid	|- ( -. W e. _V -> K = (/) )
42	41	fveq2d	|- ( -. W e. _V -> ( le ` K ) = ( le ` (/) ) )
43	23 39 42	3eqtr4a	|- ( -. W e. _V -> .<_ = ( le ` K ) )
44	22 43	pm2.61i	|- .<_ = ( le ` K )