Theorem riesz3 9910

Description: A continuous linear functional can be expressed as an inner product. Existence part of Theorem 3.9 of [Beran] p. 104.

Hypotheses

Ref	Expression
nlelch.1	|- T e. LinFn
nlelch.2	|- T e. ConFn

Assertion

Ref	Expression
riesz3	|- E.w e. H~ A.v e. H~ (T` v) = (v .ih w)

Distinct variable group:   w,v,T

Proof of Theorem riesz3

Step	Hyp	Ref	Expression
1		fveq2 3709	. . . . . . . . 9 |- ((_|_` (null` T)) = 0H -> (_|_` (_|_` (null` T))) = (_|_` 0H))
2		nlelch.1	. . . . . . . . . . 11 |- T e. LinFn
3		nlelch.2	. . . . . . . . . . 11 |- T e. ConFn
4	2, 3	nlelch 9909	. . . . . . . . . 10 |- (null` T) e. CH
5	4	ococ 9162	. . . . . . . . 9 |- (_|_` (_|_` (null` T))) = (null` T)
6		choc0 9205	. . . . . . . . 9 |- (_|_` 0H) = H~
7	1, 5, 6	3eqtr3g 1522	. . . . . . . 8 |- ((_|_` (null` T)) = 0H -> (null` T) = H~)
8	7	eleq2d 1533	. . . . . . 7 |- ((_|_` (null` T)) = 0H -> (v e. (null` T) <-> v e. H~))
9	8	biimpar 417	. . . . . 6 |- (((_|_` (null` T)) = 0H /\ v e. H~) -> v e. (null` T))
10	2	lnfnf 9885	. . . . . . 7 |- T:H~-->CC
11		elnlfn2t 9769	. . . . . . 7 |- ((T:H~-->CC /\ v e. (null` T)) -> (T` v) = 0)
12	10, 11	mpan 693	. . . . . 6 |- (v e. (null` T) -> (T` v) = 0)
13	9, 12	syl 10	. . . . 5 |- (((_|_` (null` T)) = 0H /\ v e. H~) -> (T` v) = 0)
14		hi02t 8884	. . . . . 6 |- (v e. H~ -> (v .ih 0h) = 0)
15	14	adantl 388	. . . . 5 |- (((_|_` (null` T)) = 0H /\ v e. H~) -> (v .ih 0h) = 0)
16	13, 15	eqtr4d 1502	. . . 4 |- (((_|_` (null` T)) = 0H /\ v e. H~) -> (T` v) = (v .ih 0h))
17	16	r19.21aiva 1706	. . 3 |- ((_|_` (null` T)) = 0H -> A.v e. H~ (T` v) = (v .ih 0h))
18		ax-hv0cl 8794	. . . 4 |- 0h e. H~
19		opreq2 3954	. . . . . . 7 |- (w = 0h -> (v .ih w) = (v .ih 0h))
20	19	eqeq2d 1478	. . . . . 6 |- (w = 0h -> ((T` v) = (v .ih w) <-> (T` v) = (v .ih 0h)))
21	20	ralbidv 1655	. . . . 5 |- (w = 0h -> (A.v e. H~ (T` v) = (v .ih w) <-> A.v e. H~ (T` v) = (v .ih 0h)))
22	21	rcla4ev 1868	. . . 4 |- ((0h e. H~ /\ A.v e. H~ (T` v) = (v .ih 0h)) -> E.w e. H~ A.v e. H~ (T` v) = (v .ih w))
23	18, 22	mpan 693	. . 3 |- (A.v e. H~ (T` v) = (v .ih 0h) -> E.w e. H~ A.v e. H~ (T` v) = (v .ih w))
24	17, 23	syl 10	. 2 |- ((_|_` (null` T)) = 0H -> E.w e. H~ A.v e. H~ (T` v) = (v .ih w))
25	4	choccl 9101	. . . 4 |- (_|_` (null` T)) e. CH
26	25	chne0 9291	. . 3 |- ((_|_` (null` T)) =/= 0H <-> E.u e. (_|_` (null` T))u =/= 0h)
27	25	chel 9023	. . . . 5 |- (u e. (_|_` (null` T)) -> u e. H~)
28		opreq2 3954	. . . . . . . . . 10 |- (w = ((*` ((T` u) / (u .ih u))) .h u) -> (v .ih w) = (v .ih ((*` ((T` u) / (u .ih u))) .h u)))
29	28	eqeq2d 1478	. . . . . . . . 9 |- (w = ((*` ((T` u) / (u .ih u))) .h u) -> ((T` v) = (v .ih w) <-> (T` v) = (v .ih ((*` ((T` u) / (u .ih u))) .h u))))
30	29	ralbidv 1655	. . . . . . . 8 |- (w = ((*` ((T` u) / (u .ih u))) .h u) -> (A.v e. H~ (T` v) = (v .ih w) <-> A.v e. H~ (T` v) = (v .ih ((*` ((T` u) / (u .ih u))) .h u))))
31	30	rcla4ev 1868	. . . . . . 7 |- ((((*` ((T` u) / (u .ih u))) .h u) e. H~ /\ A.v e. H~ (T` v) = (v .ih ((*` ((T` u) / (u .ih u))) .h u))) -> E.w e. H~ A.v e. H~ (T` v) = (v .ih w))
32		hvmulclt 8804	. . . . . . . . 9 |- (((*` ((T` u) / (u .ih u))) e. CC /\ u e. H~) -> ((*` ((T` u) / (u .ih u))) .h u) e. H~)
33		divclt 5681	. . . . . . . . . . 11 |- (((T` u) e. CC /\ (u .ih u) e. CC /\ (u .ih u) =/= 0) -> ((T` u) / (u .ih u)) e. CC)
34	10	ffvelrni 3800	. . . . . . . . . . . 12 |- (u e. H~ -> (T` u) e. CC)
35	34	adantr 389	. . . . . . . . . . 11 |- ((u e. H~ /\ u =/= 0h) -> (T` u) e. CC)
36		hiclt 8868	. . . . . . . . . . . . 13 |- ((u e. H~ /\ u e. H~) -> (u .ih u) e. CC)
37	36	anidms 434	. . . . . . . . . . . 12 |- (u e. H~ -> (u .ih u) e. CC)
38	37	adantr 389	. . . . . . . . . . 11 |- ((u e. H~ /\ u =/= 0h) -> (u .ih u) e. CC)
39		his6t 8886	. . . . . . . . . . . . 13 |- (u e. H~ -> ((u .ih u) = 0 <-> u = 0h))
40	39	necon3bid 1593	. . . . . . . . . . . 12 |- (u e. H~ -> ((u .ih u) =/= 0 <-> u =/= 0h))
41	40	biimpar 417	. . . . . . . . . . 11 |- ((u e. H~ /\ u =/= 0h) -> (u .ih u) =/= 0)
42	33, 35, 38, 41	syl3anc 856	. . . . . . . . . 10 |- ((u e. H~ /\ u =/= 0h) -> ((T` u) / (u .ih u)) e. CC)
43		cjclt 6696	. . . . . . . . . 10 |- (((T` u) / (u .ih u)) e. CC -> (*` ((T` u) / (u .ih u))) e. CC)
44	42, 43	syl 10	. . . . . . . . 9 |- ((u e. H~ /\ u =/= 0h) -> (*` ((T` u) / (u .ih u))) e. CC)
45		pm3.26 319	. . . . . . . . 9 |- ((u e. H~ /\ u =/= 0h) -> u e. H~)
46	32, 44, 45	sylanc 471	. . . . . . . 8 |- ((u e. H~ /\ u =/= 0h) -> ((*` ((T` u) / (u .ih u))) .h u) e. H~)
47	46	adantll 392	. . . . . . 7 |- (((u e. (_|_` (null` T)) /\ u e. H~) /\ u =/= 0h) -> ((*` ((T` u) / (u .ih u))) .h u) e. H~)
48		his2subt 8879	. . . . . . . . . . . . . . . 16 |- ((((T` u) .h v) e. H~ /\ ((T` v) .h u) e. H~ /\ u e. H~) -> ((((T` u) .h v) -h ((T` v) .h u)) .ih u) = ((((T` u) .h v) .ih u) - (((T` v) .h u) .ih u)))
49		hvmulclt 8804	. . . . . . . . . . . . . . . . 17 |- (((T` u) e. CC /\ v e. H~) -> ((T` u) .h v) e. H~)
50	49, 34	sylan 448	. . . . . . . . . . . . . . . 16 |- ((u e. H~ /\ v e. H~) -> ((T` u) .h v) e. H~)
51		hvmulclt 8804	. . . . . . . . . . . . . . . . . 18 |- (((T` v) e. CC /\ u e. H~) -> ((T` v) .h u) e. H~)
52	10	ffvelrni 3800	. . . . . . . . . . . . . . . . . 18 |- (v e. H~ -> (T` v) e. CC)
53	51, 52	sylan 448	. . . . . . . . . . . . . . . . 17 |- ((v e. H~ /\ u e. H~) -> ((T` v) .h u) e. H~)
54	53	ancoms 436	. . . . . . . . . . . . . . . 16 |- ((u e. H~ /\ v e. H~) -> ((T` v) .h u) e. H~)
55		pm3.26 319	. . . . . . . . . . . . . . . 16 |- ((u e. H~ /\ v e. H~) -> u e. H~)
56	48, 50, 54, 55	syl3anc 856	. . . . . . . . . . . . . . 15 |- ((u e. H~ /\ v e. H~) -> ((((T` u) .h v) -h ((T` v) .h u)) .ih u) = ((((T` u) .h v) .ih u) - (((T` v) .h u) .ih u)))
57		ax-his3 8872	. . . . . . . . . . . . . . . . 17 |- (((T` u) e. CC /\ v e. H~ /\ u e. H~) -> (((T` u) .h v) .ih u) = ((T` u) x. (v .ih u)))
58	34	adantr 389	. . . . . . . . . . . . . . . . 17 |- ((u e. H~ /\ v e. H~) -> (T` u) e. CC)
59		pm3.27 323	. . . . . . . . . . . . . . . . 17 |- ((u e. H~ /\ v e. H~) -> v e. H~)
60	57, 58, 59, 55	syl3anc 856	. . . . . . . . . . . . . . . 16 |- ((u e. H~ /\ v e. H~) -> (((T` u) .h v) .ih u) = ((T` u) x. (v .ih u)))
61		ax-his3 8872	. . . . . . . . . . . . . . . . 17 |- (((T` v) e. CC /\ u e. H~ /\ u e. H~) -> (((T` v) .h u) .ih u) = ((T` v) x. (u .ih u)))
62	52	adantl 388	. . . . . . . . . . . . . . . . 17 |- ((u e. H~ /\ v e. H~) -> (T` v) e. CC)
63	61, 62, 55, 55	syl3anc 856	. . . . . . . . . . . . . . . 16 |- ((u e. H~ /\ v e. H~) -> (((T` v) .h u) .ih u) = ((T` v) x. (u .ih u)))
64	60, 63	opreq12d 3963	. . . . . . . . . . . . . . 15 |- ((u e. H~ /\ v e. H~) -> ((((T` u) .h v) .ih u) - (((T` v) .h u) .ih u)) = (((T` u) x. (v .ih u)) - ((T` v) x. (u .ih u))))
65	56, 64	eqtr2d 1500	. . . . . . . . . . . . . 14 |- ((u e. H~ /\ v e. H~