Metamath Proof Explorer

Theorem prdsxmetlem

Description: The product metric is an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Hypotheses prdsdsf.y ⊢ 𝑌 = ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) )
prdsdsf.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
prdsdsf.v ⊢ 𝑉 = ( Base ‘ 𝑅 )
prdsdsf.e ⊢ 𝐸 = ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) )
prdsdsf.d ⊢ 𝐷 = ( dist ‘ 𝑌 )
prdsdsf.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑊 )
prdsdsf.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑋 )
prdsdsf.r ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑅 ∈ 𝑍 )
prdsdsf.m ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐸 ∈ ( ∞Met ‘ 𝑉 ) )
Assertion prdsxmetlem ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 prdsdsf.y ⊢ 𝑌 = ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) )
2 prdsdsf.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
3 prdsdsf.v ⊢ 𝑉 = ( Base ‘ 𝑅 )
4 prdsdsf.e ⊢ 𝐸 = ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) )
5 prdsdsf.d ⊢ 𝐷 = ( dist ‘ 𝑌 )
6 prdsdsf.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑊 )
7 prdsdsf.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑋 )
8 prdsdsf.r ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑅 ∈ 𝑍 )
9 prdsdsf.m ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐸 ∈ ( ∞Met ‘ 𝑉 ) )
10 2 fvexi ⊢ 𝐵 ∈ V
11 10 a1i ⊢ ( 𝜑 → 𝐵 ∈ V )
12 1 2 3 4 5 6 7 8 9 prdsdsf ⊢ ( 𝜑 → 𝐷 : ( 𝐵 × 𝐵 ) ⟶ ( 0 [,] +∞ ) )
13 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
14 fss ⊢ ( ( 𝐷 : ( 𝐵 × 𝐵 ) ⟶ ( 0 [,] +∞ ) ∧ ( 0 [,] +∞ ) ⊆ ℝ* ) → 𝐷 : ( 𝐵 × 𝐵 ) ⟶ ℝ* )
15 12 13 14 sylancl ⊢ ( 𝜑 → 𝐷 : ( 𝐵 × 𝐵 ) ⟶ ℝ* )
16 12 fovcdmda ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( 𝑓 𝐷 𝑔 ) ∈ ( 0 [,] +∞ ) )
17 elxrge0 ⊢ ( ( 𝑓 𝐷 𝑔 ) ∈ ( 0 [,] +∞ ) ↔ ( ( 𝑓 𝐷 𝑔 ) ∈ ℝ* ∧ 0 ≤ ( 𝑓 𝐷 𝑔 ) ) )
18 17 simprbi ⊢ ( ( 𝑓 𝐷 𝑔 ) ∈ ( 0 [,] +∞ ) → 0 ≤ ( 𝑓 𝐷 𝑔 ) )
19 16 18 syl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 0 ≤ ( 𝑓 𝐷 𝑔 ) )
20 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝑆 ∈ 𝑊 )
21 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝐼 ∈ 𝑋 )
22 8 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 𝑅 ∈ 𝑍 )
23 22 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ∀ 𝑥 ∈ 𝐼 𝑅 ∈ 𝑍 )
24 simprl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝑓 ∈ 𝐵 )
25 simprr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝑔 ∈ 𝐵 )
26 1 2 20 21 23 24 25 3 4 5 prdsdsval3 ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( 𝑓 𝐷 𝑔 ) = sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) )
27 26 breq1d ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( ( 𝑓 𝐷 𝑔 ) ≤ 0 ↔ sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ≤ 0 ) )
28 9 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝐸 ∈ ( ∞Met ‘ 𝑉 ) )
29 1 2 20 21 23 3 24 prdsbascl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ∈ 𝑉 )
30 29 r19.21bi ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑓 ‘ 𝑥 ) ∈ 𝑉 )
31 1 2 20 21 23 3 25 prdsbascl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ∀ 𝑥 ∈ 𝐼 ( 𝑔 ‘ 𝑥 ) ∈ 𝑉 )
32 31 r19.21bi ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑔 ‘ 𝑥 ) ∈ 𝑉 )
33 xmetcl ⊢ ( ( 𝐸 ∈ ( ∞Met ‘ 𝑉 ) ∧ ( 𝑓 ‘ 𝑥 ) ∈ 𝑉 ∧ ( 𝑔 ‘ 𝑥 ) ∈ 𝑉 ) → ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ∈ ℝ* )
34 28 30 32 33 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ∈ ℝ* )
35 34 fmpttd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) : 𝐼 ⟶ ℝ* )
36 35 frnd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ⊆ ℝ* )
37 0xr ⊢ 0 ∈ ℝ*
38 37 a1i ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 0 ∈ ℝ* )
39 38 snssd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → { 0 } ⊆ ℝ* )
40 36 39 unssd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) ⊆ ℝ* )
41 supxrleub ⊢ ( ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) ⊆ ℝ* ∧ 0 ∈ ℝ* ) → ( sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ≤ 0 ↔ ∀ 𝑧 ∈ ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) 𝑧 ≤ 0 ) )
42 40 37 41 sylancl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ≤ 0 ↔ ∀ 𝑧 ∈ ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) 𝑧 ≤ 0 ) )
43 0le0 ⊢ 0 ≤ 0
44 c0ex ⊢ 0 ∈ V
45 breq1 ⊢ ( 𝑧 = 0 → ( 𝑧 ≤ 0 ↔ 0 ≤ 0 ) )
46 44 45 ralsn ⊢ ( ∀ 𝑧 ∈ { 0 } 𝑧 ≤ 0 ↔ 0 ≤ 0 )
47 43 46 mpbir ⊢ ∀ 𝑧 ∈ { 0 } 𝑧 ≤ 0
48 ralunb ⊢ ( ∀ 𝑧 ∈ ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) 𝑧 ≤ 0 ↔ ( ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) 𝑧 ≤ 0 ∧ ∀ 𝑧 ∈ { 0 } 𝑧 ≤ 0 ) )
49 47 48 mpbiran2 ⊢ ( ∀ 𝑧 ∈ ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) 𝑧 ≤ 0 ↔ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) 𝑧 ≤ 0 )
50 ovex ⊢ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ∈ V
51 50 rgenw ⊢ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ∈ V
52 eqid ⊢ ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) )
53 breq1 ⊢ ( 𝑧 = ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) → ( 𝑧 ≤ 0 ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ≤ 0 ) )
54 52 53 ralrnmptw ⊢ ( ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ∈ V → ( ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) 𝑧 ≤ 0 ↔ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ≤ 0 ) )
55 51 54 ax-mp ⊢ ( ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) 𝑧 ≤ 0 ↔ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ≤ 0 )
56 49 55 bitri ⊢ ( ∀ 𝑧 ∈ ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) 𝑧 ≤ 0 ↔ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ≤ 0 )
57 xmetge0 ⊢ ( ( 𝐸 ∈ ( ∞Met ‘ 𝑉 ) ∧ ( 𝑓 ‘ 𝑥 ) ∈ 𝑉 ∧ ( 𝑔 ‘ 𝑥 ) ∈ 𝑉 ) → 0 ≤ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) )
58 28 30 32 57 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → 0 ≤ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) )
59 58 biantrud ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ≤ 0 ↔ ( ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ≤ 0 ∧ 0 ≤ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ) )
60 xrletri3 ⊢ ( ( ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ∈ ℝ* ∧ 0 ∈ ℝ* ) → ( ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) = 0 ↔ ( ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ≤ 0 ∧ 0 ≤ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ) )
61 34 37 60 sylancl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) = 0 ↔ ( ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ≤ 0 ∧ 0 ≤ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ) )
62 xmeteq0 ⊢ ( ( 𝐸 ∈ ( ∞Met ‘ 𝑉 ) ∧ ( 𝑓 ‘ 𝑥 ) ∈ 𝑉 ∧ ( 𝑔 ‘ 𝑥 ) ∈ 𝑉 ) → ( ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) = 0 ↔ ( 𝑓 ‘ 𝑥 ) = ( 𝑔 ‘ 𝑥 ) ) )
63 28 30 32 62 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) = 0 ↔ ( 𝑓 ‘ 𝑥 ) = ( 𝑔 ‘ 𝑥 ) ) )
64 59 61 63 3bitr2d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ≤ 0 ↔ ( 𝑓 ‘ 𝑥 ) = ( 𝑔 ‘ 𝑥 ) ) )
65 64 ralbidva ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ≤ 0 ↔ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) = ( 𝑔 ‘ 𝑥 ) ) )
66 eqid ⊢ ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) = ( 𝑥 ∈ 𝐼 ↦ 𝑅 )
67 66 fnmpt ⊢ ( ∀ 𝑥 ∈ 𝐼 𝑅 ∈ 𝑍 → ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) Fn 𝐼 )
68 22 67 syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) Fn 𝐼 )
69 68 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) Fn 𝐼 )
70 1 2 20 21 69 24 prdsbasfn ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝑓 Fn 𝐼 )
71 1 2 20 21 69 25 prdsbasfn ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝑔 Fn 𝐼 )
72 eqfnfv ⊢ ( ( 𝑓 Fn 𝐼 ∧ 𝑔 Fn 𝐼 ) → ( 𝑓 = 𝑔 ↔ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) = ( 𝑔 ‘ 𝑥 ) ) )
73 70 71 72 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( 𝑓 = 𝑔 ↔ ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) = ( 𝑔 ‘ 𝑥 ) ) )
74 65 73 bitr4d ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ≤ 0 ↔ 𝑓 = 𝑔 ) )
75 56 74 bitrid ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( ∀ 𝑧 ∈ ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) 𝑧 ≤ 0 ↔ 𝑓 = 𝑔 ) )
76 27 42 75 3bitrd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( ( 𝑓 𝐷 𝑔 ) ≤ 0 ↔ 𝑓 = 𝑔 ) )
77 26 3adantr3 ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ) → ( 𝑓 𝐷 𝑔 ) = sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) )
78 77 3adant3 ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) → ( 𝑓 𝐷 𝑔 ) = sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) )
79 9 3ad2antl1 ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐼 ) → 𝐸 ∈ ( ∞Met ‘ 𝑉 ) )
80 29 3adantr3 ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ) → ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ∈ 𝑉 )
81 80 3adant3 ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) → ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ∈ 𝑉 )
82 81 r19.21bi ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑓 ‘ 𝑥 ) ∈ 𝑉 )
83 31 3adantr3 ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ) → ∀ 𝑥 ∈ 𝐼 ( 𝑔 ‘ 𝑥 ) ∈ 𝑉 )
84 83 3adant3 ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) → ∀ 𝑥 ∈ 𝐼 ( 𝑔 ‘ 𝑥 ) ∈ 𝑉 )
85 84 r19.21bi ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑔 ‘ 𝑥 ) ∈ 𝑉 )
86 79 82 85 33 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ∈ ℝ* )
87 6 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) → 𝑆 ∈ 𝑊 )
88 7 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) → 𝐼 ∈ 𝑋 )
89 22 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) → ∀ 𝑥 ∈ 𝐼 𝑅 ∈ 𝑍 )
90 simp23 ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) → ℎ ∈ 𝐵 )
91 1 2 87 88 89 3 90 prdsbascl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) → ∀ 𝑥 ∈ 𝐼 ( ℎ ‘ 𝑥 ) ∈ 𝑉 )
92 91 r19.21bi ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ℎ ‘ 𝑥 ) ∈ 𝑉 )
93 xmetcl ⊢ ( ( 𝐸 ∈ ( ∞Met ‘ 𝑉 ) ∧ ( ℎ ‘ 𝑥 ) ∈ 𝑉 ∧ ( 𝑓 ‘ 𝑥 ) ∈ 𝑉 ) → ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑓 ‘ 𝑥 ) ) ∈ ℝ* )
94 79 92 82 93 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑓 ‘ 𝑥 ) ) ∈ ℝ* )
95 simp3l ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) → ( ℎ 𝐷 𝑓 ) ∈ ℝ )
96 95 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ℎ 𝐷 𝑓 ) ∈ ℝ )
97 xmetge0 ⊢ ( ( 𝐸 ∈ ( ∞Met ‘ 𝑉 ) ∧ ( ℎ ‘ 𝑥 ) ∈ 𝑉 ∧ ( 𝑓 ‘ 𝑥 ) ∈ 𝑉 ) → 0 ≤ ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑓 ‘ 𝑥 ) ) )
98 79 92 82 97 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐼 ) → 0 ≤ ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑓 ‘ 𝑥 ) ) )
99 94 fmpttd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) → ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑓 ‘ 𝑥 ) ) ) : 𝐼 ⟶ ℝ* )
100 99 frnd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) → ran ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑓 ‘ 𝑥 ) ) ) ⊆ ℝ* )
101 37 a1i ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) → 0 ∈ ℝ* )
102 101 snssd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) → { 0 } ⊆ ℝ* )
103 100 102 unssd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) → ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑓 ‘ 𝑥 ) ) ) ∪ { 0 } ) ⊆ ℝ* )
104 ssun1 ⊢ ran ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑓 ‘ 𝑥 ) ) ) ⊆ ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑓 ‘ 𝑥 ) ) ) ∪ { 0 } )
105 ovex ⊢ ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑓 ‘ 𝑥 ) ) ∈ V
106 105 elabrex ⊢ ( 𝑥 ∈ 𝐼 → ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑓 ‘ 𝑥 ) ) ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐼 𝑧 = ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑓 ‘ 𝑥 ) ) } )
107 106 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑓 ‘ 𝑥 ) ) ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐼 𝑧 = ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑓 ‘ 𝑥 ) ) } )
108 eqid ⊢ ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑓 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑓 ‘ 𝑥 ) ) )
109 108 rnmpt ⊢ ran ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑓 ‘ 𝑥 ) ) ) = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐼 𝑧 = ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑓 ‘ 𝑥 ) ) }
110 107 109 eleqtrrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑓 ‘ 𝑥 ) ) ∈ ran ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑓 ‘ 𝑥 ) ) ) )
111 104 110 sselid ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑓 ‘ 𝑥 ) ) ∈ ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑓 ‘ 𝑥 ) ) ) ∪ { 0 } ) )
112 supxrub ⊢ ( ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑓 ‘ 𝑥 ) ) ) ∪ { 0 } ) ⊆ ℝ* ∧ ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑓 ‘ 𝑥 ) ) ∈ ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑓 ‘ 𝑥 ) ) ) ∪ { 0 } ) ) → ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑓 ‘ 𝑥 ) ) ≤ sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑓 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) )
113 103 111 112 syl2an2r ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑓 ‘ 𝑥 ) ) ≤ sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑓 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) )
114 simp21 ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) → 𝑓 ∈ 𝐵 )
115 1 2 87 88 89 90 114 3 4 5 prdsdsval3 ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) → ( ℎ 𝐷 𝑓 ) = sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑓 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) )
116 115 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ℎ 𝐷 𝑓 ) = sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑓 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) )
117 113 116 breqtrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑓 ‘ 𝑥 ) ) ≤ ( ℎ 𝐷 𝑓 ) )
118 xrrege0 ⊢ ( ( ( ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑓 ‘ 𝑥 ) ) ∈ ℝ* ∧ ( ℎ 𝐷 𝑓 ) ∈ ℝ ) ∧ ( 0 ≤ ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑓 ‘ 𝑥 ) ) ∧ ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑓 ‘ 𝑥 ) ) ≤ ( ℎ 𝐷 𝑓 ) ) ) → ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑓 ‘ 𝑥 ) ) ∈ ℝ )
119 94 96 98 117 118 syl22anc ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑓 ‘ 𝑥 ) ) ∈ ℝ )
120 xmetcl ⊢ ( ( 𝐸 ∈ ( ∞Met ‘ 𝑉 ) ∧ ( ℎ ‘ 𝑥 ) ∈ 𝑉 ∧ ( 𝑔 ‘ 𝑥 ) ∈ 𝑉 ) → ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ∈ ℝ* )
121 79 92 85 120 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ∈ ℝ* )
122 simp3r ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) → ( ℎ 𝐷 𝑔 ) ∈ ℝ )
123 122 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ℎ 𝐷 𝑔 ) ∈ ℝ )
124 xmetge0 ⊢ ( ( 𝐸 ∈ ( ∞Met ‘ 𝑉 ) ∧ ( ℎ ‘ 𝑥 ) ∈ 𝑉 ∧ ( 𝑔 ‘ 𝑥 ) ∈ 𝑉 ) → 0 ≤ ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) )
125 79 92 85 124 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐼 ) → 0 ≤ ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) )
126 121 fmpttd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) → ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) : 𝐼 ⟶ ℝ* )
127 126 frnd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) → ran ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ⊆ ℝ* )
128 127 102 unssd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) → ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) ⊆ ℝ* )
129 ssun1 ⊢ ran ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ⊆ ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } )
130 ovex ⊢ ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ∈ V
131 130 elabrex ⊢ ( 𝑥 ∈ 𝐼 → ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐼 𝑧 = ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) } )
132 131 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐼 𝑧 = ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) } )
133 eqid ⊢ ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) )
134 133 rnmpt ⊢ ran ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐼 𝑧 = ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) }
135 132 134 eleqtrrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ∈ ran ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) )
136 129 135 sselid ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ∈ ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) )
137 supxrub ⊢ ( ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) ⊆ ℝ* ∧ ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ∈ ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) ) → ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ≤ sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) )
138 128 136 137 syl2an2r ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ≤ sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) )
139 simp22 ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) → 𝑔 ∈ 𝐵 )
140 1 2 87 88 89 90 139 3 4 5 prdsdsval3 ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) → ( ℎ 𝐷 𝑔 ) = sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) )
141 140 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ℎ 𝐷 𝑔 ) = sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) )
142 138 141 breqtrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ≤ ( ℎ 𝐷 𝑔 ) )
143 xrrege0 ⊢ ( ( ( ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ∈ ℝ* ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ∧ ( 0 ≤ ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ∧ ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ≤ ( ℎ 𝐷 𝑔 ) ) ) → ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ∈ ℝ )
144 121 123 125 142 143 syl22anc ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ∈ ℝ )
145 119 144 readdcld ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑓 ‘ 𝑥 ) ) + ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∈ ℝ )
146 79 82 85 57 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐼 ) → 0 ≤ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) )
147 xmettri2 ⊢ ( ( 𝐸 ∈ ( ∞Met ‘ 𝑉 ) ∧ ( ( ℎ ‘ 𝑥 ) ∈ 𝑉 ∧ ( 𝑓 ‘ 𝑥 ) ∈ 𝑉 ∧ ( 𝑔 ‘ 𝑥 ) ∈ 𝑉 ) ) → ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ≤ ( ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑓 ‘ 𝑥 ) ) +𝑒 ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) )
148 79 92 82 85 147 syl13anc ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ≤ ( ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑓 ‘ 𝑥 ) ) +𝑒 ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) )
149 119 144 rexaddd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑓 ‘ 𝑥 ) ) +𝑒 ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) = ( ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑓 ‘ 𝑥 ) ) + ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) )
150 148 149 breqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ≤ ( ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑓 ‘ 𝑥 ) ) + ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) )
151 xrrege0 ⊢ ( ( ( ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ∈ ℝ* ∧ ( ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑓 ‘ 𝑥 ) ) + ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∈ ℝ ) ∧ ( 0 ≤ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ∧ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ≤ ( ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑓 ‘ 𝑥 ) ) + ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ) ) → ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ∈ ℝ )
152 86 145 146 150 151 syl22anc ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ∈ ℝ )
153 readdcl ⊢ ( ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) → ( ( ℎ 𝐷 𝑓 ) + ( ℎ 𝐷 𝑔 ) ) ∈ ℝ )
154 153 3ad2ant3 ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) → ( ( ℎ 𝐷 𝑓 ) + ( ℎ 𝐷 𝑔 ) ) ∈ ℝ )
155 154 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ℎ 𝐷 𝑓 ) + ( ℎ 𝐷 𝑔 ) ) ∈ ℝ )
156 119 144 96 123 117 142 le2addd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑓 ‘ 𝑥 ) ) + ( ( ℎ ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ≤ ( ( ℎ 𝐷 𝑓 ) + ( ℎ 𝐷 𝑔 ) ) )
157 152 145 155 150 156 letrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ≤ ( ( ℎ 𝐷 𝑓 ) + ( ℎ 𝐷 𝑔 ) ) )
158 157 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) → ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ≤ ( ( ℎ 𝐷 𝑓 ) + ( ℎ 𝐷 𝑔 ) ) )
159 86 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) → ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ∈ ℝ* )
160 breq1 ⊢ ( 𝑧 = ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) → ( 𝑧 ≤ ( ( ℎ 𝐷 𝑓 ) + ( ℎ 𝐷 𝑔 ) ) ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ≤ ( ( ℎ 𝐷 𝑓 ) + ( ℎ 𝐷 𝑔 ) ) ) )
161 52 160 ralrnmptw ⊢ ( ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ∈ ℝ* → ( ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) 𝑧 ≤ ( ( ℎ 𝐷 𝑓 ) + ( ℎ 𝐷 𝑔 ) ) ↔ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ≤ ( ( ℎ 𝐷 𝑓 ) + ( ℎ 𝐷 𝑔 ) ) ) )
162 159 161 syl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) → ( ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) 𝑧 ≤ ( ( ℎ 𝐷 𝑓 ) + ( ℎ 𝐷 𝑔 ) ) ↔ ∀ 𝑥 ∈ 𝐼 ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ≤ ( ( ℎ 𝐷 𝑓 ) + ( ℎ 𝐷 𝑔 ) ) ) )
163 158 162 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) → ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) 𝑧 ≤ ( ( ℎ 𝐷 𝑓 ) + ( ℎ 𝐷 𝑔 ) ) )
164 12 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) → 𝐷 : ( 𝐵 × 𝐵 ) ⟶ ( 0 [,] +∞ ) )
165 164 90 114 fovcdmd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) → ( ℎ 𝐷 𝑓 ) ∈ ( 0 [,] +∞ ) )
166 elxrge0 ⊢ ( ( ℎ 𝐷 𝑓 ) ∈ ( 0 [,] +∞ ) ↔ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ* ∧ 0 ≤ ( ℎ 𝐷 𝑓 ) ) )
167 166 simprbi ⊢ ( ( ℎ 𝐷 𝑓 ) ∈ ( 0 [,] +∞ ) → 0 ≤ ( ℎ 𝐷 𝑓 ) )
168 165 167 syl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) → 0 ≤ ( ℎ 𝐷 𝑓 ) )
169 164 90 139 fovcdmd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) → ( ℎ 𝐷 𝑔 ) ∈ ( 0 [,] +∞ ) )
170 elxrge0 ⊢ ( ( ℎ 𝐷 𝑔 ) ∈ ( 0 [,] +∞ ) ↔ ( ( ℎ 𝐷 𝑔 ) ∈ ℝ* ∧ 0 ≤ ( ℎ 𝐷 𝑔 ) ) )
171 170 simprbi ⊢ ( ( ℎ 𝐷 𝑔 ) ∈ ( 0 [,] +∞ ) → 0 ≤ ( ℎ 𝐷 𝑔 ) )
172 169 171 syl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) → 0 ≤ ( ℎ 𝐷 𝑔 ) )
173 95 122 168 172 addge0d ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) → 0 ≤ ( ( ℎ 𝐷 𝑓 ) + ( ℎ 𝐷 𝑔 ) ) )
174 breq1 ⊢ ( 𝑧 = 0 → ( 𝑧 ≤ ( ( ℎ 𝐷 𝑓 ) + ( ℎ 𝐷 𝑔 ) ) ↔ 0 ≤ ( ( ℎ 𝐷 𝑓 ) + ( ℎ 𝐷 𝑔 ) ) ) )
175 44 174 ralsn ⊢ ( ∀ 𝑧 ∈ { 0 } 𝑧 ≤ ( ( ℎ 𝐷 𝑓 ) + ( ℎ 𝐷 𝑔 ) ) ↔ 0 ≤ ( ( ℎ 𝐷 𝑓 ) + ( ℎ 𝐷 𝑔 ) ) )
176 173 175 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) → ∀ 𝑧 ∈ { 0 } 𝑧 ≤ ( ( ℎ 𝐷 𝑓 ) + ( ℎ 𝐷 𝑔 ) ) )
177 ralunb ⊢ ( ∀ 𝑧 ∈ ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) 𝑧 ≤ ( ( ℎ 𝐷 𝑓 ) + ( ℎ 𝐷 𝑔 ) ) ↔ ( ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) 𝑧 ≤ ( ( ℎ 𝐷 𝑓 ) + ( ℎ 𝐷 𝑔 ) ) ∧ ∀ 𝑧 ∈ { 0 } 𝑧 ≤ ( ( ℎ 𝐷 𝑓 ) + ( ℎ 𝐷 𝑔 ) ) ) )
178 163 176 177 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) → ∀ 𝑧 ∈ ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) 𝑧 ≤ ( ( ℎ 𝐷 𝑓 ) + ( ℎ 𝐷 𝑔 ) ) )
179 40 3adantr3 ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ) → ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) ⊆ ℝ* )
180 179 3adant3 ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) → ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) ⊆ ℝ* )
181 154 rexrd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) → ( ( ℎ 𝐷 𝑓 ) + ( ℎ 𝐷 𝑔 ) ) ∈ ℝ* )
182 supxrleub ⊢ ( ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) ⊆ ℝ* ∧ ( ( ℎ 𝐷 𝑓 ) + ( ℎ 𝐷 𝑔 ) ) ∈ ℝ* ) → ( sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ≤ ( ( ℎ 𝐷 𝑓 ) + ( ℎ 𝐷 𝑔 ) ) ↔ ∀ 𝑧 ∈ ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) 𝑧 ≤ ( ( ℎ 𝐷 𝑓 ) + ( ℎ 𝐷 𝑔 ) ) ) )
183 180 181 182 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) → ( sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ≤ ( ( ℎ 𝐷 𝑓 ) + ( ℎ 𝐷 𝑔 ) ) ↔ ∀ 𝑧 ∈ ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) 𝑧 ≤ ( ( ℎ 𝐷 𝑓 ) + ( ℎ 𝐷 𝑔 ) ) ) )
184 178 183 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) → sup ( ( ran ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝐸 ( 𝑔 ‘ 𝑥 ) ) ) ∪ { 0 } ) , ℝ* , < ) ≤ ( ( ℎ 𝐷 𝑓 ) + ( ℎ 𝐷 𝑔 ) ) )
185 78 184 eqbrtrd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ∧ ( ( ℎ 𝐷 𝑓 ) ∈ ℝ ∧ ( ℎ 𝐷 𝑔 ) ∈ ℝ ) ) → ( 𝑓 𝐷 𝑔 ) ≤ ( ( ℎ 𝐷 𝑓 ) + ( ℎ 𝐷 𝑔 ) ) )
186 11 15 19 76 185 isxmet2d ⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝐵 ) )