Metamath Proof Explorer


Theorem chscllem2

Description: Lemma for chscl . (Contributed by Mario Carneiro, 19-May-2014) (New usage is discouraged.)

Ref Expression
Hypotheses chscl.1
|- ( ph -> A e. CH )
chscl.2
|- ( ph -> B e. CH )
chscl.3
|- ( ph -> B C_ ( _|_ ` A ) )
chscl.4
|- ( ph -> H : NN --> ( A +H B ) )
chscl.5
|- ( ph -> H ~~>v u )
chscl.6
|- F = ( n e. NN |-> ( ( projh ` A ) ` ( H ` n ) ) )
Assertion chscllem2
|- ( ph -> F e. dom ~~>v )

Proof

Step Hyp Ref Expression
1 chscl.1
 |-  ( ph -> A e. CH )
2 chscl.2
 |-  ( ph -> B e. CH )
3 chscl.3
 |-  ( ph -> B C_ ( _|_ ` A ) )
4 chscl.4
 |-  ( ph -> H : NN --> ( A +H B ) )
5 chscl.5
 |-  ( ph -> H ~~>v u )
6 chscl.6
 |-  F = ( n e. NN |-> ( ( projh ` A ) ` ( H ` n ) ) )
7 1 2 3 4 5 6 chscllem1
 |-  ( ph -> F : NN --> A )
8 chss
 |-  ( A e. CH -> A C_ ~H )
9 1 8 syl
 |-  ( ph -> A C_ ~H )
10 7 9 fssd
 |-  ( ph -> F : NN --> ~H )
11 hlimcaui
 |-  ( H ~~>v u -> H e. Cauchy )
12 5 11 syl
 |-  ( ph -> H e. Cauchy )
