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	⊢ ( 𝑇 ∈ dom adj_ℎ → 𝑇 : ℋ ⟶ ℋ )

Proof

Step	Hyp	Ref	Expression
1		dmadjss	⊢ dom adj_ℎ ⊆ ( ℋ ↑_m ℋ )
2	1	sseli	⊢ ( 𝑇 ∈ dom adj_ℎ → 𝑇 ∈ ( ℋ ↑_m ℋ ) )
3		ax-hilex	⊢ ℋ ∈ V
4	3 3	elmap	⊢ ( 𝑇 ∈ ( ℋ ↑_m ℋ ) ↔ 𝑇 : ℋ ⟶ ℋ )
5	2 4	sylib	⊢ ( 𝑇 ∈ dom adj_ℎ → 𝑇 : ℋ ⟶ ℋ )