Metamath Proof Explorer

Theorem cnlnadjeui

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 bitrid ⊢ 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