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 adj h T BndLinOp

Proof

Step Hyp Ref Expression
1 bdopadj T BndLinOp T dom adj h
2 adjval T dom adj h adj h T = ι t | x y x ih T y = t x ih y
3 1 2 syl T BndLinOp adj h T = ι t | x y x ih T y = t x ih y
4 cnlnadj T LinOp ContOp t LinOp ContOp x y T x ih y = x ih t y
5 lncnopbd T LinOp ContOp T BndLinOp
6 lncnbd LinOp ContOp = BndLinOp
7 6 rexeqi t LinOp ContOp x y T x ih y = x ih t y t BndLinOp x y T x ih y = x ih t y
8 4 5 7 3imtr3i T BndLinOp t BndLinOp x y T x ih y = x ih t y
9 bdopf T BndLinOp T :
10 bdopf t BndLinOp t :
11 adjsym T : t : x y x ih T y = t x ih y x y x ih t y = T x ih y
12 9 10 11 syl2an T BndLinOp t BndLinOp x y x ih T y = t x ih y x y x ih t y = T x ih y
13 eqcom T x ih y = x ih t y x ih t y = T x ih y
14 13 2ralbii x y T x ih y = x ih t y x y x ih t y = T x ih y
15 12 14 bitr4di T BndLinOp t BndLinOp x y x ih T y = t x ih y x y T x ih y = x ih t y
16 15 rexbidva T BndLinOp t BndLinOp x y x ih T y = t x ih y t BndLinOp x y T x ih y = x ih t y
17 8 16 mpbird T BndLinOp t BndLinOp x y x ih T y = t x ih y
18 adjeu T : T dom adj h ∃! t x y x ih T y = t x ih y
19 9 18 syl T BndLinOp T dom adj h ∃! t x y x ih T y = t x ih y
20 1 19 mpbid T BndLinOp ∃! t x y x ih T y = t x ih y
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 ih T y = t x ih y x y x ih T y = t x ih y
26 25 rgenw t BndLinOp x y x ih T y = t x ih y x y x ih T y = t x ih y
27 riotass2 BndLinOp t BndLinOp x y x ih T y = t x ih y x y x ih T y = t x ih y t BndLinOp x y x ih T y = t x ih y ∃! t x y x ih T y = t x ih y ι t BndLinOp | x y x ih T y = t x ih y = ι t | x y x ih T y = t x ih y
28 24 26 27 mpanl12 t BndLinOp x y x ih T y = t x ih y ∃! t x y x ih T y = t x ih y ι t BndLinOp | x y x ih T y = t x ih y = ι t | x y x ih T y = t x ih y
29 17 20 28 syl2anc T BndLinOp ι t BndLinOp | x y x ih T y = t x ih y = ι t | x y x ih T y = t x ih y
30 3 29 eqtr4d T BndLinOp adj h T = ι t BndLinOp | x y x ih T y = t x ih y
31 24 a1i T BndLinOp BndLinOp
32 reuss BndLinOp t BndLinOp x y x ih T y = t x ih y ∃! t x y x ih T y = t x ih y ∃! t BndLinOp x y x ih T y = t x ih y
33 31 17 20 32 syl3anc T BndLinOp ∃! t BndLinOp x y x ih T y = t x ih y
34 riotacl ∃! t BndLinOp x y x ih T y = t x ih y ι t BndLinOp | x y x ih T y = t x ih y BndLinOp
35 33 34 syl T BndLinOp ι t BndLinOp | x y x ih T y = t x ih y BndLinOp
36 30 35 eqeltrd T BndLinOp adj h T BndLinOp