Theorem comet 13258

Description: The composition of an extended metric with a monotonic subadditive function is an extended metric. (Contributed by Mario Carneiro, 21-Mar-2015.)

Hypotheses

Ref	Expression
comet.1	⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))
comet.2	⊢ (𝜑 → 𝐹:(0[,]+∞)⟶ℝ*)
comet.3	⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]+∞)) → ((𝐹‘𝑥) = 0 ↔ 𝑥 = 0))
comet.4	⊢ ((𝜑 ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞))) → (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≤ (𝐹‘𝑦)))
comet.5	⊢ ((𝜑 ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞))) → (𝐹‘(𝑥 +𝑒 𝑦)) ≤ ((𝐹‘𝑥) +𝑒 (𝐹‘𝑦)))

Assertion

Ref	Expression
comet	⊢ (𝜑 → (𝐹 ∘ 𝐷) ∈ (∞Met‘𝑋))

Distinct variable groups:   𝑥,𝑦,𝐷   𝑥,𝐹,𝑦   𝜑,𝑥,𝑦

Allowed substitution hints:   𝑋(𝑥,𝑦)

Proof of Theorem comet

Dummy variables 𝑎 𝑏 𝑐 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		xmetrel 13102	. . . 4 ⊢ Rel ∞Met
2		comet.1	. . . 4 ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))
3		relelfvdm 5526	. . . 4 ⊢ ((Rel ∞Met ∧ 𝐷 ∈ (∞Met‘𝑋)) → 𝑋 ∈ dom ∞Met)
4	1, 2, 3	sylancr 412	. . 3 ⊢ (𝜑 → 𝑋 ∈ dom ∞Met)
5	4	elexd 2743	. 2 ⊢ (𝜑 → 𝑋 ∈ V)
6		comet.2	. . 3 ⊢ (𝜑 → 𝐹:(0[,]+∞)⟶ℝ*)
7		xmetf 13109	. . . . . 6 ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*)
8	2, 7	syl 14	. . . . 5 ⊢ (𝜑 → 𝐷:(𝑋 × 𝑋)⟶ℝ*)
9	8	ffnd 5346	. . . 4 ⊢ (𝜑 → 𝐷 Fn (𝑋 × 𝑋))
10		xmetcl 13111	. . . . . . . 8 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (𝑎𝐷𝑏) ∈ ℝ*)
11		xmetge0 13124	. . . . . . . 8 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → 0 ≤ (𝑎𝐷𝑏))
12		elxrge0 9928	. . . . . . . 8 ⊢ ((𝑎𝐷𝑏) ∈ (0[,]+∞) ↔ ((𝑎𝐷𝑏) ∈ ℝ* ∧ 0 ≤ (𝑎𝐷𝑏)))
13	10, 11, 12	sylanbrc 415	. . . . . . 7 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (𝑎𝐷𝑏) ∈ (0[,]+∞))
14	13	3expb 1199	. . . . . 6 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑎𝐷𝑏) ∈ (0[,]+∞))
15	2, 14	sylan 281	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑎𝐷𝑏) ∈ (0[,]+∞))
16	15	ralrimivva 2552	. . . 4 ⊢ (𝜑 → ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (𝑎𝐷𝑏) ∈ (0[,]+∞))
17		ffnov 5955	. . . 4 ⊢ (𝐷:(𝑋 × 𝑋)⟶(0[,]+∞) ↔ (𝐷 Fn (𝑋 × 𝑋) ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (𝑎𝐷𝑏) ∈ (0[,]+∞)))
18	9, 16, 17	sylanbrc 415	. . 3 ⊢ (𝜑 → 𝐷:(𝑋 × 𝑋)⟶(0[,]+∞))
19		fco 5361	. . 3 ⊢ ((𝐹:(0[,]+∞)⟶ℝ* ∧ 𝐷:(𝑋 × 𝑋)⟶(0[,]+∞)) → (𝐹 ∘ 𝐷):(𝑋 × 𝑋)⟶ℝ*)
20	6, 18, 19	syl2anc 409	. 2 ⊢ (𝜑 → (𝐹 ∘ 𝐷):(𝑋 × 𝑋)⟶ℝ*)
21		opelxpi 4641	. . . . . 6 ⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → ⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑋))
22		fvco3 5565	. . . . . 6 ⊢ ((𝐷:(𝑋 × 𝑋)⟶ℝ* ∧ ⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑋)) → ((𝐹 ∘ 𝐷)‘⟨𝑎, 𝑏⟩) = (𝐹‘(𝐷‘⟨𝑎, 𝑏⟩)))
23	8, 21, 22	syl2an 287	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝐹 ∘ 𝐷)‘⟨𝑎, 𝑏⟩) = (𝐹‘(𝐷‘⟨𝑎, 𝑏⟩)))
24		df-ov 5854	. . . . 5 ⊢ (𝑎(𝐹 ∘ 𝐷)𝑏) = ((𝐹 ∘ 𝐷)‘⟨𝑎, 𝑏⟩)
25		df-ov 5854	. . . . . 6 ⊢ (𝑎𝐷𝑏) = (𝐷‘⟨𝑎, 𝑏⟩)
26	25	fveq2i 5497	. . . . 5 ⊢ (𝐹‘(𝑎𝐷𝑏)) = (𝐹‘(𝐷‘⟨𝑎, 𝑏⟩))
27	23, 24, 26	3eqtr4g 2228	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑎(𝐹 ∘ 𝐷)𝑏) = (𝐹‘(𝑎𝐷𝑏)))
28	27	eqeq1d 2179	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑎(𝐹 ∘ 𝐷)𝑏) = 0 ↔ (𝐹‘(𝑎𝐷𝑏)) = 0))
29		fveq2 5494	. . . . . 6 ⊢ (𝑥 = (𝑎𝐷𝑏) → (𝐹‘𝑥) = (𝐹‘(𝑎𝐷𝑏)))
30	29	eqeq1d 2179	. . . . 5 ⊢ (𝑥 = (𝑎𝐷𝑏) → ((𝐹‘𝑥) = 0 ↔ (𝐹‘(𝑎𝐷𝑏)) = 0))
31		eqeq1 2177	. . . . 5 ⊢ (𝑥 = (𝑎𝐷𝑏) → (𝑥 = 0 ↔ (𝑎𝐷𝑏) = 0))
32	30, 31	bibi12d 234	. . . 4 ⊢ (𝑥 = (𝑎𝐷𝑏) → (((𝐹‘𝑥) = 0 ↔ 𝑥 = 0) ↔ ((𝐹‘(𝑎𝐷𝑏)) = 0 ↔ (𝑎𝐷𝑏) = 0)))
33		comet.3	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]+∞)) → ((𝐹‘𝑥) = 0 ↔ 𝑥 = 0))
34	33	ralrimiva 2543	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ (0[,]+∞)((𝐹‘𝑥) = 0 ↔ 𝑥 = 0))
35	34	adantr 274	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ∀𝑥 ∈ (0[,]+∞)((𝐹‘𝑥) = 0 ↔ 𝑥 = 0))
36	32, 35, 15	rspcdva 2839	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝐹‘(𝑎𝐷𝑏)) = 0 ↔ (𝑎𝐷𝑏) = 0))
37		xmeteq0 13118	. . . . 5 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → ((𝑎𝐷𝑏) = 0 ↔ 𝑎 = 𝑏))
38	37	3expb 1199	. . . 4 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑎𝐷𝑏) = 0 ↔ 𝑎 = 𝑏))
39	2, 38	sylan 281	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑎𝐷𝑏) = 0 ↔ 𝑎 = 𝑏))
40	28, 36, 39	3bitrd 213	. 2 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑎(𝐹 ∘ 𝐷)𝑏) = 0 ↔ 𝑎 = 𝑏))
41	6	adantr 274	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → 𝐹:(0[,]+∞)⟶ℝ*)
42	15	3adantr3 1153	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑎𝐷𝑏) ∈ (0[,]+∞))
43	41, 42	ffvelrnd 5630	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑎𝐷𝑏)) ∈ ℝ*)
44	18	adantr 274	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → 𝐷:(𝑋 × 𝑋)⟶(0[,]+∞))
45		simpr3 1000	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → 𝑐 ∈ 𝑋)
46		simpr1 998	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → 𝑎 ∈ 𝑋)
47	44, 45, 46	fovrnd 5995	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑐𝐷𝑎) ∈ (0[,]+∞))
48		simpr2 999	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → 𝑏 ∈ 𝑋)
49	44, 45, 48	fovrnd 5995	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑐𝐷𝑏) ∈ (0[,]+∞))
50		ge0xaddcl 9933	. . . . . 6 ⊢ (((𝑐𝐷𝑎) ∈ (0[,]+∞) ∧ (𝑐𝐷𝑏) ∈ (0[,]+∞)) → ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) ∈ (0[,]+∞))
51	47, 49, 50	syl2anc 409	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) ∈ (0[,]+∞))
52	41, 51	ffvelrnd 5630	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))) ∈ ℝ*)
53	41, 47	ffvelrnd 5630	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑐𝐷𝑎)) ∈ ℝ*)
54	41, 49	ffvelrnd 5630	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑐𝐷𝑏)) ∈ ℝ*)
55	53, 54	xaddcld 9834	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘(𝑐𝐷𝑏))) ∈ ℝ*)
56		3anrot 978	. . . . . . 7 ⊢ ((𝑐 ∈ 𝑋 ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ↔ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋))
57		xmettri2 13120	. . . . . . 7 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑐 ∈ 𝑋 ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑎𝐷𝑏) ≤ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)))
58	56, 57	sylan2br 286	. . . . . 6 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑎𝐷𝑏) ≤ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)))
59	2, 58	sylan 281	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑎𝐷𝑏) ≤ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)))
60		comet.4	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞))) → (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≤ (𝐹‘𝑦)))
61	60	ralrimivva 2552	. . . . . . 7 ⊢ (𝜑 → ∀𝑥 ∈ (0[,]+∞)∀𝑦 ∈ (0[,]+∞)(𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≤ (𝐹‘𝑦)))
62	61	adantr 274	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ∀𝑥 ∈ (0[,]+∞)∀𝑦 ∈ (0[,]+∞)(𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≤ (𝐹‘𝑦)))
63		breq1 3990	. . . . . . . 8 ⊢ (𝑥 = (𝑎𝐷𝑏) → (𝑥 ≤ 𝑦 ↔ (𝑎𝐷𝑏) ≤ 𝑦))
64	29	breq1d 3997	. . . . . . . 8 ⊢ (𝑥 = (𝑎𝐷𝑏) → ((𝐹‘𝑥) ≤ (𝐹‘𝑦) ↔ (𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘𝑦)))
65	63, 64	imbi12d 233	. . . . . . 7 ⊢ (𝑥 = (𝑎𝐷𝑏) → ((𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≤ (𝐹‘𝑦)) ↔ ((𝑎𝐷𝑏) ≤ 𝑦 → (𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘𝑦))))
66		breq2 3991	. . . . . . . 8 ⊢ (𝑦 = ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) → ((𝑎𝐷𝑏) ≤ 𝑦 ↔ (𝑎𝐷𝑏) ≤ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))))
67		fveq2 5494	. . . . . . . . 9 ⊢ (𝑦 = ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) → (𝐹‘𝑦) = (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))))
68	67	breq2d 3999	. . . . . . . 8 ⊢ (𝑦 = ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) → ((𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘𝑦) ↔ (𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)))))
69	66, 68	imbi12d 233	. . . . . . 7 ⊢ (𝑦 = ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) → (((𝑎𝐷𝑏) ≤ 𝑦 → (𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘𝑦)) ↔ ((𝑎𝐷𝑏) ≤ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) → (𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))))))
70	65, 69	rspc2va 2848	. . . . . 6 ⊢ ((((𝑎𝐷𝑏) ∈ (0[,]+∞) ∧ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) ∈ (0[,]+∞)) ∧ ∀𝑥 ∈ (0[,]+∞)∀𝑦 ∈ (0[,]+∞)(𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≤ (𝐹‘𝑦))) → ((𝑎𝐷𝑏) ≤ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) → (𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)))))
71	42, 51, 62, 70	syl21anc 1232	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ((𝑎𝐷𝑏) ≤ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) → (𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)))))
72	59, 71	mpd 13	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))))
73		comet.5	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞))) → (𝐹‘(𝑥 +𝑒 𝑦)) ≤ ((𝐹‘𝑥) +𝑒 (𝐹‘𝑦)))
74	73	ralrimivva 2552	. . . . . 6 ⊢ (𝜑 → ∀𝑥 ∈ (0[,]+∞)∀𝑦 ∈ (0[,]+∞)(𝐹‘(𝑥 +𝑒 𝑦)) ≤ ((𝐹‘𝑥) +𝑒 (𝐹‘𝑦)))
75	74	adantr 274	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ∀𝑥 ∈ (0[,]+∞)∀𝑦 ∈ (0[,]+∞)(𝐹‘(𝑥 +𝑒 𝑦)) ≤ ((𝐹‘𝑥) +𝑒 (𝐹‘𝑦)))
76		fvoveq1 5874	. . . . . . 7 ⊢ (𝑥 = (𝑐𝐷𝑎) → (𝐹‘(𝑥 +𝑒 𝑦)) = (𝐹‘((𝑐𝐷𝑎) +𝑒 𝑦)))
77		fveq2 5494	. . . . . . . 8 ⊢ (𝑥 = (𝑐𝐷𝑎) → (𝐹‘𝑥) = (𝐹‘(𝑐𝐷𝑎)))
78	77	oveq1d 5866	. . . . . . 7 ⊢ (𝑥 = (𝑐𝐷𝑎) → ((𝐹‘𝑥) +𝑒 (𝐹‘𝑦)) = ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘𝑦)))
79	76, 78	breq12d 4000	. . . . . 6 ⊢ (𝑥 = (𝑐𝐷𝑎) → ((𝐹‘(𝑥 +𝑒 𝑦)) ≤ ((𝐹‘𝑥) +𝑒 (𝐹‘𝑦)) ↔ (𝐹‘((𝑐𝐷𝑎) +𝑒 𝑦)) ≤ ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘𝑦))))
80		oveq2 5859	. . . . . . . 8 ⊢ (𝑦 = (𝑐𝐷𝑏) → ((𝑐𝐷𝑎) +𝑒 𝑦) = ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)))
81	80	fveq2d 5498	. . . . . . 7 ⊢ (𝑦 = (𝑐𝐷𝑏) → (𝐹‘((𝑐𝐷𝑎) +𝑒 𝑦)) = (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))))
82		fveq2 5494	. . . . . . . 8 ⊢ (𝑦 = (𝑐𝐷𝑏) → (𝐹‘𝑦) = (𝐹‘(𝑐𝐷𝑏)))
83	82	oveq2d 5867	. . . . . . 7 ⊢ (𝑦 = (𝑐𝐷𝑏) → ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘𝑦)) = ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘(𝑐𝐷𝑏))))
84	81, 83	breq12d 4000	. . . . . 6 ⊢ (𝑦 = (𝑐𝐷𝑏) → ((𝐹‘((𝑐𝐷𝑎) +𝑒 𝑦)) ≤ ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘𝑦)) ↔ (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))) ≤ ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘(𝑐𝐷𝑏)))))
85	79, 84	rspc2va 2848	. . . . 5 ⊢ ((((𝑐𝐷𝑎) ∈ (0[,]+∞) ∧ (𝑐𝐷𝑏) ∈ (0[,]+∞)) ∧ ∀𝑥 ∈ (0[,]+∞)∀𝑦 ∈ (0[,]+∞)(𝐹‘(𝑥 +𝑒 𝑦)) ≤ ((𝐹‘𝑥) +𝑒 (𝐹‘𝑦))) → (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))) ≤ ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘(𝑐𝐷𝑏))))
86	47, 49, 75, 85	syl21anc 1232	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))) ≤ ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘(𝑐𝐷𝑏))))
87	43, 52, 55, 72, 86	xrletrd 9762	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑎𝐷𝑏)) ≤ ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘(𝑐𝐷𝑏))))
88	27	3adantr3 1153	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑎(𝐹 ∘ 𝐷)𝑏) = (𝐹‘(𝑎𝐷𝑏)))
89	8	adantr 274	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → 𝐷:(𝑋 × 𝑋)⟶ℝ*)
90	45, 46	opelxpd 4642	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ⟨𝑐, 𝑎⟩ ∈ (𝑋 × 𝑋))
91		fvco3 5565	. . . . . 6 ⊢ ((𝐷:(𝑋 × 𝑋)⟶ℝ* ∧ ⟨𝑐, 𝑎⟩ ∈ (𝑋 × 𝑋)) → ((𝐹 ∘ 𝐷)‘⟨𝑐, 𝑎⟩) = (𝐹‘(𝐷‘⟨𝑐, 𝑎⟩)))
92	89, 90, 91	syl2anc 409	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ((𝐹 ∘ 𝐷)‘⟨𝑐, 𝑎⟩) = (𝐹‘(𝐷‘⟨𝑐, 𝑎⟩)))
93		df-ov 5854	. . . . 5 ⊢ (𝑐(𝐹 ∘ 𝐷)𝑎) = ((𝐹 ∘ 𝐷)‘⟨𝑐, 𝑎⟩)
94		df-ov 5854	. . . . . 6 ⊢ (𝑐𝐷𝑎) = (𝐷‘⟨𝑐, 𝑎⟩)
95	94	fveq2i 5497	. . . . 5 ⊢ (𝐹‘(𝑐𝐷𝑎)) = (𝐹‘(𝐷‘⟨𝑐, 𝑎⟩))
96	92, 93, 95	3eqtr4g 2228	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑐(𝐹 ∘ 𝐷)𝑎) = (𝐹‘(𝑐𝐷𝑎)))
97	45, 48	opelxpd 4642	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ⟨𝑐, 𝑏⟩ ∈ (𝑋 × 𝑋))
98		fvco3 5565	. . . . . 6 ⊢ ((𝐷:(𝑋 × 𝑋)⟶ℝ* ∧ ⟨𝑐, 𝑏⟩ ∈ (𝑋 × 𝑋)) → ((𝐹 ∘ 𝐷)‘⟨𝑐, 𝑏⟩) = (𝐹‘(𝐷‘⟨𝑐, 𝑏⟩)))
99	89, 97, 98	syl2anc 409	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ((𝐹 ∘ 𝐷)‘⟨𝑐, 𝑏⟩) = (𝐹‘(𝐷‘⟨𝑐, 𝑏⟩)))
100		df-ov 5854	. . . . 5 ⊢ (𝑐(𝐹 ∘ 𝐷)𝑏) = ((𝐹 ∘ 𝐷)‘⟨𝑐, 𝑏⟩)
101		df-ov 5854	. . . . . 6 ⊢ (𝑐𝐷𝑏) = (𝐷‘⟨𝑐, 𝑏⟩)
102	101	fveq2i 5497	. . . . 5 ⊢ (𝐹‘(𝑐𝐷𝑏)) = (𝐹‘(𝐷‘⟨𝑐, 𝑏⟩))
103	99, 100, 102	3eqtr4g 2228	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑐(𝐹 ∘ 𝐷)𝑏) = (𝐹‘(𝑐𝐷𝑏)))
104	96, 103	oveq12d 5869	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ((𝑐(𝐹 ∘ 𝐷)𝑎) +𝑒 (𝑐(𝐹 ∘ 𝐷)𝑏)) = ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘(𝑐𝐷𝑏))))
105	87, 88, 104	3brtr4d 4019	. 2 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑎(𝐹 ∘ 𝐷)𝑏) ≤ ((𝑐(𝐹 ∘ 𝐷)𝑎) +𝑒 (𝑐(𝐹 ∘ 𝐷)𝑏)))
106	5, 20, 40, 105	isxmetd 13106	1 ⊢ (𝜑 → (𝐹 ∘ 𝐷) ∈ (∞Met‘𝑋))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∧ w3a 973   = wceq 1348   ∈ wcel 2141  ∀wral 2448  ⟨cop 3584   class class class wbr 3987   × cxp 4607  dom cdm 4609   ∘ ccom 4613  Rel wrel 4614   Fn wfn 5191  ⟶wf 5192  ‘cfv 5196  (class class class)co 5851  0cc0 7767  +∞cpnf 7944  ℝ^*cxr 7946   ≤ cle 7948   +_𝑒 cxad 9720  [,]cicc 9841  ∞Metcxmet 12739

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-sep 4105  ax-pow 4158  ax-pr 4192  ax-un 4416  ax-setind 4519  ax-cnex 7858  ax-resscn 7859  ax-1cn 7860  ax-1re 7861  ax-icn 7862  ax-addcl 7863  ax-addrcl 7864  ax-mulcl 7865  ax-mulrcl 7866  ax-addcom 7867  ax-mulcom 7868  ax-addass 7869  ax-mulass 7870  ax-distr 7871  ax-i2m1 7872  ax-0lt1 7873  ax-1rid 7874  ax-0id 7875  ax-rnegex 7876  ax-precex 7877  ax-cnre 7878  ax-pre-ltirr 7879  ax-pre-ltwlin 7880  ax-pre-lttrn 7881  ax-pre-apti 7882  ax-pre-ltadd 7883  ax-pre-mulgt0 7884

This theorem depends on definitions:  df-bi 116  df-dc 830  df-3or 974  df-3an 975  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-nel 2436  df-ral 2453  df-rex 2454  df-reu 2455  df-rab 2457  df-v 2732  df-sbc 2956  df-csb 3050  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-if 3526  df-pw 3566  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3795  df-iun 3873  df-br 3988  df-opab 4049  df-mpt 4050  df-id 4276  df-po 4279  df-iso 4280  df-xp 4615  df-rel 4616  df-cnv 4617  df-co 4618  df-dm 4619  df-rn 4620  df-res 4621  df-ima 4622  df-iota 5158  df-fun 5198  df-fn 5199  df-f 5200  df-fv 5204  df-riota 5807  df-ov 5854  df-oprab 5855  df-mpo 5856  df-1st 6117  df-2nd 6118  df-map 6626  df-pnf 7949  df-mnf 7950  df-xr 7951  df-ltxr 7952  df-le 7953  df-sub 8085  df-neg 8086  df-2 8930  df-xadd 9723  df-icc 9845  df-xmet 12747

This theorem is referenced by:  bdxmet  13260