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 ) |