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

 Description: Lemma for cnlnadji 29063. By riesz4 29051, 𝐵 is the unique vector such that (𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤) for all 𝑣. (Contributed by NM, 17-Feb-2006.) (New usage is discouraged.)
Hypotheses
Ref Expression
cnlnadjlem.3 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇𝑔) ·ih 𝑦))
cnlnadjlem.4 𝐵 = (𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤))
Assertion
Ref Expression
cnlnadjlem3 (𝑦 ∈ ℋ → 𝐵 ∈ ℋ)
Distinct variable groups:   𝑣,𝑔,𝑤,𝑦,𝑇   𝑣,𝐺,𝑤
Allowed substitution hints:   𝐵(𝑦,𝑤,𝑣,𝑔)   𝐺(𝑦,𝑔)

StepHypRef Expression
1 cnlnadjlem.4 . 2 𝐵 = (𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤))
2 cnlnadjlem.1 . . . . . . 7 𝑇 ∈ LinOp
3 cnlnadjlem.2 . . . . . . 7 𝑇 ∈ ContOp
4 cnlnadjlem.3 . . . . . . 7 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇𝑔) ·ih 𝑦))
52, 3, 4cnlnadjlem2 29055 . . . . . 6 (𝑦 ∈ ℋ → (𝐺 ∈ LinFn ∧ 𝐺 ∈ ContFn))
6 elin 3829 . . . . . 6 (𝐺 ∈ (LinFn ∩ ContFn) ↔ (𝐺 ∈ LinFn ∧ 𝐺 ∈ ContFn))
75, 6sylibr 224 . . . . 5 (𝑦 ∈ ℋ → 𝐺 ∈ (LinFn ∩ ContFn))
8 riesz4 29051 . . . . 5 (𝐺 ∈ (LinFn ∩ ContFn) → ∃!𝑤 ∈ ℋ ∀𝑣 ∈ ℋ (𝐺𝑣) = (𝑣 ·ih 𝑤))
97, 8syl 17 . . . 4 (𝑦 ∈ ℋ → ∃!𝑤 ∈ ℋ ∀𝑣 ∈ ℋ (𝐺𝑣) = (𝑣 ·ih 𝑤))
102, 3, 4cnlnadjlem1 29054 . . . . . . 7 (𝑣 ∈ ℋ → (𝐺𝑣) = ((𝑇𝑣) ·ih 𝑦))
1110eqeq1d 2653 . . . . . 6 (𝑣 ∈ ℋ → ((𝐺𝑣) = (𝑣 ·ih 𝑤) ↔ ((𝑇𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤)))
1211ralbiia 3008 . . . . 5 (∀𝑣 ∈ ℋ (𝐺𝑣) = (𝑣 ·ih 𝑤) ↔ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤))
1312reubii 3158 . . . 4 (∃!𝑤 ∈ ℋ ∀𝑣 ∈ ℋ (𝐺𝑣) = (𝑣 ·ih 𝑤) ↔ ∃!𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤))
149, 13sylib 208 . . 3 (𝑦 ∈ ℋ → ∃!𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤))
15 riotacl 6665 . . 3 (∃!𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤) → (𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤)) ∈ ℋ)
1614, 15syl 17 . 2 (𝑦 ∈ ℋ → (𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤)) ∈ ℋ)
171, 16syl5eqel 2734 1 (𝑦 ∈ ℋ → 𝐵 ∈ ℋ)