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 ( 𝑇 ∈ BndLinOp → ( adj𝑇 ) ∈ BndLinOp )

Proof

Step Hyp Ref Expression
1 bdopadj ( 𝑇 ∈ BndLinOp → 𝑇 ∈ dom adj )
2 adjval ( 𝑇 ∈ dom adj → ( adj𝑇 ) = ( 𝑡 ∈ ( ℋ ↑m ℋ ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) ) )
3 1 2 syl ( 𝑇 ∈ BndLinOp → ( adj𝑇 ) = ( 𝑡 ∈ ( ℋ ↑m ℋ ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) ) )
4 cnlnadj ( 𝑇 ∈ ( LinOp ∩ ContOp ) → ∃ 𝑡 ∈ ( LinOp ∩ ContOp ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑡𝑦 ) ) )
5 lncnopbd ( 𝑇 ∈ ( LinOp ∩ ContOp ) ↔ 𝑇 ∈ BndLinOp )
6 lncnbd ( LinOp ∩ ContOp ) = BndLinOp
7 6 rexeqi ( ∃ 𝑡 ∈ ( LinOp ∩ ContOp ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑡𝑦 ) ) ↔ ∃ 𝑡 ∈ BndLinOp ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑡𝑦 ) ) )
8 4 5 7 3imtr3i ( 𝑇 ∈ BndLinOp → ∃ 𝑡 ∈ BndLinOp ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑡𝑦 ) ) )
9 bdopf ( 𝑇 ∈ BndLinOp → 𝑇 : ℋ ⟶ ℋ )
10 bdopf ( 𝑡 ∈ BndLinOp → 𝑡 : ℋ ⟶ ℋ )
11 adjsym ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑡 : ℋ ⟶ ℋ ) → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡𝑦 ) ) = ( ( 𝑇𝑥 ) ·ih 𝑦 ) ) )
12 9 10 11 syl2an ( ( 𝑇 ∈ BndLinOp ∧ 𝑡 ∈ BndLinOp ) → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡𝑦 ) ) = ( ( 𝑇𝑥 ) ·ih 𝑦 ) ) )
13 eqcom ( ( ( 𝑇𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑡𝑦 ) ) ↔ ( 𝑥 ·ih ( 𝑡𝑦 ) ) = ( ( 𝑇𝑥 ) ·ih 𝑦 ) )
14 13 2ralbii ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑡𝑦 ) ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑡𝑦 ) ) = ( ( 𝑇𝑥 ) ·ih 𝑦 ) )
15 12 14 bitr4di ( ( 𝑇 ∈ BndLinOp ∧ 𝑡 ∈ BndLinOp ) → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑡𝑦 ) ) ) )
16 15 rexbidva ( 𝑇 ∈ BndLinOp → ( ∃ 𝑡 ∈ BndLinOp ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) ↔ ∃ 𝑡 ∈ BndLinOp ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑡𝑦 ) ) ) )
17 8 16 mpbird ( 𝑇 ∈ BndLinOp → ∃ 𝑡 ∈ BndLinOp ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) )
18 adjeu ( 𝑇 : ℋ ⟶ ℋ → ( 𝑇 ∈ dom adj ↔ ∃! 𝑡 ∈ ( ℋ ↑m ℋ ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) ) )
19 9 18 syl ( 𝑇 ∈ BndLinOp → ( 𝑇 ∈ dom adj ↔ ∃! 𝑡 ∈ ( ℋ ↑m ℋ ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) ) )
20 1 19 mpbid ( 𝑇 ∈ BndLinOp → ∃! 𝑡 ∈ ( ℋ ↑m ℋ ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) )
21 ax-hilex ℋ ∈ V
22 21 21 elmap ( 𝑡 ∈ ( ℋ ↑m ℋ ) ↔ 𝑡 : ℋ ⟶ ℋ )
23 10 22 sylibr ( 𝑡 ∈ BndLinOp → 𝑡 ∈ ( ℋ ↑m ℋ ) )
24 23 ssriv BndLinOp ⊆ ( ℋ ↑m ℋ )
25 id ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) → ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) )
26 25 rgenw 𝑡 ∈ BndLinOp ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) → ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) )
27 riotass2 ( ( ( BndLinOp ⊆ ( ℋ ↑m ℋ ) ∧ ∀ 𝑡 ∈ BndLinOp ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) → ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) ) ) ∧ ( ∃ 𝑡 ∈ BndLinOp ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) ∧ ∃! 𝑡 ∈ ( ℋ ↑m ℋ ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) ) ) → ( 𝑡 ∈ BndLinOp ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) ) = ( 𝑡 ∈ ( ℋ ↑m ℋ ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) ) )
28 24 26 27 mpanl12 ( ( ∃ 𝑡 ∈ BndLinOp ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) ∧ ∃! 𝑡 ∈ ( ℋ ↑m ℋ ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) ) → ( 𝑡 ∈ BndLinOp ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) ) = ( 𝑡 ∈ ( ℋ ↑m ℋ ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) ) )
29 17 20 28 syl2anc ( 𝑇 ∈ BndLinOp → ( 𝑡 ∈ BndLinOp ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) ) = ( 𝑡 ∈ ( ℋ ↑m ℋ ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) ) )
30 3 29 eqtr4d ( 𝑇 ∈ BndLinOp → ( adj𝑇 ) = ( 𝑡 ∈ BndLinOp ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) ) )
31 24 a1i ( 𝑇 ∈ BndLinOp → BndLinOp ⊆ ( ℋ ↑m ℋ ) )
32 reuss ( ( BndLinOp ⊆ ( ℋ ↑m ℋ ) ∧ ∃ 𝑡 ∈ BndLinOp ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) ∧ ∃! 𝑡 ∈ ( ℋ ↑m ℋ ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) ) → ∃! 𝑡 ∈ BndLinOp ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) )
33 31 17 20 32 syl3anc ( 𝑇 ∈ BndLinOp → ∃! 𝑡 ∈ BndLinOp ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) )
34 riotacl ( ∃! 𝑡 ∈ BndLinOp ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) → ( 𝑡 ∈ BndLinOp ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) ) ∈ BndLinOp )
35 33 34 syl ( 𝑇 ∈ BndLinOp → ( 𝑡 ∈ BndLinOp ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇𝑦 ) ) = ( ( 𝑡𝑥 ) ·ih 𝑦 ) ) ∈ BndLinOp )
36 30 35 eqeltrd ( 𝑇 ∈ BndLinOp → ( adj𝑇 ) ∈ BndLinOp )