13 hcaucvg
 |-  ( ( H e. Cauchy /\ x e. RR+ ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( normh ` ( ( H ` j ) -h ( H ` k ) ) ) < x )
14 12 13 sylan
 |-  ( ( ph /\ x e. RR+ ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( normh ` ( ( H ` j ) -h ( H ` k ) ) ) < x )
15 eluznn
 |-  ( ( j e. NN /\ k e. ( ZZ>= ` j ) ) -> k e. NN )
16 15 adantll
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> k e. NN )
17 chsh
 |-  ( A e. CH -> A e. SH )
18 1 17 syl
 |-  ( ph -> A e. SH )
19 chsh
 |-  ( B e. CH -> B e. SH )
20 2 19 syl
 |-  ( ph -> B e. SH )
21 shscl
 |-  ( ( A e. SH /\ B e. SH ) -> ( A +H B ) e. SH )
22 18 20 21 syl2anc
 |-  ( ph -> ( A +H B ) e. SH )
23 shss
 |-  ( ( A +H B ) e. SH -> ( A +H B ) C_ ~H )
24 22 23 syl
 |-  ( ph -> ( A +H B ) C_ ~H )
25 24 adantr
 |-  ( ( ph /\ j e. NN ) -> ( A +H B ) C_ ~H )
26 4 ffvelrnda
 |-  ( ( ph /\ j e. NN ) -> ( H ` j ) e. ( A +H B ) )
27 25 26 sseldd
 |-  ( ( ph /\ j e. NN ) -> ( H ` j ) e. ~H )
28 27 adantrr
 |-  ( ( ph /\ ( j e. NN /\ k e. NN ) ) -> ( H ` j ) e. ~H )
29 4 24 fssd
 |-  ( ph -> H : NN --> ~H )
30 29 adantr
 |-  ( ( ph /\ ( j e. NN /\ k e. NN ) ) -> H : NN --> ~H )
31 simprr
 |-  ( ( ph /\ ( j e. NN /\ k e. NN ) ) -> k e. NN )
32 30 31 ffvelrnd
 |-  ( ( ph /\ ( j e. NN /\ k e. NN ) ) -> ( H ` k ) e. ~H )
33 hvsubcl
 |-  ( ( ( H ` j ) e. ~H /\ ( H ` k ) e. ~H ) -> ( ( H ` j ) -h ( H ` k ) ) e. ~H )
34 28 32 33 syl2anc
 |-  ( ( ph /\ ( j e. NN /\ k e. NN ) ) -> ( ( H ` j ) -h ( H ` k ) ) e. ~H )
35 9 adantr
 |-  ( ( ph /\ j e. NN ) -> A C_ ~H )
36 7 ffvelrnda
 |-  ( ( ph /\ j e. NN ) -> ( F ` j ) e. A )
37 35 36 sseldd
 |-  ( ( ph /\ j e. NN ) -> ( F ` j ) e. ~H )
38 37 adantrr
 |-  ( ( ph /\ ( j e. NN /\ k e. NN ) ) -> ( F ` j ) e. ~H )
39 9 adantr
 |-  ( ( ph /\ ( j e. NN /\ k e. NN ) ) -> A C_ ~H )
40 7 adantr
 |-  ( ( ph /\ ( j e. NN /\ k e. NN ) ) -> F : NN --> A )
41 40 31 ffvelrnd
 |-  ( ( ph /\ ( j e. NN /\ k e. NN ) ) -> ( F ` k ) e. A )
42 39 41 sseldd
 |-  ( ( ph /\ ( j e. NN /\ k e. NN ) ) -> ( F ` k ) e. ~H )
43 hvsubcl
 |-  ( ( ( F ` j ) e. ~H /\ ( F ` k ) e. ~H ) -> ( ( F ` j ) -h ( F ` k ) ) e. ~H )
44 38 42 43 syl2anc
 |-  ( ( ph /\ ( j e. NN /\ k e. NN ) ) -> ( ( F ` j ) -h ( F ` k ) ) e. ~H )
45 hvsubcl
 |-  ( ( ( ( H ` j ) -h ( H ` k ) ) e. ~H /\ ( ( F ` j ) -h ( F ` k ) ) e. ~H ) -> ( ( ( H ` j ) -h ( H ` k ) ) -h ( ( F ` j ) -h ( F ` k ) ) ) e. ~H )
46 34 44 45 syl2anc
 |-  ( ( ph /\ ( j e. NN /\ k e. NN ) ) -> ( ( ( H ` j ) -h ( H ` k ) ) -h ( ( F ` j ) -h ( F ` k ) ) ) e. ~H )
47 normcl
 |-  ( ( ( ( H ` j ) -h ( H ` k ) ) -h ( ( F ` j ) -h ( F ` k ) ) ) e. ~H -> ( normh ` ( ( ( H ` j ) -h ( H ` k ) ) -h ( ( F ` j ) -h ( F ` k ) ) ) ) e. RR )
48 46 47 syl
 |-  ( ( ph /\ ( j e. NN /\ k e. NN ) ) -> ( normh ` ( ( ( H ` j ) -h ( H ` k ) ) -h ( ( F ` j ) -h ( F ` k ) ) ) ) e. RR )
49 48 sqge0d
 |-  ( ( ph /\ ( j e. NN /\ k e. NN ) ) -> 0 <_ ( ( normh ` ( ( ( H ` j ) -h ( H ` k ) ) -h ( ( F ` j ) -h ( F ` k ) ) ) ) ^ 2 ) )
50 normcl
 |-  ( ( ( F ` j ) -h ( F ` k ) ) e. ~H -> ( normh ` ( ( F ` j ) -h ( F ` k ) ) ) e. RR )
51 44 50 syl
 |-  ( ( ph /\ ( j e. NN /\ k e. NN ) ) -> ( normh ` ( ( F ` j ) -h ( F ` k ) ) ) e. RR )
52 51 resqcld
 |-  ( ( ph /\ ( j e. NN /\ k e. NN ) ) -> ( ( normh ` ( ( F ` j ) -h ( F ` k ) ) ) ^ 2 ) e. RR )
53 48 resqcld
 |-  ( ( ph /\ ( j e. NN /\ k e. NN ) ) -> ( ( normh ` ( ( ( H ` j ) -h ( H ` k ) ) -h ( ( F ` j ) -h ( F ` k ) ) ) ) ^ 2 ) e. RR )
54 52 53 addge01d
 |-  ( ( ph /\ ( j e. NN /\ k e. NN ) ) -> ( 0 <_ ( ( normh ` ( ( ( H ` j ) -h ( H ` k ) ) -h ( ( F ` j ) -h ( F ` k ) ) ) ) ^ 2 ) <-> ( ( normh ` ( ( F ` j ) -h ( F ` k ) ) ) ^ 2 ) <_ ( ( ( normh ` ( ( F ` j ) -h ( F ` k ) ) ) ^ 2 ) + ( ( normh ` ( ( ( H ` j ) -h ( H ` k ) ) -h ( ( F ` j ) -h ( F ` k ) ) ) ) ^ 2 ) ) ) )
55 49 54 mpbid
 |-  ( ( ph /\ ( j e. NN /\ k e. NN ) ) -> ( ( normh ` ( ( F ` j ) -h ( F ` k ) ) ) ^ 2 ) <_ ( ( ( normh ` ( ( F ` j ) -h ( F ` k ) ) ) ^ 2 ) + ( ( normh ` ( ( ( H ` j ) -h ( H ` k ) ) -h ( ( F ` j ) -h ( F ` k ) ) ) ) ^ 2 ) ) )
56 18 adantr
 |-  ( ( ph /\ ( j e. NN /\ k e. NN ) ) -> A e. SH )
57 36 adantrr
 |-  ( ( ph /\ ( j e. NN /\ k e. NN ) ) -> ( F ` j ) e. A )
58 shsubcl
 |-  ( ( A e. SH /\ ( F ` j ) e. A /\ ( F ` k ) e. A ) -> ( ( F ` j ) -h ( F ` k ) ) e. A )
59 56 57 41 58 syl3anc
 |-  ( ( ph /\ ( j e. NN /\ k e. NN ) ) -> ( ( F ` j ) -h ( F ` k ) ) e. A )
60 hvsubsub4
 |-  ( ( ( ( H ` j ) e. ~H /\ ( H ` k ) e. ~H ) /\ ( ( F ` j ) e. ~H /\ ( F ` k ) e. ~H ) ) -> ( ( ( H ` j ) -h ( H ` k ) ) -h ( ( F ` j ) -h ( F ` k ) ) ) = ( ( ( H ` j ) -h ( F ` j ) ) -h ( ( H ` k ) -h ( F ` k ) ) ) )
61 28 32 38 42 60 syl22anc
 |-  ( ( ph /\ ( j e. NN /\ k e. NN ) ) -> ( ( ( H ` j ) -h ( H ` k ) ) -h ( ( F ` j ) -h ( F ` k ) ) ) = ( ( ( H ` j ) -h ( F ` j ) ) -h ( ( H ` k ) -h ( F ` k ) ) ) )
62 ocsh
 |-  ( A C_ ~H -> ( _|_ ` A ) e. SH )
63 39 62 syl
 |-  ( ( ph /\ ( j e. NN /\ k e. NN ) ) -> ( _|_ ` A ) e. SH )
64 2fveq3
 |-  ( n = j -> ( ( projh ` A ) ` ( H ` n ) ) = ( ( projh ` A ) ` ( H ` j ) ) )
65 fvex
 |-  ( ( projh ` A ) ` ( H ` j ) ) e. _V
66 64 6 65 fvmpt
 |-  ( j e. NN -> ( F ` j ) = ( ( projh ` A ) ` ( H ` j ) ) )
