Theorem h2hcau 8849

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 8848	. . . . . . . . . . . . . . . . . 18 |- (((f` z) e. H~ /\ (f` w) e. H~) -> ((f` z)D(f` w)) = (normh` ((f` z) -h (f` w))))
6	5	breq1d 2629	. . . . . . . . . . . . . . . . 17 |- (((f` z) e. H~ /\ (f` w) e. H~) -> (((f` z)D(f` w)) < x <-> (normh` ((f` z) -h (f` w))) < x))
7		ibar 643	. . . . . . . . . . . . . . . . 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 530	. . . . . . . . . . . . . . . 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 777	. . . . . . . . . . . . . . . 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 538	. . . . . . . . . . . . . . 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 3814	. . . . . . . . . . . . . . . 16 |- ((f:NN-->H~ /\ z e. NN) -> (f` z) e. H~)
12	11	adantr 389	. . . . . . . . . . . . . . 15 |- (((f:NN-->H~ /\ z e. NN) /\ w e. NN) -> (f` z) e. H~)
13		ffvelrn 3814	. . . . . . . . . . . . . . . 16 |- ((f:NN-->H~ /\ w e. NN) -> (f` w) e. H~)
14	13	adantlr 393	. . . . . . . . . . . . . . 15 |- (((f:NN-->H~ /\ z e. NN) /\ w e. NN) -> (f` w) e. H~)
15	10, 12, 14	sylanc 471	. . . . . . . . . . . . . 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 612	. . . . . . . . . . . . 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 1659	. . . . . . . . . . . 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 1659	. . . . . . . . . . 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 1664	. . . . . . . . . 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 6159	. . . . . . . . . . 11 |- 1 e. ZZ
21		nnuz 6439	. . . . . . . . . . 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 539	. . . . . . . . 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 612	. . . . . . . 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 1663	. . . . . . 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 3637	. . . . . . . . 9 |- (f:NN-->H~ -> f (_ (NN X. H~))
27		nnsscn 5928	. . . . . . . . . . 11 |- NN (_ CC
28		ssid 2080	. . . . . . . . . . 11 |- H~ (_ H~
29		ssxp 3256	. . . . . . . . . . 11 |- ((NN (_ CC /\ H~ (_ H~) -> (NN X. H~) (_ (CC X. H~))
30	27, 28, 29	mp2an 697	. . . . . . . . . 10 |- (NN X. H~) (_ (CC X. H~)
31		sstr 2072	. . . . . . . . . 10 |- ((f (_ (NN X. H~) /\ (NN X. H~) (_ (CC X. H~)) -> f (_ (CC X. H~))
32	30, 31	mpan2 696	. . . . . . . . 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 727	. . . . . . 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 530	. . . . . 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 645	. . . . 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 (