Hilbert Space Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HSE Home  >  Th. List  >  nmopadjlei Structured version   Visualization version   GIF version

 Description: Property of the norm of an adjoint. Part of proof of Theorem 3.10 of [Beran] p. 104. (Contributed by NM, 22-Feb-2006.) (New usage is discouraged.)
Hypothesis
Ref Expression
Assertion
Ref Expression

Dummy variables 𝑓 𝑔 𝑣 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 bdopssadj 29068 . . . . . 6 BndLinOp ⊆ dom adj
2 nmopadjle.1 . . . . . 6 𝑇 ∈ BndLinOp
31, 2sselii 3633 . . . . 5 𝑇 ∈ dom adj
4 adjvalval 28924 . . . . 5 ((𝑇 ∈ dom adj𝐴 ∈ ℋ) → ((adj𝑇)‘𝐴) = (𝑓 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝐴) = (𝑣 ·ih 𝑓)))
53, 4mpan 706 . . . 4 (𝐴 ∈ ℋ → ((adj𝑇)‘𝐴) = (𝑓 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝐴) = (𝑣 ·ih 𝑓)))
6 oveq2 6698 . . . . . . . 8 (𝑧 = 𝐴 → ((𝑇𝑣) ·ih 𝑧) = ((𝑇𝑣) ·ih 𝐴))
76eqeq1d 2653 . . . . . . 7 (𝑧 = 𝐴 → (((𝑇𝑣) ·ih 𝑧) = (𝑣 ·ih 𝑓) ↔ ((𝑇𝑣) ·ih 𝐴) = (𝑣 ·ih 𝑓)))
87ralbidv 3015 . . . . . 6 (𝑧 = 𝐴 → (∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑧) = (𝑣 ·ih 𝑓) ↔ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝐴) = (𝑣 ·ih 𝑓)))
98riotabidv 6653 . . . . 5 (𝑧 = 𝐴 → (𝑓 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑧) = (𝑣 ·ih 𝑓)) = (𝑓 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝐴) = (𝑣 ·ih 𝑓)))
10 eqid 2651 . . . . 5 (𝑧 ∈ ℋ ↦ (𝑓 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑧) = (𝑣 ·ih 𝑓))) = (𝑧 ∈ ℋ ↦ (𝑓 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑧) = (𝑣 ·ih 𝑓)))
11 riotaex 6655 . . . . 5 (𝑓 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝐴) = (𝑣 ·ih 𝑓)) ∈ V
129, 10, 11fvmpt 6321 . . . 4 (𝐴 ∈ ℋ → ((𝑧 ∈ ℋ ↦ (𝑓 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑧) = (𝑣 ·ih 𝑓)))‘𝐴) = (𝑓 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝐴) = (𝑣 ·ih 𝑓)))
135, 12eqtr4d 2688 . . 3 (𝐴 ∈ ℋ → ((adj𝑇)‘𝐴) = ((𝑧 ∈ ℋ ↦ (𝑓 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑧) = (𝑣 ·ih 𝑓)))‘𝐴))
1413fveq2d 6233 . 2 (𝐴 ∈ ℋ → (norm‘((adj𝑇)‘𝐴)) = (norm‘((𝑧 ∈ ℋ ↦ (𝑓 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑧) = (𝑣 ·ih 𝑓)))‘𝐴)))
15 inss1 3866 . . . 4 (LinOp ∩ ContOp) ⊆ LinOp
16 lncnbd 29025 . . . . 5 (LinOp ∩ ContOp) = BndLinOp
172, 16eleqtrri 2729 . . . 4 𝑇 ∈ (LinOp ∩ ContOp)
1815, 17sselii 3633 . . 3 𝑇 ∈ LinOp
19 inss2 3867 . . . 4 (LinOp ∩ ContOp) ⊆ ContOp
2019, 17sselii 3633 . . 3 𝑇 ∈ ContOp
21 eqid 2651 . . 3 (𝑔 ∈ ℋ ↦ ((𝑇𝑔) ·ih 𝑧)) = (𝑔 ∈ ℋ ↦ ((𝑇𝑔) ·ih 𝑧))
22 oveq2 6698 . . . . . 6 (𝑓 = 𝑤 → (𝑣 ·ih 𝑓) = (𝑣 ·ih 𝑤))
2322eqeq2d 2661 . . . . 5 (𝑓 = 𝑤 → (((𝑇𝑣) ·ih 𝑧) = (𝑣 ·ih 𝑓) ↔ ((𝑇𝑣) ·ih 𝑧) = (𝑣 ·ih 𝑤)))
2423ralbidv 3015 . . . 4 (𝑓 = 𝑤 → (∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑧) = (𝑣 ·ih 𝑓) ↔ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑧) = (𝑣 ·ih 𝑤)))
2524cbvriotav 6662 . . 3 (𝑓 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑧) = (𝑣 ·ih 𝑓)) = (𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑧) = (𝑣 ·ih 𝑤))
2618, 20, 21, 25, 10cnlnadjlem7 29060 . 2 (𝐴 ∈ ℋ → (norm‘((𝑧 ∈ ℋ ↦ (𝑓 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑧) = (𝑣 ·ih 𝑓)))‘𝐴)) ≤ ((normop𝑇) · (norm𝐴)))
2714, 26eqbrtrd 4707 1 (𝐴 ∈ ℋ → (norm‘((adj𝑇)‘𝐴)) ≤ ((normop𝑇) · (norm𝐴)))