Description: Ordering on the Hilbert lattice of closed subspaces. (Contributed by Mario Carneiro, 25-Oct-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | thlval.k | |
|
thlbas.c | |
||
thlleval.l | |
||
Assertion | thlleval | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | thlval.k | |
|
2 | thlbas.c | |
|
3 | thlleval.l | |
|
4 | 2 | fvexi | |
5 | eqid | |
|
6 | eqid | |
|
7 | 1 2 5 6 | thlle | |
8 | 3 7 | eqtr4i | |
9 | 5 8 | ipole | |
10 | 4 9 | mp3an1 | |