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

Theorem cnlnadjlem5 32001
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.)
Hypotheses
Ref Expression
cnlnadjlem.1 𝑇 ∈ LinOp
cnlnadjlem.2 𝑇 ∈ ContOp
cnlnadjlem.3 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇𝑔) ·ih 𝑦))
cnlnadjlem.4 𝐵 = (𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤))
cnlnadjlem.5 𝐹 = (𝑦 ∈ ℋ ↦ 𝐵)
Assertion
Ref Expression
cnlnadjlem5 ((𝐴 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝑇𝐶) ·ih 𝐴) = (𝐶 ·ih (𝐹𝐴)))
Distinct variable groups:   𝑣,𝑔,𝑤,𝑦,𝐴   𝑤,𝐹   𝑇,𝑔,𝑣,𝑤,𝑦   𝑣,𝐺,𝑤
Allowed substitution hints:   𝐵(𝑦,𝑤,𝑣,𝑔)   𝐶(𝑦,𝑤,𝑣,𝑔)   𝐹(𝑦,𝑣,𝑔)   𝐺(𝑦,𝑔)

Proof of Theorem cnlnadjlem5
Dummy variable 𝑓 is distinct from all other variables.
StepHypRef 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 𝑦(𝑦 ∈ ℋ ↦ 𝐵)
75, 6nfcxfr 2890 . . . . . . 7 𝑦𝐹
87, 1nffv 6903 . . . . . 6 𝑦(𝐹𝐴)
93, 4, 8nfov 7446 . . . . 5 𝑦(𝑓 ·ih (𝐹𝐴))
109nfeq2 2910 . . . 4 𝑦((𝑇𝑓) ·ih 𝐴) = (𝑓 ·ih (𝐹𝐴))
112, 10nfralw 3299 . . 3 𝑦𝑓 ∈ ℋ ((𝑇𝑓) ·ih 𝐴) = (𝑓 ·ih (𝐹𝐴))
12 oveq2 7424 . . . . 5 (𝑦 = 𝐴 → ((𝑇𝑓) ·ih 𝑦) = ((𝑇𝑓) ·ih 𝐴))
13 fveq2 6893 . . . . . 6 (𝑦 = 𝐴 → (𝐹𝑦) = (𝐹𝐴))
1413oveq2d 7432 . . . . 5 (𝑦 = 𝐴 → (𝑓 ·ih (𝐹𝑦)) = (𝑓 ·ih (𝐹𝐴)))
1512, 14eqeq12d 2742 . . . 4 (𝑦 = 𝐴 → (((𝑇𝑓) ·ih 𝑦) = (𝑓 ·ih (𝐹𝑦)) ↔ ((𝑇𝑓) ·ih 𝐴) = (𝑓 ·ih (𝐹𝐴))))
1615ralbidv 3168 . . 3 (𝑦 = 𝐴 → (∀𝑓 ∈ ℋ ((𝑇𝑓) ·ih 𝑦) = (𝑓 ·ih (𝐹𝑦)) ↔ ∀𝑓 ∈ ℋ ((𝑇𝑓) ·ih 𝐴) = (𝑓 ·ih (𝐹𝐴))))
17 cnlnadjlem.4 . . . . . . 7 𝐵 = (𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤))
18 riotaex 7376 . . . . . . 7 (𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤)) ∈ V
1917, 18eqeltri 2822 . . . . . 6 𝐵 ∈ V
205fvmpt2 7012 . . . . . 6 ((𝑦 ∈ ℋ ∧ 𝐵 ∈ V) → (𝐹𝑦) = 𝐵)
2119, 20mpan2 689 . . . . 5 (𝑦 ∈ ℋ → (𝐹𝑦) = 𝐵)
22 fveq2 6893 . . . . . . . . . . . . 13 (𝑣 = 𝑓 → (𝑇𝑣) = (𝑇𝑓))
2322oveq1d 7431 . . . . . . . . . . . 12 (𝑣 = 𝑓 → ((𝑇𝑣) ·ih 𝑦) = ((𝑇𝑓) ·ih 𝑦))
24 oveq1 7423 . . . . . . . . . . . 12 (𝑣 = 𝑓 → (𝑣 ·ih 𝑤) = (𝑓 ·ih 𝑤))
2523, 24eqeq12d 2742 . . . . . . . . . . 11 (𝑣 = 𝑓 → (((𝑇𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤) ↔ ((𝑇𝑓) ·ih 𝑦) = (𝑓 ·ih 𝑤)))
2625cbvralvw 3225 . . . . . . . . . 10 (∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤) ↔ ∀𝑓 ∈ ℋ ((𝑇𝑓) ·ih 𝑦) = (𝑓 ·ih 𝑤))
2726a1i 11 . . . . . . . . 9 (𝑤 ∈ ℋ → (∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤) ↔ ∀𝑓 ∈ ℋ ((𝑇𝑓) ·ih 𝑦) = (𝑓 ·ih 𝑤)))
28 cnlnadjlem.1 . . . . . . . . . . . 12 𝑇 ∈ LinOp
29 cnlnadjlem.2 . . . . . . . . . . . 12 𝑇 ∈ ContOp
30 cnlnadjlem.3 . . . . . . . . . . . 12 𝐺 = (𝑔 ∈ ℋ ↦ ((𝑇𝑔) ·ih 𝑦))
3128, 29, 30cnlnadjlem1 31997 . . . . . . . . . . 11 (𝑓 ∈ ℋ → (𝐺𝑓) = ((𝑇𝑓) ·ih 𝑦))
3231eqeq1d 2728 . . . . . . . . . 10 (𝑓 ∈ ℋ → ((𝐺𝑓) = (𝑓 ·ih 𝑤) ↔ ((𝑇𝑓) ·ih 𝑦) = (𝑓 ·ih 𝑤)))
3332ralbiia 3081 . . . . . . . . 9 (∀𝑓 ∈ ℋ (𝐺𝑓) = (𝑓 ·ih 𝑤) ↔ ∀𝑓 ∈ ℋ ((𝑇𝑓) ·ih 𝑦) = (𝑓 ·ih 𝑤))
3427, 33bitr4di 288 . . . . . . . 8 (𝑤 ∈ ℋ → (∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤) ↔ ∀𝑓 ∈ ℋ (𝐺𝑓) = (𝑓 ·ih 𝑤)))
3534riotabiia 7393 . . . . . . 7 (𝑤 ∈ ℋ ∀𝑣 ∈ ℋ ((𝑇𝑣) ·ih 𝑦) = (𝑣 ·ih 𝑤)) = (𝑤 ∈ ℋ ∀𝑓 ∈ ℋ (𝐺𝑓) = (𝑓 ·ih 𝑤))
3617, 35eqtri 2754 . . . . . 6 𝐵 = (𝑤 ∈ ℋ ∀𝑓 ∈ ℋ (𝐺𝑓) = (𝑓 ·ih 𝑤))
3728, 29, 30cnlnadjlem2 31998 . . . . . . . 8 (𝑦 ∈ ℋ → (𝐺 ∈ LinFn ∧ 𝐺 ∈ ContFn))
38 elin 3962 . . . . . . . 8 (𝐺 ∈ (LinFn ∩ ContFn) ↔ (𝐺 ∈ LinFn ∧ 𝐺 ∈ ContFn))
3937, 38sylibr 233 . . . . . . 7 (𝑦 ∈ ℋ → 𝐺 ∈ (LinFn ∩ ContFn))
40 riesz4 31994 . . . . . . 7 (𝐺 ∈ (LinFn ∩ ContFn) → ∃!𝑤 ∈ ℋ ∀𝑓 ∈ ℋ (𝐺𝑓) = (𝑓 ·ih 𝑤))
41 riotacl2 7389 . . . . . . 7 (∃!𝑤 ∈ ℋ ∀𝑓 ∈ ℋ (𝐺𝑓) = (𝑓 ·ih 𝑤) → (𝑤 ∈ ℋ ∀𝑓 ∈ ℋ (𝐺𝑓) = (𝑓 ·ih 𝑤)) ∈ {𝑤 ∈ ℋ ∣ ∀𝑓 ∈ ℋ (𝐺𝑓) = (𝑓 ·ih 𝑤)})
4239, 40, 413syl 18 . . . . . 6 (𝑦 ∈ ℋ → (𝑤 ∈ ℋ ∀𝑓 ∈ ℋ (𝐺𝑓) = (𝑓 ·ih 𝑤)) ∈ {𝑤 ∈ ℋ ∣ ∀𝑓 ∈ ℋ (𝐺𝑓) = (𝑓 ·ih 𝑤)})
4336, 42eqeltrid 2830 . . . . 5 (𝑦 ∈ ℋ → 𝐵 ∈ {𝑤 ∈ ℋ ∣ ∀𝑓 ∈ ℋ (𝐺𝑓) = (𝑓 ·ih 𝑤)})
4421, 43eqeltrd 2826 . . . 4 (𝑦 ∈ ℋ → (𝐹𝑦) ∈ {𝑤 ∈ ℋ ∣ ∀𝑓 ∈ ℋ (𝐺𝑓) = (𝑓 ·ih 𝑤)})
45 oveq2 7424 . . . . . . . . 9 (𝑤 = (𝐹𝑦) → (𝑓 ·ih 𝑤) = (𝑓 ·ih (𝐹𝑦)))
4645eqeq2d 2737 . . . . . . . 8 (𝑤 = (𝐹𝑦) → (((𝑇𝑓) ·ih 𝑦) = (𝑓 ·ih 𝑤) ↔ ((𝑇𝑓) ·ih 𝑦) = (𝑓 ·ih (𝐹𝑦))))
4746ralbidv 3168 . . . . . . 7 (𝑤 = (𝐹𝑦) → (∀𝑓 ∈ ℋ ((𝑇𝑓) ·ih 𝑦) = (𝑓 ·ih 𝑤) ↔ ∀𝑓 ∈ ℋ ((𝑇𝑓) ·ih 𝑦) = (𝑓 ·ih (𝐹𝑦))))
4833, 47bitrid 282 . . . . . 6 (𝑤 = (𝐹𝑦) → (∀𝑓 ∈ ℋ (𝐺𝑓) = (𝑓 ·ih 𝑤) ↔ ∀𝑓 ∈ ℋ ((𝑇𝑓) ·ih 𝑦) = (𝑓 ·ih (𝐹𝑦))))
4948elrab 3680 . . . . 5 ((𝐹𝑦) ∈ {𝑤 ∈ ℋ ∣ ∀𝑓 ∈ ℋ (𝐺𝑓) = (𝑓 ·ih 𝑤)} ↔ ((𝐹𝑦) ∈ ℋ ∧ ∀𝑓 ∈ ℋ ((𝑇𝑓) ·ih 𝑦) = (𝑓 ·ih (𝐹𝑦))))
5049simprbi 495 . . . 4 ((𝐹𝑦) ∈ {𝑤 ∈ ℋ ∣ ∀𝑓 ∈ ℋ (𝐺𝑓) = (𝑓 ·ih 𝑤)} → ∀𝑓 ∈ ℋ ((𝑇𝑓) ·ih 𝑦) = (𝑓 ·ih (𝐹𝑦)))
5144, 50syl 17 . . 3 (𝑦 ∈ ℋ → ∀𝑓 ∈ ℋ ((𝑇𝑓) ·ih 𝑦) = (𝑓 ·ih (𝐹𝑦)))
521, 11, 16, 51vtoclgaf 3556 . 2 (𝐴 ∈ ℋ → ∀𝑓 ∈ ℋ ((𝑇𝑓) ·ih 𝐴) = (𝑓 ·ih (𝐹𝐴)))
53 fveq2 6893 . . . . 5 (𝑓 = 𝐶 → (𝑇𝑓) = (𝑇𝐶))
5453oveq1d 7431 . . . 4 (𝑓 = 𝐶 → ((𝑇𝑓) ·ih 𝐴) = ((𝑇𝐶) ·ih 𝐴))
55 oveq1 7423 . . . 4 (𝑓 = 𝐶 → (𝑓 ·ih (𝐹𝐴)) = (𝐶 ·ih (𝐹𝐴)))
5654, 55eqeq12d 2742 . . 3 (𝑓 = 𝐶 → (((𝑇𝑓) ·ih 𝐴) = (𝑓 ·ih (𝐹𝐴)) ↔ ((𝑇𝐶) ·ih 𝐴) = (𝐶 ·ih (𝐹𝐴))))
5756rspccva 3606 . 2 ((∀𝑓 ∈ ℋ ((𝑇𝑓) ·ih 𝐴) = (𝑓 ·ih (𝐹𝐴)) ∧ 𝐶 ∈ ℋ) → ((𝑇𝐶) ·ih 𝐴) = (𝐶 ·ih (𝐹𝐴)))
5852, 57sylan 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