This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )