Theorem hlimunii 5143

Description: A Hilbert space sequence converges to at most one limit.

Hypotheses

Ref	Expression
hlimuni.1	|- A e. V
hlimuni.2	|- B e. V
hlimuni.3	|- F e. V
hlimunii.3	|- (F ~~>v A /\ F ~~>v B)

Assertion

Ref	Expression
hlimunii	|- A = B

Proof of Theorem hlimunii

Step	Hyp	Ref	Expression
1		nn2get 4438	. . . . 5 |- ((y e. NN /\ w e. NN) -> E.z e. NN (y <_ z /\ w <_ z))
2	1	rgen2 1248	. . . 4 |- A.y e. NN A.w e. NN E.z e. NN (y <_ z /\ w <_ z)
3		hlimunii.3	. . . . . . . . . 10 |- (F ~~>v A /\ F ~~>v B)
4	3	pm3.26i 257	. . . . . . . . 9 |- F ~~>v A
5		hlimuni.3	. . . . . . . . . 10 |- F e. V
6		hlimuni.1	. . . . . . . . . 10 |- A e. V
7	5, 6	hlimvec 5110	. . . . . . . . 9 |- (F ~~>v A -> A e. H~)
8	4, 7	ax-mp 6	. . . . . . . 8 |- A e. H~
9	3	pm3.27i 261	. . . . . . . . 9 |- F ~~>v B
10		hlimuni.2	. . . . . . . . . 10 |- B e. V
11	5, 10	hlimvec 5110	. . . . . . . . 9 |- (F ~~>v B -> B e. H~)
12	9, 11	ax-mp 6	. . . . . . . 8 |- B e. H~
13	8, 12	hvsubcl 5002	. . . . . . 7 |- (A -v B) e. H~
14	13	normcl 5081	. . . . . 6 |- (norm` (A -v B)) e. RR
15		2re 4470	. . . . . 6 |- 2 e. RR
16		2pos 4479	. . . . . 6 |- 0 < 2
17	14, 15, 16	divgt0lem 4389	. . . . 5 |- (0 < (norm` (A -v B)) -> 0 < ((norm` (A -v B)) / 2))
18	5, 6	hlimconv 5111	. . . . . . . 8 |- (F ~~>v A -> A.x e. RR (0 < x -> E.y e. NN A.z e. NN (y <_ z -> (norm` ((F` z) -v A)) < x)))
19	4, 18	ax-mp 6	. . . . . . 7 |- A.x e. RR (0 < x -> E.y e. NN A.z e. NN (y <_ z -> (norm` ((F` z) -v A)) < x))
20	15, 16	gt0ne0i 4345	. . . . . . . 8 |- 2 =/= 0
21	14, 15, 20	redivcl 4274	. . . . . . 7 |- ((norm` (A -v B)) / 2) e. RR
22		breq2 2066	. . . . . . . . 9 |- (x = ((norm` (A -v B)) / 2) -> (0 < x <-> 0 < ((norm` (A -v B)) / 2)))
23		breq2 2066	. . . . . . . . . . . 12 |- (x = ((norm` (A -v B)) / 2) -> ((norm` ((F` z) -v A)) < x <-> (norm` ((F` z) -v A)) < ((norm` (A -v B)) / 2)))
24	23	imbi2d 464	. . . . . . . . . . 11 |- (x = ((norm` (A -v B)) / 2) -> ((y <_ z -> (norm` ((F` z) -v A)) < x) <-> (y <_ z -> (norm` ((F` z) -v A)) < ((norm` (A -v B)) / 2))))
25	24	biraldv 1219	. . . . . . . . . 10 |- (x = ((norm` (A -v B)) / 2) -> (A.z e. NN (y <_ z -> (norm` ((F` z) -v A)) < x) <-> A.z e. NN (y <_ z -> (norm` ((F` z) -v A)) < ((norm` (A -v B)) / 2))))
26	25	birexdv 1220	. . . . . . . . 9 |- (x = ((norm` (A -v B)) / 2) -> (E.y e. NN A.z e. NN (y <_ z -> (norm` ((F` z) -v A)) < x) <-> E.y e. NN A.z e. NN (y <_ z -> (norm` ((F` z) -v A)) < ((norm` (A -v B)) / 2))))
27	22, 26	imbi12d 474	. . . . . . . 8 |- (x = ((norm` (A -v B)) / 2) -> ((0 < x -> E.y e. NN A.z e. NN (y <_ z -> (norm` ((F` z) -v A)) < x)) <-> (0 < ((norm` (A -v B)) / 2) -> E.y e. NN A.z e. NN (y <_ z -> (norm` ((F` z) -v A)) < ((norm` (A -v B)) / 2)))))
28	27	rcla4v 1402	. . . . . . 7 |- (A.x e. RR (0 < x -> E.y e. NN A.z e. NN (y <_ z -> (norm` ((F` z) -v A)) < x)) -> (((norm` (A -v B)) / 2) e. RR -> (0 < ((norm` (A -v B)) / 2) -> E.y e. NN A.z e. NN (y <_ z -> (norm` ((F` z) -v A)) < ((norm` (A -v B)) / 2)))))
29	19, 21, 28	mp2 43	. . . . . 6 |- (0 < ((norm` (A -v B)) / 2) -> E.y e. NN A.z e. NN (y <_ z -> (norm` ((F` z) -v A)) < ((norm` (A -v B)) / 2)))
30	5, 10	hlimconv 5111	. . . . . . . 8 |- (F ~~>v B -> A.x e. RR (0 < x -> E.w e. NN A.z e. NN (w <_ z -> (norm` ((F` z) -v B)) < x)))
31	9, 30	ax-mp 6	. . . . . . 7 |- A.x e. RR (0 < x -> E.w e. NN A.z e. NN (w <_ z -> (norm` ((F` z) -v B)) < x))
32		breq2 2066	. . . . . . . . . . . 12 |- (x = ((norm` (A -v B)) / 2) -> ((norm` ((F` z) -v B)) < x <-> (norm` ((F` z) -v B)) < ((norm` (A -v B)) / 2)))
33	32	imbi2d 464	. . . . . . . . . . 11 |- (x = ((norm` (A -v B)) / 2) -> ((w <_ z -> (norm` ((F` z) -v B)) < x) <-> (w <_ z -> (norm` ((F` z) -v B)) < ((norm` (A -v B)) / 2))))
34	33	biraldv 1219	. . . . . . . . . 10 |- (x = ((norm` (A -v B)) / 2) -> (A.z e. NN (w <_ z -> (norm` ((F` z) -v B)) < x) <-> A.z e. NN (w <_ z -> (norm` ((F` z) -v B)) < ((norm` (A -v B)) / 2))))
35	34	birexdv 1220	. . . . . . . . 9 |- (x = ((norm` (A -v B)) / 2) -> (E.w e. NN A.z e. NN (w <_ z -> (norm` ((F` z) -v B)) < x) <-> E.w e. NN A.z e. NN (w <_ z -> (norm` ((F` z) -v B)) < ((norm` (A -v B)) / 2))))
36	22, 35	imbi12d 474	. . . . . . . 8 |- (x = ((norm` (A -v B)) / 2) -> ((0 < x -> E.w e. NN A.z e. NN (w <_ z -> (norm` ((F` z) -v B)) < x)) <-> (0 < ((norm` (A -v B)) / 2) -> E.w e. NN A.z e. NN (w <_ z -> (norm` ((F` z) -v B)) < ((norm` (A -v B)) / 2)))))
37	36	rcla4v 1402	. . . . . . 7 |- (A.x e. RR (0 < x -> E.w e. NN A.z e. NN (w <_ z -> (norm` ((F` z) -v B)) < x)) -> (((norm` (A -v B)) / 2) e. RR -> (0 < ((norm` (A -v B)) / 2) -> E.w e. NN A.z e. NN (w <_ z -> (norm` ((F` z) -v B)) < ((norm` (A -v B)) / 2)))))
38	31, 21, 37	mp2 43	. . . . . 6 |- (0 < ((norm` (A -v B)) / 2) -> E.w e. NN A.z e. NN (w <_ z -> (norm` ((F` z) -v B)) < ((norm` (A -v B)) / 2)))
39	29, 38	jca 236	. . . . 5 |- (0 < ((norm` (A -v B)) / 2) -> (E.y e. NN A.z e. NN (y <_ z -> (norm` ((F` z) -v A)) < ((norm` (A -v B)) / 2)) /\ E.w e. NN A.z e. NN (w <_ z -> (norm` ((F` z) -v B)) < ((norm` (A -v B)) / 2))))
40		r19.26 1289	. . . . . . . . 9 |- (A.z e. NN ((y <_ z -> (norm` ((F` z) -v A)) < ((norm` (A -v B)) / 2)) /\ (w <_ z -> (norm` ((F` z) -v B)) < ((norm` (A -v B)) / 2))) <-> (A.z e. NN (y <_ z -> (norm` ((F` z) -v A)) < ((norm` (A -v B)) / 2)) /\ A.z e. NN (w <_ z -> (norm` ((F` z) -v B)) < ((norm` (A -v B)) / 2))))
41	14	ltnr 4338	. . . . . . . . . . . . 13 |- -. (norm` (A -v B)) < (norm` (A -v B))
42	5, 6	hlimseq 5109	. . . . . . . . . . . . . . . . . . 19 |- (F ~~>v A -> F:NN-->H~)
43	4, 42	ax-mp 6	. . . . . . . . . . . . . . . . . 18 |- F:NN-->H~
44		ffvrn 2890	. . . . . . . . . . . . . . . . . 18 |- ((F:NN-->H~ /\ z e. NN) -> (F` z) e. H~)
45	43, 44	mpan 518	. . . . . . . . . . . . . . . . 17 |- (z e. NN -> (F` z) e. H~)
46		normsubt 5091	. . . . . . . . . . . . . . . . . 18 |- (((F` z) e. H~ /\ A e. H~) -> (norm` ((F` z) -v A)) = (norm` (A -v (F` z))))
47	8, 46	mpan2 519	. . . . . . . . . . . . . . . . 17 |- ((F` z) e. H~ -> (norm` ((F` z) -v A)) = (norm` (A -v (F` z))))
48	45, 47	syl 12	. . . . . . . . . . . . . . . 16 |- (z e. NN -> (norm` ((F` z) -v A)) = (norm` (A -v (F` z))))
49	48	breq1d 2071	. . . . . . . . . . . . . . 15 |- (z e. NN -> (