Theorem thlleval

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 )
	thlleval.l	|- .<_ = ( le ` K )
Assertion	thlleval	|- ( ( S e. C /\ T e. C ) -> ( S .<_ T <-> S C_ T ) )

Proof

Step	Hyp	Ref	Expression
1		thlval.k	|- K = ( toHL ` W )
2		thlbas.c	|- C = ( ClSubSp ` W )
3		thlleval.l	|- .<_ = ( le ` K )
4	2	fvexi	|- C e. _V
5		eqid	|- ( toInc ` C ) = ( toInc ` C )
6		eqid	|- ( le ` ( toInc ` C ) ) = ( le ` ( toInc ` C ) )
7	1 2 5 6	thlle	|- ( le ` ( toInc ` C ) ) = ( le ` K )
8	3 7	eqtr4i	|- .<_ = ( le ` ( toInc ` C ) )
9	5 8	ipole	|- ( ( C e. _V /\ S e. C /\ T e. C ) -> ( S .<_ T <-> S C_ T ) )
10	4 9	mp3an1	|- ( ( S e. C /\ T e. C ) -> ( S .<_ T <-> S C_ T ) )