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

Metamath Proof Explorer

Theorem cnlnadji

Description: Every continuous linear operator has an adjoint. Theorem 3.10 of Beran p. 104. (Contributed by NM, 18-Feb-2006) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	cnlnadj.1	⊢ 𝑇 ∈ LinOp
		cnlnadj.2	⊢ 𝑇 ∈ ContOp
	Assertion	cnlnadji	⊢ ∃ 𝑡 ∈ ( LinOp ∩ ContOp ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·_ih 𝑦 ) = ( 𝑥 ·_ih ( 𝑡 ‘ 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		cnlnadj.1	⊢ 𝑇 ∈ LinOp
2		cnlnadj.2	⊢ 𝑇 ∈ ContOp
3		eqid	⊢ ( 𝑔 ∈ ℋ ↦ ( ( 𝑇 ‘ 𝑔 ) ·_ih 𝑧 ) ) = ( 𝑔 ∈ ℋ ↦ ( ( 𝑇 ‘ 𝑔 ) ·_ih 𝑧 ) )
4		oveq2	⊢ ( 𝑓 = 𝑤 → ( 𝑣 ·_ih 𝑓 ) = ( 𝑣 ·_ih 𝑤 ) )
5	4	eqeq2d	⊢ ( 𝑓 = 𝑤 → ( ( ( 𝑇 ‘ 𝑣 ) ·_ih 𝑧 ) = ( 𝑣 ·_ih 𝑓 ) ↔ ( ( 𝑇 ‘ 𝑣 ) ·_ih 𝑧 ) = ( 𝑣 ·_ih 𝑤 ) ) )
6	5	ralbidv	⊢ ( 𝑓 = 𝑤 → ( ∀ 𝑣 ∈ ℋ ( ( 𝑇 ‘ 𝑣 ) ·_ih 𝑧 ) = ( 𝑣 ·_ih 𝑓 ) ↔ ∀ 𝑣 ∈ ℋ ( ( 𝑇 ‘ 𝑣 ) ·_ih 𝑧 ) = ( 𝑣 ·_ih 𝑤 ) ) )
7	6	cbvriotavw	⊢ ( ℩ 𝑓 ∈ ℋ ∀ 𝑣 ∈ ℋ ( ( 𝑇 ‘ 𝑣 ) ·_ih 𝑧 ) = ( 𝑣 ·_ih 𝑓 ) ) = ( ℩ 𝑤 ∈ ℋ ∀ 𝑣 ∈ ℋ ( ( 𝑇 ‘ 𝑣 ) ·_ih 𝑧 ) = ( 𝑣 ·_ih 𝑤 ) )
8		eqid	⊢ ( 𝑧 ∈ ℋ ↦ ( ℩ 𝑓 ∈ ℋ ∀ 𝑣 ∈ ℋ ( ( 𝑇 ‘ 𝑣 ) ·_ih 𝑧 ) = ( 𝑣 ·_ih 𝑓 ) ) ) = ( 𝑧 ∈ ℋ ↦ ( ℩ 𝑓 ∈ ℋ ∀ 𝑣 ∈ ℋ ( ( 𝑇 ‘ 𝑣 ) ·_ih 𝑧 ) = ( 𝑣 ·_ih 𝑓 ) ) )
9	1 2 3 7 8	cnlnadjlem9	⊢ ∃ 𝑡 ∈ ( LinOp ∩ ContOp ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·_ih 𝑦 ) = ( 𝑥 ·_ih ( 𝑡 ‘ 𝑦 ) )