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

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

Proof of Theorem cnlnadjlem3
StepHypRef Expression
1 cnlnadjlem.4 . 2 𝐵 = (𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤))
2 cnlnadjlem.1 . . . . . . 7 𝑇 ∈ LinOp
3 cnlnadjlem.2 . . . . . . 7 𝑇 ∈ ConOp
4 cnlnadjlem.3 . . . . . . 7 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇𝑔) ·ih 𝑦))
52, 3, 4cnlnadjlem2 28311 . . . . . 6 (𝑦 ∈ ℋ → (𝐺 ∈ LinFn ∧ 𝐺 ∈ ConFn))
6 elin 3758 . . . . . 6 (𝐺 ∈ (LinFn ∩ ConFn) ↔ (𝐺 ∈ LinFn ∧ 𝐺 ∈ ConFn))
75, 6sylibr 223 . . . . 5 (𝑦 ∈ ℋ → 𝐺 ∈ (LinFn ∩ ConFn))
8 riesz4 28307 . . . . 5 (𝐺 ∈ (LinFn ∩ ConFn) → ∃!𝑤 ∈ ℋ ∀𝑣 ∈ ℋ (𝐺𝑣) = (𝑣 ·ih 𝑤))
97, 8syl 17 . . . 4 (𝑦 ∈ ℋ → ∃!𝑤 ∈ ℋ ∀𝑣 ∈ ℋ (𝐺𝑣) = (𝑣 ·ih 𝑤))
102, 3, 4cnlnadjlem1 28310 . . . . . . 7 (𝑣 ∈ ℋ → (𝐺𝑣) = ((𝑇𝑣) ·ih 𝑦))
1110eqeq1d 2612 . . . . . 6 (𝑣 ∈ ℋ → ((𝐺𝑣) = (𝑣 ·ih 𝑤) ↔ ((𝑇𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤)))
1211ralbiia 2962 . . . . 5 (∀𝑣 ∈ ℋ (𝐺𝑣) = (𝑣 ·ih 𝑤) ↔ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤))
1312reubii 3105 . . . 4 (∃!𝑤 ∈ ℋ ∀𝑣 ∈ ℋ (𝐺𝑣) = (𝑣 ·ih 𝑤) ↔ ∃!𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤))
149, 13sylib 207 . . 3 (𝑦 ∈ ℋ → ∃!𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤))
15 riotacl 6525 . . 3 (∃!𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤) → (𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤)) ∈ ℋ)
1614, 15syl 17 . 2 (𝑦 ∈ ℋ → (𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤)) ∈ ℋ)
171, 16syl5eqel 2692 1 (𝑦 ∈ ℋ → 𝐵 ∈ ℋ)