Theorem comet 13040

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 12884	. . . 4 ⊢ Rel ∞Met
2		comet.1	. . . 4 ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))
3		relelfvdm 5512	. . . 4 ⊢ ((Rel ∞Met ∧ 𝐷 ∈ (∞Met‘𝑋)) → 𝑋 ∈ dom ∞Met)
4	1, 2, 3	sylancr 411	. . 3 ⊢ (𝜑 → 𝑋 ∈ dom ∞Met)
5	4	elexd 2734	. 2 ⊢ (𝜑 → 𝑋 ∈ V)
6		comet.2	. . 3 ⊢ (𝜑 → 𝐹:(0[,]+∞)⟶ℝ*)
7		xmetf 12891	. . . . . 6 ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*)
8	2, 7	syl 14	. . . . 5 ⊢ (𝜑 → 𝐷:(𝑋 × 𝑋)⟶ℝ*)
9	8	ffnd 5332	. . . 4 ⊢ (𝜑 → 𝐷 Fn (𝑋 × 𝑋))
10		xmetcl 12893	. . . . . . . 8 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (𝑎𝐷𝑏) ∈ ℝ*)
11		xmetge0 12906	. . . . . . . 8 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → 0 ≤ (𝑎𝐷𝑏))
12		elxrge0 9905	. . . . . . . 8 ⊢ ((𝑎𝐷𝑏) ∈ (0[,]+∞) ↔ ((𝑎𝐷𝑏) ∈ ℝ* ∧ 0 ≤ (𝑎𝐷𝑏)))
13	10, 11, 12	sylanbrc 414	. . . . . . 7 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (𝑎𝐷𝑏) ∈ (0[,]+∞))
14	13	3expb 1193	. . . . . 6 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑎𝐷𝑏) ∈ (0[,]+∞))
15	2, 14	sylan 281	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑎𝐷𝑏) ∈ (0[,]+∞))
16	15	ralrimivva 2546	. . . 4 ⊢ (𝜑 → ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (𝑎𝐷𝑏) ∈ (0[,]+∞))
17		ffnov 5937	. . . 4 ⊢ (𝐷:(𝑋 × 𝑋)⟶(0[,]+∞) ↔ (𝐷 Fn (𝑋 × 𝑋) ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (𝑎𝐷𝑏) ∈ (0[,]+∞)))
18	9, 16, 17	sylanbrc 414	. . 3 ⊢ (𝜑 → 𝐷:(𝑋 × 𝑋)⟶(0[,]+∞))
19		fco 5347	. . 3 ⊢ ((𝐹:(0[,]+∞)⟶ℝ* ∧ 𝐷:(𝑋 × 𝑋)⟶(0[,]+∞)) → (𝐹 ∘ 𝐷):(𝑋 × 𝑋)⟶ℝ*)
20	6, 18, 19	syl2anc 409	. 2 ⊢ (𝜑 → (𝐹 ∘ 𝐷):(𝑋 × 𝑋)⟶ℝ*)
21		opelxpi 4630	. . . . . 6 ⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → ⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑋))
22		fvco3 5551	. . . . . 6 ⊢ ((𝐷:(𝑋 × 𝑋)⟶ℝ* ∧ ⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑋)) → ((𝐹 ∘ 𝐷)‘⟨𝑎, 𝑏⟩) = (𝐹‘(𝐷‘⟨𝑎, 𝑏⟩)))
23	8, 21, 22	syl2an 287	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝐹 ∘ 𝐷)‘⟨𝑎, 𝑏⟩) = (𝐹‘(𝐷‘⟨𝑎, 𝑏⟩)))
24		df-ov 5839	. . . . 5 ⊢ (𝑎(𝐹 ∘ 𝐷)𝑏) = ((𝐹 ∘ 𝐷)‘⟨𝑎, 𝑏⟩)
25		df-ov 5839	. . . . . 6 ⊢ (𝑎𝐷𝑏) = (𝐷‘⟨𝑎, 𝑏⟩)
26	25	fveq2i 5483	. . . . 5 ⊢ (𝐹‘(𝑎𝐷𝑏)) = (𝐹‘(𝐷‘⟨𝑎, 𝑏⟩))
27	23, 24, 26	3eqtr4g 2222	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑎(𝐹 ∘ 𝐷)𝑏) = (𝐹‘(𝑎𝐷𝑏)))
28	27	eqeq1d 2173	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑎(𝐹 ∘ 𝐷)𝑏) = 0 ↔ (𝐹‘(𝑎𝐷𝑏)) = 0))
29		fveq2 5480	. . . . . 6 ⊢ (𝑥 = (𝑎𝐷𝑏) → (𝐹‘𝑥) = (𝐹‘(𝑎𝐷𝑏)))
30	29	eqeq1d 2173	. . . . 5 ⊢ (𝑥 = (𝑎𝐷𝑏) → ((𝐹‘𝑥) = 0 ↔ (𝐹‘(𝑎𝐷𝑏)) = 0))
31		eqeq1 2171	. . . . 5 ⊢ (𝑥 = (𝑎𝐷𝑏) → (𝑥 = 0 ↔ (𝑎𝐷𝑏) = 0))
32	30, 31	bibi12d 234	. . . 4 ⊢ (𝑥 = (𝑎𝐷𝑏) → (((𝐹‘𝑥) = 0 ↔ 𝑥 = 0) ↔ ((𝐹‘(𝑎𝐷𝑏)) = 0 ↔ (𝑎𝐷𝑏) = 0)))
33		comet.3	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]+∞)) → ((𝐹‘𝑥) = 0 ↔ 𝑥 = 0))
34	33	ralrimiva 2537	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ (0[,]+∞)((𝐹‘𝑥) = 0 ↔ 𝑥 = 0))
35	34	adantr 274	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ∀𝑥 ∈ (0[,]+∞)((𝐹‘𝑥) = 0 ↔ 𝑥 = 0))
36	32, 35, 15	rspcdva 2830	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝐹‘(𝑎𝐷𝑏)) = 0 ↔ (𝑎𝐷𝑏) = 0))
37		xmeteq0 12900	. . . . 5 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → ((𝑎𝐷𝑏) = 0 ↔ 𝑎 = 𝑏))
38	37	3expb 1193	. . . 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 1147	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑎𝐷𝑏) ∈ (0[,]+∞))
43	41, 42	ffvelrnd 5615	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑎𝐷𝑏)) ∈ ℝ*)
44	18	adantr 274	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → 𝐷:(𝑋 × 𝑋)⟶(0[,]+∞))
45		simpr3 994	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → 𝑐 ∈ 𝑋)
46		simpr1 992	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → 𝑎 ∈ 𝑋)
47	44, 45, 46	fovrnd 5977	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑐𝐷𝑎) ∈ (0[,]+∞))
48		simpr2 993	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → 𝑏 ∈ 𝑋)
49	44, 45, 48	fovrnd 5977	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑐𝐷𝑏) ∈ (0[,]+∞))
50		ge0xaddcl 9910	. . . . . 6 ⊢ (((𝑐𝐷𝑎) ∈ (0[,]+∞) ∧ (𝑐𝐷𝑏) ∈ (0[,]+∞)) → ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) ∈ (0[,]+∞))
51	47, 49, 50	syl2anc 409	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) ∈ (0[,]+∞))
52	41, 51	ffvelrnd 5615	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))) ∈ ℝ*)
53	41, 47	ffvelrnd 5615	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑐𝐷𝑎)) ∈ ℝ*)
54	41, 49	ffvelrnd 5615	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑐𝐷𝑏)) ∈ ℝ*)
55	53, 54	xaddcld 9811	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘(𝑐𝐷𝑏))) ∈ ℝ*)
56		3anrot 972	. . . . . . 7 ⊢ ((𝑐 ∈ 𝑋 ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ↔ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋))
57		xmettri2 12902	. . . . . . 7 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑐 ∈ 𝑋 ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑎𝐷𝑏) ≤ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)))
58	56, 57	sylan2br 286	. . . . . 6 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑎𝐷𝑏) ≤ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)))
59	2, 58	sylan 281	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑎𝐷𝑏) ≤ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)))
60		comet.4	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞))) → (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≤ (𝐹‘𝑦)))
61	60	ralrimivva 2546	. . . . . . 7 ⊢ (𝜑 → ∀𝑥 ∈ (0[,]+∞)∀𝑦 ∈ (0[,]+∞)(𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≤ (𝐹‘𝑦)))
62	61	adantr 274	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ∀𝑥 ∈ (0[,]+∞)∀𝑦 ∈ (0[,]+∞)(𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≤ (𝐹‘𝑦)))
63		breq1 3979	. . . . . . . 8 ⊢ (𝑥 = (𝑎𝐷𝑏) → (𝑥 ≤ 𝑦 ↔ (𝑎𝐷𝑏) ≤ 𝑦))
64	29	breq1d 3986	. . . . . . . 8 ⊢ (𝑥 = (𝑎𝐷𝑏) → ((𝐹‘𝑥) ≤ (𝐹‘𝑦) ↔ (𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘𝑦)))
65	63, 64	imbi12d 233	. . . . . . 7 ⊢ (𝑥 = (𝑎𝐷𝑏) → ((𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≤ (𝐹‘𝑦)) ↔ ((𝑎𝐷𝑏) ≤ 𝑦 → (𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘𝑦))))
66		breq2 3980	. . . . . . . 8 ⊢ (𝑦 = ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) → ((𝑎𝐷𝑏) ≤ 𝑦 ↔ (𝑎𝐷𝑏) ≤ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))))
67		fveq2 5480	. . . . . . . . 9 ⊢ (𝑦 = ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) → (𝐹‘𝑦) = (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))))
68	67	breq2d 3988	. . . . . . . 8 ⊢ (𝑦 = ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) → ((𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘𝑦) ↔ (𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)))))
69	66, 68	imbi12d 233	. . . . . . 7 ⊢ (𝑦 = ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) → (((𝑎𝐷𝑏) ≤ 𝑦 → (𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘𝑦)) ↔ ((𝑎𝐷𝑏) ≤ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) → (𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))))))
70	65, 69	rspc2va 2839	. . . . . 6 ⊢ ((((𝑎𝐷𝑏) ∈ (0[,]+∞) ∧ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) ∈ (0[,]+∞)) ∧ ∀𝑥 ∈ (0[,]+∞)∀𝑦 ∈ (0[,]+∞)(𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≤ (𝐹‘𝑦))) → ((𝑎𝐷𝑏) ≤ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) → (𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)))))
71	42, 51, 62, 70	syl21anc 1226	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ((𝑎𝐷𝑏) ≤ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) → (𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)))))
72	59, 71	mpd 13	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))))
73		comet.5	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞))) → (𝐹‘(𝑥 +𝑒 𝑦)) ≤ ((𝐹‘𝑥) +𝑒 (𝐹‘𝑦)))
74	73	ralrimivva 2546	. . . . . 6 ⊢ (𝜑 → ∀𝑥 ∈ (0[,]+∞)∀𝑦 ∈ (0[,]+∞)(𝐹‘(𝑥 +𝑒 𝑦)) ≤ ((𝐹‘𝑥) +𝑒 (𝐹‘𝑦)))
75	74	adantr 274	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ∀𝑥 ∈ (0[,]+∞)∀𝑦 ∈ (0[,]+∞)(𝐹‘(𝑥 +𝑒 𝑦)) ≤ ((𝐹‘𝑥) +𝑒 (𝐹‘𝑦)))
76		fvoveq1 5859	. . . . . . 7 ⊢ (𝑥 = (𝑐𝐷𝑎) → (𝐹‘(𝑥 +𝑒 𝑦)) = (𝐹‘((𝑐𝐷𝑎) +𝑒 𝑦)))
77		fveq2 5480	. . . . . . . 8 ⊢ (𝑥 = (𝑐𝐷𝑎) → (𝐹‘𝑥) = (𝐹‘(𝑐𝐷𝑎)))
78	77	oveq1d 5851	. . . . . . 7 ⊢ (𝑥 = (𝑐𝐷𝑎) → ((𝐹‘𝑥) +𝑒 (𝐹‘𝑦)) = ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘𝑦)))
79	76, 78	breq12d 3989	. . . . . 6 ⊢ (𝑥 = (𝑐𝐷𝑎) → ((𝐹‘(𝑥 +𝑒 𝑦)) ≤ ((𝐹‘𝑥) +𝑒 (𝐹‘𝑦)) ↔ (𝐹‘((𝑐𝐷𝑎) +𝑒 𝑦)) ≤ ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘𝑦))))
80		oveq2 5844	. . . . . . . 8 ⊢ (𝑦 = (𝑐𝐷𝑏) → ((𝑐𝐷𝑎) +𝑒 𝑦) = ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)))
81	80	fveq2d 5484	. . . . . . 7 ⊢ (𝑦 = (𝑐𝐷𝑏) → (𝐹‘((𝑐𝐷𝑎) +𝑒 𝑦)) = (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))))
82		fveq2 5480	. . . . . . . 8 ⊢ (𝑦 = (𝑐𝐷𝑏) → (𝐹‘𝑦) = (𝐹‘(𝑐𝐷𝑏)))
83	82	oveq2d 5852	. . . . . . 7 ⊢ (𝑦 = (𝑐𝐷𝑏) → ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘𝑦)) = ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘(𝑐𝐷𝑏))))
84	81, 83	breq12d 3989	. . . . . 6 ⊢ (𝑦 = (𝑐𝐷𝑏) → ((𝐹‘((𝑐𝐷𝑎) +𝑒 𝑦)) ≤ ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘𝑦)) ↔ (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))) ≤ ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘(𝑐𝐷𝑏)))))
85	79, 84	rspc2va 2839	. . . . 5 ⊢ ((((𝑐𝐷𝑎) ∈ (0[,]+∞) ∧ (𝑐𝐷𝑏) ∈ (0[,]+∞)) ∧ ∀𝑥 ∈ (0[,]+∞)∀𝑦 ∈ (0[,]+∞)(𝐹‘(𝑥 +𝑒 𝑦)) ≤ ((𝐹‘𝑥) +𝑒 (𝐹‘𝑦))) → (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))) ≤ ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘(𝑐𝐷𝑏))))
86	47, 49, 75, 85	syl21anc 1226	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))) ≤ ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘(𝑐𝐷𝑏))))
87	43, 52, 55, 72, 86	xrletrd 9739	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑎𝐷𝑏)) ≤ ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘(𝑐𝐷𝑏))))
88	27	3adantr3 1147	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑎(𝐹 ∘ 𝐷)𝑏) = (𝐹‘(𝑎𝐷𝑏)))
89	8	adantr 274	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → 𝐷:(𝑋 × 𝑋)⟶ℝ*)
90	45, 46	opelxpd 4631	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ⟨𝑐, 𝑎⟩ ∈ (𝑋 × 𝑋))
91		fvco3 5551	. . . . . 6 ⊢ ((𝐷:(𝑋 × 𝑋)⟶ℝ* ∧ ⟨𝑐, 𝑎⟩ ∈ (𝑋 × 𝑋)) → ((𝐹 ∘ 𝐷)‘⟨𝑐, 𝑎⟩) = (𝐹‘(𝐷‘⟨𝑐, 𝑎⟩)))
92	89, 90, 91	syl2anc 409	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ((𝐹 ∘ 𝐷)‘⟨𝑐, 𝑎⟩) = (𝐹‘(𝐷‘⟨𝑐, 𝑎⟩)))
93		df-ov 5839	. . . . 5 ⊢ (𝑐(𝐹 ∘ 𝐷)𝑎) = ((𝐹 ∘ 𝐷)‘⟨𝑐, 𝑎⟩)
94		df-ov 5839	. . . . . 6 ⊢ (𝑐𝐷𝑎) = (𝐷‘⟨𝑐, 𝑎⟩)
95	94	fveq2i 5483	. . . . 5 ⊢ (𝐹‘(𝑐𝐷𝑎)) = (𝐹‘(𝐷‘⟨𝑐, 𝑎⟩))
96	92, 93, 95	3eqtr4g 2222	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑐(𝐹 ∘ 𝐷)𝑎) = (𝐹‘(𝑐𝐷𝑎)))
97	45, 48	opelxpd 4631	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ⟨𝑐, 𝑏⟩ ∈ (𝑋 × 𝑋))
98		fvco3 5551	. . . . . 6 ⊢ ((𝐷:(𝑋 × 𝑋)⟶ℝ* ∧ ⟨𝑐, 𝑏⟩ ∈ (𝑋 × 𝑋)) → ((𝐹 ∘ 𝐷)‘⟨𝑐, 𝑏⟩) = (𝐹‘(𝐷‘⟨𝑐, 𝑏⟩)))
99	89, 97, 98	syl2anc 409	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ((𝐹 ∘ 𝐷)‘⟨𝑐, 𝑏⟩) = (𝐹‘(𝐷‘⟨𝑐, 𝑏⟩)))
100		df-ov 5839	. . . . 5 ⊢ (𝑐(𝐹 ∘ 𝐷)𝑏) = ((𝐹 ∘ 𝐷)‘⟨𝑐, 𝑏⟩)
101		df-ov 5839	. . . . . 6 ⊢ (𝑐𝐷𝑏) = (𝐷‘⟨𝑐, 𝑏⟩)
102	101	fveq2i 5483	. . . . 5 ⊢ (𝐹‘(𝑐𝐷𝑏)) = (𝐹‘(𝐷‘⟨𝑐, 𝑏⟩))
103	99, 100, 102	3eqtr4g 2222	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑐(𝐹 ∘ 𝐷)𝑏) = (𝐹‘(𝑐𝐷𝑏)))
104	96, 103	oveq12d 5854	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ((𝑐(𝐹 ∘ 𝐷)𝑎) +𝑒 (𝑐(𝐹 ∘ 𝐷)𝑏)) = ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘(𝑐𝐷𝑏))))
105	87, 88, 104	3brtr4d 4008	. 2 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑎(𝐹 ∘ 𝐷)𝑏) ≤ ((𝑐(𝐹 ∘ 𝐷)𝑎) +𝑒 (𝑐(𝐹 ∘ 𝐷)𝑏)))
106	5, 20, 40, 105	isxmetd 12888	1 ⊢ (𝜑 → (𝐹 ∘ 𝐷) ∈ (∞Met‘𝑋))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∧ w3a 967   = wceq 1342   ∈ wcel 2135  ∀wral 2442  ⟨cop 3573   class class class wbr 3976   × cxp 4596  dom cdm 4598   ∘ ccom 4602  Rel wrel 4603   Fn wfn 5177  ⟶wf 5178  ‘cfv 5182  (class class class)co 5836  0cc0 7744  +∞cpnf 7921  ℝ^*cxr 7923   ≤ cle 7925   +_𝑒 cxad 9697  [,]cicc 9818  ∞Metcxmet 12521

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 604  ax-in2 605  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-13 2137  ax-14 2138  ax-ext 2146  ax-sep 4094  ax-pow 4147  ax-pr 4181  ax-un 4405  ax-setind 4508  ax-cnex 7835  ax-resscn 7836  ax-1cn 7837  ax-1re 7838  ax-icn 7839  ax-addcl 7840  ax-addrcl 7841  ax-mulcl 7842  ax-mulrcl 7843  ax-addcom 7844  ax-mulcom 7845  ax-addass 7846  ax-mulass 7847  ax-distr 7848  ax-i2m1 7849  ax-0lt1 7850  ax-1rid 7851  ax-0id 7852  ax-rnegex 7853  ax-precex 7854  ax-cnre 7855  ax-pre-ltirr 7856  ax-pre-ltwlin 7857  ax-pre-lttrn 7858  ax-pre-apti 7859  ax-pre-ltadd 7860  ax-pre-mulgt0 7861

