Metamath Proof Explorer

Theorem rrnequiv

Description: The supremum metric on RR ^ I is equivalent to the Rn metric. (Contributed by Jeff Madsen, 15-Sep-2015)

Ref Expression
Hypotheses rrnequiv.y 
|- Y = ( ( CCfld |`s RR ) ^s I )
rrnequiv.d 
|- D = ( dist ` Y )
rrnequiv.1 
|- X = ( RR ^m I )
rrnequiv.i 
|- ( ph -> I e. Fin )
Assertion rrnequiv 
|- ( ( ph /\ ( F e. X /\ G e. X ) ) -> ( ( F D G ) <_ ( F ( Rn ` I ) G ) /\ ( F ( Rn ` I ) G ) <_ ( ( sqrt ` ( # ` I ) ) x. ( F D G ) ) ) )

Proof

Step Hyp Ref Expression
1 rrnequiv.y 
 |-  Y = ( ( CCfld |`s RR ) ^s I )
2 rrnequiv.d 
 |-  D = ( dist ` Y )
3 rrnequiv.1 
 |-  X = ( RR ^m I )
4 rrnequiv.i 
 |-  ( ph -> I e. Fin )
5 ovex 
 |-  ( CCfld |`s RR ) e. _V
6 4 adantr 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> I e. Fin )
7 reex 
 |-  RR e. _V
8 eqid 
 |-  ( CCfld |`s RR ) = ( CCfld |`s RR )
9 eqid 
 |-  ( Scalar ` CCfld ) = ( Scalar ` CCfld )
10 8 9 resssca 
 |-  ( RR e. _V -> ( Scalar ` CCfld ) = ( Scalar ` ( CCfld |`s RR ) ) )
11 7 10 ax-mp 
 |-  ( Scalar ` CCfld ) = ( Scalar ` ( CCfld |`s RR ) )
12 1 11 pwsval 
 |-  ( ( ( CCfld |`s RR ) e. _V /\ I e. Fin ) -> Y = ( ( Scalar ` CCfld ) Xs_ ( I X. { ( CCfld |`s RR ) } ) ) )
13 5 6 12 sylancr 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> Y = ( ( Scalar ` CCfld ) Xs_ ( I X. { ( CCfld |`s RR ) } ) ) )
14 13 fveq2d 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> ( dist ` Y ) = ( dist ` ( ( Scalar ` CCfld ) Xs_ ( I X. { ( CCfld |`s RR ) } ) ) ) )
15 2 14 eqtrid 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> D = ( dist ` ( ( Scalar ` CCfld ) Xs_ ( I X. { ( CCfld |`s RR ) } ) ) ) )
16 15 oveqd 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> ( F D G ) = ( F ( dist ` ( ( Scalar ` CCfld ) Xs_ ( I X. { ( CCfld |`s RR ) } ) ) ) G ) )
17 fconstmpt 
 |-  ( I X. { ( CCfld |`s RR ) } ) = ( k e. I |-> ( CCfld |`s RR ) )
18 17 oveq2i 
 |-  ( ( Scalar ` CCfld ) Xs_ ( I X. { ( CCfld |`s RR ) } ) ) = ( ( Scalar ` CCfld ) Xs_ ( k e. I |-> ( CCfld |`s RR ) ) )
19 eqid 
 |-  ( Base ` ( ( Scalar ` CCfld ) Xs_ ( I X. { ( CCfld |`s RR ) } ) ) ) = ( Base ` ( ( Scalar ` CCfld ) Xs_ ( I X. { ( CCfld |`s RR ) } ) ) )
20 fvexd 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> ( Scalar ` CCfld ) e. _V )
21 5 a1i 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ k e. I ) -> ( CCfld |`s RR ) e. _V )
22 21 ralrimiva 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> A. k e. I ( CCfld |`s RR ) e. _V )
23 simprl 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> F e. X )
24 ax-resscn 
 |-  RR C_ CC
25 cnfldbas 
 |-  CC = ( Base ` CCfld )
