cnlnadjlem4 - Hilbert Space Explorer

Hilbert Space Explorer

< Previous Next >
Related theorems
GIF version

Theorem cnlnadjlem4 10027

Description: Lemma for cnlnadji 10033. The values of auxiliary function F are vectors.

**Hypotheses**
Ref	Expression
cnlnadjlem.1	⊢ T ∈ LinOp
cnlnadjlem.2	⊢ T ∈ ConOp
cnlnadjlem.3	⊢ G = {⟨g, h⟩∣(g ∈ ℋ ⋀ h = ((T ‘g) ·_ih y))}
cnlnadjlem.4	⊢ B = ∪{w ∈ ℋ ∣∀v ∈ ℋ ((T ‘v) ·_ih y) = (v ·_ih w)}
cnlnadjlem.5	⊢ F = {⟨y, u⟩∣(y ∈ ℋ ⋀ u = B)}

**Assertion**
Ref	Expression
cnlnadjlem4	⊢ (A ∈ ℋ → (F ‘A) ∈ ℋ )

Distinct variable groups: g,h,u,v,w,y,A u,B w,F v,G,w T,g,h,u,v,w,y

**Proof of Theorem cnlnadjlem4**
Step	Hyp	Ref	Expression
1		opreq2 3985	. . . . . . . 8 ⊢ (y = A → ((T ‘v) ·_ih y) = ((T ‘v) ·_ih A))
2	1	eqeq1d 1490	. . . . . . 7 ⊢ (y = A → (((T ‘v) ·_ih y) = (v ·_ih w) ↔ ((T ‘v) ·_ih A) = (v ·_ih w)))
3	2	ralbidv 1670	. . . . . 6 ⊢ (y = A → (∀v ∈ ℋ ((T ‘v) ·_ih y) = (v ·_ih w) ↔ ∀v ∈ ℋ ((T ‘v) ·_ih A) = (v ·_ih w)))
4	3	rabbisdv 1814	. . . . 5 ⊢ (y = A → {w ∈ ℋ ∣∀v ∈ ℋ ((T ‘v) ·_ih y) = (v ·_ih w)} = {w ∈ ℋ ∣∀v ∈ ℋ ((T ‘v) ·_ih A) = (v ·_ih w)})
5	4	unieqd 2526	. . . 4 ⊢ (y = A → ∪{w ∈ ℋ ∣∀v ∈ ℋ ((T ‘v) ·_ih y) = (v ·_ih w)} = ∪{w ∈ ℋ ∣∀v ∈ ℋ ((T ‘v) ·_ih A) = (v ·_ih w)})
6		cnlnadjlem.4	. . . 4 ⊢ B = ∪{w ∈ ℋ ∣∀v ∈ ℋ ((T ‘v) ·_ih y) = (v ·_ih w)}
7	5, 6	syl5eq 1526	. . 3 ⊢ (y = A → B = ∪{w ∈ ℋ ∣∀v ∈ ℋ ((T ‘v) ·_ih A) = (v ·_ih w)})
8		cnlnadjlem.5	. . 3 ⊢ F = {⟨y, u⟩∣(y ∈ ℋ ⋀ u = B)}
9		ax-hilex 8893	. . . . 5 ⊢ ℋ ∈ V
10	9	rabex 2740	. . . 4 ⊢ {w ∈ ℋ ∣∀v ∈ ℋ ((T ‘v) ·_ih A) = (v ·_ih w)} ∈ V
11	10	uniex 2886	. . 3 ⊢ ∪{w ∈ ℋ ∣∀v ∈ ℋ ((T ‘v) ·_ih A) = (v ·_ih w)} ∈ V
12	7, 8, 11	fvopab4 3796	. 2 ⊢ (A ∈ ℋ → (F ‘A) = ∪{w ∈ ℋ ∣∀v ∈ ℋ ((T ‘v) ·_ih A) = (v ·_ih w)})
13	3	reubidv 1787	. . . 4 ⊢ (y = A → (∃!w ∈ ℋ ∀v ∈ ℋ ((T ‘v) ·_ih y) = (v ·_ih w) ↔ ∃!w ∈ ℋ ∀v ∈ ℋ ((T ‘v) ·_ih A) = (v ·_ih w)))
14		cnlnadjlem.1	. . . . . . . 8 ⊢ T ∈ LinOp
15		cnlnadjlem.2	. . . . . . . 8 ⊢ T ∈ ConOp
16		cnlnadjlem.3	. . . . . . . 8 ⊢ G = {⟨g, h⟩∣(g ∈ ℋ ⋀ h = ((T ‘g) ·_ih y))}
17	14, 15, 16	cnlnadjlem2 10025	. . . . . . 7 ⊢ (y ∈ ℋ → (G ∈ LinFn ⋀ G ∈ ConFn))
18		elin 2218	. . . . . . 7 ⊢ (G ∈ (LinFn ∩ ConFn) ↔ (G ∈ LinFn ⋀ G ∈ ConFn))
19	17, 18	sylibr 200	. . . . . 6 ⊢ (y ∈ ℋ → G ∈ (LinFn ∩ ConFn))
20		riesz4 10021	. . . . . 6 ⊢ (G ∈ (LinFn ∩ ConFn) → ∃!w ∈ ℋ ∀v ∈ ℋ (G ‘v) = (v ·_ih w))
21	19, 20	syl 10	. . . . 5 ⊢ (y ∈ ℋ → ∃!w ∈ ℋ ∀v ∈ ℋ (G ‘v) = (v ·_ih w))
22	14, 15, 16	cnlnadjlem1 10024	. . . . . . . 8 ⊢ (v ∈ ℋ → (G ‘v) = ((T ‘v) ·_ih y))
23	22	eqeq1d 1490	. . . . . . 7 ⊢ (v ∈ ℋ → ((G ‘v) = (v ·_ih w) ↔ ((T ‘v) ·_ih y) = (v ·_ih w)))
24	23	ralbiia 1680	. . . . . 6 ⊢ (∀v ∈ ℋ (G ‘v) = (v ·_ih w) ↔ ∀v ∈ ℋ ((T ‘v) ·_ih y) = (v ·_ih w))
25	24	reubii 1789	. . . . 5 ⊢ (∃!w ∈ ℋ ∀v ∈ ℋ (G ‘v) = (v ·_ih w) ↔ ∃!w ∈ ℋ ∀v ∈ ℋ ((T ‘v) ·_ih y) = (v ·_ih w))
26	21, 25	sylib 198	. . . 4 ⊢ (y ∈ ℋ → ∃!w ∈ ℋ ∀v ∈ ℋ ((T ‘v) ·_ih y) = (v ·_ih w))
27	13, 26	vtoclga 1859	. . 3 ⊢ (A ∈ ℋ → ∃!w ∈ ℋ ∀v ∈ ℋ ((T ‘v) ·_ih A) = (v ·_ih w))
28		reucl 2901	. . 3 ⊢ (∃!w ∈ ℋ ∀v ∈ ℋ ((T ‘v) ·_ih A) = (v ·_ih w) → ∪{w ∈ ℋ ∣∀v ∈ ℋ ((T ‘v) ·_ih A) = (v ·_ih w)} ∈ ℋ )
29	27, 28	syl 10	. 2 ⊢ (A ∈ ℋ → ∪{w ∈ ℋ ∣∀v ∈ ℋ ((T ‘v) ·_ih A) = (v ·_ih w)} ∈ ℋ )
30	12, 29	eqeltrd 1555	1 ⊢ (A ∈ ℋ → (F ‘A) ∈ ℋ )

