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 ( 𝑡 ‘ 𝑦 ) )