26 8 25 ressbas2 
 |-  ( RR C_ CC -> RR = ( Base ` ( CCfld |`s RR ) ) )
27 24 26 ax-mp 
 |-  RR = ( Base ` ( CCfld |`s RR ) )
28 1 27 pwsbas 
 |-  ( ( ( CCfld |`s RR ) e. _V /\ I e. Fin ) -> ( RR ^m I ) = ( Base ` Y ) )
29 5 6 28 sylancr 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> ( RR ^m I ) = ( Base ` Y ) )
30 13 fveq2d 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> ( Base ` Y ) = ( Base ` ( ( Scalar ` CCfld ) Xs_ ( I X. { ( CCfld |`s RR ) } ) ) ) )
31 29 30 eqtrd 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> ( RR ^m I ) = ( Base ` ( ( Scalar ` CCfld ) Xs_ ( I X. { ( CCfld |`s RR ) } ) ) ) )
32 3 31 eqtrid 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> X = ( Base ` ( ( Scalar ` CCfld ) Xs_ ( I X. { ( CCfld |`s RR ) } ) ) ) )
33 23 32 eleqtrd 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> F e. ( Base ` ( ( Scalar ` CCfld ) Xs_ ( I X. { ( CCfld |`s RR ) } ) ) ) )
34 simprr 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> G e. X )
35 34 32 eleqtrd 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> G e. ( Base ` ( ( Scalar ` CCfld ) Xs_ ( I X. { ( CCfld |`s RR ) } ) ) ) )
36 cnfldds 
 |-  ( abs o. - ) = ( dist ` CCfld )
37 8 36 ressds 
 |-  ( RR e. _V -> ( abs o. - ) = ( dist ` ( CCfld |`s RR ) ) )
38 7 37 ax-mp 
 |-  ( abs o. - ) = ( dist ` ( CCfld |`s RR ) )
39 38 reseq1i 
 |-  ( ( abs o. - ) |` ( RR X. RR ) ) = ( ( dist ` ( CCfld |`s RR ) ) |` ( RR X. RR ) )
40 eqid 
 |-  ( dist ` ( ( Scalar ` CCfld ) Xs_ ( I X. { ( CCfld |`s RR ) } ) ) ) = ( dist ` ( ( Scalar ` CCfld ) Xs_ ( I X. { ( CCfld |`s RR ) } ) ) )
41 18 19 20 6 22 33 35 27 39 40 prdsdsval3 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> ( F ( dist ` ( ( Scalar ` CCfld ) Xs_ ( I X. { ( CCfld |`s RR ) } ) ) ) G ) = sup ( ( ran ( k e. I |-> ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) ) u. { 0 } ) , RR* , < ) )
42 16 41 eqtrd 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> ( F D G ) = sup ( ( ran ( k e. I |-> ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) ) u. { 0 } ) , RR* , < ) )
43 eqid 
 |-  ( ( abs o. - ) |` ( RR X. RR ) ) = ( ( abs o. - ) |` ( RR X. RR ) )
44 3 43 rrndstprj1 
 |-  ( ( ( I e. Fin /\ k e. I ) /\ ( F e. X /\ G e. X ) ) -> ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) <_ ( F ( Rn ` I ) G ) )
45 44 an32s 
 |-  ( ( ( I e. Fin /\ ( F e. X /\ G e. X ) ) /\ k e. I ) -> ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) <_ ( F ( Rn ` I ) G ) )
46 4 45 sylanl1 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ k e. I ) -> ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) <_ ( F ( Rn ` I ) G ) )
47 46 ralrimiva 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> A. k e. I ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) <_ ( F ( Rn ` I ) G ) )
48 ovex 
 |-  ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) e. _V
49 48 rgenw 
 |-  A. k e. I ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) e. _V
50 eqid 
 |-  ( k e. I |-> ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) ) = ( k e. I |-> ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) )
51 breq1 
 |-  ( z = ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) -> ( z <_ ( F ( Rn ` I ) G ) <-> ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) <_ ( F ( Rn ` I ) G ) ) )
52 50 51 ralrnmptw 
 |-  ( A. k e. I ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) e. _V -> ( A. z e. ran ( k e. I |-> ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) ) z <_ ( F ( Rn ` I ) G ) <-> A. k e. I ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) <_ ( F ( Rn ` I ) G ) ) )
53 49 52 ax-mp 
 |-  ( A. z e. ran ( k e. I |-> ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) ) z <_ ( F ( Rn ` I ) G ) <-> A. k e. I ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) <_ ( F ( Rn ` I ) G ) )
54 47 53 sylibr 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> A. z e. ran ( k e. I |-> ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) ) z <_ ( F ( Rn ` I ) G ) )
55 3 rrnmet 
 |-  ( I e. Fin -> ( Rn ` I ) e. ( Met ` X ) )
