Metamath Proof Explorer

Theorem cnlnadjeu

Description: Every continuous linear operator has a unique adjoint. Theorem 3.10 of Beran p. 104. (Contributed by NM, 19-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion cnlnadjeu ⊢ T ∈ LinOp ∩ ContOp → ∃! t ∈ LinOp ∩ ContOp ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih t ⁡ y

Proof

Step Hyp Ref Expression
1 fveq1 ⊢ T = if T ∈ LinOp ∩ ContOp T 0 hop → T ⁡ x = if T ∈ LinOp ∩ ContOp T 0 hop ⁡ x
2 1 oveq1d ⊢ T = if T ∈ LinOp ∩ ContOp T 0 hop → T ⁡ x ⋅ ih y = if T ∈ LinOp ∩ ContOp T 0 hop ⁡ x ⋅ ih y
3 2 eqeq1d ⊢ T = if T ∈ LinOp ∩ ContOp T 0 hop → T ⁡ x ⋅ ih y = x ⋅ ih t ⁡ y ↔ if T ∈ LinOp ∩ ContOp T 0 hop ⁡ x ⋅ ih y = x ⋅ ih t ⁡ y
4 3 2ralbidv ⊢ T = if T ∈ LinOp ∩ ContOp T 0 hop → ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih t ⁡ y ↔ ∀ x ∈ ℋ ∀ y ∈ ℋ if T ∈ LinOp ∩ ContOp T 0 hop ⁡ x ⋅ ih y = x ⋅ ih t ⁡ y
5 4 reubidv ⊢ T = if T ∈ LinOp ∩ ContOp T 0 hop → ∃! t ∈ LinOp ∩ ContOp ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih t ⁡ y ↔ ∃! t ∈ LinOp ∩ ContOp ∀ x ∈ ℋ ∀ y ∈ ℋ if T ∈ LinOp ∩ ContOp T 0 hop ⁡ x ⋅ ih y = x ⋅ ih t ⁡ y
6 inss1 ⊢ LinOp ∩ ContOp ⊆ LinOp
7 0lnop ⊢ 0 hop ∈ LinOp
8 0cnop ⊢ 0 hop ∈ ContOp
9 elin ⊢ 0 hop ∈ LinOp ∩ ContOp ↔ 0 hop ∈ LinOp ∧ 0 hop ∈ ContOp
10 7 8 9 mpbir2an ⊢ 0 hop ∈ LinOp ∩ ContOp
11 10 elimel ⊢ if T ∈ LinOp ∩ ContOp T 0 hop ∈ LinOp ∩ ContOp
12 6 11 sselii ⊢ if T ∈ LinOp ∩ ContOp T 0 hop ∈ LinOp
13 inss2 ⊢ LinOp ∩ ContOp ⊆ ContOp
14 13 11 sselii ⊢ if T ∈ LinOp ∩ ContOp T 0 hop ∈ ContOp
15 12 14 cnlnadjeui ⊢ ∃! t ∈ LinOp ∩ ContOp ∀ x ∈ ℋ ∀ y ∈ ℋ if T ∈ LinOp ∩ ContOp T 0 hop ⁡ x ⋅ ih y = x ⋅ ih t ⁡ y
16 5 15 dedth ⊢ T ∈ LinOp ∩ ContOp → ∃! t ∈ LinOp ∩ ContOp ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih t ⁡ y