Theorem riesz1t 9913

Description: Part 1 of the Riesz representation theorem for bounded linear functionals. A linear functional is bounded iff its value can be expressed as an inner product. Part of Theorem 17.3 of [Halmos] p. 31. For part 2, see riesz2t 9914. For the continuous linear functional version, see riesz3 9910 and riesz4t 9912.

Assertion

Ref	Expression
riesz1t	|- (T e. LinFn -> ((normfn` T) e. RR <-> E.y e. H~ A.x e. H~ (T` x) = (x .ih y)))

Distinct variable group:   x,y,T

Proof of Theorem riesz1t

Step	Hyp	Ref	Expression
1		lnfncnbdt 9907	. 2 |- (T e. LinFn -> (T e. ConFn <-> (normfn` T) e. RR))
2		elin 2197	. . . . 5 |- (T e. (LinFn i^i ConFn) <-> (T e. LinFn /\ T e. ConFn))
3		fveq1 3708	. . . . . . . 8 |- (T = if(T e. (LinFn i^i ConFn), T, (H~ X. {0})) -> (T` x) = (if(T e. (LinFn i^i ConFn), T, (H~ X. {0}))` x))
4	3	eqeq1d 1475	. . . . . . 7 |- (T = if(T e. (LinFn i^i ConFn), T, (H~ X. {0})) -> ((T` x) = (x .ih y) <-> (if(T e. (LinFn i^i ConFn), T, (H~ X. {0}))` x) = (x .ih y)))
5	4	rexralbidv 1674	. . . . . 6 |- (T = if(T e. (LinFn i^i ConFn), T, (H~ X. {0})) -> (E.y e. H~ A.x e. H~ (T` x) = (x .ih y) <-> E.y e. H~ A.x e. H~ (if(T e. (LinFn i^i ConFn), T, (H~ X. {0}))` x) = (x .ih y)))
6		inss1 2220	. . . . . . . 8 |- (LinFn i^i ConFn) (_ LinFn
7		elin 2197	. . . . . . . . . 10 |- ((H~ X. {0}) e. (LinFn i^i ConFn) <-> ((H~ X. {0}) e. LinFn /\ (H~ X. {0}) e. ConFn))
8		0lnfn 9825	. . . . . . . . . 10 |- (H~ X. {0}) e. LinFn
9		0cnfn 9820	. . . . . . . . . 10 |- (H~ X. {0}) e. ConFn
10	7, 8, 9	mpbir2an 728	. . . . . . . . 9 |- (H~ X. {0}) e. (LinFn i^i ConFn)
11	10	elimel 2384	. . . . . . . 8 |- if(T e. (LinFn i^i ConFn), T, (H~ X. {0})) e. (LinFn i^i ConFn)
12	6, 11	sselii 2056	. . . . . . 7 |- if(T e. (LinFn i^i ConFn), T, (H~ X. {0})) e. LinFn
13		inss2 2221	. . . . . . . 8 |- (LinFn i^i ConFn) (_ ConFn
14	13, 11	sselii 2056	. . . . . . 7 |- if(T e. (LinFn i^i ConFn), T, (H~ X. {0})) e. ConFn
15	12, 14	riesz3 9910	. . . . . 6 |- E.y e. H~ A.x e. H~ (if(T e. (LinFn i^i ConFn), T, (H~ X. {0}))` x) = (x .ih y)
16	5, 15	dedth 2373	. . . . 5 |- (T e. (LinFn i^i ConFn) -> E.y e. H~ A.x e. H~ (T` x) = (x .ih y))
17	2, 16	sylbir 201	. . . 4 |- ((T e. LinFn /\ T e. ConFn) -> E.y e. H~ A.x e. H~ (T` x) = (x .ih y))
18	17	ex 373	. . 3 |- (T e. LinFn -> (T e. ConFn -> E.y e. H~ A.x e. H~ (T` x) = (x .ih y)))
19		fveq2 3709	. . . . . . . . . . . 12 |- ((T` x) = (x .ih y) -> (abs` (T` x)) = (abs` (x .ih y)))
20	19	adantl 388	. . . . . . . . . . 11 |- ((((T e. LinFn /\ x e. H~) /\ y e. H~) /\ (T` x) = (x .ih y)) -> (abs` (T` x)) = (abs` (x .ih y)))
21		bcst 8969	. . . . . . . . . . . . . 14 |- ((x e. H~ /\ y e. H~) -> (abs` (x .ih y)) <_ ((normh` x) x. (normh` y)))
22		axmulcom 5248	. . . . . . . . . . . . . . . 16 |- (((normh` x) e. CC /\ (normh` y) e. CC) -> ((normh` x) x. (normh` y)) = ((normh` y) x. (normh` x)))
23		recnt 5285	. . . . . . . . . . . . . . . 16 |- ((normh` x) e. RR -> (normh` x) e. CC)
24		recnt 5285	. . . . . . . . . . . . . . . 16 |- ((normh` y) e. RR -> (normh` y) e. CC)
25	22, 23, 24	syl2an 454	. . . . . . . . . . . . . . 15 |- (((normh` x) e. RR /\ (normh` y) e. RR) -> ((normh` x) x. (normh` y)) = ((normh` y) x. (normh` x)))
26		normclt 8912	. . . . . . . . . . . . . . 15 |- (x e. H~ -> (normh` x) e. RR)
27		normclt 8912	. . . . . . . . . . . . . . 15 |- (y e. H~ -> (normh` y) e. RR)
28	25, 26, 27	syl2an 454	. . . . . . . . . . . . . 14 |- ((x e. H~ /\ y e. H~) -> ((normh` x) x. (normh` y)) = ((normh` y) x. (normh` x)))
29	21, 28	breqtrd 2629	. . . . . . . . . . . . 13 |- ((x e. H~ /\ y e. H~) -> (abs` (x .ih y)) <_ ((normh` y) x. (normh` x)))
30	29	adantll 392	. . . . . . . . . . . 12 |- (((T e. LinFn /\ x e. H~) /\ y e. H~) -> (abs` (x .ih y)) <_ ((normh` y) x. (normh` x)))
31	30	adantr 389	. . . . . . . . . . 11 |- ((((T e. LinFn /\ x e. H~) /\ y e. H~) /\ (T` x) = (x .ih y)) -> (abs` (x .ih y)) <_ ((normh` y) x. (normh` x)))
32	20, 31	eqbrtrd 2625	. . . . . . . . . 10 |- ((((T e. LinFn /\ x e. H~) /\ y e. H~) /\ (T` x) = (x .ih y)) -> (abs` (T` x)) <_ ((normh` y) x. (normh` x)))
33	32	ex 373	. . . . . . . . 9 |- (((T e. LinFn /\ x e. H~) /\ y e. H~) -> ((T` x) = (x .ih y) -> (abs` (T` x)) <_ ((normh` y) x. (normh` x))))
34	33	an1rs 488	. . . . . . . 8 |- (((T e. LinFn /\ y e. H~) /\ x e. H~) -> ((T` x) = (x .ih y) -> (abs` (T` x)) <_ ((normh` y) x. (normh` x))))
35	34	r19.20dva 1701	. . . . . . 7 |- ((T e. LinFn /\ y e. H~) -> (A.x e. H~ (T` x) = (x .ih y) -> A.x e. H~ (abs` (T` x)) <_ ((normh` y) x. (normh` x))))
36	27	adantl 388	. . . . . . 7 |- ((T e. LinFn /\ y e. H~) -> (normh` y) e. RR)
37	35, 36	jctild 599	. . . . . 6 |- ((T e. LinFn /\ y e. H~) -> (A.x e. H~ (T` x) = (x .ih y) -> ((normh` y) e. RR /\ A.x e. H~ (abs` (T` x)) <_ ((normh` y) x. (normh` x)))))
38		opreq1 3953	. . . . . . . . 9 |- (z = (normh` y) -> (z x. (normh` x)) = ((normh` y) x. (normh` x)))
39	38	breq2d 2620	. . . . . . . 8 |- (z = (normh` y) -> ((abs` (T` x)) <_ (z x. (normh` x)) <-> (abs` (T` x)) <_ ((normh` y) x. (normh` x))))
40	39	ralbidv 1655	. . . . . . 7 |- (z = (normh` y) -> (A.x e. H~ (abs` (T` x)) <_ (z x. (normh` x)) <-> A.x e. H~ (abs` (T` x)) <_ ((normh` y) x. (normh` x))))
41	40	rcla4ev 1868	. . . . . 6 |- (((normh` y) e. RR /\ A.x e. H~ (abs` (T` x)) <_ ((normh` y) x. (normh` x))) -> E.z e. RR A.x e. H~ (abs` (T` x)) <_ (z x. (normh` x)))
42	37, 41	syl6 22	. . . . 5 |- ((T e. LinFn /\ y e. H~) -> (A.x e. H~ (T` x) = (x .ih y) -> E.z e. RR A.x e. H~ (abs` (T` x)) <_ (z x. (normh` x))))
43	42	r19.23adva 1739	. . . 4 |- (T e. LinFn -> (E.y e. H~ A.x e. H~ (T` x) = (x .ih y) -> E.z e. RR A.x e. H~ (abs` (T` x)) <_ (z x. (normh` x))))
44		lnfncont 9906	. . . 4 |- (T e. LinFn -> (T e. ConFn <-> E.z e. RR A.x e. H~ (abs` (T` x)) <_ (z x. (normh` x))))
45	43, 44	sylibrd 204	. . 3 |- (T e. LinFn -> (E.y e. H~ A.x e. H~ (T` x) = (x .ih y) -> T e. ConFn))
46	18, 45	impbid 514	. 2 |- (T e. LinFn -> (T e. ConFn <-> E.y e. H~ A.x e. H~ (T` x) = (x .ih y)))
47	1, 46	bitr3d 528	1 |- (T e. LinFn -> ((normfn` T) e. RR <-> E.y e. H~ A.x e. H~ (T` x) = (x .ih y)))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   = wceq 953   e. wcel 955  A.wral 1637  E.wrex 1638   i^i cin 2036  ifcif 2351  {csn 2399   class class class wbr 2609   X. cxp 3158  ` cfv 3172  (class class class)co 3948  CCcc 5204  RRcr 5205  0cc0 5206   x. cmul 5211   <_ cle 5267  abscabs 6681  H~chil 8727   .ih csp 8732  normhcno 8733  norm_fncnmf 8759  ConFnccnf 8761  LinFnclf 8762

This theorem is referenced by:  rnbra 9953

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-9 962  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-rep 2683  ax-sep 2693  ax-nul 2700  ax-pow 2732  ax-pr 2769  ax-un 2857  ax-reg 4565  ax-inf2 4597  ax-ac 4716  ax-hilex 8790  ax-hfvadd 8791  ax-hvcom 8792  ax-hvass 8793  ax-hv0cl 8794  ax-hvaddid 8795  ax-hfvmul 8796  ax-hvmulid 8797  ax-hvmulass 8798  ax-hvdistr1 8799  ax-hvdistr2 8800  ax-hvmul0 8801  ax-hfi 8867  ax-his1 8870  ax-his2 8871  ax-his3 8872  ax-his4 8873  ax-hcompl 8992

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 774  df-3an 775  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-nel 1580  df-ral 1641  df-rex 1642  df-reu 1643  df-rab 1644  df-v 1803  df-sbc 1932  df-csb 1992  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-pss 2045  df-nul 2271  df-if 2352  df-pw 2392  df-sn 2402  df-pr 2403  df-tp 2405  df-op 2406  df-uni 2494  df-int 2524  df-iun 2558  df-iin 2559  df-br 2610  df-opab 2657  df-tr 2671  df-eprel 2821  df-id 2824  df-po 2831  df-so 2841  df-fr 2907  df-we 2924  df-ord 2941  df-on 2942  df-lim 2943  df-suc 2944  df-om 3122  df-xp 3174  df-rel 3175  df-cnv 3176  df-co 3177  df-dm 3178  df-rn 3179  df-res 3180  df-ima 3181  df-fun 3182  df-fn 3183  df-f 3184  df-f1 3185  df-fo 3186  df-f1o 3187  df-fv 3188  df-rdg 3917  df-opr 3950  df-oprab 3951  df-1st 4063  df-2nd 4064  df-1o 4117  df-oadd 4119  df-omul 4120  df-er 4245  df-ec</