56 6 55 syl 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> ( Rn ` I ) e. ( Met ` X ) )
57 metge0 
 |-  ( ( ( Rn ` I ) e. ( Met ` X ) /\ F e. X /\ G e. X ) -> 0 <_ ( F ( Rn ` I ) G ) )
58 56 23 34 57 syl3anc 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> 0 <_ ( F ( Rn ` I ) G ) )
59 elsni 
 |-  ( z e. { 0 } -> z = 0 )
60 59 breq1d 
 |-  ( z e. { 0 } -> ( z <_ ( F ( Rn ` I ) G ) <-> 0 <_ ( F ( Rn ` I ) G ) ) )
61 58 60 syl5ibrcom 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> ( z e. { 0 } -> z <_ ( F ( Rn ` I ) G ) ) )
62 61 ralrimiv 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> A. z e. { 0 } z <_ ( F ( Rn ` I ) G ) )
63 ralunb 
 |-  ( A. z e. ( ran ( k e. I |-> ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) ) u. { 0 } ) z <_ ( F ( Rn ` I ) G ) <-> ( A. z e. ran ( k e. I |-> ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) ) z <_ ( F ( Rn ` I ) G ) /\ A. z e. { 0 } z <_ ( F ( Rn ` I ) G ) ) )
64 54 62 63 sylanbrc 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> A. z e. ( ran ( k e. I |-> ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) ) u. { 0 } ) z <_ ( F ( Rn ` I ) G ) )
65 18 19 20 6 22 27 33 prdsbascl 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> A. k e. I ( F ` k ) e. RR )
66 65 r19.21bi 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ k e. I ) -> ( F ` k ) e. RR )
67 18 19 20 6 22 27 35 prdsbascl 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> A. k e. I ( G ` k ) e. RR )
68 67 r19.21bi 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ k e. I ) -> ( G ` k ) e. RR )
69 43 remet 
 |-  ( ( abs o. - ) |` ( RR X. RR ) ) e. ( Met ` RR )
70 metcl 
 |-  ( ( ( ( abs o. - ) |` ( RR X. RR ) ) e. ( Met ` RR ) /\ ( F ` k ) e. RR /\ ( G ` k ) e. RR ) -> ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) e. RR )
71 69 70 mp3an1 
 |-  ( ( ( F ` k ) e. RR /\ ( G ` k ) e. RR ) -> ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) e. RR )
72 66 68 71 syl2anc 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ k e. I ) -> ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) e. RR )
73 72 fmpttd 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> ( k e. I |-> ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) ) : I --> RR )
74 73 frnd 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> ran ( k e. I |-> ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) ) C_ RR )
75 ressxr 
 |-  RR C_ RR*
76 74 75 sstrdi 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> ran ( k e. I |-> ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) ) C_ RR* )
77 0xr 
 |-  0 e. RR*
