Theorem h2hlm 8850

Description: The limit sequences of Hilbert space.

Hypotheses

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

Assertion

Ref	Expression
h2hlm	|- ~~>v = ((~~>m` D) |` (H~ ^m NN))

Proof of Theorem h2hlm

Step	Hyp	Ref	Expression
1		h2hl.1	. . . . . . . . . . . . . . . . . . . 20 |- U = <.<. +h , .h >., normh>.
2		h2hl.2	. . . . . . . . . . . . . . . . . . . 20 |- U e. NrmCVec
3		h2hl.4	. . . . . . . . . . . . . . . . . . . 20 |- H~ = (Base` U)
4		h2hl.3	. . . . . . . . . . . . . . . . . . . 20 |- D = (IndMet` U)
5	1, 2, 3, 4	h2hmetdval 8848	. . . . . . . . . . . . . . . . . . 19 |- (((f` z) e. H~ /\ w e. H~) -> ((f` z)Dw) = (normh` ((f` z) -h w)))
6	5	breq1d 2629	. . . . . . . . . . . . . . . . . 18 |- (((f` z) e. H~ /\ w e. H~) -> (((f` z)Dw) < x <-> (normh` ((f` z) -h w)) < x))
7		ibar 643	. . . . . . . . . . . . . . . . . . 19 |- ((f` z) e. H~ -> (((f` z)Dw) < x <-> ((f` z) e. H~ /\ ((f` z)Dw) < x)))
8	7	adantr 389	. . . . . . . . . . . . . . . . . 18 |- (((f` z) e. H~ /\ w e. H~) -> (((f` z)Dw) < x <-> ((f` z) e. H~ /\ ((f` z)Dw) < x)))
9	6, 8	bitr3d 530	. . . . . . . . . . . . . . . . 17 |- (((f` z) e. H~ /\ w e. H~) -> ((normh` ((f` z) -h w)) < x <-> ((f` z) e. H~ /\ ((f` z)Dw) < x)))
10		ffvelrn 3814	. . . . . . . . . . . . . . . . 17 |- ((f:NN-->H~ /\ z e. NN) -> (f` z) e. H~)
11	9, 10	sylan 448	. . . . . . . . . . . . . . . 16 |- (((f:NN-->H~ /\ z e. NN) /\ w e. H~) -> ((normh` ((f` z) -h w)) < x <-> ((f` z) e. H~ /\ ((f` z)Dw) < x)))
12	11	an1rs 489	. . . . . . . . . . . . . . 15 |- (((f:NN-->H~ /\ w e. H~) /\ z e. NN) -> ((normh` ((f` z) -h w)) < x <-> ((f` z) e. H~ /\ ((f` z)Dw) < x)))
13	12	imbi2d 612	. . . . . . . . . . . . . 14 |- (((f:NN-->H~ /\ w e. H~) /\ z e. NN) -> ((y <_ z -> (normh` ((f` z) -h w)) < x) <-> (y <_ z -> ((f` z) e. H~ /\ ((f` z)Dw) < x))))
14	13	ralbidva 1659	. . . . . . . . . . . . 13 |- ((f:NN-->H~ /\ w e. H~) -> (A.z e. NN (y <_ z -> (normh` ((f` z) -h w)) < x) <-> A.z e. NN (y <_ z -> ((f` z) e. H~ /\ ((f` z)Dw) < x))))
15	14	rexbidv 1664	. . . . . . . . . . . 12 |- ((f:NN-->H~ /\ w e. H~) -> (E.y e. NN A.z e. NN (y <_ z -> (normh` ((f` z) -h w)) < x) <-> E.y e. NN A.z e. NN (y <_ z -> ((f` z) e. H~ /\ ((f` z)Dw) < x))))
16		1z 6159	. . . . . . . . . . . . 13 |- 1 e. ZZ
17		nnuz 6439	. . . . . . . . . . . . . 14 |- NN = (ZZ>` 1)
18	17	eqimss2i 2112	. . . . . . . . . . . . 13 |- (ZZ>` 1) (_ NN
19		nnssz 6151	. . . . . . . . . . . . 13 |- NN (_ ZZ
20	16, 18, 19, 16, 18, 19	cvg3 6923	. . . . . . . . . . . 12 |- (E.y e. ZZ A.z e. ZZ (y <_ z -> ((f` z) e. H~ /\ ((f` z)Dw) < x)) <-> E.y e. NN A.z e. NN (y <_ z -> ((f` z) e. H~ /\ ((f` z)Dw) < x)))
21	15, 20	syl6bbr 538	. . . . . . . . . . 11 |- ((f:NN-->H~ /\ w e. H~) -> (E.y e. NN A.z e. NN (y <_ z -> (normh` ((f` z) -h w)) < x) <-> E.y e. ZZ A.z e. ZZ (y <_ z -> ((f` z) e. H~ /\ ((f` z)Dw) < x))))
22	21	imbi2d 612	. . . . . . . . . 10 |- ((f:NN-->H~ /\ w e. H~) -> ((0 < x -> E.y e. NN A.z e. NN (y <_ z -> (normh` ((f` z) -h w)) < x)) <-> (0 < x -> E.y e. ZZ A.z e. ZZ (y <_ z -> ((f` z) e. H~ /\ ((f` z)Dw) < x)))))
23	22	ralbidv 1663	. . . . . . . . 9 |- ((f:NN-->H~ /\ w e. H~) -> (A.x e. RR (0 < x -> E.y e. NN A.z e. NN (y <_ z -> (normh` ((f` z) -h w)) < x)) <-> A.x e. RR (0 < x -> E.y e. ZZ A.z e. ZZ (y <_ z -> ((f` z) e. H~ /\ ((f` z)Dw) < x)))))
24	23	pm5.32da 649	. . . . . . . 8 |- (f:NN-->H~ -> ((w e. H~ /\ A.x e. RR (0 < x -> E.y e. NN A.z e. NN (y <_ z -> (normh` ((f` z) -h w)) < x))) <-> (w e. H~ /\ A.x e. RR (0 < x -> E.y e. ZZ A.z e. ZZ (y <_ z -> ((f` z) e. H~ /\ ((f` z)Dw) < x))))))
25		fssxp 3637	. . . . . . . . . 10 |- (f:NN-->H~ -> f (_ (NN X. H~))
26		nnsscn 5928	. . . . . . . . . . . 12 |- NN (_ CC
27		ssid 2080	. . . . . . . . . . . 12 |- H~ (_ H~
28		ssxp 3256	. . . . . . . . . . . 12 |- ((NN (_ CC /\ H~ (_ H~) -> (NN X. H~) (_ (CC X. H~))
29	26, 27, 28	mp2an 697	. . . . . . . . . . 11 |- (NN X. H~) (_ (CC X. H~)
30		sstr 2072	. . . . . . . . . . 11 |- ((f (_ (NN X. H~) /\ (NN X. H~) (_ (CC X. H~)) -> f (_ (CC X. H~))
31	29, 30	mpan2 696	. . . . . . . . . 10 |- (f (_ (NN X. H~) -> f (_ (CC X. H~))
32	25, 31	syl 10	. . . . . . . . 9 |- (f:NN-->H~ -> f (_ (CC X. H~))
33	32	biantrurd 727	. . . . . . . 8 |- (f:NN-->H~ -> ((w e. H~ /\ A.x e. RR (0 < x -> E.y e. ZZ A.z e. ZZ (y <_ z -> ((f` z) e. H~ /\ ((f` z)Dw) < x)))) <-> (f (_ (CC X. H~) /\ (w e. H~ /\ A.x e. RR (0 < x -> E.y e. ZZ A.z e. ZZ (y <_ z -> ((f` z) e. H~ /\ ((f` z)Dw) < x)))))))
34	24, 33	bitrd 528	. . . . . . 7 |- (f:NN-->H~ -> ((w e. H~ /\ A.x e. RR (0 < x -> E.y e. NN A.z e. NN (y <_ z -> (normh` ((f` z) -h w)) < x))) <-> (f (_ (CC X. H~) /\ (w e. H~ /\ A.x e. RR (0 < x -> E.y e. ZZ A.z e. ZZ (y <_ z -> ((f` z) e. H~ /\ ((f` z)Dw) < x)))))))
35		3anass 779	. . . . . . 7 |- ((f (_ (CC X. H~) /\ w e. H~ /\ A.x e. RR (0 < x -> E.y e. ZZ A.z e. ZZ (y <_ z -> ((f` z) e. H~ /\ ((f` z)Dw) < x)))) <-> (f (_ (CC X. H~) /\ (w e. H~ /\ A.x e. RR (0 < x -> E.y e. ZZ A.z e. ZZ (y <_ z -> ((f` z) e. H~ /\ ((f` z)Dw) < x))))))
36	34, 35	syl6bbr 538	. . . . . 6 |- (f:NN-->H~ -> ((w e. H~ /\ A.x e. RR (0 < x -> E.y e. NN A.z e. NN (y <_ z -> (normh` ((f` z) -h w)) < x))) <-> (f (_ (CC X. H~) /\ w e. H~ /\ A.x e. RR (0 < x -> E.y e. ZZ A.z e. ZZ (y <_ z -> ((f` z) e. H~ /\ ((f` z)Dw) < x))))))
37	36	pm5.32i 645	. . . . 5 |- ((f:NN-->H~ /\ (w e. H~ /\ A.x e. RR (0 < x -> E.y e. NN A.z e. NN (y <_ z -> (normh` ((f` z) -h w)) < x)))) <-> (f:NN-->H~ /\ (f (_ (CC X. H~) /\ w e. H~ /\ A.x e. RR (0 < x -> E.y e. ZZ A.z e. ZZ (y <_ z -> ((f` z) e. H~ /\ ((f` z)Dw) < x))))))
38		anass 439	. . . . 5 |- (((f:NN-->H~ /\ w e. H~) /\ A.x e. RR (0 < x -> E.y e. NN A.z e. NN (y <_ z -> (normh` ((f` z) -h w)) < x))) <-> (f:NN-->H~ /\ (w e. H~ /\ A.x e. RR (0 < x -> E.y e. NN A.z e. NN (y <_ z -> (normh` ((f` z) -h w)) < x)))))
39	3	hlex 8600	. . . . . . 7 |- H~ e. V
40		nnex 5933	. . . . . . 7 |- NN e. V
41	39, 40	elmap 4334	. . . . . 6 |- (f e. (H~ ^m NN) <-> f:NN-->H~)
42	41	anbi1i 481	. . . . 5 |- ((f e. (H~ ^m NN) /\ (f (_ (CC X. H~) /\ w e. H~ /\ A.x e. RR (0 < x -> E.y e. ZZ A.z