Theorem comet 15583

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 15427	. . . 4 ⊢ Rel ∞Met
2		comet.1	. . . 4 ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))
3		relelfvdm 5725	. . . 4 ⊢ ((Rel ∞Met ∧ 𝐷 ∈ (∞Met‘𝑋)) → 𝑋 ∈ dom ∞Met)
4	1, 2, 3	sylancr 418	. . 3 ⊢ (𝜑 → 𝑋 ∈ dom ∞Met)
5	4	elexd 2835	. 2 ⊢ (𝜑 → 𝑋 ∈ V)
6		comet.2	. . 3 ⊢ (𝜑 → 𝐹:(0[,]+∞)⟶ℝ*)
7		xmetf 15434	. . . . . 6 ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*)
8	2, 7	syl 14	. . . . 5 ⊢ (𝜑 → 𝐷:(𝑋 × 𝑋)⟶ℝ*)
9	8	ffnd 5532	. . . 4 ⊢ (𝜑 → 𝐷 Fn (𝑋 × 𝑋))
10		xmetcl 15436	. . . . . . . 8 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (𝑎𝐷𝑏) ∈ ℝ*)
11		xmetge0 15449	. . . . . . . 8 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → 0 ≤ (𝑎𝐷𝑏))
12		elxrge0 10363	. . . . . . . 8 ⊢ ((𝑎𝐷𝑏) ∈ (0[,]+∞) ↔ ((𝑎𝐷𝑏) ∈ ℝ* ∧ 0 ≤ (𝑎𝐷𝑏)))
13	10, 11, 12	sylanbrc 421	. . . . . . 7 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (𝑎𝐷𝑏) ∈ (0[,]+∞))
14	13	3expb 1235	. . . . . 6 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑎𝐷𝑏) ∈ (0[,]+∞))
15	2, 14	sylan 283	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑎𝐷𝑏) ∈ (0[,]+∞))
16	15	ralrimivva 2632	. . . 4 ⊢ (𝜑 → ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (𝑎𝐷𝑏) ∈ (0[,]+∞))
17		ffnov 6186	. . . 4 ⊢ (𝐷:(𝑋 × 𝑋)⟶(0[,]+∞) ↔ (𝐷 Fn (𝑋 × 𝑋) ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (𝑎𝐷𝑏) ∈ (0[,]+∞)))
18	9, 16, 17	sylanbrc 421	. . 3 ⊢ (𝜑 → 𝐷:(𝑋 × 𝑋)⟶(0[,]+∞))
19		fco 5550	. . 3 ⊢ ((𝐹:(0[,]+∞)⟶ℝ* ∧ 𝐷:(𝑋 × 𝑋)⟶(0[,]+∞)) → (𝐹 ∘ 𝐷):(𝑋 × 𝑋)⟶ℝ*)
20	6, 18, 19	syl2anc 415	. 2 ⊢ (𝜑 → (𝐹 ∘ 𝐷):(𝑋 × 𝑋)⟶ℝ*)
21		opelxpi 4804	. . . . . 6 ⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → ⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑋))
22		fvco3 5773	. . . . . 6 ⊢ ((𝐷:(𝑋 × 𝑋)⟶ℝ* ∧ ⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑋)) → ((𝐹 ∘ 𝐷)‘⟨𝑎, 𝑏⟩) = (𝐹‘(𝐷‘⟨𝑎, 𝑏⟩)))
23	8, 21, 22	syl2an 289	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝐹 ∘ 𝐷)‘⟨𝑎, 𝑏⟩) = (𝐹‘(𝐷‘⟨𝑎, 𝑏⟩)))
24		df-ov 6082	. . . . 5 ⊢ (𝑎(𝐹 ∘ 𝐷)𝑏) = ((𝐹 ∘ 𝐷)‘⟨𝑎, 𝑏⟩)
25		df-ov 6082	. . . . . 6 ⊢ (𝑎𝐷𝑏) = (𝐷‘⟨𝑎, 𝑏⟩)
26	25	fveq2i 5696	. . . . 5 ⊢ (𝐹‘(𝑎𝐷𝑏)) = (𝐹‘(𝐷‘⟨𝑎, 𝑏⟩))
27	23, 24, 26	3eqtr4g 2296	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑎(𝐹 ∘ 𝐷)𝑏) = (𝐹‘(𝑎𝐷𝑏)))
28	27	eqeq1d 2247	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑎(𝐹 ∘ 𝐷)𝑏) = 0 ↔ (𝐹‘(𝑎𝐷𝑏)) = 0))
29		fveq2 5693	. . . . . 6 ⊢ (𝑥 = (𝑎𝐷𝑏) → (𝐹‘𝑥) = (𝐹‘(𝑎𝐷𝑏)))
30	29	eqeq1d 2247	. . . . 5 ⊢ (𝑥 = (𝑎𝐷𝑏) → ((𝐹‘𝑥) = 0 ↔ (𝐹‘(𝑎𝐷𝑏)) = 0))
31		eqeq1 2245	. . . . 5 ⊢ (𝑥 = (𝑎𝐷𝑏) → (𝑥 = 0 ↔ (𝑎𝐷𝑏) = 0))
32	30, 31	bibi12d 235	. . . 4 ⊢ (𝑥 = (𝑎𝐷𝑏) → (((𝐹‘𝑥) = 0 ↔ 𝑥 = 0) ↔ ((𝐹‘(𝑎𝐷𝑏)) = 0 ↔ (𝑎𝐷𝑏) = 0)))
33		comet.3	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]+∞)) → ((𝐹‘𝑥) = 0 ↔ 𝑥 = 0))
34	33	ralrimiva 2623	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ (0[,]+∞)((𝐹‘𝑥) = 0 ↔ 𝑥 = 0))
35	34	adantr 276	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ∀𝑥 ∈ (0[,]+∞)((𝐹‘𝑥) = 0 ↔ 𝑥 = 0))
36	32, 35, 15	rspcdva 2934	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝐹‘(𝑎𝐷𝑏)) = 0 ↔ (𝑎𝐷𝑏) = 0))
37		xmeteq0 15443	. . . . 5 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → ((𝑎𝐷𝑏) = 0 ↔ 𝑎 = 𝑏))
38	37	3expb 1235	. . . 4 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑎𝐷𝑏) = 0 ↔ 𝑎 = 𝑏))
39	2, 38	sylan 283	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑎𝐷𝑏) = 0 ↔ 𝑎 = 𝑏))
40	28, 36, 39	3bitrd 214	. 2 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑎(𝐹 ∘ 𝐷)𝑏) = 0 ↔ 𝑎 = 𝑏))
41	6	adantr 276	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → 𝐹:(0[,]+∞)⟶ℝ*)
42	15	3adantr3 1189	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑎𝐷𝑏) ∈ (0[,]+∞))
43	41, 42	ffvelcdmd 5838	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑎𝐷𝑏)) ∈ ℝ*)
44	18	adantr 276	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → 𝐷:(𝑋 × 𝑋)⟶(0[,]+∞))
45		simpr3 1036	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → 𝑐 ∈ 𝑋)
46		simpr1 1034	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → 𝑎 ∈ 𝑋)
47	44, 45, 46	fovcdmd 6228	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑐𝐷𝑎) ∈ (0[,]+∞))
48		simpr2 1035	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → 𝑏 ∈ 𝑋)
49	44, 45, 48	fovcdmd 6228	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑐𝐷𝑏) ∈ (0[,]+∞))
50		ge0xaddcl 10368	. . . . . 6 ⊢ (((𝑐𝐷𝑎) ∈ (0[,]+∞) ∧ (𝑐𝐷𝑏) ∈ (0[,]+∞)) → ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) ∈ (0[,]+∞))
51	47, 49, 50	syl2anc 415	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) ∈ (0[,]+∞))
52	41, 51	ffvelcdmd 5838	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))) ∈ ℝ*)
53	41, 47	ffvelcdmd 5838	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑐𝐷𝑎)) ∈ ℝ*)
54	41, 49	ffvelcdmd 5838	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑐𝐷𝑏)) ∈ ℝ*)
55	53, 54	xaddcld 10269	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘(𝑐𝐷𝑏))) ∈ ℝ*)
56		3anrot 1014	. . . . . . 7 ⊢ ((𝑐 ∈ 𝑋 ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ↔ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋))
57		xmettri2 15445	. . . . . . 7 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑐 ∈ 𝑋 ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑎𝐷𝑏) ≤ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)))
58	56, 57	sylan2br 288	. . . . . 6 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑎𝐷𝑏) ≤ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)))
59	2, 58	sylan 283	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑎𝐷𝑏) ≤ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)))
60		comet.4	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞))) → (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≤ (𝐹‘𝑦)))
61	60	ralrimivva 2632	. . . . . . 7 ⊢ (𝜑 → ∀𝑥 ∈ (0[,]+∞)∀𝑦 ∈ (0[,]+∞)(𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≤ (𝐹‘𝑦)))
62	61	adantr 276	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ∀𝑥 ∈ (0[,]+∞)∀𝑦 ∈ (0[,]+∞)(𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≤ (𝐹‘𝑦)))
63		breq1 4131	. . . . . . . 8 ⊢ (𝑥 = (𝑎𝐷𝑏) → (𝑥 ≤ 𝑦 ↔ (𝑎𝐷𝑏) ≤ 𝑦))
64	29	breq1d 4138	. . . . . . . 8 ⊢ (𝑥 = (𝑎𝐷𝑏) → ((𝐹‘𝑥) ≤ (𝐹‘𝑦) ↔ (𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘𝑦)))
65	63, 64	imbi12d 234	. . . . . . 7 ⊢ (𝑥 = (𝑎𝐷𝑏) → ((𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≤ (𝐹‘𝑦)) ↔ ((𝑎𝐷𝑏) ≤ 𝑦 → (𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘𝑦))))
66		breq2 4132	. . . . . . . 8 ⊢ (𝑦 = ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) → ((𝑎𝐷𝑏) ≤ 𝑦 ↔ (𝑎𝐷𝑏) ≤ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))))
67		fveq2 5693	. . . . . . . . 9 ⊢ (𝑦 = ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) → (𝐹‘𝑦) = (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))))
68	67	breq2d 4140	. . . . . . . 8 ⊢ (𝑦 = ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) → ((𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘𝑦) ↔ (𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)))))
69	66, 68	imbi12d 234	. . . . . . 7 ⊢ (𝑦 = ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) → (((𝑎𝐷𝑏) ≤ 𝑦 → (𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘𝑦)) ↔ ((𝑎𝐷𝑏) ≤ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) → (𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))))))
70	65, 69	rspc2va 2944	. . . . . 6 ⊢ ((((𝑎𝐷𝑏) ∈ (0[,]+∞) ∧ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) ∈ (0[,]+∞)) ∧ ∀𝑥 ∈ (0[,]+∞)∀𝑦 ∈ (0[,]+∞)(𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≤ (𝐹‘𝑦))) → ((𝑎𝐷𝑏) ≤ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) → (𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)))))
71	42, 51, 62, 70	syl21anc 1277	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ((𝑎𝐷𝑏) ≤ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) → (𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)))))
72	59, 71	mpd 13	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))))
73		comet.5	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞))) → (𝐹‘(𝑥 +𝑒 𝑦)) ≤ ((𝐹‘𝑥) +𝑒 (𝐹‘𝑦)))
74	73	ralrimivva 2632	. . . . . 6 ⊢ (𝜑 → ∀𝑥 ∈ (0[,]+∞)∀𝑦 ∈ (0[,]+∞)(𝐹‘(𝑥 +𝑒 𝑦)) ≤ ((𝐹‘𝑥) +𝑒 (𝐹‘𝑦)))
75	74	adantr 276	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ∀𝑥 ∈ (0[,]+∞)∀𝑦 ∈ (0[,]+∞)(𝐹‘(𝑥 +𝑒 𝑦)) ≤ ((𝐹‘𝑥) +𝑒 (𝐹‘𝑦)))
76		fvoveq1 6102	. . . . . . 7 ⊢ (𝑥 = (𝑐𝐷𝑎) → (𝐹‘(𝑥 +𝑒 𝑦)) = (𝐹‘((𝑐𝐷𝑎) +𝑒 𝑦)))
77		fveq2 5693	. . . . . . . 8 ⊢ (𝑥 = (𝑐𝐷𝑎) → (𝐹‘𝑥) = (𝐹‘(𝑐𝐷𝑎)))
78	77	oveq1d 6094	. . . . . . 7 ⊢ (𝑥 = (𝑐𝐷𝑎) → ((𝐹‘𝑥) +𝑒 (𝐹‘𝑦)) = ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘𝑦)))
79	76, 78	breq12d 4141	. . . . . 6 ⊢ (𝑥 = (𝑐𝐷𝑎) → ((𝐹‘(𝑥 +𝑒 𝑦)) ≤ ((𝐹‘𝑥) +𝑒 (𝐹‘𝑦)) ↔ (𝐹‘((𝑐𝐷𝑎) +𝑒 𝑦)) ≤ ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘𝑦))))
80		oveq2 6087	. . . . . . . 8 ⊢ (𝑦 = (𝑐𝐷𝑏) → ((𝑐𝐷𝑎) +𝑒 𝑦) = ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)))
81	80	fveq2d 5697	. . . . . . 7 ⊢ (𝑦 = (𝑐𝐷𝑏) → (𝐹‘((𝑐𝐷𝑎) +𝑒 𝑦)) = (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))))
82		fveq2 5693	. . . . . . . 8 ⊢ (𝑦 = (𝑐𝐷𝑏) → (𝐹‘𝑦) = (𝐹‘(𝑐𝐷𝑏)))
83	82	oveq2d 6095	. . . . . . 7 ⊢ (𝑦 = (𝑐𝐷𝑏) → ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘𝑦)) = ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘(𝑐𝐷𝑏))))
84	81, 83	breq12d 4141	. . . . . 6 ⊢ (𝑦 = (𝑐𝐷𝑏) → ((𝐹‘((𝑐𝐷𝑎) +𝑒 𝑦)) ≤ ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘𝑦)) ↔ (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))) ≤ ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘(𝑐𝐷𝑏)))))
85	79, 84	rspc2va 2944	. . . . 5 ⊢ ((((𝑐𝐷𝑎) ∈ (0[,]+∞) ∧ (𝑐𝐷𝑏) ∈ (0[,]+∞)) ∧ ∀𝑥 ∈ (0[,]+∞)∀𝑦 ∈ (0[,]+∞)(𝐹‘(𝑥 +𝑒 𝑦)) ≤ ((𝐹‘𝑥) +𝑒 (𝐹‘𝑦))) → (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))) ≤ ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘(𝑐𝐷𝑏))))
86	47, 49, 75, 85	syl21anc 1277	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))) ≤ ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘(𝑐𝐷𝑏))))
87	43, 52, 55, 72, 86	xrletrd 10197	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑎𝐷𝑏)) ≤ ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘(𝑐𝐷𝑏))))
88	27	3adantr3 1189	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑎(𝐹 ∘ 𝐷)𝑏) = (𝐹‘(𝑎𝐷𝑏)))
89	8	adantr 276	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → 𝐷:(𝑋 × 𝑋)⟶ℝ*)
90	45, 46	opelxpd 4805	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ⟨𝑐, 𝑎⟩ ∈ (𝑋 × 𝑋))
91		fvco3 5773	. . . . . 6 ⊢ ((𝐷:(𝑋 × 𝑋)⟶ℝ* ∧ ⟨𝑐, 𝑎⟩ ∈ (𝑋 × 𝑋)) → ((𝐹 ∘ 𝐷)‘⟨𝑐, 𝑎⟩) = (𝐹‘(𝐷‘⟨𝑐, 𝑎⟩)))
92	89, 90, 91	syl2anc 415	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ((𝐹 ∘ 𝐷)‘⟨𝑐, 𝑎⟩) = (𝐹‘(𝐷‘⟨𝑐, 𝑎⟩)))
93		df-ov 6082	. . . . 5 ⊢ (𝑐(𝐹 ∘ 𝐷)𝑎) = ((𝐹 ∘ 𝐷)‘⟨𝑐, 𝑎⟩)
94		df-ov 6082	. . . . . 6 ⊢ (𝑐𝐷𝑎) = (𝐷‘⟨𝑐, 𝑎⟩)
95	94	fveq2i 5696	. . . . 5 ⊢ (𝐹‘(𝑐𝐷𝑎)) = (𝐹‘(𝐷‘⟨𝑐, 𝑎⟩))
96	92, 93, 95	3eqtr4g 2296	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑐(𝐹 ∘ 𝐷)𝑎) = (𝐹‘(𝑐𝐷𝑎)))
97	45, 48	opelxpd 4805	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ⟨𝑐, 𝑏⟩ ∈ (𝑋 × 𝑋))
98		fvco3 5773	. . . . . 6 ⊢ ((𝐷:(𝑋 × 𝑋)⟶ℝ* ∧ ⟨𝑐, 𝑏⟩ ∈ (𝑋 × 𝑋)) → ((𝐹 ∘ 𝐷)‘⟨𝑐, 𝑏⟩) = (𝐹‘(𝐷‘⟨𝑐, 𝑏⟩)))
99	89, 97, 98	syl2anc 415	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ((𝐹 ∘ 𝐷)‘⟨𝑐, 𝑏⟩) = (𝐹‘(𝐷‘⟨𝑐, 𝑏⟩)))
100		df-ov 6082	. . . . 5 ⊢ (𝑐(𝐹 ∘ 𝐷)𝑏) = ((𝐹 ∘ 𝐷)‘⟨𝑐, 𝑏⟩)
101		df-ov 6082	. . . . . 6 ⊢ (𝑐𝐷𝑏) = (𝐷‘⟨𝑐, 𝑏⟩)
102	101	fveq2i 5696	. . . . 5 ⊢ (𝐹‘(𝑐𝐷𝑏)) = (𝐹‘(𝐷‘⟨𝑐, 𝑏⟩))
103	99, 100, 102	3eqtr4g 2296	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑐(𝐹 ∘ 𝐷)𝑏) = (𝐹‘(𝑐𝐷𝑏)))
104	96, 103	oveq12d 6097	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ((𝑐(𝐹 ∘ 𝐷)𝑎) +𝑒 (𝑐(𝐹 ∘ 𝐷)𝑏)) = ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘(𝑐𝐷𝑏))))
105	87, 88, 104	3brtr4d 4160	. 2 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑎(𝐹 ∘ 𝐷)𝑏) ≤ ((𝑐(𝐹 ∘ 𝐷)𝑎) +𝑒 (𝑐(𝐹 ∘ 𝐷)𝑏)))
106	5, 20, 40, 105	isxmetd 15431	1 ⊢ (𝜑 → (𝐹 ∘ 𝐷) ∈ (∞Met‘𝑋))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   ∧ w3a 1009   = wceq 1402   ∈ wcel 2209  ∀wral 2528  ⟨cop 3711   class class class wbr 4128   × cxp 4770  dom cdm 4772   ∘ ccom 4776  Rel wrel 4777   Fn wfn 5370  ⟶wf 5371  ‘cfv 5375  (class class class)co 6079  0cc0 8173  +∞cpnf 8351  ℝ^*cxr 8353   ≤ cle 8355   +_𝑒 cxad 10155  [,]cicc 10276  ∞Metcxmet 14856

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4247  ax-pow 4309  ax-pr 4344  ax-un 4576  ax-setind 4682  ax-cnex 8264  ax-resscn 8265  ax-1cn 8266  ax-1re 8267  ax-icn 8268  ax-addcl 8269  ax-addrcl 8270  ax-mulcl 8271  ax-mulrcl 8272  ax-addcom 8273  ax-mulcom 8274  ax-addass 8275  ax-mulass 8276  ax-distr 8277  ax-i2m1 8278  ax-0lt1 8279  ax-1rid 8280  ax-0id 8281  ax-rnegex 8282  ax-precex 8283  ax-cnre 8284  ax-pre-ltirr 8285  ax-pre-ltwlin 8286  ax-pre-lttrn 8287  ax-pre-apti 8288  ax-pre-ltadd 8289  ax-pre-mulgt0 8290

This theorem depends on definitions:  df-bi 117  df-dc 847  df-3or 1010  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-nel 2516  df-ral 2533  df-rex 2534  df-reu 2535  df-rab 2537  df-v 2823  df-sbc 3052  df-csb 3148  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-if 3639  df-pw 3690  df-sn 3714  df-pr 3715  df-op 3717  df-uni 3934  df-iun 4012  df-br 4129  df-opab 4191  df-mpt 4192  df-id 4436  df-po 4439  df-iso 4440  df-xp 4778  df-rel 4779  df-cnv 4780  df-co 4781  df-dm 4782  df-rn 4783  df-res 4784  df-ima 4785  df-iota 5335  df-fun 5377  df-fn 5378  df-f 5379  df-fv 5383  df-riota 6032  df-ov 6082  df-oprab 6083  df-mpo 6084  df-1st 6368  df-2nd 6369  df-map 6918  df-pnf 8356  df-mnf 8357  df-xr 8358  df-ltxr 8359  df-le 8360  df-sub 8493  df-neg 8494  df-2 9346  df-xadd 10158  df-icc 10280  df-xmet 14864

This theorem is referenced by:  bdxmet  15585