df-thl

Description: Define the Hilbert lattice of closed subspaces of a given pre-Hilbert space. (Contributed by Mario Carneiro, 25-Oct-2015)

		Ref	Expression
	Assertion	df-thl	$⊢ toHL = (h \in V ⟼ toInc (ClSubSp (h)) sSet ⟨oc (ndx), ocv (h)⟩)$

Step	Hyp	Ref	Expression
0		cthl	$class toHL$
1		vh	$setvar h$
2		cvv	$class V$
3		cipo	$class toInc$
4		ccss	$class ClSubSp$
5	1	cv	$setvar h$
6	5 4	cfv	$class ClSubSp (h)$
7	6 3	cfv	$class toInc (ClSubSp (h))$
8		csts	$class sSet$
9		coc	$class oc$
10		cnx	$class ndx$
11	10 9	cfv	$class oc (ndx)$
12		cocv	$class ocv$
13	5 12	cfv	$class ocv (h)$
14	11 13	cop	$class ⟨oc (ndx), ocv (h)⟩$
15	7 14 8	co	$class (toInc (ClSubSp (h)) sSet ⟨oc (ndx), ocv (h)⟩)$
16	1 2 15	cmpt	$class (h \in V ⟼ toInc (ClSubSp (h)) sSet ⟨oc (ndx), ocv (h)⟩)$
17	0 16	wceq	$wff toHL = (h \in V ⟼ toInc (ClSubSp (h)) sSet ⟨oc (ndx), ocv (h)⟩)$

Metamath Proof Explorer