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 28324 . . . . . 6 BndLinOp ⊆ dom adj
2 nmopadjle.1 . . . . . 6 𝑇 ∈ BndLinOp
31, 2sselii 3565 . . . . 5 𝑇 ∈ dom adj
4 adjvalval 28180 . . . . 5 ((𝑇 ∈ dom adj𝐴 ∈ ℋ) → ((adj𝑇)‘𝐴) = (𝑓 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝐴) = (𝑣 ·ih 𝑓)))
53, 4mpan 702 . . . 4 (𝐴 ∈ ℋ → ((adj𝑇)‘𝐴) = (𝑓 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝐴) = (𝑣 ·ih 𝑓)))
6 oveq2 6557 . . . . . . . 8 (𝑧 = 𝐴 → ((𝑇𝑣) ·ih 𝑧) = ((𝑇𝑣) ·ih 𝐴))
76eqeq1d 2612 . . . . . . 7 (𝑧 = 𝐴 → (((𝑇𝑣) ·ih 𝑧) = (𝑣 ·ih 𝑓) ↔ ((𝑇𝑣) ·ih 𝐴) = (𝑣 ·ih 𝑓)))
87ralbidv 2969 . . . . . 6 (𝑧 = 𝐴 → (∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑧) = (𝑣 ·ih 𝑓) ↔ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝐴) = (𝑣 ·ih 𝑓)))
98riotabidv 6513 . . . . 5 (𝑧 = 𝐴 → (𝑓 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑧) = (𝑣 ·ih 𝑓)) = (𝑓 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝐴) = (𝑣 ·ih 𝑓)))
10 eqid 2610 . . . . 5 (𝑧 ∈ ℋ ↦ (𝑓 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑧) = (𝑣 ·ih 𝑓))) = (𝑧 ∈ ℋ ↦ (𝑓 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑧) = (𝑣 ·ih 𝑓)))
11 riotaex 6515 . . . . 5 (𝑓 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝐴) = (𝑣 ·ih 𝑓)) ∈ V
129, 10, 11fvmpt 6191 . . . 4 (𝐴 ∈ ℋ → ((𝑧 ∈ ℋ ↦ (𝑓 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑧) = (𝑣 ·ih 𝑓)))‘𝐴) = (𝑓 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝐴) = (𝑣 ·ih 𝑓)))
135, 12eqtr4d 2647 . . 3 (𝐴 ∈ ℋ → ((adj𝑇)‘𝐴) = ((𝑧 ∈ ℋ ↦ (𝑓 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑧) = (𝑣 ·ih 𝑓)))‘𝐴))
1413fveq2d 6107 . 2 (𝐴 ∈ ℋ → (norm‘((adj𝑇)‘𝐴)) = (norm‘((𝑧 ∈ ℋ ↦ (𝑓 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑧) = (𝑣 ·ih 𝑓)))‘𝐴)))
15 inss1 3795 . . . 4 (LinOp ∩ ConOp) ⊆ LinOp
16 lncnbd 28281 . . . . 5 (LinOp ∩ ConOp) = BndLinOp
172, 16eleqtrri 2687 . . . 4 𝑇 ∈ (LinOp ∩ ConOp)
1815, 17sselii 3565 . . 3 𝑇 ∈ LinOp
19 inss2 3796 . . . 4 (LinOp ∩ ConOp) ⊆ ConOp
2019, 17sselii 3565 . . 3 𝑇 ∈ ConOp
21 eqid 2610 . . 3 (𝑔 ∈ ℋ ↦ ((𝑇𝑔) ·ih 𝑧)) = (𝑔 ∈ ℋ ↦ ((𝑇𝑔) ·ih 𝑧))
22 oveq2 6557 . . . . . 6 (𝑓 = 𝑤 → (𝑣 ·ih 𝑓) = (𝑣 ·ih 𝑤))
2322eqeq2d 2620 . . . . 5 (𝑓 = 𝑤 → (((𝑇𝑣) ·ih 𝑧) = (𝑣 ·ih 𝑓) ↔ ((𝑇𝑣) ·ih 𝑧) = (𝑣 ·ih 𝑤)))
2423ralbidv 2969 . . . 4 (𝑓 = 𝑤 → (∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑧) = (𝑣 ·ih 𝑓) ↔ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑧) = (𝑣 ·ih 𝑤)))
2524cbvriotav 6522 . . 3 (𝑓 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑧) = (𝑣 ·ih 𝑓)) = (𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑧) = (𝑣 ·ih 𝑤))
2618, 20, 21, 25, 10cnlnadjlem7 28316 . 2 (𝐴 ∈ ℋ → (norm‘((𝑧 ∈ ℋ ↦ (𝑓 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑧) = (𝑣 ·ih 𝑓)))‘𝐴)) ≤ ((normop𝑇) · (norm𝐴)))
2714, 26eqbrtrd 4605 1 (𝐴 ∈ ℋ → (norm‘((adj𝑇)‘𝐴)) ≤ ((normop𝑇) · (norm𝐴)))