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=ℂfld↾𝑠ℝ↑𝑠I
rrnequiv.d ⊢D=dist⁡Y
rrnequiv.1 ⊢X=ℝI
rrnequiv.i ⊢φ→I∈Fin
Assertion rrnequiv ⊢φ∧F∈X∧G∈X→FDG≤Fℝn⁡IG∧Fℝn⁡IG≤I⁢FDG

Proof

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