This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dmadjop

Description: A member of the domain of the adjoint function is a Hilbert space operator. (Contributed by NM, 15-Feb-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	dmadjop	$⊢ T \in dom {adj}_{h} \to T : ℋ ⟶ ℋ$

Proof

Step	Hyp	Ref	Expression
1		dmadjss	$⊢ dom {adj}_{h} \subseteq ℋ^{ℋ}$
2	1	sseli	$⊢ T \in dom {adj}_{h} \to T \in (ℋ^{ℋ})$
3		ax-hilex	$⊢ ℋ \in V$
4	3 3	elmap	$⊢ T \in (ℋ^{ℋ}) \leftrightarrow T : ℋ ⟶ ℋ$
5	2 4	sylib	$⊢ T \in dom {adj}_{h} \to T : ℋ ⟶ ℋ$