78 77 a1i 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> 0 e. RR* )
79 78 snssd 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> { 0 } C_ RR* )
80 76 79 unssd 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> ( ran ( k e. I |-> ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) ) u. { 0 } ) C_ RR* )
81 metcl 
 |-  ( ( ( Rn ` I ) e. ( Met ` X ) /\ F e. X /\ G e. X ) -> ( F ( Rn ` I ) G ) e. RR )
82 56 23 34 81 syl3anc 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> ( F ( Rn ` I ) G ) e. RR )
83 75 82 sselid 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> ( F ( Rn ` I ) G ) e. RR* )
84 supxrleub 
 |-  ( ( ( ran ( k e. I |-> ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) ) u. { 0 } ) C_ RR* /\ ( F ( Rn ` I ) G ) e. RR* ) -> ( sup ( ( ran ( k e. I |-> ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) ) u. { 0 } ) , RR* , < ) <_ ( F ( Rn ` I ) G ) <-> A. z e. ( ran ( k e. I |-> ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) ) u. { 0 } ) z <_ ( F ( Rn ` I ) G ) ) )
85 80 83 84 syl2anc 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> ( sup ( ( ran ( k e. I |-> ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) ) u. { 0 } ) , RR* , < ) <_ ( F ( Rn ` I ) G ) <-> A. z e. ( ran ( k e. I |-> ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) ) u. { 0 } ) z <_ ( F ( Rn ` I ) G ) ) )
86 64 85 mpbird 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> sup ( ( ran ( k e. I |-> ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) ) u. { 0 } ) , RR* , < ) <_ ( F ( Rn ` I ) G ) )
87 42 86 eqbrtrd 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> ( F D G ) <_ ( F ( Rn ` I ) G ) )
88 rzal 
 |-  ( I = (/) -> A. k e. I ( F ` k ) = ( G ` k ) )
89 23 3 eleqtrdi 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> F e. ( RR ^m I ) )
90 elmapi 
 |-  ( F e. ( RR ^m I ) -> F : I --> RR )
91 ffn 
 |-  ( F : I --> RR -> F Fn I )
92 89 90 91 3syl 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> F Fn I )
93 34 3 eleqtrdi 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> G e. ( RR ^m I ) )
94 elmapi 
 |-  ( G e. ( RR ^m I ) -> G : I --> RR )
95 ffn 
 |-  ( G : I --> RR -> G Fn I )
96 93 94 95 3syl 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> G Fn I )
97 eqfnfv 
 |-  ( ( F Fn I /\ G Fn I ) -> ( F = G <-> A. k e. I ( F ` k ) = ( G ` k ) ) )
