# Metamath Proof Explorer

Description: Every continuous linear operator has a unique 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 cnlnadjeui $⊢ ∃! 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 1 2 cnlnadji $⊢ ∃ t ∈ LinOp ∩ ContOp ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih t ⁡ y$
4 adjmo $⊢ ∃* t t : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = t ⁡ x ⋅ ih y$
5 inss1 $⊢ LinOp ∩ ContOp ⊆ LinOp$
6 5 sseli $⊢ t ∈ LinOp ∩ ContOp → t ∈ LinOp$
7 lnopf $⊢ t ∈ LinOp → t : ℋ ⟶ ℋ$
8 6 7 syl $⊢ t ∈ LinOp ∩ ContOp → t : ℋ ⟶ ℋ$
9 simpl $⊢ t : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih t ⁡ y → t : ℋ ⟶ ℋ$
10 eqcom $⊢ T ⁡ x ⋅ ih y = x ⋅ ih t ⁡ y ↔ x ⋅ ih t ⁡ y = T ⁡ x ⋅ ih y$
11 10 2ralbii $⊢ ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih t ⁡ y ↔ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih t ⁡ y = T ⁡ x ⋅ ih y$
12 1 lnopfi $⊢ T : ℋ ⟶ ℋ$
13 adjsym $⊢ t : ℋ ⟶ ℋ ∧ T : ℋ ⟶ ℋ → ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih t ⁡ y = T ⁡ x ⋅ ih y ↔ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = t ⁡ x ⋅ ih y$
14 12 13 mpan2 $⊢ t : ℋ ⟶ ℋ → ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih t ⁡ y = T ⁡ x ⋅ ih y ↔ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = t ⁡ x ⋅ ih y$
15 11 14 syl5bb $⊢ t : ℋ ⟶ ℋ → ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih t ⁡ y ↔ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = t ⁡ x ⋅ ih y$
16 15 biimpa $⊢ t : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih t ⁡ y → ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = t ⁡ x ⋅ ih y$
17 9 16 jca $⊢ t : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih t ⁡ y → t : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = t ⁡ x ⋅ ih y$
18 8 17 sylan $⊢ t ∈ LinOp ∩ ContOp ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih t ⁡ y → t : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = t ⁡ x ⋅ ih y$
19 18 moimi $⊢ ∃* t t : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = t ⁡ x ⋅ ih y → ∃* t t ∈ LinOp ∩ ContOp ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih t ⁡ y$
20 df-rmo $⊢ ∃* t ∈ LinOp ∩ ContOp ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih t ⁡ y ↔ ∃* t t ∈ LinOp ∩ ContOp ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih t ⁡ y$
21 19 20 sylibr $⊢ ∃* t t : ℋ ⟶ ℋ ∧ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = t ⁡ x ⋅ ih y → ∃* t ∈ LinOp ∩ ContOp ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih t ⁡ y$
22 4 21 ax-mp $⊢ ∃* t ∈ LinOp ∩ ContOp ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih t ⁡ y$
23 reu5 $⊢ ∃! 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 ∧ ∃* t ∈ LinOp ∩ ContOp ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih t ⁡ y$
24 3 22 23 mpbir2an $⊢ ∃! t ∈ LinOp ∩ ContOp ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih t ⁡ y$