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 ffvelcdmda 
 |-  ( ( 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 ffvelcdmd 
 |-  ( ( 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 ffvelcdmda 
 |-  ( ( 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 ffvelcdmd 
 |-  ( ( 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 )