Metamath Proof Explorer


Theorem hlim2

Description: The limit of a sequence on a Hilbert space. (Contributed by NM, 16-Aug-1999) (Revised by Mario Carneiro, 14-May-2014) (New usage is discouraged.)

Ref Expression
Assertion hlim2 F : A F v A x + y z y norm F z - A < x

Proof

Step Hyp Ref Expression
1 breq2 w = A F v w F v A
2 oveq2 w = A F z - w = F z - A
3 2 fveq2d w = A norm F z - w = norm F z - A
4 3 breq1d w = A norm F z - w < x norm F z - A < x
5 4 rexralbidv w = A y z y norm F z - w < x y z y norm F z - A < x
6 5 ralbidv w = A x + y z y norm F z - w < x x + y z y norm F z - A < x
7 1 6 bibi12d w = A F v w x + y z y norm F z - w < x F v A x + y z y norm F z - A < x
8 7 imbi2d w = A F : F v w x + y z y norm F z - w < x F : F v A x + y z y norm F z - A < x
9 vex w V
10 9 hlimi F v w F : w x + y z y norm F z - w < x
11 10 baib F : w F v w x + y z y norm F z - w < x
12 11 expcom w F : F v w x + y z y norm F z - w < x
13 8 12 vtoclga A F : F v A x + y z y norm F z - A < x
14 13 impcom F : A F v A x + y z y norm F z - A < x