67 66 eqcomd
 |-  ( j e. NN -> ( ( projh ` A ) ` ( H ` j ) ) = ( F ` j ) )
68 67 adantl
 |-  ( ( ph /\ j e. NN ) -> ( ( projh ` A ) ` ( H ` j ) ) = ( F ` j ) )
69 1 adantr
 |-  ( ( ph /\ j e. NN ) -> A e. CH )
70 9 62 syl
 |-  ( ph -> ( _|_ ` A ) e. SH )
71 shless
 |-  ( ( ( B e. SH /\ ( _|_ ` A ) e. SH /\ A e. SH ) /\ B C_ ( _|_ ` A ) ) -> ( B +H A ) C_ ( ( _|_ ` A ) +H A ) )
72 20 70 18 3 71 syl31anc
 |-  ( ph -> ( B +H A ) C_ ( ( _|_ ` A ) +H A ) )
73 shscom
 |-  ( ( A e. SH /\ B e. SH ) -> ( A +H B ) = ( B +H A ) )
74 18 20 73 syl2anc
 |-  ( ph -> ( A +H B ) = ( B +H A ) )
75 shscom
 |-  ( ( A e. SH /\ ( _|_ ` A ) e. SH ) -> ( A +H ( _|_ ` A ) ) = ( ( _|_ ` A ) +H A ) )
76 18 70 75 syl2anc
 |-  ( ph -> ( A +H ( _|_ ` A ) ) = ( ( _|_ ` A ) +H A ) )
77 72 74 76 3sstr4d
 |-  ( ph -> ( A +H B ) C_ ( A +H ( _|_ ` A ) ) )
78 77 adantr
 |-  ( ( ph /\ j e. NN ) -> ( A +H B ) C_ ( A +H ( _|_ ` A ) ) )
79 78 26 sseldd
 |-  ( ( ph /\ j e. NN ) -> ( H ` j ) e. ( A +H ( _|_ ` A ) ) )
80 pjpreeq
 |-  ( ( A e. CH /\ ( H ` j ) e. ( A +H ( _|_ ` A ) ) ) -> ( ( ( projh ` A ) ` ( H ` j ) ) = ( F ` j ) <-> ( ( F ` j ) e. A /\ E. x e. ( _|_ ` A ) ( H ` j ) = ( ( F ` j ) +h x ) ) ) )
81 69 79 80 syl2anc
 |-  ( ( ph /\ j e. NN ) -> ( ( ( projh ` A ) ` ( H ` j ) ) = ( F ` j ) <-> ( ( F ` j ) e. A /\ E. x e. ( _|_ ` A ) ( H ` j ) = ( ( F ` j ) +h x ) ) ) )
82 68 81 mpbid
 |-  ( ( ph /\ j e. NN ) -> ( ( F ` j ) e. A /\ E. x e. ( _|_ ` A ) ( H ` j ) = ( ( F ` j ) +h x ) ) )
83 82 simprd
 |-  ( ( ph /\ j e. NN ) -> E. x e. ( _|_ ` A ) ( H ` j ) = ( ( F ` j ) +h x ) )
84 27 adantr
 |-  ( ( ( ph /\ j e. NN ) /\ x e. ( _|_ ` A ) ) -> ( H ` j ) e. ~H )
85 37 adantr
 |-  ( ( ( ph /\ j e. NN ) /\ x e. ( _|_ ` A ) ) -> ( F ` j ) e. ~H )
86 shss
 |-  ( ( _|_ ` A ) e. SH -> ( _|_ ` A ) C_ ~H )
87 70 86 syl
 |-  ( ph -> ( _|_ ` A ) C_ ~H )
