Metamath Proof Explorer

Theorem cnlnadj

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

Proof

Step Hyp Ref Expression
1 cnlnadjeu ⊢ T ∈ LinOp ∩ ContOp → ∃! t ∈ LinOp ∩ ContOp ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih t ⁡ y
2 reurex ⊢ ∃! t ∈ LinOp ∩ ContOp ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih t ⁡ y → ∃ t ∈ LinOp ∩ ContOp ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih t ⁡ y
3 1 2 syl ⊢ T ∈ LinOp ∩ ContOp → ∃ t ∈ LinOp ∩ ContOp ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih t ⁡ y