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