This theorem depends on definitions:  df-bi 116  df-dc 825  df-3or 968  df-3an 969  df-tru 1345  df-fal 1348  df-nf 1448  df-sb 1750  df-eu 2016  df-mo 2017  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-ne 2335  df-nel 2430  df-ral 2447  df-rex 2448  df-reu 2449  df-rab 2451  df-v 2723  df-sbc 2947  df-csb 3041  df-dif 3113  df-un 3115  df-in 3117  df-ss 3124  df-if 3516  df-pw 3555  df-sn 3576  df-pr 3577  df-op 3579  df-uni 3784  df-iun 3862  df-br 3977  df-opab 4038  df-mpt 4039  df-id 4265  df-po 4268  df-iso 4269  df-xp 4604  df-rel 4605  df-cnv 4606  df-co 4607  df-dm 4608  df-rn 4609  df-res 4610  df-ima 4611  df-iota 5147  df-fun 5184  df-fn 5185  df-f 5186  df-fv 5190  df-riota 5792  df-ov 5839  df-oprab 5840  df-mpo 5841  df-1st 6100  df-2nd 6101  df-map 6607  df-pnf 7926  df-mnf 7927  df-xr 7928  df-ltxr 7929  df-le 7930  df-sub 8062  df-neg 8063  df-2 8907  df-xadd 9700  df-icc 9822  df-xmet 12529

This theorem is referenced by:  bdxmet  13042