98 92 96 97 syl2anc 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> ( F = G <-> A. k e. I ( F ` k ) = ( G ` k ) ) )
99 88 98 imbitrrid 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> ( I = (/) -> F = G ) )
100 99 imp 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ I = (/) ) -> F = G )
101 100 oveq1d 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ I = (/) ) -> ( F ( Rn ` I ) G ) = ( G ( Rn ` I ) G ) )
102 met0 
 |-  ( ( ( Rn ` I ) e. ( Met ` X ) /\ G e. X ) -> ( G ( Rn ` I ) G ) = 0 )
103 56 34 102 syl2anc 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> ( G ( Rn ` I ) G ) = 0 )
104 hashcl 
 |-  ( I e. Fin -> ( # ` I ) e. NN0 )
105 6 104 syl 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> ( # ` I ) e. NN0 )
106 105 nn0red 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> ( # ` I ) e. RR )
107 105 nn0ge0d 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> 0 <_ ( # ` I ) )
108 106 107 resqrtcld 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> ( sqrt ` ( # ` I ) ) e. RR )
109 1 2 3 repwsmet 
 |-  ( I e. Fin -> D e. ( Met ` X ) )
110 6 109 syl 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> D e. ( Met ` X ) )
111 metcl 
 |-  ( ( D e. ( Met ` X ) /\ F e. X /\ G e. X ) -> ( F D G ) e. RR )
112 110 23 34 111 syl3anc 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> ( F D G ) e. RR )
113 106 107 sqrtge0d 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> 0 <_ ( sqrt ` ( # ` I ) ) )
114 metge0 
 |-  ( ( D e. ( Met ` X ) /\ F e. X /\ G e. X ) -> 0 <_ ( F D G ) )
115 110 23 34 114 syl3anc 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> 0 <_ ( F D G ) )
116 108 112 113 115 mulge0d 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> 0 <_ ( ( sqrt ` ( # ` I ) ) x. ( F D G ) ) )
117 103 116 eqbrtrd 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> ( G ( Rn ` I ) G ) <_ ( ( sqrt ` ( # ` I ) ) x. ( F D G ) ) )
118 117 adantr 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ I = (/) ) -> ( G ( Rn ` I ) G ) <_ ( ( sqrt ` ( # ` I ) ) x. ( F D G ) ) )
119 101 118 eqbrtrd 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ I = (/) ) -> ( F ( Rn ` I ) G ) <_ ( ( sqrt ` ( # ` I ) ) x. ( F D G ) ) )
120 82 adantr 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) -> ( F ( Rn ` I ) G ) e. RR )
121 108 112 remulcld 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> ( ( sqrt ` ( # ` I ) ) x. ( F D G ) ) e. RR )
122 121 adantr 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) -> ( ( sqrt ` ( # ` I ) ) x. ( F D G ) ) e. RR )
123 rpre 
 |-  ( r e. RR+ -> r e. RR )
124 123 ad2antll 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) -> r e. RR )
125 122 124 readdcld 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) -> ( ( ( sqrt ` ( # ` I ) ) x. ( F D G ) ) + r ) e. RR )
126 6 adantr 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) -> I e. Fin )
127 simprl 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) -> I =/= (/) )
128 eldifsn 
 |-  ( I e. ( Fin \ { (/) } ) <-> ( I e. Fin /\ I =/= (/) ) )
129 126 127 128 sylanbrc 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) -> I e. ( Fin \ { (/) } ) )
130 23 adantr 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) -> F e. X )
131 34 adantr 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) -> G e. X )
132 112 adantr 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) -> ( F D G ) e. RR )
133 simprr 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) -> r e. RR+ )
134 hashnncl 
 |-  ( I e. Fin -> ( ( # ` I ) e. NN <-> I =/= (/) ) )
135 126 134 syl 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) -> ( ( # ` I ) e. NN <-> I =/= (/) ) )
136 127 135 mpbird 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) -> ( # ` I ) e. NN )
137 136 nnrpd 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) -> ( # ` I ) e. RR+ )
138 137 rpsqrtcld 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) -> ( sqrt ` ( # ` I ) ) e. RR+ )
139 133 138 rpdivcld 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) -> ( r / ( sqrt ` ( # ` I ) ) ) e. RR+ )
140 139 rpred 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) -> ( r / ( sqrt ` ( # ` I ) ) ) e. RR )
141 132 140 readdcld 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) -> ( ( F D G ) + ( r / ( sqrt ` ( # ` I ) ) ) ) e. RR )
142 0red 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) -> 0 e. RR )
143 115 adantr 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) -> 0 <_ ( F D G ) )
144 132 139 ltaddrpd 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) -> ( F D G ) < ( ( F D G ) + ( r / ( sqrt ` ( # ` I ) ) ) ) )
145 142 132 141 143 144 lelttrd 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) -> 0 < ( ( F D G ) + ( r / ( sqrt ` ( # ` I ) ) ) ) )
146 141 145 elrpd 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) -> ( ( F D G ) + ( r / ( sqrt ` ( # ` I ) ) ) ) e. RR+ )
147 72 adantlr 
 |-  ( ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) /\ k e. I ) -> ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) e. RR )
148 132 adantr 
 |-  ( ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) /\ k e. I ) -> ( F D G ) e. RR )
149 141 adantr 
 |-  ( ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) /\ k e. I ) -> ( ( F D G ) + ( r / ( sqrt ` ( # ` I ) ) ) ) e. RR )