Colors of variables: wff set class

Syntax hints: → wi 3 ⋀ wa 223 = wceq 960 ∈ wcel 962 ∀wral 1652 ∃!wreu 1654 {crab 1655 ∩ cin 2057 ∪cuni 2517 {copab 2681 ‘cfv 3198 (class class class)co 3979 ℋ chil 8812 ·_ih csp 8817 ConOpcco 8839 LinOpclo 8840 ConFnccnf 8846 LinFnclf 8847

This theorem is referenced by: cnlnadjlem6 10029 cnlnadjlem7 10030

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 966 ax-gen 967 ax-8 968 ax-9 969 ax-10 970 ax-11 971 ax-12 972 ax-13 973 ax-14 974 ax-17 975 ax-4 977 ax-5o 979 ax-6o 982 ax-9o 1127 ax-10o 1144 ax-16 1214 ax-11o 1222 ax-ext 1464 ax-rep 2708 ax-sep 2718 ax-nul 2725 ax-pow 2758 ax-pr 2795 ax-un 2882 ax-reg 4608 ax-inf2 4642 ax-ac 4761 ax-hilex 8893 ax-hfvadd 8894 ax-hvcom 8895 ax-hvass 8896 ax-hv0cl 8897 ax-hvaddid 8898 ax-hfvmul 8899 ax-hvmulid 8900 ax-hvmulass 8901 ax-hvdistr1 8902 ax-hvdistr2 8903 ax-hvmul0 8904 ax-hfi 8970 ax-his1 8973 ax-his2 8974 ax-his3 8975 ax-his4 8976 ax-hcompl 9095

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3or 780 df-3an 781 df-ex 985 df-sb 1176 df-eu 1386 df-mo 1387 df-clab 1470 df-cleq 1475 df-clel 1478 df-ne 1594 df-nel 1595 df-ral 1656 df-rex 1657 df-reu 1658 df-rab 1659 df-v 1819 df-sbc 1949 df-csb 2012 df-dif 2060 df-un 2061 df-in 2062 df-ss 2064 df-pss 2066 df-nul 2292 df-if 2374 df-pw 2414 df-sn 2424 df-pr 2425 df-tp 2427 df-op 2428 df-uni 2518 df-int 2548 df-iun 2582 df-iin 2583 df-br 2635 df-opab 2682 df-tr 2696 df-eprel 2848 df-id 2851 df-po 2856 df-so 2866 df-fr 2933 df-we 2950 df-ord 2967 df-on 2968 df-lim 2969 df-suc 2970 df-om 3148 df-xp 3200 df-rel 3201 df-cnv 3202 df-co 3203 df-dm 3204 df-rn 3205 df-res 3206 df-ima 3207 df-fun 3208 df-fn 3209 df-f 3210 df-f1 3211 df-fo 3212 df-f1o 3213 df-fv 3214 df-rdg 3948 df-opr 3981 df-oprab 3982 df-1st 4095 df-2nd 4096 df-1o 4149 df-oadd 4151 df-omul 4152 df-er 4277 df-ec 4279 df-qs 4282 df-map 4342 df-en 4386 df-dom 4387 df-sdom 4388 df-sup 4589 df-r1 4660 df-rank 4661 df-ni 5020 df-pli 5021 df-mi 5022 df-lti 5023 df-plpq 5055 df-mpq 5056 df-enq 5057 df-nq 5058 df-plq 5059 df-mq 5060 df-rq 5061 df-ltq 5062 df-1q 5063 df-np 5106 df-1p 5107 df-plp 5108 df-mp 5109 df-ltp 5110 df-plpr 5184 df-mpr 5185 df-enr 5186 df-nr 5187 df-plr 5188 df-mr 5189 df-ltr 5190 df-0r 5191 df-1r 5192 df-m1r 5193 df-c 5260 df-0 5261 df-1 5262 df-i 5263 df-r 5264 df-plus 5265 df-mul 5266 df-lt 5267 df-sub 5376 df-neg 5378 df-pnf 5507 df-mnf 5508 df-xr 5509 df-ltxr 5510 df-le 5511 df-div 5723 df-n 5939 df-2 5984 df-3 5985 df-4 5986 df-n0 6132 df-z 6168 df-q 6258 df-fl 6284 df-ioo 6328 df-uz 6386 df-fz 6436 df-seq1 6509 df-shft 6542 df-seqz 6564 df-exp 6600 df-sqr 6702 df-re 6783 df-im 6784 df-cj 6785 df-abs 6786 df-clim 7007 df-sum 7012 df-top 7625 df-bases 7627 df-topgen 7628 df-cld 7689 df-ntr 7690 df-cls 7691 df-cn 7780 df-cnp 7781 df-haus 7808 df-met 7819 df-bl 7821 df-opn 7822 df-lm 7948 df-grp 8063 df-gid 8064 df-ginv 8065 df-gdiv 8066 df-abl 8125 df-vc 8190 df-nv 8236 df-va 8239 df-ba 8240 df-sm 8241 df-0v 8242 df-vs 8243 df-nm 8244 df-ims 8245 df-ip 8375 df-ph 8497 df-hnorm 8861 df-hvsub 8864 df-hlim 8865 df-hcau 8866 df-sh 9100 df-ch 9116 df-oc 9148 df-ch0 9149 df-nmop 9789 df-cnop 9790 df-lnop 9791 df-nmfn 9795 df-nlfn 9796 df-cnfn 9797 df-lnfn 9798