![]() |
Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > HSE Home > Th. List > cnlnadjlem5 | Structured version Visualization version GIF version |
Description: Lemma for cnlnadji 32006. 𝐹 is an adjoint of 𝑇 (later, we will show it is unique). (Contributed by NM, 18-Feb-2006.) (New usage is discouraged.) |
Ref | Expression |
---|---|
cnlnadjlem.1 | ⊢ 𝑇 ∈ LinOp |
cnlnadjlem.2 | ⊢ 𝑇 ∈ ContOp |
cnlnadjlem.3 | ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦)) |
cnlnadjlem.4 | ⊢ 𝐵 = (℩𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤)) |
cnlnadjlem.5 | ⊢ 𝐹 = (𝑦 ∈ ℋ ↦ 𝐵) |
Ref | Expression |
---|---|
cnlnadjlem5 | ⊢ ((𝐴 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝑇‘𝐶) ·ih 𝐴) = (𝐶 ·ih (𝐹‘𝐴))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2892 | . . 3 ⊢ Ⅎ𝑦𝐴 | |
2 | nfcv 2892 | . . . 4 ⊢ Ⅎ𝑦 ℋ | |
3 | nfcv 2892 | . . . . . 6 ⊢ Ⅎ𝑦𝑓 | |
4 | nfcv 2892 | . . . . . 6 ⊢ Ⅎ𝑦 ·ih | |
5 | cnlnadjlem.5 | . . . . . . . 8 ⊢ 𝐹 = (𝑦 ∈ ℋ ↦ 𝐵) | |
6 | nfmpt1 5253 | . . . . . . . 8 ⊢ Ⅎ𝑦(𝑦 ∈ ℋ ↦ 𝐵) | |
7 | 5, 6 | nfcxfr 2890 | . . . . . . 7 ⊢ Ⅎ𝑦𝐹 |
8 | 7, 1 | nffv 6903 | . . . . . 6 ⊢ Ⅎ𝑦(𝐹‘𝐴) |
9 | 3, 4, 8 | nfov 7446 | . . . . 5 ⊢ Ⅎ𝑦(𝑓 ·ih (𝐹‘𝐴)) |
10 | 9 | nfeq2 2910 | . . . 4 ⊢ Ⅎ𝑦((𝑇‘𝑓) ·ih 𝐴) = (𝑓 ·ih (𝐹‘𝐴)) |
11 | 2, 10 | nfralw 3299 | . . 3 ⊢ Ⅎ𝑦∀𝑓 ∈ ℋ ((𝑇‘𝑓) ·ih 𝐴) = (𝑓 ·ih (𝐹‘𝐴)) |
12 | oveq2 7424 | . . . . 5 ⊢ (𝑦 = 𝐴 → ((𝑇‘𝑓) ·ih 𝑦) = ((𝑇‘𝑓) ·ih 𝐴)) | |
13 | fveq2 6893 | . . . . . 6 ⊢ (𝑦 = 𝐴 → (𝐹‘𝑦) = (𝐹‘𝐴)) | |
14 | 13 | oveq2d 7432 | . . . . 5 ⊢ (𝑦 = 𝐴 → (𝑓 ·ih (𝐹‘𝑦)) = (𝑓 ·ih (𝐹‘𝐴))) |
15 | 12, 14 | eqeq12d 2742 | . . . 4 ⊢ (𝑦 = 𝐴 → (((𝑇‘𝑓) ·ih 𝑦) = (𝑓 ·ih (𝐹‘𝑦)) ↔ ((𝑇‘𝑓) ·ih 𝐴) = (𝑓 ·ih (𝐹‘𝐴)))) |
16 | 15 | ralbidv 3168 | . . 3 ⊢ (𝑦 = 𝐴 → (∀𝑓 ∈ ℋ ((𝑇‘𝑓) ·ih 𝑦) = (𝑓 ·ih (𝐹‘𝑦)) ↔ ∀𝑓 ∈ ℋ ((𝑇‘𝑓) ·ih 𝐴) = (𝑓 ·ih (𝐹‘𝐴)))) |
17 | cnlnadjlem.4 | . . . . . . 7 ⊢ 𝐵 = (℩𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤)) | |
18 | riotaex 7376 | . . . . . . 7 ⊢ (℩𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤)) ∈ V | |
19 | 17, 18 | eqeltri 2822 | . . . . . 6 ⊢ 𝐵 ∈ V |
20 | 5 | fvmpt2 7012 | . . . . . 6 ⊢ ((𝑦 ∈ ℋ ∧ 𝐵 ∈ V) → (𝐹‘𝑦) = 𝐵) |
21 | 19, 20 | mpan2 689 | . . . . 5 ⊢ (𝑦 ∈ ℋ → (𝐹‘𝑦) = 𝐵) |
22 | fveq2 6893 | . . . . . . . . . . . . 13 ⊢ (𝑣 = 𝑓 → (𝑇‘𝑣) = (𝑇‘𝑓)) | |
23 | 22 | oveq1d 7431 | . . . . . . . . . . . 12 ⊢ (𝑣 = 𝑓 → ((𝑇‘𝑣) ·ih 𝑦) = ((𝑇‘𝑓) ·ih 𝑦)) |
24 | oveq1 7423 | . . . . . . . . . . . 12 ⊢ (𝑣 = 𝑓 → (𝑣 ·ih 𝑤) = (𝑓 ·ih 𝑤)) | |
25 | 23, 24 | eqeq12d 2742 | . . . . . . . . . . 11 ⊢ (𝑣 = 𝑓 → (((𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤) ↔ ((𝑇‘𝑓) ·ih 𝑦) = (𝑓 ·ih 𝑤))) |
26 | 25 | cbvralvw 3225 | . . . . . . . . . 10 ⊢ (∀𝑣 ∈ ℋ ((𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤) ↔ ∀𝑓 ∈ ℋ ((𝑇‘𝑓) ·ih 𝑦) = (𝑓 ·ih 𝑤)) |
27 | 26 | a1i 11 | . . . . . . . . 9 ⊢ (𝑤 ∈ ℋ → (∀𝑣 ∈ ℋ ((𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤) ↔ ∀𝑓 ∈ ℋ ((𝑇‘𝑓) ·ih 𝑦) = (𝑓 ·ih 𝑤))) |
28 | cnlnadjlem.1 | . . . . . . . . . . . 12 ⊢ 𝑇 ∈ LinOp | |
29 | cnlnadjlem.2 | . . . . . . . . . . . 12 ⊢ 𝑇 ∈ ContOp | |
30 | cnlnadjlem.3 | . . . . . . . . . . . 12 ⊢ 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇‘𝑔) ·ih 𝑦)) | |
31 | 28, 29, 30 | cnlnadjlem1 31997 | . . . . . . . . . . 11 ⊢ (𝑓 ∈ ℋ → (𝐺‘𝑓) = ((𝑇‘𝑓) ·ih 𝑦)) |
32 | 31 | eqeq1d 2728 | . . . . . . . . . 10 ⊢ (𝑓 ∈ ℋ → ((𝐺‘𝑓) = (𝑓 ·ih 𝑤) ↔ ((𝑇‘𝑓) ·ih 𝑦) = (𝑓 ·ih 𝑤))) |
33 | 32 | ralbiia 3081 | . . . . . . . . 9 ⊢ (∀𝑓 ∈ ℋ (𝐺‘𝑓) = (𝑓 ·ih 𝑤) ↔ ∀𝑓 ∈ ℋ ((𝑇‘𝑓) ·ih 𝑦) = (𝑓 ·ih 𝑤)) |
34 | 27, 33 | bitr4di 288 | . . . . . . . 8 ⊢ (𝑤 ∈ ℋ → (∀𝑣 ∈ ℋ ((𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤) ↔ ∀𝑓 ∈ ℋ (𝐺‘𝑓) = (𝑓 ·ih 𝑤))) |
35 | 34 | riotabiia 7393 | . . . . . . 7 ⊢ (℩𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇‘𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤)) = (℩𝑤 ∈ ℋ ∀𝑓 ∈ ℋ (𝐺‘𝑓) = (𝑓 ·ih 𝑤)) |
36 | 17, 35 | eqtri 2754 | . . . . . 6 ⊢ 𝐵 = (℩𝑤 ∈ ℋ ∀𝑓 ∈ ℋ (𝐺‘𝑓) = (𝑓 ·ih 𝑤)) |
37 | 28, 29, 30 | cnlnadjlem2 31998 | . . . . . . . 8 ⊢ (𝑦 ∈ ℋ → (𝐺 ∈ LinFn ∧ 𝐺 ∈ ContFn)) |
38 | elin 3962 | . . . . . . . 8 ⊢ (𝐺 ∈ (LinFn ∩ ContFn) ↔ (𝐺 ∈ LinFn ∧ 𝐺 ∈ ContFn)) | |
39 | 37, 38 | sylibr 233 | . . . . . . 7 ⊢ (𝑦 ∈ ℋ → 𝐺 ∈ (LinFn ∩ ContFn)) |
40 | riesz4 31994 | . . . . . . 7 ⊢ (𝐺 ∈ (LinFn ∩ ContFn) → ∃!𝑤 ∈ ℋ ∀𝑓 ∈ ℋ (𝐺‘𝑓) = (𝑓 ·ih 𝑤)) | |
41 | riotacl2 7389 | . . . . . . 7 ⊢ (∃!𝑤 ∈ ℋ ∀𝑓 ∈ ℋ (𝐺‘𝑓) = (𝑓 ·ih 𝑤) → (℩𝑤 ∈ ℋ ∀𝑓 ∈ ℋ (𝐺‘𝑓) = (𝑓 ·ih 𝑤)) ∈ {𝑤 ∈ ℋ ∣ ∀𝑓 ∈ ℋ (𝐺‘𝑓) = (𝑓 ·ih 𝑤)}) | |
42 | 39, 40, 41 | 3syl 18 | . . . . . 6 ⊢ (𝑦 ∈ ℋ → (℩𝑤 ∈ ℋ ∀𝑓 ∈ ℋ (𝐺‘𝑓) = (𝑓 ·ih 𝑤)) ∈ {𝑤 ∈ ℋ ∣ ∀𝑓 ∈ ℋ (𝐺‘𝑓) = (𝑓 ·ih 𝑤)}) |
43 | 36, 42 | eqeltrid 2830 | . . . . 5 ⊢ (𝑦 ∈ ℋ → 𝐵 ∈ {𝑤 ∈ ℋ ∣ ∀𝑓 ∈ ℋ (𝐺‘𝑓) = (𝑓 ·ih 𝑤)}) |
44 | 21, 43 | eqeltrd 2826 | . . . 4 ⊢ (𝑦 ∈ ℋ → (𝐹‘𝑦) ∈ {𝑤 ∈ ℋ ∣ ∀𝑓 ∈ ℋ (𝐺‘𝑓) = (𝑓 ·ih 𝑤)}) |
45 | oveq2 7424 | . . . . . . . . 9 ⊢ (𝑤 = (𝐹‘𝑦) → (𝑓 ·ih 𝑤) = (𝑓 ·ih (𝐹‘𝑦))) | |
46 | 45 | eqeq2d 2737 | . . . . . . . 8 ⊢ (𝑤 = (𝐹‘𝑦) → (((𝑇‘𝑓) ·ih 𝑦) = (𝑓 ·ih 𝑤) ↔ ((𝑇‘𝑓) ·ih 𝑦) = (𝑓 ·ih (𝐹‘𝑦)))) |
47 | 46 | ralbidv 3168 | . . . . . . 7 ⊢ (𝑤 = (𝐹‘𝑦) → (∀𝑓 ∈ ℋ ((𝑇‘𝑓) ·ih 𝑦) = (𝑓 ·ih 𝑤) ↔ ∀𝑓 ∈ ℋ ((𝑇‘𝑓) ·ih 𝑦) = (𝑓 ·ih (𝐹‘𝑦)))) |
48 | 33, 47 | bitrid 282 | . . . . . 6 ⊢ (𝑤 = (𝐹‘𝑦) → (∀𝑓 ∈ ℋ (𝐺‘𝑓) = (𝑓 ·ih 𝑤) ↔ ∀𝑓 ∈ ℋ ((𝑇‘𝑓) ·ih 𝑦) = (𝑓 ·ih (𝐹‘𝑦)))) |
49 | 48 | elrab 3680 | . . . . 5 ⊢ ((𝐹‘𝑦) ∈ {𝑤 ∈ ℋ ∣ ∀𝑓 ∈ ℋ (𝐺‘𝑓) = (𝑓 ·ih 𝑤)} ↔ ((𝐹‘𝑦) ∈ ℋ ∧ ∀𝑓 ∈ ℋ ((𝑇‘𝑓) ·ih 𝑦) = (𝑓 ·ih (𝐹‘𝑦)))) |
50 | 49 | simprbi 495 | . . . 4 ⊢ ((𝐹‘𝑦) ∈ {𝑤 ∈ ℋ ∣ ∀𝑓 ∈ ℋ (𝐺‘𝑓) = (𝑓 ·ih 𝑤)} → ∀𝑓 ∈ ℋ ((𝑇‘𝑓) ·ih 𝑦) = (𝑓 ·ih (𝐹‘𝑦))) |
51 | 44, 50 | syl 17 | . . 3 ⊢ (𝑦 ∈ ℋ → ∀𝑓 ∈ ℋ ((𝑇‘𝑓) ·ih 𝑦) = (𝑓 ·ih (𝐹‘𝑦))) |
52 | 1, 11, 16, 51 | vtoclgaf 3556 | . 2 ⊢ (𝐴 ∈ ℋ → ∀𝑓 ∈ ℋ ((𝑇‘𝑓) ·ih 𝐴) = (𝑓 ·ih (𝐹‘𝐴))) |
53 | fveq2 6893 | . . . . 5 ⊢ (𝑓 = 𝐶 → (𝑇‘𝑓) = (𝑇‘𝐶)) | |
54 | 53 | oveq1d 7431 | . . . 4 ⊢ (𝑓 = 𝐶 → ((𝑇‘𝑓) ·ih 𝐴) = ((𝑇‘𝐶) ·ih 𝐴)) |
55 | oveq1 7423 | . . . 4 ⊢ (𝑓 = 𝐶 → (𝑓 ·ih (𝐹‘𝐴)) = (𝐶 ·ih (𝐹‘𝐴))) | |
56 | 54, 55 | eqeq12d 2742 | . . 3 ⊢ (𝑓 = 𝐶 → (((𝑇‘𝑓) ·ih 𝐴) = (𝑓 ·ih (𝐹‘𝐴)) ↔ ((𝑇‘𝐶) ·ih 𝐴) = (𝐶 ·ih (𝐹‘𝐴)))) |
57 | 56 | rspccva 3606 | . 2 ⊢ ((∀𝑓 ∈ ℋ ((𝑇‘𝑓) ·ih 𝐴) = (𝑓 ·ih (𝐹‘𝐴)) ∧ 𝐶 ∈ ℋ) → ((𝑇‘𝐶) ·ih 𝐴) = (𝐶 ·ih (𝐹‘𝐴))) |
58 | 52, 57 | sylan 578 | 1 ⊢ ((𝐴 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝑇‘𝐶) ·ih 𝐴) = (𝐶 ·ih (𝐹‘𝐴))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 = wceq 1534 ∈ wcel 2099 ∀wral 3051 ∃!wreu 3362 {crab 3419 Vcvv 3462 ∩ cin 3945 ↦ cmpt 5228 ‘cfv 6546 ℩crio 7371 (class class class)co 7416 ℋchba 30849 ·ih csp 30852 ContOpccop 30876 LinOpclo 30877 ContFnccnfn 30883 LinFnclf 30884 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2697 ax-rep 5282 ax-sep 5296 ax-nul 5303 ax-pow 5361 ax-pr 5425 ax-un 7738 ax-inf2 9677 ax-cc 10469 ax-cnex 11205 ax-resscn 11206 ax-1cn 11207 ax-icn 11208 ax-addcl 11209 ax-addrcl 11210 ax-mulcl 11211 ax-mulrcl 11212 ax-mulcom 11213 ax-addass 11214 ax-mulass 11215 ax-distr 11216 ax-i2m1 11217 ax-1ne0 11218 ax-1rid 11219 ax-rnegex 11220 ax-rrecex 11221 ax-cnre 11222 ax-pre-lttri 11223 ax-pre-lttrn 11224 ax-pre-ltadd 11225 ax-pre-mulgt0 11226 ax-pre-sup 11227 ax-addf 11228 ax-mulf 11229 ax-hilex 30929 ax-hfvadd 30930 ax-hvcom 30931 ax-hvass 30932 ax-hv0cl 30933 ax-hvaddid 30934 ax-hfvmul 30935 ax-hvmulid 30936 ax-hvmulass 30937 ax-hvdistr1 30938 ax-hvdistr2 30939 ax-hvmul0 30940 ax-hfi 31009 ax-his1 31012 ax-his2 31013 ax-his3 31014 ax-his4 31015 ax-hcompl 31132 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2704 df-cleq 2718 df-clel 2803 df-nfc 2878 df-ne 2931 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3364 df-reu 3365 df-rab 3420 df-v 3464 df-sbc 3776 df-csb 3892 df-dif 3949 df-un 3951 df-in 3953 df-ss 3963 df-pss 3966 df-nul 4323 df-if 4524 df-pw 4599 df-sn 4624 df-pr 4626 df-tp 4628 df-op 4630 df-uni 4906 df-int 4947 df-iun 4995 df-iin 4996 df-br 5146 df-opab 5208 df-mpt 5229 df-tr 5263 df-id 5572 df-eprel 5578 df-po 5586 df-so 5587 df-fr 5629 df-se 5630 df-we 5631 df-xp 5680 df-rel 5681 df-cnv 5682 df-co 5683 df-dm 5684 df-rn 5685 df-res 5686 df-ima 5687 df-pred 6304 df-ord 6371 df-on 6372 df-lim 6373 df-suc 6374 df-iota 6498 df-fun 6548 df-fn 6549 df-f 6550 df-f1 6551 df-fo 6552 df-f1o 6553 df-fv 6554 df-isom 6555 df-riota 7372 df-ov 7419 df-oprab 7420 df-mpo 7421 df-of 7682 df-om 7869 df-1st 7995 df-2nd 7996 df-supp 8167 df-frecs 8288 df-wrecs 8319 df-recs 8393 df-rdg 8432 df-1o 8488 df-2o 8489 df-oadd 8492 df-omul 8493 df-er 8726 df-map 8849 df-pm 8850 df-ixp 8919 df-en 8967 df-dom 8968 df-sdom 8969 df-fin 8970 df-fsupp 9399 df-fi 9447 df-sup 9478 df-inf 9479 df-oi 9546 df-card 9975 df-acn 9978 df-pnf 11291 df-mnf 11292 df-xr 11293 df-ltxr 11294 df-le 11295 df-sub 11487 df-neg 11488 df-div 11913 df-nn 12259 df-2 12321 df-3 12322 df-4 12323 df-5 12324 df-6 12325 df-7 12326 df-8 12327 df-9 12328 df-n0 12519 df-z 12605 df-dec 12724 df-uz 12869 df-q 12979 df-rp 13023 df-xneg 13140 df-xadd 13141 df-xmul 13142 df-ioo 13376 df-ico 13378 df-icc 13379 df-fz 13533 df-fzo 13676 df-fl 13806 df-seq 14016 df-exp 14076 df-hash 14343 df-cj 15099 df-re 15100 df-im 15101 df-sqrt 15235 df-abs 15236 df-clim 15485 df-rlim 15486 df-sum 15686 df-struct 17144 df-sets 17161 df-slot 17179 df-ndx 17191 df-base 17209 df-ress 17238 df-plusg 17274 df-mulr 17275 df-starv 17276 df-sca 17277 df-vsca 17278 df-ip 17279 df-tset 17280 df-ple 17281 df-ds 17283 df-unif 17284 df-hom 17285 df-cco 17286 df-rest 17432 df-topn 17433 df-0g 17451 df-gsum 17452 df-topgen 17453 df-pt 17454 df-prds 17457 df-xrs 17512 df-qtop 17517 df-imas 17518 df-xps 17520 df-mre 17594 df-mrc 17595 df-acs 17597 df-mgm 18628 df-sgrp 18707 df-mnd 18723 df-submnd 18769 df-mulg 19058 df-cntz 19307 df-cmn 19776 df-psmet 21331 df-xmet 21332 df-met 21333 df-bl 21334 df-mopn 21335 df-fbas 21336 df-fg 21337 df-cnfld 21340 df-top 22884 df-topon 22901 df-topsp 22923 df-bases 22937 df-cld 23011 df-ntr 23012 df-cls 23013 df-nei 23090 df-cn 23219 df-cnp 23220 df-lm 23221 df-t1 23306 df-haus 23307 df-tx 23554 df-hmeo 23747 df-fil 23838 df-fm 23930 df-flim 23931 df-flf 23932 df-xms 24314 df-ms 24315 df-tms 24316 df-cfil 25271 df-cau 25272 df-cmet 25273 df-grpo 30423 df-gid 30424 df-ginv 30425 df-gdiv 30426 df-ablo 30475 df-vc 30489 df-nv 30522 df-va 30525 df-ba 30526 df-sm 30527 df-0v 30528 df-vs 30529 df-nmcv 30530 df-ims 30531 df-dip 30631 df-ssp 30652 df-ph 30743 df-cbn 30793 df-hnorm 30898 df-hba 30899 df-hvsub 30901 df-hlim 30902 df-hcau 30903 df-sh 31137 df-ch 31151 df-oc 31182 df-ch0 31183 df-nmop 31769 df-cnop 31770 df-lnop 31771 df-nmfn 31775 df-nlfn 31776 df-cnfn 31777 df-lnfn 31778 |
This theorem is referenced by: cnlnadjlem6 32002 cnlnadjlem7 32003 cnlnadjlem9 32005 |
Copyright terms: Public domain | W3C validator |