88 87 adantr
 |-  ( ( ph /\ j e. NN ) -> ( _|_ ` A ) C_ ~H )
89 88 sselda
 |-  ( ( ( ph /\ j e. NN ) /\ x e. ( _|_ ` A ) ) -> x e. ~H )
90 hvsubadd
 |-  ( ( ( H ` j ) e. ~H /\ ( F ` j ) e. ~H /\ x e. ~H ) -> ( ( ( H ` j ) -h ( F ` j ) ) = x <-> ( ( F ` j ) +h x ) = ( H ` j ) ) )
91 84 85 89 90 syl3anc
 |-  ( ( ( ph /\ j e. NN ) /\ x e. ( _|_ ` A ) ) -> ( ( ( H ` j ) -h ( F ` j ) ) = x <-> ( ( F ` j ) +h x ) = ( H ` j ) ) )
92 eqcom
 |-  ( x = ( ( H ` j ) -h ( F ` j ) ) <-> ( ( H ` j ) -h ( F ` j ) ) = x )
93 eqcom
 |-  ( ( H ` j ) = ( ( F ` j ) +h x ) <-> ( ( F ` j ) +h x ) = ( H ` j ) )
94 91 92 93 3bitr4g
 |-  ( ( ( ph /\ j e. NN ) /\ x e. ( _|_ ` A ) ) -> ( x = ( ( H ` j ) -h ( F ` j ) ) <-> ( H ` j ) = ( ( F ` j ) +h x ) ) )
