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 ⊢ T ∈ LinOp
cnlnadj.2 ⊢ T ∈ ContOp
Assertion cnlnadji ⊢ ∃ t ∈ LinOp ∩ ContOp ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih t ⁡ y

Proof

Step Hyp Ref Expression
1 cnlnadj.1 ⊢ T ∈ LinOp
2 cnlnadj.2 ⊢ T ∈ ContOp
3 eqid ⊢ g ∈ ℋ ⟼ T ⁡ g ⋅ ih z = g ∈ ℋ ⟼ T ⁡ g ⋅ ih z
4 oveq2 ⊢ f = w → v ⋅ ih f = v ⋅ ih w
5 4 eqeq2d ⊢ f = w → T ⁡ v ⋅ ih z = v ⋅ ih f ↔ T ⁡ v ⋅ ih z = v ⋅ ih w
6 5 ralbidv ⊢ f = w → ∀ v ∈ ℋ T ⁡ v ⋅ ih z = v ⋅ ih f ↔ ∀ v ∈ ℋ T ⁡ v ⋅ ih z = v ⋅ ih w
7 6 cbvriotavw ⊢ ι f ∈ ℋ | ∀ v ∈ ℋ T ⁡ v ⋅ ih z = v ⋅ ih f = ι w ∈ ℋ | ∀ v ∈ ℋ T ⁡ v ⋅ ih z = v ⋅ ih w
8 eqid ⊢ z ∈ ℋ ⟼ ι f ∈ ℋ | ∀ v ∈ ℋ T ⁡ v ⋅ ih z = v ⋅ ih f = z ∈ ℋ ⟼ ι f ∈ ℋ | ∀ v ∈ ℋ T ⁡ v ⋅ ih z = v ⋅ ih f
9 1 2 3 7 8 cnlnadjlem9 ⊢ ∃ t ∈ LinOp ∩ ContOp ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih t ⁡ y