prdsxmetlem

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

	Ref	Expression
Hypotheses	prdsdsf.y	⊢ 𝑌 = ( 𝑆 X_s ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) )
	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	⊢ 𝑌 = ( 𝑆 X_s ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) )
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 ‘ 𝐵 ) )

Metamath Proof Explorer

Theorem prdsxmetlem

Proof