Metamath Proof Explorer


Theorem thlleval

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

Ref Expression
Hypotheses thlval.k K=toHLW
thlbas.c C=ClSubSpW
thlleval.l ˙=K
Assertion thlleval SCTCS˙TST

Proof

Step Hyp Ref Expression
1 thlval.k K=toHLW
2 thlbas.c C=ClSubSpW
3 thlleval.l ˙=K
4 2 fvexi CV
5 eqid toIncC=toIncC
6 eqid toIncC=toIncC
7 1 2 5 6 thlle toIncC=K
8 3 7 eqtr4i ˙=toIncC
9 5 8 ipole CVSCTCS˙TST
10 4 9 mp3an1 SCTCS˙TST