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⋅ihy=x⋅iht⁡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⋅ihy=x⋅iht⁡y
4 adjmo ⊢∃*tt:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋx⋅ihT⁡y=t⁡x⋅ihy
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⋅ihy=x⋅iht⁡y→t:ℋ⟶ℋ
10 eqcom ⊢T⁡x⋅ihy=x⋅iht⁡y↔x⋅iht⁡y=T⁡x⋅ihy
11 10 2ralbii ⊢∀x∈ℋ∀y∈ℋT⁡x⋅ihy=x⋅iht⁡y↔∀x∈ℋ∀y∈ℋx⋅iht⁡y=T⁡x⋅ihy
12 1 lnopfi ⊢T:ℋ⟶ℋ
13 adjsym ⊢t:ℋ⟶ℋ∧T:ℋ⟶ℋ→∀x∈ℋ∀y∈ℋx⋅iht⁡y=T⁡x⋅ihy↔∀x∈ℋ∀y∈ℋx⋅ihT⁡y=t⁡x⋅ihy
14 12 13 mpan2 ⊢t:ℋ⟶ℋ→∀x∈ℋ∀y∈ℋx⋅iht⁡y=T⁡x⋅ihy↔∀x∈ℋ∀y∈ℋx⋅ihT⁡y=t⁡x⋅ihy
15 11 14 bitrid ⊢t:ℋ⟶ℋ→∀x∈ℋ∀y∈ℋT⁡x⋅ihy=x⋅iht⁡y↔∀x∈ℋ∀y∈ℋx⋅ihT⁡y=t⁡x⋅ihy
16 15 biimpa ⊢t:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋT⁡x⋅ihy=x⋅iht⁡y→∀x∈ℋ∀y∈ℋx⋅ihT⁡y=t⁡x⋅ihy
17 9 16 jca ⊢t:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋT⁡x⋅ihy=x⋅iht⁡y→t:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋx⋅ihT⁡y=t⁡x⋅ihy
18 8 17 sylan ⊢t∈LinOp∩ContOp∧∀x∈ℋ∀y∈ℋT⁡x⋅ihy=x⋅iht⁡y→t:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋx⋅ihT⁡y=t⁡x⋅ihy
19 18 moimi ⊢∃*tt:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋx⋅ihT⁡y=t⁡x⋅ihy→∃*tt∈LinOp∩ContOp∧∀x∈ℋ∀y∈ℋT⁡x⋅ihy=x⋅iht⁡y
20 df-rmo ⊢∃*t∈LinOp∩ContOp∀x∈ℋ∀y∈ℋT⁡x⋅ihy=x⋅iht⁡y↔∃*tt∈LinOp∩ContOp∧∀x∈ℋ∀y∈ℋT⁡x⋅ihy=x⋅iht⁡y
21 19 20 sylibr ⊢∃*tt:ℋ⟶ℋ∧∀x∈ℋ∀y∈ℋx⋅ihT⁡y=t⁡x⋅ihy→∃*t∈LinOp∩ContOp∀x∈ℋ∀y∈ℋT⁡x⋅ihy=x⋅iht⁡y
22 4 21 ax-mp ⊢∃*t∈LinOp∩ContOp∀x∈ℋ∀y∈ℋT⁡x⋅ihy=x⋅iht⁡y
23 reu5 ⊢∃!t∈LinOp∩ContOp∀x∈ℋ∀y∈ℋT⁡x⋅ihy=x⋅iht⁡y↔∃t∈LinOp∩ContOp∀x∈ℋ∀y∈ℋT⁡x⋅ihy=x⋅iht⁡y∧∃*t∈LinOp∩ContOp∀x∈ℋ∀y∈ℋT⁡x⋅ihy=x⋅iht⁡y
24 3 22 23 mpbir2an ⊢∃!t∈LinOp∩ContOp∀x∈ℋ∀y∈ℋT⁡x⋅ihy=x⋅iht⁡y