Theorem h2hcau 8844

Description: The Cauchy sequences of Hilbert space.

Hypotheses

Ref	Expression
h2hc.1	|- U = <.<. +h , .h >., normh>.
h2hc.2	|- U e. NrmCVec
h2hc.4	|- H~ = (Base` U)
h2hc.3	|- D = (IndMet` U)

Assertion

Ref	Expression
h2hcau	|- Cauchy = ((Cau` D) i^i (H~ ^m NN))

Proof of Theorem h2hcau

Step	Hyp	Ref	Expression
1		h2hc.1	. . . . . . . . . . . . . . . . . . 19 |- U = <.<. +h , .h >., normh>.
2		h2hc.2	. . . . . . . . . . . . . . . . . . 19 |- U e. NrmCVec
3		h2hc.4	. . . . . . . . . . . . . . . . . . 19 |- H~ = (Base` U)
4		h2hc.3	. . . . . . . . . . . . . . . . . . 19 |- D = (IndMet` U)
5	1, 2, 3, 4	h2hmetdval 8843	. . . . . . . . . . . . . . . . . 18 |- (((f` z) e. H~ /\ (f` w) e. H~) -> ((f` z)D(f` w)) = (normh` ((f` z) -h (f` w))))
6	5	breq1d 2634	. . . . . . . . . . . . . . . . 17 |- (((f` z) e. H~ /\ (f` w) e. H~) -> (((f` z)D(f` w)) < x <-> (normh` ((f` z) -h (f` w))) < x))
7		ibar 645	. . . . . . . . . . . . . . . . 17 |- (((f` z) e. H~ /\ (f` w) e. H~) -> (((f` z)D(f` w)) < x <-> (((f` z) e. H~ /\ (f` w) e. H~) /\ ((f` z)D(f` w)) < x)))
8	6, 7	bitr3d 532	. . . . . . . . . . . . . . . 16 |- (((f` z) e. H~ /\ (f` w) e. H~) -> ((normh` ((f` z) -h (f` w))) < x <-> (((f` z) e. H~ /\ (f` w) e. H~) /\ ((f` z)D(f` w)) < x)))
9		df-3an 779	. . . . . . . . . . . . . . . 16 |- (((f` z) e. H~ /\ (f` w) e. H~ /\ ((f` z)D(f` w)) < x) <-> (((f` z) e. H~ /\ (f` w) e. H~) /\ ((f` z)D(f` w)) < x))
10	8, 9	syl6bbr 540	. . . . . . . . . . . . . . 15 |- (((f` z) e. H~ /\ (f` w) e. H~) -> ((normh` ((f` z) -h (f` w))) < x <-> ((f` z) e. H~ /\ (f` w) e. H~ /\ ((f` z)D(f` w)) < x)))
11		ffvelrn 3820	. . . . . . . . . . . . . . . 16 |- ((f:NN-->H~ /\ z e. NN) -> (f` z) e. H~)
12	11	adantr 391	. . . . . . . . . . . . . . 15 |- (((f:NN-->H~ /\ z e. NN) /\ w e. NN) -> (f` z) e. H~)
13		ffvelrn 3820	. . . . . . . . . . . . . . . 16 |- ((f:NN-->H~ /\ w e. NN) -> (f` w) e. H~)
14	13	adantlr 395	. . . . . . . . . . . . . . 15 |- (((f:NN-->H~ /\ z e. NN) /\ w e. NN) -> (f` w) e. H~)
15	10, 12, 14	sylanc 473	. . . . . . . . . . . . . 14 |- (((f:NN-->H~ /\ z e. NN) /\ w e. NN) -> ((normh` ((f` z) -h (f` w))) < x <-> ((f` z) e. H~ /\ (f` w) e. H~ /\ ((f` z)D(f` w)) < x)))
16	15	imbi2d 614	. . . . . . . . . . . . 13 |- (((f:NN-->H~ /\ z e. NN) /\ w e. NN) -> (((y <_ z /\ y <_ w) -> (normh` ((f` z) -h (f` w))) < x) <-> ((y <_ z /\ y <_ w) -> ((f` z) e. H~ /\ (f` w) e. H~ /\ ((f` z)D(f` w)) < x))))
17	16	ralbidva 1662	. . . . . . . . . . . 12 |- ((f:NN-->H~ /\ z e. NN) -> (A.w e. NN ((y <_ z /\ y <_ w) -> (normh` ((f` z) -h (f` w))) < x) <-> A.w e. NN ((y <_ z /\ y <_ w) -> ((f` z) e. H~ /\ (f` w) e. H~ /\ ((f` z)D(f` w)) < x))))
18	17	ralbidva 1662	. . . . . . . . . . 11 |- (f:NN-->H~ -> (A.z e. NN A.w e. NN ((y <_ z /\ y <_ w) -> (normh` ((f` z) -h (f` w))) < x) <-> A.z e. NN A.w e. NN ((y <_ z /\ y <_ w) -> ((f` z) e. H~ /\ (f` w) e. H~ /\ ((f` z)D(f` w)) < x))))
19	18	rexbidv 1667	. . . . . . . . . 10 |- (f:NN-->H~ -> (E.y e. NN A.z e. NN A.w e. NN ((y <_ z /\ y <_ w) -> (normh` ((f` z) -h (f` w))) < x) <-> E.y e. NN A.z e. NN A.w e. NN ((y <_ z /\ y <_ w) -> ((f` z) e. H~ /\ (f` w) e. H~ /\ ((f` z)D(f` w)) < x))))
20		1z 6161	. . . . . . . . . . 11 |- 1 e. ZZ
21		nnuz 6440	. . . . . . . . . . 11 |- NN = (ZZ>` 1)
22	20, 21	cau5 6919	. . . . . . . . . 10 |- (E.y e. ZZ A.z e. ZZ A.w e. ZZ ((y <_ z /\ y <_ w) -> ((f` z) e. H~ /\ (f` w) e. H~ /\ ((f` z)D(f` w)) < x)) <-> E.y e. NN A.z e. NN A.w e. NN ((y <_ z /\ y <_ w) -> ((f` z) e. H~ /\ (f` w) e. H~ /\ ((f` z)D(f` w)) < x)))
23	19, 22	syl6rbbr 541	. . . . . . . . 9 |- (f:NN-->H~ -> (E.y e. ZZ A.z e. ZZ A.w e. ZZ ((y <_ z /\ y <_ w) -> ((f` z) e. H~ /\ (f` w) e. H~ /\ ((f` z)D(f` w)) < x)) <-> E.y e. NN A.z e. NN A.w e. NN ((y <_ z /\ y <_ w) -> (normh` ((f` z) -h (f` w))) < x)))
24	23	imbi2d 614	. . . . . . . 8 |- (f:NN-->H~ -> ((0 < x -> E.y e. ZZ A.z e. ZZ A.w e. ZZ ((y <_ z /\ y <_ w) -> ((f` z) e. H~ /\ (f` w) e. H~ /\ ((f` z)D(f` w)) < x))) <-> (0 < x -> E.y e. NN A.z e. NN A.w e. NN ((y <_ z /\ y <_ w) -> (normh` ((f` z) -h (f` w))) < x))))
25	24	ralbidv 1666	. . . . . . 7 |- (f:NN-->H~ -> (A.x e. RR (0 < x -> E.y e. ZZ A.z e. ZZ A.w e. ZZ ((y <_ z /\ y <_ w) -> ((f` z) e. H~ /\ (f` w) e. H~ /\ ((f` z)D(f` w)) < x))) <-> A.x e. RR (0 < x -> E.y e. NN A.z e. NN A.w e. NN ((y <_ z /\ y <_ w) -> (normh` ((f` z) -h (f` w))) < x))))
26		fssxp 3643	. . . . . . . . 9 |- (f:NN-->H~ -> f (_ (NN X. H~))
27		nnsscn 5930	. . . . . . . . . . 11 |- NN (_ CC
28		ssid 2083	. . . . . . . . . . 11 |- H~ (_ H~
29		ssxp 3262	. . . . . . . . . . 11 |- ((NN (_ CC /\ H~ (_ H~) -> (NN X. H~) (_ (CC X. H~))
30	27, 28, 29	mp2an 699	. . . . . . . . . 10 |- (NN X. H~) (_ (CC X. H~)
31		sstr 2075	. . . . . . . . . 10 |- ((f (_ (NN X. H~) /\ (NN X. H~) (_ (CC X. H~)) -> f (_ (CC X. H~))
32	30, 31	mpan2 698	. . . . . . . . 9 |- (f (_ (NN X. H~) -> f (_ (CC X. H~))
33	26, 32	syl 10	. . . . . . . 8 |- (f:NN-->H~ -> f (_ (CC X. H~))
34	33	biantrurd 729	. . . . . . 7 |- (f:NN-->H~ -> (A.x e. RR (0 < x -> E.y e. ZZ A.z e. ZZ A.w e. ZZ ((y <_ z /\ y <_ w) -> ((f` z) e. H~ /\ (f` w) e. H~ /\ ((f` z)D(f` w)) < x))) <-> (f (_ (CC X. H~) /\ A.x e. RR (0 < x -> E.y e. ZZ A.z e. ZZ A.w e. ZZ ((y <_ z /\ y <_ w) -> ((f` z) e. H~ /\ (f` w) e. H~ /\ ((f` z)D(f` w)) < x))))))
35	25, 34	bitr3d 532	. . . . . 6 |- (f:NN-->H~ -> (A.x e. RR (0 < x -> E.y e. NN A.z e. NN A.w e. NN ((y <_ z /\ y <_ w) -> (normh` ((f` z) -h (f` w))) < x)) <-> (f (_ (CC X. H~) /\ A.x e. RR (0 < x -> E.y e. ZZ A.z e. ZZ A.w e. ZZ ((y <_ z /\ y <_ w) -> ((f` z) e. H~ /\ (f` w) e. H~ /\ ((f` z)D(f` w)) < x))))))
36	35	pm5.32i 647	. . . . 5 |- ((f:NN-->H~ /\ A.x e. RR (0 < x -> E.y e. NN A.z e. NN A.w e. NN ((y <_ z /\ y <_ w) -> (normh` ((f` z) -h (f` w))) < x))) <-> (f:NN-->H~ /\ (f (_ (CC X. H~) /\ A.x e. RR (0 < x -> E.y e. ZZ A.z e. ZZ A.w e. ZZ ((<