Theorem hhcms 9011

Description: The Hilbert space induced metric determines a complete metric space.

Hypotheses

Ref	Expression
hhcms.1	|- U = <.<. +h , .h >., normh>.
hhcms.2	|- D = (IndMet` U)

Assertion

Ref	Expression
hhcms	|- D e. CMet

Proof of Theorem hhcms

Step	Hyp	Ref	Expression
1		hhcms.1	. . 3 |- U = <.<. +h , .h >., normh>.
2		hhcms.2	. . 3 |- D = (IndMet` U)
3	1, 2	hhmetba 8981	. 2 |- H~ = dom dom D
4	1, 2	hhmet 8980	. 2 |- D e. Met
5		1z 6114	. . . . . . . 8 |- 1 e. ZZ
6		nnuz 6379	. . . . . . . 8 |- NN = (ZZ>` 1)
7	3, 5, 6	lmbrf2 7883	. . . . . . 7 |- ((D e. Met /\ x e. H~ /\ f:NN-->H~) -> (f(~~>m` D)x <-> A.y e. RR (0 < y -> E.j e. NN A.k e. NN (j <_ k -> ((f` k)Dx) < y))))
8	4, 7	mp3an1 901	. . . . . 6 |- ((x e. H~ /\ f:NN-->H~) -> (f(~~>m` D)x <-> A.y e. RR (0 < y -> E.j e. NN A.k e. NN (j <_ k -> ((f` k)Dx) < y))))
9	8	ancoms 436	. . . . 5 |- ((f:NN-->H~ /\ x e. H~) -> (f(~~>m` D)x <-> A.y e. RR (0 < y -> E.j e. NN A.k e. NN (j <_ k -> ((f` k)Dx) < y))))
10		visset 1809	. . . . . . 7 |- f e. V
11		visset 1809	. . . . . . 7 |- x e. V
12	10, 11	hlimconv 8998	. . . . . 6 |- (f ~~>v x -> A.y e. RR (0 < y -> E.j e. NN A.k e. NN (j <_ k -> (normh` ((f` k) -h x)) < y)))
13	1, 2	hhmetdval 8982	. . . . . . . . . . . . 13 |- (((f` k) e. H~ /\ x e. H~) -> ((f` k)Dx) = (normh` ((f` k) -h x)))
14		ffvelrn 3805	. . . . . . . . . . . . . 14 |- ((f:NN-->H~ /\ k e. NN) -> (f` k) e. H~)
15	10, 11	hlimseq 8996	. . . . . . . . . . . . . 14 |- (f ~~>v x -> f:NN-->H~)
16	14, 15	sylan 448	. . . . . . . . . . . . 13 |- ((f ~~>v x /\ k e. NN) -> (f` k) e. H~)
17	10, 11	hlimvec 8997	. . . . . . . . . . . . . 14 |- (f ~~>v x -> x e. H~)
18	17	adantr 389	. . . . . . . . . . . . 13 |- ((f ~~>v x /\ k e. NN) -> x e. H~)
19	13, 16, 18	sylanc 471	. . . . . . . . . . . 12 |- ((f ~~>v x /\ k e. NN) -> ((f` k)Dx) = (normh` ((f` k) -h x)))
20	19	breq1d 2624	. . . . . . . . . . 11 |- ((f ~~>v x /\ k e. NN) -> (((f` k)Dx) < y <-> (normh` ((f` k) -h x)) < y))
21	20	imbi2d 611	. . . . . . . . . 10 |- ((f ~~>v x /\ k e. NN) -> ((j <_ k -> ((f` k)Dx) < y) <-> (j <_ k -> (normh` ((f` k) -h x)) < y)))
22	21	ralbidva 1656	. . . . . . . . 9 |- (f ~~>v x -> (A.k e. NN (j <_ k -> ((f` k)Dx) < y) <-> A.k e. NN (j <_ k -> (normh` ((f` k) -h x)) < y)))
23	22	rexbidv 1661	. . . . . . . 8 |- (f ~~>v x -> (E.j e. NN A.k e. NN (j <_ k -> ((f` k)Dx) < y) <-> E.j e. NN A.k e. NN (j <_ k -> (normh` ((f` k) -h x)) < y)))
24	23	imbi2d 611	. . . . . . 7 |- (f ~~>v x -> ((0 < y -> E.j e. NN A.k e. NN (j <_ k -> ((f` k)Dx) < y)) <-> (0 < y -> E.j e. NN A.k e. NN (j <_ k -> (normh` ((f` k) -h x)) < y))))
25	24	ralbidv 1660	. . . . . 6 |- (f ~~>v x -> (A.y e. RR (0 < y -> E.j e. NN A.k e. NN (j <_ k -> ((f` k)Dx) < y)) <-> A.y e. RR (0 < y -> E.j e. NN A.k e. NN (j <_ k -> (normh` ((f` k) -h x)) < y))))
26	12, 25	mpbird 196	. . . . 5 |- (f ~~>v x -> A.y e. RR (0 < y -> E.j e. NN A.k e. NN (j <_ k -> ((f` k)Dx) < y)))
27	9, 26	syl5bir 210	. . . 4 |- ((f:NN-->H~ /\ x e. H~) -> (f ~~>v x -> f(~~>m` D)x))
28	27	r19.22dva 1736	. . 3 |- (f:NN-->H~ -> (E.x e. H~ f ~~>v x -> E.x e. H~ f(~~>m` D)x))
29		pm3.27 323	. . 3 |- ((f e. (Cau` D) /\ f:NN-->H~) -> f:NN-->H~)
30		hcau2 8994	. . . . 5 |- (f e. Cauchy <-> (f:NN-->H~ /\ A.y e. RR (0 < y -> E.j e. NN A.k e. NN (j <_ k -> (normh` ((f` k) -h (f` j))) < y))))
31		ax-hcompl 9010	. . . . 5 |- (f e. Cauchy -> E.x e. H~ f ~~>v x)
32	30, 31	sylbir 201	. . . 4 |- ((f:NN-->H~ /\ A.y e. RR (0 < y -> E.j e. NN A.k e. NN (j <_ k -> (normh` ((f` k) -h (f` j))) < y))) -> E.x e. H~ f ~~>v x)
33	3, 5, 6	iscauf 7891	. . . . . . 7 |- ((D e. Met /\ f:NN-->H~) -> (f e. (Cau` D) <-> A.y e. RR (0 < y -> E.j e. NN A.k e. NN (j <_ k -> ((f` j)D(f` k)) < y))))
34	4, 33	mpan 694	. . . . . 6 |- (f:NN-->H~ -> (f e. (Cau` D) <-> A.y e. RR (0 < y -> E.j e. NN A.k e. NN (j <_ k -> ((f` j)D(f` k)) < y))))
35	1, 2	hhmetdval 8982	. . . . . . . . . . . . . 14 |- (((f` j) e. H~ /\ (f` k) e. H~) -> ((f` j)D(f` k)) = (normh` ((f` j) -h (f` k))))
36		normsubt 8949	. . . . . . . . . . . . . 14 |- (((f` j) e. H~ /\ (f` k) e. H~) -> (normh` ((f` j) -h (f` k))) = (normh` ((f` k) -h (f` j))))
37	35, 36	eqtrd 1504	. . . . . . . . . . . . 13 |- (((f` j) e. H~ /\ (f` k) e. H~) -> ((f` j)D(f` k)) = (normh` ((f` k) -h (f` j))))
38	37	breq1d 2624	. . . . . . . . . . . 12 |- (((f` j) e. H~ /\ (f` k) e. H~) -> (((f` j)D(f` k)) < y <-> (normh` ((f` k) -h (f` j))) < y))
39		ffvelrn 3805	. . . . . . . . . . . . 13 |- ((f:NN-->H~ /\ j e. NN) -> (f` j) e. H~)
40	39	adantr 389	. . . . . . . . . . . 12 |- (((f:NN-->H~ /\ j e. NN) /\ k e. NN) -> (f` j) e. H~)
41	14	adantlr 393	. . . . . . . . . . . 12 |- (((f:NN-->H~ /\ j e. NN) /\ k e. NN) -> (f` k) e. H~)
42	38, 40, 41	sylanc 471	. . . . . . . . . . 11 |- (((f:NN-->H~ /\ j e. NN) /\ k e. NN) -> (((f` j)D(f` k)) < y <-> (normh` ((f` k) -h (f` j))) < y))
43	42	imbi2d 611	. . . . . . . . . 10 |- (((f:NN-->H~ /\ j e. NN) /\ k e. NN) -> ((j <_ k -> ((f` j)D(f` k)) < y) <-> (j <_ k -> (normh` ((f` k) -h (f` j))) < y)))
44	43	ralbidva 1656	. . . . . . . . 9 |- ((f:NN-->H~ /\ j e. NN) -> (A.k e. NN (j <_ k -> ((f` j)D(f` k)) < y) <-> A.k e. NN (j <_ k -> (normh` ((f` k) -h (f` j))) < y)))
45	44	rexbidva 1657	. . . . . . . 8 |- (f:NN-->H~ -> (E.j e. NN A.k e. NN (j <_ k -> ((f` j)D(f` k)) < y) <-> E.j e. NN A.k e. NN (j <_ k -> (normh` ((f` k) -h (f` j))) < y)))
46	45	imbi2d 611	. . . . . . 7 |- (f:NN-->H~ -> ((0 < y -> E.j e. NN A.k e. NN (j <_ k -> ((f` j)D(f` k)) < y)) <-> (0 < y -> E.j e. NN A.k e. NN (j <_ k -> (normh` ((f` k) -h (f` j))) < y))))
47	46	ralbidv 1660	. . . . . 6 |- (f:NN-->H~ -> (A.y e. RR (0 < y -> E.j e. NN A.k e. NN (j <_ k -> ((f` j)D(f` k)) < y)) <-> A.y e. RR (0 < y -> E.j e. NN A.k e. NN (j <_ k -> (normh` ((f` k) -h (f` j))) < y))))
48	34, 47	bitrd 527	. . . . 5 |- (f:NN-->H~ -> (f e. (Cau` D) <-> A.y e. RR (0 < y -> E.j e. NN A.k e. NN (j <_ k -> (normh` ((f` k) -h (f` j))) < y))))
49	48	biimpac 418	. . . 4 |- ((f e. (Cau` D) /\ f:NN-->H~) -> A.y e. RR (0 < y