95 94 rexbidva
 |-  ( ( ph /\ j e. NN ) -> ( E. x e. ( _|_ ` A ) x = ( ( H ` j ) -h ( F ` j ) ) <-> E. x e. ( _|_ ` A ) ( H ` j ) = ( ( F ` j ) +h x ) ) )
96 83 95 mpbird
 |-  ( ( ph /\ j e. NN ) -> E. x e. ( _|_ ` A ) x = ( ( H ` j ) -h ( F ` j ) ) )
97 risset
 |-  ( ( ( H ` j ) -h ( F ` j ) ) e. ( _|_ ` A ) <-> E. x e. ( _|_ ` A ) x = ( ( H ` j ) -h ( F ` j ) ) )
98 96 97 sylibr
 |-  ( ( ph /\ j e. NN ) -> ( ( H ` j ) -h ( F ` j ) ) e. ( _|_ ` A ) )
99 98 adantrr
 |-  ( ( ph /\ ( j e. NN /\ k e. NN ) ) -> ( ( H ` j ) -h ( F ` j ) ) e. ( _|_ ` A ) )
100 eleq1w
 |-  ( j = k -> ( j e. NN <-> k e. NN ) )
101 100 anbi2d
 |-  ( j = k -> ( ( ph /\ j e. NN ) <-> ( ph /\ k e. NN ) ) )
102 fveq2
 |-  ( j = k -> ( H ` j ) = ( H ` k ) )
103 fveq2
 |-  ( j = k -> ( F ` j ) = ( F ` k ) )
104 102 103 oveq12d
 |-  ( j = k -> ( ( H ` j ) -h ( F ` j ) ) = ( ( H ` k ) -h ( F ` k ) ) )
105 104 eleq1d
 |-  ( j = k -> ( ( ( H ` j ) -h ( F ` j ) ) e. ( _|_ ` A ) <-> ( ( H ` k ) -h ( F ` k ) ) e. ( _|_ ` A ) ) )
106 101 105 imbi12d
 |-  ( j = k -> ( ( ( ph /\ j e. NN ) -> ( ( H ` j ) -h ( F ` j ) ) e. ( _|_ ` A ) ) <-> ( ( ph /\ k e. NN ) -> ( ( H ` k ) -h ( F ` k ) ) e. ( _|_ ` A ) ) ) )
107 106 98 chvarvv
 |-  ( ( ph /\ k e. NN ) -> ( ( H ` k ) -h ( F ` k ) ) e. ( _|_ ` A ) )
108 107 adantrl
 |-  ( ( ph /\ ( j e. NN /\ k e. NN ) ) -> ( ( H ` k ) -h ( F ` k ) ) e. ( _|_ ` A ) )
109 shsubcl
 |-  ( ( ( _|_ ` A ) e. SH /\ ( ( H ` j ) -h ( F ` j ) ) e. ( _|_ ` A ) /\ ( ( H ` k ) -h ( F ` k ) ) e. ( _|_ ` A ) ) -> ( ( ( H ` j ) -h ( F ` j ) ) -h ( ( H ` k ) -h ( F ` k ) ) ) e. ( _|_ ` A ) )
110 63 99 108 109 syl3anc
 |-  ( ( ph /\ ( j e. NN /\ k e. NN ) ) -> ( ( ( H ` j ) -h ( F ` j ) ) -h ( ( H ` k ) -h ( F ` k ) ) ) e. ( _|_ ` A ) )
111 61 110 eqeltrd
 |-  ( ( ph /\ ( j e. NN /\ k e. NN ) ) -> ( ( ( H ` j ) -h ( H ` k ) ) -h ( ( F ` j ) -h ( F ` k ) ) ) e. ( _|_ ` A ) )
112 shocorth
 |-  ( A e. SH -> ( ( ( ( F ` j ) -h ( F ` k ) ) e. A /\ ( ( ( H ` j ) -h ( H ` k ) ) -h ( ( F ` j ) -h ( F ` k ) ) ) e. ( _|_ ` A ) ) -> ( ( ( F ` j ) -h ( F ` k ) ) .ih ( ( ( H ` j ) -h ( H ` k ) ) -h ( ( F ` j ) -h ( F ` k ) ) ) ) = 0 ) )