150 80 ad2antrr 
 |-  ( ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) /\ k e. I ) -> ( ran ( k e. I |-> ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) ) u. { 0 } ) C_ RR* )
151 ssun1 
 |-  ran ( k e. I |-> ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) ) C_ ( ran ( k e. I |-> ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) ) u. { 0 } )
152 simpr 
 |-  ( ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) /\ k e. I ) -> k e. I )
153 50 elrnmpt1 
 |-  ( ( k e. I /\ ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) e. _V ) -> ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) e. ran ( k e. I |-> ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) ) )
154 152 48 153 sylancl 
 |-  ( ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) /\ k e. I ) -> ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) e. ran ( k e. I |-> ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) ) )
155 151 154 sselid 
 |-  ( ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) /\ k e. I ) -> ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) e. ( ran ( k e. I |-> ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) ) u. { 0 } ) )
156 supxrub 
 |-  ( ( ( ran ( k e. I |-> ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) ) u. { 0 } ) C_ RR* /\ ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) e. ( ran ( k e. I |-> ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) ) u. { 0 } ) ) -> ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) <_ sup ( ( ran ( k e. I |-> ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) ) u. { 0 } ) , RR* , < ) )
157 150 155 156 syl2anc 
 |-  ( ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) /\ k e. I ) -> ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) <_ sup ( ( ran ( k e. I |-> ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) ) u. { 0 } ) , RR* , < ) )
158 42 ad2antrr 
 |-  ( ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) /\ k e. I ) -> ( F D G ) = sup ( ( ran ( k e. I |-> ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) ) u. { 0 } ) , RR* , < ) )
159 157 158 breqtrrd 
 |-  ( ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) /\ k e. I ) -> ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) <_ ( F D G ) )
160 144 adantr 
 |-  ( ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) /\ k e. I ) -> ( F D G ) < ( ( F D G ) + ( r / ( sqrt ` ( # ` I ) ) ) ) )
161 147 148 149 159 160 lelttrd 
 |-  ( ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) /\ k e. I ) -> ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) < ( ( F D G ) + ( r / ( sqrt ` ( # ` I ) ) ) ) )
