Metamath Proof Explorer

Theorem adjbdln

Description: The adjoint of a bounded linear operator is a bounded linear operator. (Contributed by NM, 19-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion adjbdln ⊢T∈BndLinOp→adjh⁡T∈BndLinOp

Proof

Step Hyp Ref Expression
1 bdopadj ⊢T∈BndLinOp→T∈dom⁡adjh
2 adjval ⊢T∈dom⁡adjh→adjh⁡T=ιt∈ℋℋ|∀x∈ℋ∀y∈ℋx⋅ihT⁡y=t⁡x⋅ihy
3 1 2 syl ⊢T∈BndLinOp→adjh⁡T=ιt∈ℋℋ|∀x∈ℋ∀y∈ℋx⋅ihT⁡y=t⁡x⋅ihy
4 cnlnadj ⊢T∈LinOp∩ContOp→∃t∈LinOp∩ContOp∀x∈ℋ∀y∈ℋT⁡x⋅ihy=x⋅iht⁡y
5 lncnopbd ⊢T∈LinOp∩ContOp↔T∈BndLinOp
6 lncnbd ⊢LinOp∩ContOp=BndLinOp
7 6 rexeqi ⊢∃t∈LinOp∩ContOp∀x∈ℋ∀y∈ℋT⁡x⋅ihy=x⋅iht⁡y↔∃t∈BndLinOp∀x∈ℋ∀y∈ℋT⁡x⋅ihy=x⋅iht⁡y
8 4 5 7 3imtr3i ⊢T∈BndLinOp→∃t∈BndLinOp∀x∈ℋ∀y∈ℋT⁡x⋅ihy=x⋅iht⁡y
9 bdopf ⊢T∈BndLinOp→T:ℋ⟶ℋ
10 bdopf ⊢t∈BndLinOp→t:ℋ⟶ℋ
11 adjsym ⊢T:ℋ⟶ℋ∧t:ℋ⟶ℋ→∀x∈ℋ∀y∈ℋx⋅ihT⁡y=t⁡x⋅ihy↔∀x∈ℋ∀y∈ℋx⋅iht⁡y=T⁡x⋅ihy
12 9 10 11 syl2an ⊢T∈BndLinOp∧t∈BndLinOp→∀x∈ℋ∀y∈ℋx⋅ihT⁡y=t⁡x⋅ihy↔∀x∈ℋ∀y∈ℋx⋅iht⁡y=T⁡x⋅ihy
13 eqcom ⊢T⁡x⋅ihy=x⋅iht⁡y↔x⋅iht⁡y=T⁡x⋅ihy
14 13 2ralbii ⊢∀x∈ℋ∀y∈ℋT⁡x⋅ihy=x⋅iht⁡y↔∀x∈ℋ∀y∈ℋx⋅iht⁡y=T⁡x⋅ihy
15 12 14 bitr4di ⊢T∈BndLinOp∧t∈BndLinOp→∀x∈ℋ∀y∈ℋx⋅ihT⁡y=t⁡x⋅ihy↔∀x∈ℋ∀y∈ℋT⁡x⋅ihy=x⋅iht⁡y
16 15 rexbidva ⊢T∈BndLinOp→∃t∈BndLinOp∀x∈ℋ∀y∈ℋx⋅ihT⁡y=t⁡x⋅ihy↔∃t∈BndLinOp∀x∈ℋ∀y∈ℋT⁡x⋅ihy=x⋅iht⁡y
17 8 16 mpbird ⊢T∈BndLinOp→∃t∈BndLinOp∀x∈ℋ∀y∈ℋx⋅ihT⁡y=t⁡x⋅ihy
18 adjeu ⊢T:ℋ⟶ℋ→T∈dom⁡adjh↔∃!t∈ℋℋ∀x∈ℋ∀y∈ℋx⋅ihT⁡y=t⁡x⋅ihy
19 9 18 syl ⊢T∈BndLinOp→T∈dom⁡adjh↔∃!t∈ℋℋ∀x∈ℋ∀y∈ℋx⋅ihT⁡y=t⁡x⋅ihy
20 1 19 mpbid ⊢T∈BndLinOp→∃!t∈ℋℋ∀x∈ℋ∀y∈ℋx⋅ihT⁡y=t⁡x⋅ihy
21 ax-hilex ⊢ℋ∈V
22 21 21 elmap ⊢t∈ℋℋ↔t:ℋ⟶ℋ
23 10 22 sylibr ⊢t∈BndLinOp→t∈ℋℋ
24 23 ssriv ⊢BndLinOp⊆ℋℋ
25 id ⊢∀x∈ℋ∀y∈ℋx⋅ihT⁡y=t⁡x⋅ihy→∀x∈ℋ∀y∈ℋx⋅ihT⁡y=t⁡x⋅ihy
26 25 rgenw ⊢∀t∈BndLinOp∀x∈ℋ∀y∈ℋx⋅ihT⁡y=t⁡x⋅ihy→∀x∈ℋ∀y∈ℋx⋅ihT⁡y=t⁡x⋅ihy
27 riotass2 ⊢BndLinOp⊆ℋℋ∧∀t∈BndLinOp∀x∈ℋ∀y∈ℋx⋅ihT⁡y=t⁡x⋅ihy→∀x∈ℋ∀y∈ℋx⋅ihT⁡y=t⁡x⋅ihy∧∃t∈BndLinOp∀x∈ℋ∀y∈ℋx⋅ihT⁡y=t⁡x⋅ihy∧∃!t∈ℋℋ∀x∈ℋ∀y∈ℋx⋅ihT⁡y=t⁡x⋅ihy→ιt∈BndLinOp|∀x∈ℋ∀y∈ℋx⋅ihT⁡y=t⁡x⋅ihy=ιt∈ℋℋ|∀x∈ℋ∀y∈ℋx⋅ihT⁡y=t⁡x⋅ihy
28 24 26 27 mpanl12 ⊢∃t∈BndLinOp∀x∈ℋ∀y∈ℋx⋅ihT⁡y=t⁡x⋅ihy∧∃!t∈ℋℋ∀x∈ℋ∀y∈ℋx⋅ihT⁡y=t⁡x⋅ihy→ιt∈BndLinOp|∀x∈ℋ∀y∈ℋx⋅ihT⁡y=t⁡x⋅ihy=ιt∈ℋℋ|∀x∈ℋ∀y∈ℋx⋅ihT⁡y=t⁡x⋅ihy
29 17 20 28 syl2anc ⊢T∈BndLinOp→ιt∈BndLinOp|∀x∈ℋ∀y∈ℋx⋅ihT⁡y=t⁡x⋅ihy=ιt∈ℋℋ|∀x∈ℋ∀y∈ℋx⋅ihT⁡y=t⁡x⋅ihy
30 3 29 eqtr4d ⊢T∈BndLinOp→adjh⁡T=ιt∈BndLinOp|∀x∈ℋ∀y∈ℋx⋅ihT⁡y=t⁡x⋅ihy
31 24 a1i ⊢T∈BndLinOp→BndLinOp⊆ℋℋ
32 reuss ⊢BndLinOp⊆ℋℋ∧∃t∈BndLinOp∀x∈ℋ∀y∈ℋx⋅ihT⁡y=t⁡x⋅ihy∧∃!t∈ℋℋ∀x∈ℋ∀y∈ℋx⋅ihT⁡y=t⁡x⋅ihy→∃!t∈BndLinOp∀x∈ℋ∀y∈ℋx⋅ihT⁡y=t⁡x⋅ihy
33 31 17 20 32 syl3anc ⊢T∈BndLinOp→∃!t∈BndLinOp∀x∈ℋ∀y∈ℋx⋅ihT⁡y=t⁡x⋅ihy
34 riotacl ⊢∃!t∈BndLinOp∀x∈ℋ∀y∈ℋx⋅ihT⁡y=t⁡x⋅ihy→ιt∈BndLinOp|∀x∈ℋ∀y∈ℋx⋅ihT⁡y=t⁡x⋅ihy∈BndLinOp
35 33 34 syl ⊢T∈BndLinOp→ιt∈BndLinOp|∀x∈ℋ∀y∈ℋx⋅ihT⁡y=t⁡x⋅ihy∈BndLinOp
36 30 35 eqeltrd ⊢T∈BndLinOp→adjh⁡T∈BndLinOp