113 56 112 syl
 |-  ( ( ph /\ ( j e. NN /\ k e. NN ) ) -> ( ( ( ( F ` j ) -h ( F ` k ) ) e. A /\ ( ( ( H ` j ) -h ( H ` k ) ) -h ( ( F ` j ) -h ( F ` k ) ) ) e. ( _|_ ` A ) ) -> ( ( ( F ` j ) -h ( F ` k ) ) .ih ( ( ( H ` j ) -h ( H ` k ) ) -h ( ( F ` j ) -h ( F ` k ) ) ) ) = 0 ) )
114 59 111 113 mp2and
 |-  ( ( ph /\ ( j e. NN /\ k e. NN ) ) -> ( ( ( F ` j ) -h ( F ` k ) ) .ih ( ( ( H ` j ) -h ( H ` k ) ) -h ( ( F ` j ) -h ( F ` k ) ) ) ) = 0 )
115 normpyth
 |-  ( ( ( ( F ` j ) -h ( F ` k ) ) e. ~H /\ ( ( ( H ` j ) -h ( H ` k ) ) -h ( ( F ` j ) -h ( F ` k ) ) ) e. ~H ) -> ( ( ( ( F ` j ) -h ( F ` k ) ) .ih ( ( ( H ` j ) -h ( H ` k ) ) -h ( ( F ` j ) -h ( F ` k ) ) ) ) = 0 -> ( ( normh ` ( ( ( F ` j ) -h ( F ` k ) ) +h ( ( ( H ` j ) -h ( H ` k ) ) -h ( ( F ` j ) -h ( F ` k ) ) ) ) ) ^ 2 ) = ( ( ( normh ` ( ( F ` j ) -h ( F ` k ) ) ) ^ 2 ) + ( ( normh ` ( ( ( H ` j ) -h ( H ` k ) ) -h ( ( F ` j ) -h ( F ` k ) ) ) ) ^ 2 ) ) ) )