162 161 ralrimiva 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) -> A. k e. I ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) < ( ( F D G ) + ( r / ( sqrt ` ( # ` I ) ) ) ) )
163 3 43 rrndstprj2 
 |-  ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( ( ( F D G ) + ( r / ( sqrt ` ( # ` I ) ) ) ) e. RR+ /\ A. k e. I ( ( F ` k ) ( ( abs o. - ) |` ( RR X. RR ) ) ( G ` k ) ) < ( ( F D G ) + ( r / ( sqrt ` ( # ` I ) ) ) ) ) ) -> ( F ( Rn ` I ) G ) < ( ( ( F D G ) + ( r / ( sqrt ` ( # ` I ) ) ) ) x. ( sqrt ` ( # ` I ) ) ) )
164 129 130 131 146 162 163 syl32anc 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) -> ( F ( Rn ` I ) G ) < ( ( ( F D G ) + ( r / ( sqrt ` ( # ` I ) ) ) ) x. ( sqrt ` ( # ` I ) ) ) )
165 132 recnd 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) -> ( F D G ) e. CC )
166 140 recnd 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) -> ( r / ( sqrt ` ( # ` I ) ) ) e. CC )
167 108 adantr 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) -> ( sqrt ` ( # ` I ) ) e. RR )
168 167 recnd 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) -> ( sqrt ` ( # ` I ) ) e. CC )
169 165 166 168 adddird 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) -> ( ( ( F D G ) + ( r / ( sqrt ` ( # ` I ) ) ) ) x. ( sqrt ` ( # ` I ) ) ) = ( ( ( F D G ) x. ( sqrt ` ( # ` I ) ) ) + ( ( r / ( sqrt ` ( # ` I ) ) ) x. ( sqrt ` ( # ` I ) ) ) ) )
170 165 168 mulcomd 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) -> ( ( F D G ) x. ( sqrt ` ( # ` I ) ) ) = ( ( sqrt ` ( # ` I ) ) x. ( F D G ) ) )
171 124 recnd 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) -> r e. CC )
172 138 rpne0d 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) -> ( sqrt ` ( # ` I ) ) =/= 0 )
173 171 168 172 divcan1d 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) -> ( ( r / ( sqrt ` ( # ` I ) ) ) x. ( sqrt ` ( # ` I ) ) ) = r )
174 170 173 oveq12d 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) -> ( ( ( F D G ) x. ( sqrt ` ( # ` I ) ) ) + ( ( r / ( sqrt ` ( # ` I ) ) ) x. ( sqrt ` ( # ` I ) ) ) ) = ( ( ( sqrt ` ( # ` I ) ) x. ( F D G ) ) + r ) )
175 169 174 eqtrd 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) -> ( ( ( F D G ) + ( r / ( sqrt ` ( # ` I ) ) ) ) x. ( sqrt ` ( # ` I ) ) ) = ( ( ( sqrt ` ( # ` I ) ) x. ( F D G ) ) + r ) )
176 164 175 breqtrd 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) -> ( F ( Rn ` I ) G ) < ( ( ( sqrt ` ( # ` I ) ) x. ( F D G ) ) + r ) )
177 120 125 176 ltled 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ ( I =/= (/) /\ r e. RR+ ) ) -> ( F ( Rn ` I ) G ) <_ ( ( ( sqrt ` ( # ` I ) ) x. ( F D G ) ) + r ) )
178 177 anassrs 
 |-  ( ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ I =/= (/) ) /\ r e. RR+ ) -> ( F ( Rn ` I ) G ) <_ ( ( ( sqrt ` ( # ` I ) ) x. ( F D G ) ) + r ) )
179 178 ralrimiva 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ I =/= (/) ) -> A. r e. RR+ ( F ( Rn ` I ) G ) <_ ( ( ( sqrt ` ( # ` I ) ) x. ( F D G ) ) + r ) )
180 alrple 
 |-  ( ( ( F ( Rn ` I ) G ) e. RR /\ ( ( sqrt ` ( # ` I ) ) x. ( F D G ) ) e. RR ) -> ( ( F ( Rn ` I ) G ) <_ ( ( sqrt ` ( # ` I ) ) x. ( F D G ) ) <-> A. r e. RR+ ( F ( Rn ` I ) G ) <_ ( ( ( sqrt ` ( # ` I ) ) x. ( F D G ) ) + r ) ) )
181 82 121 180 syl2anc 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> ( ( F ( Rn ` I ) G ) <_ ( ( sqrt ` ( # ` I ) ) x. ( F D G ) ) <-> A. r e. RR+ ( F ( Rn ` I ) G ) <_ ( ( ( sqrt ` ( # ` I ) ) x. ( F D G ) ) + r ) ) )
182 181 adantr 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ I =/= (/) ) -> ( ( F ( Rn ` I ) G ) <_ ( ( sqrt ` ( # ` I ) ) x. ( F D G ) ) <-> A. r e. RR+ ( F ( Rn ` I ) G ) <_ ( ( ( sqrt ` ( # ` I ) ) x. ( F D G ) ) + r ) ) )
183 179 182 mpbird 
 |-  ( ( ( ph /\ ( F e. X /\ G e. X ) ) /\ I =/= (/) ) -> ( F ( Rn ` I ) G ) <_ ( ( sqrt ` ( # ` I ) ) x. ( F D G ) ) )
184 119 183 pm2.61dane 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> ( F ( Rn ` I ) G ) <_ ( ( sqrt ` ( # ` I ) ) x. ( F D G ) ) )
185 87 184 jca 
 |-  ( ( ph /\ ( F e. X /\ G e. X ) ) -> ( ( F D G ) <_ ( F ( Rn ` I ) G ) /\ ( F ( Rn ` I ) G ) <_ ( ( sqrt ` ( # ` I ) ) x. ( F D G ) ) ) )