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

 Description: Lemma for cnlnadji 28319. 𝐹 is an adjoint of 𝑇 (later, we will show it is unique). (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.)
Hypotheses
Ref Expression
cnlnadjlem.3 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇𝑔) ·ih 𝑦))
cnlnadjlem.4 𝐵 = (𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤))
cnlnadjlem.5 𝐹 = (𝑦 ∈ ℋ ↦ 𝐵)
Assertion
Ref Expression
cnlnadjlem5 ((𝐴 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝑇𝐶) ·ih 𝐴) = (𝐶 ·ih (𝐹𝐴)))
Distinct variable groups:   𝑣,𝑔,𝑤,𝑦,𝐴   𝑤,𝐹   𝑇,𝑔,𝑣,𝑤,𝑦   𝑣,𝐺,𝑤
Allowed substitution hints:   𝐵(𝑦,𝑤,𝑣,𝑔)   𝐶(𝑦,𝑤,𝑣,𝑔)   𝐹(𝑦,𝑣,𝑔)   𝐺(𝑦,𝑔)

Dummy variable 𝑓 is distinct from all other variables.
StepHypRef Expression
1 nfcv 2751 . . 3 𝑦𝐴
2 nfcv 2751 . . . 4 𝑦
3 nfcv 2751 . . . . . 6 𝑦𝑓
4 nfcv 2751 . . . . . 6 𝑦 ·ih
5 cnlnadjlem.5 . . . . . . . 8 𝐹 = (𝑦 ∈ ℋ ↦ 𝐵)
6 nfmpt1 4675 . . . . . . . 8 𝑦(𝑦 ∈ ℋ ↦ 𝐵)
75, 6nfcxfr 2749 . . . . . . 7 𝑦𝐹
87, 1nffv 6110 . . . . . 6 𝑦(𝐹𝐴)
93, 4, 8nfov 6575 . . . . 5 𝑦(𝑓 ·ih (𝐹𝐴))
109nfeq2 2766 . . . 4 𝑦((𝑇𝑓) ·ih 𝐴) = (𝑓 ·ih (𝐹𝐴))
112, 10nfral 2929 . . 3 𝑦𝑓 ∈ ℋ ((𝑇𝑓) ·ih 𝐴) = (𝑓 ·ih (𝐹𝐴))
12 oveq2 6557 . . . . 5 (𝑦 = 𝐴 → ((𝑇𝑓) ·ih 𝑦) = ((𝑇𝑓) ·ih 𝐴))
13 fveq2 6103 . . . . . 6 (𝑦 = 𝐴 → (𝐹𝑦) = (𝐹𝐴))
1413oveq2d 6565 . . . . 5 (𝑦 = 𝐴 → (𝑓 ·ih (𝐹𝑦)) = (𝑓 ·ih (𝐹𝐴)))
1512, 14eqeq12d 2625 . . . 4 (𝑦 = 𝐴 → (((𝑇𝑓) ·ih 𝑦) = (𝑓 ·ih (𝐹𝑦)) ↔ ((𝑇𝑓) ·ih 𝐴) = (𝑓 ·ih (𝐹𝐴))))
1615ralbidv 2969 . . 3 (𝑦 = 𝐴 → (∀𝑓 ∈ ℋ ((𝑇𝑓) ·ih 𝑦) = (𝑓 ·ih (𝐹𝑦)) ↔ ∀𝑓 ∈ ℋ ((𝑇𝑓) ·ih 𝐴) = (𝑓 ·ih (𝐹𝐴))))
17 cnlnadjlem.4 . . . . . . 7 𝐵 = (𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤))
18 riotaex 6515 . . . . . . 7 (𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤)) ∈ V
1917, 18eqeltri 2684 . . . . . 6 𝐵 ∈ V
205fvmpt2 6200 . . . . . 6 ((𝑦 ∈ ℋ ∧ 𝐵 ∈ V) → (𝐹𝑦) = 𝐵)
2119, 20mpan2 703 . . . . 5 (𝑦 ∈ ℋ → (𝐹𝑦) = 𝐵)
22 fveq2 6103 . . . . . . . . . . . . 13 (𝑣 = 𝑓 → (𝑇𝑣) = (𝑇𝑓))
2322oveq1d 6564 . . . . . . . . . . . 12 (𝑣 = 𝑓 → ((𝑇𝑣) ·ih 𝑦) = ((𝑇𝑓) ·ih 𝑦))
24 oveq1 6556 . . . . . . . . . . . 12 (𝑣 = 𝑓 → (𝑣 ·ih 𝑤) = (𝑓 ·ih 𝑤))
2523, 24eqeq12d 2625 . . . . . . . . . . 11 (𝑣 = 𝑓 → (((𝑇𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤) ↔ ((𝑇𝑓) ·ih 𝑦) = (𝑓 ·ih 𝑤)))
2625cbvralv 3147 . . . . . . . . . 10 (∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤) ↔ ∀𝑓 ∈ ℋ ((𝑇𝑓) ·ih 𝑦) = (𝑓 ·ih 𝑤))
2726a1i 11 . . . . . . . . 9 (𝑤 ∈ ℋ → (∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤) ↔ ∀𝑓 ∈ ℋ ((𝑇𝑓) ·ih 𝑦) = (𝑓 ·ih 𝑤)))
28 cnlnadjlem.1 . . . . . . . . . . . 12 𝑇 ∈ LinOp
29 cnlnadjlem.2 . . . . . . . . . . . 12 𝑇 ∈ ConOp
30 cnlnadjlem.3 . . . . . . . . . . . 12 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇𝑔) ·ih 𝑦))
3128, 29, 30cnlnadjlem1 28310 . . . . . . . . . . 11 (𝑓 ∈ ℋ → (𝐺𝑓) = ((𝑇𝑓) ·ih 𝑦))
3231eqeq1d 2612 . . . . . . . . . 10 (𝑓 ∈ ℋ → ((𝐺𝑓) = (𝑓 ·ih 𝑤) ↔ ((𝑇𝑓) ·ih 𝑦) = (𝑓 ·ih 𝑤)))
3332ralbiia 2962 . . . . . . . . 9 (∀𝑓 ∈ ℋ (𝐺𝑓) = (𝑓 ·ih 𝑤) ↔ ∀𝑓 ∈ ℋ ((𝑇𝑓) ·ih 𝑦) = (𝑓 ·ih 𝑤))
3427, 33syl6bbr 277 . . . . . . . 8 (𝑤 ∈ ℋ → (∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤) ↔ ∀𝑓 ∈ ℋ (𝐺𝑓) = (𝑓 ·ih 𝑤)))
3534riotabiia 6528 . . . . . . 7 (𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤)) = (𝑤 ∈ ℋ ∀𝑓 ∈ ℋ (𝐺𝑓) = (𝑓 ·ih 𝑤))
3617, 35eqtri 2632 . . . . . 6 𝐵 = (𝑤 ∈ ℋ ∀𝑓 ∈ ℋ (𝐺𝑓) = (𝑓 ·ih 𝑤))
3728, 29, 30cnlnadjlem2 28311 . . . . . . . 8 (𝑦 ∈ ℋ → (𝐺 ∈ LinFn ∧ 𝐺 ∈ ConFn))
38 elin 3758 . . . . . . . 8 (𝐺 ∈ (LinFn ∩ ConFn) ↔ (𝐺 ∈ LinFn ∧ 𝐺 ∈ ConFn))
3937, 38sylibr 223 . . . . . . 7 (𝑦 ∈ ℋ → 𝐺 ∈ (LinFn ∩ ConFn))
40 riesz4 28307 . . . . . . 7 (𝐺 ∈ (LinFn ∩ ConFn) → ∃!𝑤 ∈ ℋ ∀𝑓 ∈ ℋ (𝐺𝑓) = (𝑓 ·ih 𝑤))
41 riotacl2 6524 . . . . . . 7 (∃!𝑤 ∈ ℋ ∀𝑓 ∈ ℋ (𝐺𝑓) = (𝑓 ·ih 𝑤) → (𝑤 ∈ ℋ ∀𝑓 ∈ ℋ (𝐺𝑓) = (𝑓 ·ih 𝑤)) ∈ {𝑤 ∈ ℋ ∣ ∀𝑓 ∈ ℋ (𝐺𝑓) = (𝑓 ·ih 𝑤)})
4239, 40, 413syl 18 . . . . . 6 (𝑦 ∈ ℋ → (𝑤 ∈ ℋ ∀𝑓 ∈ ℋ (𝐺𝑓) = (𝑓 ·ih 𝑤)) ∈ {𝑤 ∈ ℋ ∣ ∀𝑓 ∈ ℋ (𝐺𝑓) = (𝑓 ·ih 𝑤)})
4336, 42syl5eqel 2692 . . . . 5 (𝑦 ∈ ℋ → 𝐵 ∈ {𝑤 ∈ ℋ ∣ ∀𝑓 ∈ ℋ (𝐺𝑓) = (𝑓 ·ih 𝑤)})
4421, 43eqeltrd 2688 . . . 4 (𝑦 ∈ ℋ → (𝐹𝑦) ∈ {𝑤 ∈ ℋ ∣ ∀𝑓 ∈ ℋ (𝐺𝑓) = (𝑓 ·ih 𝑤)})
45 oveq2 6557 . . . . . . . . 9 (𝑤 = (𝐹𝑦) → (𝑓 ·ih 𝑤) = (𝑓 ·ih (𝐹𝑦)))
4645eqeq2d 2620 . . . . . . . 8 (𝑤 = (𝐹𝑦) → (((𝑇𝑓) ·ih 𝑦) = (𝑓 ·ih 𝑤) ↔ ((𝑇𝑓) ·ih 𝑦) = (𝑓 ·ih (𝐹𝑦))))
4746ralbidv 2969 . . . . . . 7 (𝑤 = (𝐹𝑦) → (∀𝑓 ∈ ℋ ((𝑇𝑓) ·ih 𝑦) = (𝑓 ·ih 𝑤) ↔ ∀𝑓 ∈ ℋ ((𝑇𝑓) ·ih 𝑦) = (𝑓 ·ih (𝐹𝑦))))
4833, 47syl5bb 271 . . . . . 6 (𝑤 = (𝐹𝑦) → (∀𝑓 ∈ ℋ (𝐺𝑓) = (𝑓 ·ih 𝑤) ↔ ∀𝑓 ∈ ℋ ((𝑇𝑓) ·ih 𝑦) = (𝑓 ·ih (𝐹𝑦))))
4948elrab 3331 . . . . 5 ((𝐹𝑦) ∈ {𝑤 ∈ ℋ ∣ ∀𝑓 ∈ ℋ (𝐺𝑓) = (𝑓 ·ih 𝑤)} ↔ ((𝐹𝑦) ∈ ℋ ∧ ∀𝑓 ∈ ℋ ((𝑇𝑓) ·ih 𝑦) = (𝑓 ·ih (𝐹𝑦))))
5049simprbi 479 . . . 4 ((𝐹𝑦) ∈ {𝑤 ∈ ℋ ∣ ∀𝑓 ∈ ℋ (𝐺𝑓) = (𝑓 ·ih 𝑤)} → ∀𝑓 ∈ ℋ ((𝑇𝑓) ·ih 𝑦) = (𝑓 ·ih (𝐹𝑦)))
5144, 50syl 17 . . 3 (𝑦 ∈ ℋ → ∀𝑓 ∈ ℋ ((𝑇𝑓) ·ih 𝑦) = (𝑓 ·ih (𝐹𝑦)))
521, 11, 16, 51vtoclgaf 3244 . 2 (𝐴 ∈ ℋ → ∀𝑓 ∈ ℋ ((𝑇𝑓) ·ih 𝐴) = (𝑓 ·ih (𝐹𝐴)))
53 fveq2 6103 . . . . 5 (𝑓 = 𝐶 → (𝑇𝑓) = (𝑇𝐶))
5453oveq1d 6564 . . . 4 (𝑓 = 𝐶 → ((𝑇𝑓) ·ih 𝐴) = ((𝑇𝐶) ·ih 𝐴))
55 oveq1 6556 . . . 4 (𝑓 = 𝐶 → (𝑓 ·ih (𝐹𝐴)) = (𝐶 ·ih (𝐹𝐴)))
5654, 55eqeq12d 2625 . . 3 (𝑓 = 𝐶 → (((𝑇𝑓) ·ih 𝐴) = (𝑓 ·ih (𝐹𝐴)) ↔ ((𝑇𝐶) ·ih 𝐴) = (𝐶 ·ih (𝐹𝐴))))
5756rspccva 3281 . 2 ((∀𝑓 ∈ ℋ ((𝑇𝑓) ·ih 𝐴) = (𝑓 ·ih (𝐹𝐴)) ∧ 𝐶 ∈ ℋ) → ((𝑇𝐶) ·ih 𝐴) = (𝐶 ·ih (𝐹𝐴)))
5852, 57sylan 487 1 ((𝐴 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝑇𝐶) ·ih 𝐴) = (𝐶 ·ih (𝐹𝐴)))