116 44 46 115 syl2anc
 |-  ( ( ph /\ ( j e. NN /\ k e. NN ) ) -> ( ( ( ( F ` j ) -h ( F ` k ) ) .ih ( ( ( H ` j ) -h ( H ` k ) ) -h ( ( F ` j ) -h ( F ` k ) ) ) ) = 0 -> ( ( normh ` ( ( ( F ` j ) -h ( F ` k ) ) +h ( ( ( H ` j ) -h ( H ` k ) ) -h ( ( F ` j ) -h ( F ` k ) ) ) ) ) ^ 2 ) = ( ( ( normh ` ( ( F ` j ) -h ( F ` k ) ) ) ^ 2 ) + ( ( normh ` ( ( ( H ` j ) -h ( H ` k ) ) -h ( ( F ` j ) -h ( F ` k ) ) ) ) ^ 2 ) ) ) )
117 114 116 mpd
 |-  ( ( ph /\ ( j e. NN /\ k e. NN ) ) -> ( ( normh ` ( ( ( F ` j ) -h ( F ` k ) ) +h ( ( ( H ` j ) -h ( H ` k ) ) -h ( ( F ` j ) -h ( F ` k ) ) ) ) ) ^ 2 ) = ( ( ( normh ` ( ( F ` j ) -h ( F ` k ) ) ) ^ 2 ) + ( ( normh ` ( ( ( H ` j ) -h ( H ` k ) ) -h ( ( F ` j ) -h ( F ` k ) ) ) ) ^ 2 ) ) )
118 hvpncan3
 |-  ( ( ( ( F ` j ) -h ( F ` k ) ) e. ~H /\ ( ( H ` j ) -h ( H ` k ) ) e. ~H ) -> ( ( ( F ` j ) -h ( F ` k ) ) +h ( ( ( H ` j ) -h ( H ` k ) ) -h ( ( F ` j ) -h ( F ` k ) ) ) ) = ( ( H ` j ) -h ( H ` k ) ) )
119 44 34 118 syl2anc
 |-  ( ( ph /\ ( j e. NN /\ k e. NN ) ) -> ( ( ( F ` j ) -h ( F ` k ) ) +h ( ( ( H ` j ) -h ( H ` k ) ) -h ( ( F ` j ) -h ( F ` k ) ) ) ) = ( ( H ` j ) -h ( H ` k ) ) )
120 119 fveq2d
 |-  ( ( ph /\ ( j e. NN /\ k e. NN ) ) -> ( normh ` ( ( ( F ` j ) -h ( F ` k ) ) +h ( ( ( H ` j ) -h ( H ` k ) ) -h ( ( F ` j ) -h ( F ` k ) ) ) ) ) = ( normh ` ( ( H ` j ) -h ( H ` k ) ) ) )
121 120 oveq1d
 |-  ( ( ph /\ ( j e. NN /\ k e. NN ) ) -> ( ( normh ` ( ( ( F ` j ) -h ( F ` k ) ) +h ( ( ( H ` j ) -h ( H ` k ) ) -h ( ( F ` j ) -h ( F ` k ) ) ) ) ) ^ 2 ) = ( ( normh ` ( ( H ` j ) -h ( H ` k ) ) ) ^ 2 ) )
122 117 121 eqtr3d
 |-  ( ( ph /\ ( j e. NN /\ k e. NN ) ) -> ( ( ( normh ` ( ( F ` j ) -h ( F ` k ) ) ) ^ 2 ) + ( ( normh ` ( ( ( H ` j ) -h ( H ` k ) ) -h ( ( F ` j ) -h ( F ` k ) ) ) ) ^ 2 ) ) = ( ( normh ` ( ( H ` j ) -h ( H ` k ) ) ) ^ 2 ) )
123 55 122 breqtrd
 |-  ( ( ph /\ ( j e. NN /\ k e. NN ) ) -> ( ( normh ` ( ( F ` j ) -h ( F ` k ) ) ) ^ 2 ) <_ ( ( normh ` ( ( H ` j ) -h ( H ` k ) ) ) ^ 2 ) )
124 normcl
 |-  ( ( ( H ` j ) -h ( H ` k ) ) e. ~H -> ( normh ` ( ( H ` j ) -h ( H ` k ) ) ) e. RR )
125 34 124 syl
 |-  ( ( ph /\ ( j e. NN /\ k e. NN ) ) -> ( normh ` ( ( H ` j ) -h ( H ` k ) ) ) e. RR )
126 normge0
 |-  ( ( ( F ` j ) -h ( F ` k ) ) e. ~H -> 0 <_ ( normh ` ( ( F ` j ) -h ( F ` k ) ) ) )
127 44 126 syl
 |-  ( ( ph /\ ( j e. NN /\ k e. NN ) ) -> 0 <_ ( normh ` ( ( F ` j ) -h ( F ` k ) ) ) )
128 normge0
 |-  ( ( ( H ` j ) -h ( H ` k ) ) e. ~H -> 0 <_ ( normh ` ( ( H ` j ) -h ( H ` k ) ) ) )
129 34 128 syl
 |-  ( ( ph /\ ( j e. NN /\ k e. NN ) ) -> 0 <_ ( normh ` ( ( H ` j ) -h ( H ` k ) ) ) )
130 51 125 127 129 le2sqd
 |-  ( ( ph /\ ( j e. NN /\ k e. NN ) ) -> ( ( normh ` ( ( F ` j ) -h ( F ` k ) ) ) <_ ( normh ` ( ( H ` j ) -h ( H ` k ) ) ) <-> ( ( normh ` ( ( F ` j ) -h ( F ` k ) ) ) ^ 2 ) <_ ( ( normh ` ( ( H ` j ) -h ( H ` k ) ) ) ^ 2 ) ) )
131 123 130 mpbird
 |-  ( ( ph /\ ( j e. NN /\ k e. NN ) ) -> ( normh ` ( ( F ` j ) -h ( F ` k ) ) ) <_ ( normh ` ( ( H ` j ) -h ( H ` k ) ) ) )
132 131 adantlr
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. NN /\ k e. NN ) ) -> ( normh ` ( ( F ` j ) -h ( F ` k ) ) ) <_ ( normh ` ( ( H ` j ) -h ( H ` k ) ) ) )
133 51 adantlr
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. NN /\ k e. NN ) ) -> ( normh ` ( ( F ` j ) -h ( F ` k ) ) ) e. RR )
134 125 adantlr
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. NN /\ k e. NN ) ) -> ( normh ` ( ( H ` j ) -h ( H ` k ) ) ) e. RR )
135 rpre
 |-  ( x e. RR+ -> x e. RR )
136 135 ad2antlr
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. NN /\ k e. NN ) ) -> x e. RR )
137 lelttr
 |-  ( ( ( normh ` ( ( F ` j ) -h ( F ` k ) ) ) e. RR /\ ( normh ` ( ( H ` j ) -h ( H ` k ) ) ) e. RR /\ x e. RR ) -> ( ( ( normh ` ( ( F ` j ) -h ( F ` k ) ) ) <_ ( normh ` ( ( H ` j ) -h ( H ` k ) ) ) /\ ( normh ` ( ( H ` j ) -h ( H ` k ) ) ) < x ) -> ( normh ` ( ( F ` j ) -h ( F ` k ) ) ) < x ) )
138 133 134 136 137 syl3anc
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. NN /\ k e. NN ) ) -> ( ( ( normh ` ( ( F ` j ) -h ( F ` k ) ) ) <_ ( normh ` ( ( H ` j ) -h ( H ` k ) ) ) /\ ( normh ` ( ( H ` j ) -h ( H ` k ) ) ) < x ) -> ( normh ` ( ( F ` j ) -h ( F ` k ) ) ) < x ) )
139 132 138 mpand
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. NN /\ k e. NN ) ) -> ( ( normh ` ( ( H ` j ) -h ( H ` k ) ) ) < x -> ( normh ` ( ( F ` j ) -h ( F ` k ) ) ) < x ) )
140 139 anassrs
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) /\ k e. NN ) -> ( ( normh ` ( ( H ` j ) -h ( H ` k ) ) ) < x -> ( normh ` ( ( F ` j ) -h ( F ` k ) ) ) < x ) )
141 16 140 syldan
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( normh ` ( ( H ` j ) -h ( H ` k ) ) ) < x -> ( normh ` ( ( F ` j ) -h ( F ` k ) ) ) < x ) )
142 141 ralimdva
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. NN ) -> ( A. k e. ( ZZ>= ` j ) ( normh ` ( ( H ` j ) -h ( H ` k ) ) ) < x -> A. k e. ( ZZ>= ` j ) ( normh ` ( ( F ` j ) -h ( F ` k ) ) ) < x ) )
143 142 reximdva
 |-  ( ( ph /\ x e. RR+ ) -> ( E. j e. NN A. k e. ( ZZ>= ` j ) ( normh ` ( ( H ` j ) -h ( H ` k ) ) ) < x -> E. j e. NN A. k e. ( ZZ>= ` j ) ( normh ` ( ( F ` j ) -h ( F ` k ) ) ) < x ) )
144 14 143 mpd
 |-  ( ( ph /\ x e. RR+ ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( normh ` ( ( F ` j ) -h ( F ` k ) ) ) < x )
145 144 ralrimiva
 |-  ( ph -> A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( normh ` ( ( F ` j ) -h ( F ` k ) ) ) < x )
146 hcau
 |-  ( F e. Cauchy <-> ( F : NN --> ~H /\ A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( normh ` ( ( F ` j ) -h ( F ` k ) ) ) < x ) )
147 10 145 146 sylanbrc
 |-  ( ph -> F e. Cauchy )
148 ax-hcompl
 |-  ( F e. Cauchy -> E. x e. ~H F ~~>v x )
149 hlimf
 |-  ~~>v : dom ~~>v --> ~H
150 ffn
 |-  ( ~~>v : dom ~~>v --> ~H -> ~~>v Fn dom ~~>v )
151 149 150 ax-mp
 |-  ~~>v Fn dom ~~>v
152 fnbr
 |-  ( ( ~~>v Fn dom ~~>v /\ F ~~>v x ) -> F e. dom ~~>v )
153 151 152 mpan
 |-  ( F ~~>v x -> F e. dom ~~>v )
154 153 rexlimivw
 |-  ( E. x e. ~H F ~~>v x -> F e. dom ~~>v )
155 147 148 154 3syl
 |-  ( ph -> F e. dom ~~>v )