Theorem xpsdsval 22420

Description: Value of the metric in a binary structure product. (Contributed by Mario Carneiro, 20-Aug-2015.)

Hypotheses

Ref	Expression
xpsds.t	⊢ 𝑇 = (𝑅 ×s 𝑆)
xpsds.x	⊢ 𝑋 = (Base‘𝑅)
xpsds.y	⊢ 𝑌 = (Base‘𝑆)
xpsds.1	⊢ (𝜑 → 𝑅 ∈ 𝑉)
xpsds.2	⊢ (𝜑 → 𝑆 ∈ 𝑊)
xpsds.p	⊢ 𝑃 = (dist‘𝑇)
xpsds.m	⊢ 𝑀 = ((dist‘𝑅) ↾ (𝑋 × 𝑋))
xpsds.n	⊢ 𝑁 = ((dist‘𝑆) ↾ (𝑌 × 𝑌))
xpsds.3	⊢ (𝜑 → 𝑀 ∈ (∞Met‘𝑋))
xpsds.4	⊢ (𝜑 → 𝑁 ∈ (∞Met‘𝑌))
xpsds.a	⊢ (𝜑 → 𝐴 ∈ 𝑋)
xpsds.b	⊢ (𝜑 → 𝐵 ∈ 𝑌)
xpsds.c	⊢ (𝜑 → 𝐶 ∈ 𝑋)
xpsds.d	⊢ (𝜑 → 𝐷 ∈ 𝑌)

Assertion

Ref	Expression
xpsdsval	⊢ (𝜑 → (⟨𝐴, 𝐵⟩𝑃⟨𝐶, 𝐷⟩) = sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ))

Proof of Theorem xpsdsval

Dummy variables 𝑥 𝑘 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		xpsds.t	. . . . 5 ⊢ 𝑇 = (𝑅 ×s 𝑆)
2		xpsds.x	. . . . 5 ⊢ 𝑋 = (Base‘𝑅)
3		xpsds.y	. . . . 5 ⊢ 𝑌 = (Base‘𝑆)
4		xpsds.1	. . . . 5 ⊢ (𝜑 → 𝑅 ∈ 𝑉)
5		xpsds.2	. . . . 5 ⊢ (𝜑 → 𝑆 ∈ 𝑊)
6		eqid 2817	. . . . 5 ⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))
7		eqid 2817	. . . . 5 ⊢ (Scalar‘𝑅) = (Scalar‘𝑅)
8		eqid 2817	. . . . 5 ⊢ ((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})) = ((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))
9	1, 2, 3, 4, 5, 6, 7, 8	xpsval 16457	. . . 4 ⊢ (𝜑 → 𝑇 = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) “s ((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))))
10	1, 2, 3, 4, 5, 6, 7, 8	xpslem 16458	. . . 4 ⊢ (𝜑 → ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) = (Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))))
11	6	xpsff1o2 16456	. . . . 5 ⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))
12		f1ocnv 6375	. . . . 5 ⊢ ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))–1-1-onto→(𝑋 × 𝑌))
13	11, 12	mp1i 13	. . . 4 ⊢ (𝜑 → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))–1-1-onto→(𝑋 × 𝑌))
14		ovexd 6918	. . . 4 ⊢ (𝜑 → ((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})) ∈ V)
15		eqid 2817	. . . 4 ⊢ ((dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ↾ (ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) × ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))) = ((dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ↾ (ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) × ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))))
16		xpsds.p	. . . 4 ⊢ 𝑃 = (dist‘𝑇)
17		xpsds.m	. . . . . 6 ⊢ 𝑀 = ((dist‘𝑅) ↾ (𝑋 × 𝑋))
18		xpsds.n	. . . . . 6 ⊢ 𝑁 = ((dist‘𝑆) ↾ (𝑌 × 𝑌))
19		xpsds.3	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ (∞Met‘𝑋))
20		xpsds.4	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ (∞Met‘𝑌))
21	1, 2, 3, 4, 5, 16, 17, 18, 19, 20	xpsxmetlem 22418	. . . . 5 ⊢ (𝜑 → (dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ∈ (∞Met‘ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))))
22		ssid 3831	. . . . 5 ⊢ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) ⊆ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))
23		xmetres2 22400	. . . . 5 ⊢ (((dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ∈ (∞Met‘ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) ∧ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) ⊆ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) → ((dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ↾ (ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) × ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))) ∈ (∞Met‘ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))))
24	21, 22, 23	sylancl 576	. . . 4 ⊢ (𝜑 → ((dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ↾ (ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) × ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))) ∈ (∞Met‘ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))))
25		df-ov 6887	. . . . . 6 ⊢ (𝐴(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))𝐵) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘⟨𝐴, 𝐵⟩)
26		xpsds.a	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ 𝑋)
27		xpsds.b	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ 𝑌)
28	6	xpsfval 16452	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → (𝐴(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))𝐵) = ◡({𝐴} +𝑐 {𝐵}))
29	26, 27, 28	syl2anc 575	. . . . . 6 ⊢ (𝜑 → (𝐴(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))𝐵) = ◡({𝐴} +𝑐 {𝐵}))
30	25, 29	syl5eqr 2865	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘⟨𝐴, 𝐵⟩) = ◡({𝐴} +𝑐 {𝐵}))
31		opelxpi 5360	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → ⟨𝐴, 𝐵⟩ ∈ (𝑋 × 𝑌))
32	26, 27, 31	syl2anc 575	. . . . . 6 ⊢ (𝜑 → ⟨𝐴, 𝐵⟩ ∈ (𝑋 × 𝑌))
33		f1of 6363	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)⟶ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))
34	11, 33	ax-mp 5	. . . . . . 7 ⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)⟶ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))
35	34	ffvelrni 6590	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝑋 × 𝑌) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘⟨𝐴, 𝐵⟩) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))
36	32, 35	syl 17	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘⟨𝐴, 𝐵⟩) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))
37	30, 36	eqeltrrd 2897	. . . 4 ⊢ (𝜑 → ◡({𝐴} +𝑐 {𝐵}) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))
38		df-ov 6887	. . . . . 6 ⊢ (𝐶(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))𝐷) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘⟨𝐶, 𝐷⟩)
39		xpsds.c	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ 𝑋)
40		xpsds.d	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ 𝑌)
41	6	xpsfval 16452	. . . . . . 7 ⊢ ((𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) → (𝐶(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))𝐷) = ◡({𝐶} +𝑐 {𝐷}))
42	39, 40, 41	syl2anc 575	. . . . . 6 ⊢ (𝜑 → (𝐶(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))𝐷) = ◡({𝐶} +𝑐 {𝐷}))
43	38, 42	syl5eqr 2865	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘⟨𝐶, 𝐷⟩) = ◡({𝐶} +𝑐 {𝐷}))
44		opelxpi 5360	. . . . . . 7 ⊢ ((𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) → ⟨𝐶, 𝐷⟩ ∈ (𝑋 × 𝑌))
45	39, 40, 44	syl2anc 575	. . . . . 6 ⊢ (𝜑 → ⟨𝐶, 𝐷⟩ ∈ (𝑋 × 𝑌))
46	34	ffvelrni 6590	. . . . . 6 ⊢ (⟨𝐶, 𝐷⟩ ∈ (𝑋 × 𝑌) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘⟨𝐶, 𝐷⟩) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))
47	45, 46	syl 17	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘⟨𝐶, 𝐷⟩) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))
48	43, 47	eqeltrrd 2897	. . . 4 ⊢ (𝜑 → ◡({𝐶} +𝑐 {𝐷}) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))
49	9, 10, 13, 14, 15, 16, 24, 37, 48	imasdsf1o 22413	. . 3 ⊢ (𝜑 → ((◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐴} +𝑐 {𝐵}))𝑃(◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐶} +𝑐 {𝐷}))) = (◡({𝐴} +𝑐 {𝐵})((dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ↾ (ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) × ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))))◡({𝐶} +𝑐 {𝐷})))
50	37, 48	ovresd 7041	. . 3 ⊢ (𝜑 → (◡({𝐴} +𝑐 {𝐵})((dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ↾ (ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) × ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))))◡({𝐶} +𝑐 {𝐷})) = (◡({𝐴} +𝑐 {𝐵})(dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))◡({𝐶} +𝑐 {𝐷})))
51	49, 50	eqtrd 2851	. 2 ⊢ (𝜑 → ((◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐴} +𝑐 {𝐵}))𝑃(◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐶} +𝑐 {𝐷}))) = (◡({𝐴} +𝑐 {𝐵})(dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))◡({𝐶} +𝑐 {𝐷})))
52		f1ocnvfv 6768	. . . . 5 ⊢ (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) ∧ ⟨𝐴, 𝐵⟩ ∈ (𝑋 × 𝑌)) → (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘⟨𝐴, 𝐵⟩) = ◡({𝐴} +𝑐 {𝐵}) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐴} +𝑐 {𝐵})) = ⟨𝐴, 𝐵⟩))
53	11, 32, 52	sylancr 577	. . . 4 ⊢ (𝜑 → (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘⟨𝐴, 𝐵⟩) = ◡({𝐴} +𝑐 {𝐵}) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐴} +𝑐 {𝐵})) = ⟨𝐴, 𝐵⟩))
54	30, 53	mpd 15	. . 3 ⊢ (𝜑 → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐴} +𝑐 {𝐵})) = ⟨𝐴, 𝐵⟩)
55		f1ocnvfv 6768	. . . . 5 ⊢ (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) ∧ ⟨𝐶, 𝐷⟩ ∈ (𝑋 × 𝑌)) → (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘⟨𝐶, 𝐷⟩) = ◡({𝐶} +𝑐 {𝐷}) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐶} +𝑐 {𝐷})) = ⟨𝐶, 𝐷⟩))
56	11, 45, 55	sylancr 577	. . . 4 ⊢ (𝜑 → (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘⟨𝐶, 𝐷⟩) = ◡({𝐶} +𝑐 {𝐷}) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐶} +𝑐 {𝐷})) = ⟨𝐶, 𝐷⟩))
57	43, 56	mpd 15	. . 3 ⊢ (𝜑 → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐶} +𝑐 {𝐷})) = ⟨𝐶, 𝐷⟩)
58	54, 57	oveq12d 6902	. 2 ⊢ (𝜑 → ((◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐴} +𝑐 {𝐵}))𝑃(◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐶} +𝑐 {𝐷}))) = (⟨𝐴, 𝐵⟩𝑃⟨𝐶, 𝐷⟩))
59		eqid 2817	. . . 4 ⊢ (Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) = (Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))
60		fvexd 6433	. . . 4 ⊢ (𝜑 → (Scalar‘𝑅) ∈ V)
61		2on 7815	. . . . 5 ⊢ 2𝑜 ∈ On
62	61	a1i 11	. . . 4 ⊢ (𝜑 → 2𝑜 ∈ On)
63		xpscfn 16444	. . . . 5 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → ◡({𝑅} +𝑐 {𝑆}) Fn 2𝑜)
64	4, 5, 63	syl2anc 575	. . . 4 ⊢ (𝜑 → ◡({𝑅} +𝑐 {𝑆}) Fn 2𝑜)
65	37, 10	eleqtrd 2898	. . . 4 ⊢ (𝜑 → ◡({𝐴} +𝑐 {𝐵}) ∈ (Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))))
66	48, 10	eleqtrd 2898	. . . 4 ⊢ (𝜑 → ◡({𝐶} +𝑐 {𝐷}) ∈ (Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))))
67		eqid 2817	. . . 4 ⊢ (dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) = (dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))
68	8, 59, 60, 62, 64, 65, 66, 67	prdsdsval 16363	. . 3 ⊢ (𝜑 → (◡({𝐴} +𝑐 {𝐵})(dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))◡({𝐶} +𝑐 {𝐷})) = sup((ran (𝑘 ∈ 2𝑜 ↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))) ∪ {0}), ℝ*, < ))
69		df2o3 7820	. . . . . . . . . . 11 ⊢ 2𝑜 = {∅, 1𝑜}
70	69	rexeqi 3343	. . . . . . . . . 10 ⊢ (∃𝑘 ∈ 2𝑜 𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)) ↔ ∃𝑘 ∈ {∅, 1𝑜}𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)))
71		0ex 4997	. . . . . . . . . . 11 ⊢ ∅ ∈ V
72		1oex 7814	. . . . . . . . . . 11 ⊢ 1𝑜 ∈ V
73		2fveq3 6423	. . . . . . . . . . . . 13 ⊢ (𝑘 = ∅ → (dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) = (dist‘(◡({𝑅} +𝑐 {𝑆})‘∅)))
74		fveq2 6418	. . . . . . . . . . . . 13 ⊢ (𝑘 = ∅ → (◡({𝐴} +𝑐 {𝐵})‘𝑘) = (◡({𝐴} +𝑐 {𝐵})‘∅))
75		fveq2 6418	. . . . . . . . . . . . 13 ⊢ (𝑘 = ∅ → (◡({𝐶} +𝑐 {𝐷})‘𝑘) = (◡({𝐶} +𝑐 {𝐷})‘∅))
76	73, 74, 75	oveq123d 6905	. . . . . . . . . . . 12 ⊢ (𝑘 = ∅ → ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)) = ((◡({𝐴} +𝑐 {𝐵})‘∅)(dist‘(◡({𝑅} +𝑐 {𝑆})‘∅))(◡({𝐶} +𝑐 {𝐷})‘∅)))
77	76	eqeq2d 2827	. . . . . . . . . . 11 ⊢ (𝑘 = ∅ → (𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)) ↔ 𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘∅)(dist‘(◡({𝑅} +𝑐 {𝑆})‘∅))(◡({𝐶} +𝑐 {𝐷})‘∅))))
78		2fveq3 6423	. . . . . . . . . . . . 13 ⊢ (𝑘 = 1𝑜 → (dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) = (dist‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜)))
79		fveq2 6418	. . . . . . . . . . . . 13 ⊢ (𝑘 = 1𝑜 → (◡({𝐴} +𝑐 {𝐵})‘𝑘) = (◡({𝐴} +𝑐 {𝐵})‘1𝑜))
80		fveq2 6418	. . . . . . . . . . . . 13 ⊢ (𝑘 = 1𝑜 → (◡({𝐶} +𝑐 {𝐷})‘𝑘) = (◡({𝐶} +𝑐 {𝐷})‘1𝑜))
81	78, 79, 80	oveq123d 6905	. . . . . . . . . . . 12 ⊢ (𝑘 = 1𝑜 → ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)) = ((◡({𝐴} +𝑐 {𝐵})‘1𝑜)(dist‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜))(◡({𝐶} +𝑐 {𝐷})‘1𝑜)))
82	81	eqeq2d 2827	. . . . . . . . . . 11 ⊢ (𝑘 = 1𝑜 → (𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)) ↔ 𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘1𝑜)(dist‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜))(◡({𝐶} +𝑐 {𝐷})‘1𝑜))))
83	71, 72, 77, 82	rexpr 4442	. . . . . . . . . 10 ⊢ (∃𝑘 ∈ {∅, 1𝑜}𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)) ↔ (𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘∅)(dist‘(◡({𝑅} +𝑐 {𝑆})‘∅))(◡({𝐶} +𝑐 {𝐷})‘∅)) ∨ 𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘1𝑜)(dist‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜))(◡({𝐶} +𝑐 {𝐷})‘1𝑜))))
84	70, 83	bitri 266	. . . . . . . . 9 ⊢ (∃𝑘 ∈ 2𝑜 𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)) ↔ (𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘∅)(dist‘(◡({𝑅} +𝑐 {𝑆})‘∅))(◡({𝐶} +𝑐 {𝐷})‘∅)) ∨ 𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘1𝑜)(dist‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜))(◡({𝐶} +𝑐 {𝐷})‘1𝑜))))
85		xpsc0 16445	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ 𝑉 → (◡({𝑅} +𝑐 {𝑆})‘∅) = 𝑅)
86	4, 85	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (◡({𝑅} +𝑐 {𝑆})‘∅) = 𝑅)
87	86	fveq2d 6422	. . . . . . . . . . . . 13 ⊢ (𝜑 → (dist‘(◡({𝑅} +𝑐 {𝑆})‘∅)) = (dist‘𝑅))
88		xpsc0 16445	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ 𝑋 → (◡({𝐴} +𝑐 {𝐵})‘∅) = 𝐴)
89	26, 88	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (◡({𝐴} +𝑐 {𝐵})‘∅) = 𝐴)
90		xpsc0 16445	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∈ 𝑋 → (◡({𝐶} +𝑐 {𝐷})‘∅) = 𝐶)
91	39, 90	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (◡({𝐶} +𝑐 {𝐷})‘∅) = 𝐶)
92	87, 89, 91	oveq123d 6905	. . . . . . . . . . . 12 ⊢ (𝜑 → ((◡({𝐴} +𝑐 {𝐵})‘∅)(dist‘(◡({𝑅} +𝑐 {𝑆})‘∅))(◡({𝐶} +𝑐 {𝐷})‘∅)) = (𝐴(dist‘𝑅)𝐶))
93	17	oveqi 6897	. . . . . . . . . . . . 13 ⊢ (𝐴𝑀𝐶) = (𝐴((dist‘𝑅) ↾ (𝑋 × 𝑋))𝐶)
94	26, 39	ovresd 7041	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴((dist‘𝑅) ↾ (𝑋 × 𝑋))𝐶) = (𝐴(dist‘𝑅)𝐶))
95	93, 94	syl5eq 2863	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴𝑀𝐶) = (𝐴(dist‘𝑅)𝐶))
96	92, 95	eqtr4d 2854	. . . . . . . . . . 11 ⊢ (𝜑 → ((◡({𝐴} +𝑐 {𝐵})‘∅)(dist‘(◡({𝑅} +𝑐 {𝑆})‘∅))(◡({𝐶} +𝑐 {𝐷})‘∅)) = (𝐴𝑀𝐶))
97	96	eqeq2d 2827	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘∅)(dist‘(◡({𝑅} +𝑐 {𝑆})‘∅))(◡({𝐶} +𝑐 {𝐷})‘∅)) ↔ 𝑥 = (𝐴𝑀𝐶)))
98		xpsc1 16446	. . . . . . . . . . . . . . 15 ⊢ (𝑆 ∈ 𝑊 → (◡({𝑅} +𝑐 {𝑆})‘1𝑜) = 𝑆)
99	5, 98	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (◡({𝑅} +𝑐 {𝑆})‘1𝑜) = 𝑆)
100	99	fveq2d 6422	. . . . . . . . . . . . 13 ⊢ (𝜑 → (dist‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜)) = (dist‘𝑆))
101		xpsc1 16446	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ 𝑌 → (◡({𝐴} +𝑐 {𝐵})‘1𝑜) = 𝐵)
102	27, 101	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (◡({𝐴} +𝑐 {𝐵})‘1𝑜) = 𝐵)
103		xpsc1 16446	. . . . . . . . . . . . . 14 ⊢ (𝐷 ∈ 𝑌 → (◡({𝐶} +𝑐 {𝐷})‘1𝑜) = 𝐷)
104	40, 103	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (◡({𝐶} +𝑐 {𝐷})‘1𝑜) = 𝐷)
105	100, 102, 104	oveq123d 6905	. . . . . . . . . . . 12 ⊢ (𝜑 → ((◡({𝐴} +𝑐 {𝐵})‘1𝑜)(dist‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜))(◡({𝐶} +𝑐 {𝐷})‘1𝑜)) = (𝐵(dist‘𝑆)𝐷))
106	18	oveqi 6897	. . . . . . . . . . . . 13 ⊢ (𝐵𝑁𝐷) = (𝐵((dist‘𝑆) ↾ (𝑌 × 𝑌))𝐷)
107	27, 40	ovresd 7041	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵((dist‘𝑆) ↾ (𝑌 × 𝑌))𝐷) = (𝐵(dist‘𝑆)𝐷))
108	106, 107	syl5eq 2863	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵𝑁𝐷) = (𝐵(dist‘𝑆)𝐷))
109	105, 108	eqtr4d 2854	. . . . . . . . . . 11 ⊢ (𝜑 → ((◡({𝐴} +𝑐 {𝐵})‘1𝑜)(dist‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜))(◡({𝐶} +𝑐 {𝐷})‘1𝑜)) = (𝐵𝑁𝐷))
110	109	eqeq2d 2827	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘1𝑜)(dist‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜))(◡({𝐶} +𝑐 {𝐷})‘1𝑜)) ↔ 𝑥 = (𝐵𝑁𝐷)))
111	97, 110	orbi12d 933	. . . . . . . . 9 ⊢ (𝜑 → ((𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘∅)(dist‘(◡({𝑅} +𝑐 {𝑆})‘∅))(◡({𝐶} +𝑐 {𝐷})‘∅)) ∨ 𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘1𝑜)(dist‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜))(◡({𝐶} +𝑐 {𝐷})‘1𝑜))) ↔ (𝑥 = (𝐴𝑀𝐶) ∨ 𝑥 = (𝐵𝑁𝐷))))
112	84, 111	syl5bb 274	. . . . . . . 8 ⊢ (𝜑 → (∃𝑘 ∈ 2𝑜 𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)) ↔ (𝑥 = (𝐴𝑀𝐶) ∨ 𝑥 = (𝐵𝑁𝐷))))
113		vex 3405	. . . . . . . . 9 ⊢ 𝑥 ∈ V
114		eqid 2817	. . . . . . . . . 10 ⊢ (𝑘 ∈ 2𝑜 ↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))) = (𝑘 ∈ 2𝑜 ↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)))
115	114	elrnmpt 5587	. . . . . . . . 9 ⊢ (𝑥 ∈ V → (𝑥 ∈ ran (𝑘 ∈ 2𝑜 ↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))) ↔ ∃𝑘 ∈ 2𝑜 𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))))
116	113, 115	ax-mp 5	. . . . . . . 8 ⊢ (𝑥 ∈ ran (𝑘 ∈ 2𝑜 ↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))) ↔ ∃𝑘 ∈ 2𝑜 𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)))
117	113	elpr 4404	. . . . . . . 8 ⊢ (𝑥 ∈ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ↔ (𝑥 = (𝐴𝑀𝐶) ∨ 𝑥 = (𝐵𝑁𝐷)))
118	112, 116, 117	3bitr4g 305	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ ran (𝑘 ∈ 2𝑜 ↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))) ↔ 𝑥 ∈ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)}))
119	118	eqrdv 2815	. . . . . 6 ⊢ (𝜑 → ran (𝑘 ∈ 2𝑜 ↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))) = {(𝐴𝑀𝐶), (𝐵𝑁𝐷)})
120	119	uneq1d 3976	. . . . 5 ⊢ (𝜑 → (ran (𝑘 ∈ 2𝑜 ↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))) ∪ {0}) = ({(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ∪ {0}))
121		uncom 3967	. . . . 5 ⊢ ({(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ∪ {0}) = ({0} ∪ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)})
122	120, 121	syl6eq 2867	. . . 4 ⊢ (𝜑 → (ran (𝑘 ∈ 2𝑜 ↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))) ∪ {0}) = ({0} ∪ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)}))
123	122	supeq1d 8601	. . 3 ⊢ (𝜑 → sup((ran (𝑘 ∈ 2𝑜 ↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))) ∪ {0}), ℝ*, < ) = sup(({0} ∪ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)}), ℝ*, < ))
124		0xr 10381	. . . . . 6 ⊢ 0 ∈ ℝ*
125	124	a1i 11	. . . . 5 ⊢ (𝜑 → 0 ∈ ℝ*)
126	125	snssd 4541	. . . 4 ⊢ (𝜑 → {0} ⊆ ℝ*)
127		xmetcl 22370	. . . . . 6 ⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (𝐴𝑀𝐶) ∈ ℝ*)
128	19, 26, 39, 127	syl3anc 1483	. . . . 5 ⊢ (𝜑 → (𝐴𝑀𝐶) ∈ ℝ*)
129		xmetcl 22370	. . . . . 6 ⊢ ((𝑁 ∈ (∞Met‘𝑌) ∧ 𝐵 ∈ 𝑌 ∧ 𝐷 ∈ 𝑌) → (𝐵𝑁𝐷) ∈ ℝ*)
130	20, 27, 40, 129	syl3anc 1483	. . . . 5 ⊢ (𝜑 → (𝐵𝑁𝐷) ∈ ℝ*)
131		prssi 4553	. . . . 5 ⊢ (((𝐴𝑀𝐶) ∈ ℝ* ∧ (𝐵𝑁𝐷) ∈ ℝ*) → {(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ⊆ ℝ*)
132	128, 130, 131	syl2anc 575	. . . 4 ⊢ (𝜑 → {(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ⊆ ℝ*)
133		xrltso 12210	. . . . . 6 ⊢ < Or ℝ*
134		supsn 8627	. . . . . 6 ⊢ (( < Or ℝ* ∧ 0 ∈ ℝ*) → sup({0}, ℝ*, < ) = 0)
135	133, 124, 134	mp2an 675	. . . . 5 ⊢ sup({0}, ℝ*, < ) = 0
136		supxrcl 12383	. . . . . . 7 ⊢ ({(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ⊆ ℝ* → sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ) ∈ ℝ*)
137	132, 136	syl 17	. . . . . 6 ⊢ (𝜑 → sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ) ∈ ℝ*)
138		xmetge0 22383	. . . . . . 7 ⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → 0 ≤ (𝐴𝑀𝐶))
139	19, 26, 39, 138	syl3anc 1483	. . . . . 6 ⊢ (𝜑 → 0 ≤ (𝐴𝑀𝐶))
140		ovex 6916	. . . . . . . 8 ⊢ (𝐴𝑀𝐶) ∈ V
141	140	prid1 4499	. . . . . . 7 ⊢ (𝐴𝑀𝐶) ∈ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)}
142		supxrub 12392	. . . . . . 7 ⊢ (({(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ⊆ ℝ* ∧ (𝐴𝑀𝐶) ∈ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)}) → (𝐴𝑀𝐶) ≤ sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ))
143	132, 141, 142	sylancl 576	. . . . . 6 ⊢ (𝜑 → (𝐴𝑀𝐶) ≤ sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ))
144	125, 128, 137, 139, 143	xrletrd 12231	. . . . 5 ⊢ (𝜑 → 0 ≤ sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ))
145	135, 144	syl5eqbr 4890	. . . 4 ⊢ (𝜑 → sup({0}, ℝ*, < ) ≤ sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ))
146		supxrun 12384	. . . 4 ⊢ (({0} ⊆ ℝ* ∧ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ⊆ ℝ* ∧ sup({0}, ℝ*, < ) ≤ sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < )) → sup(({0} ∪ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)}), ℝ*, < ) = sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ))
147	126, 132, 145, 146	syl3anc 1483	. . 3 ⊢ (𝜑 → sup(({0} ∪ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)}), ℝ*, < ) = sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ))
148	68, 123, 147	3eqtrd 2855	. 2 ⊢ (𝜑 → (◡({𝐴} +𝑐 {𝐵})(dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))◡({𝐶} +𝑐 {𝐷})) = sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ))
149	51, 58, 148	3eqtr3d 2859	1 ⊢ (𝜑 → (⟨𝐴, 𝐵⟩𝑃⟨𝐶, 𝐷⟩) = sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ))

Syntax hints:   → wi 4   ↔ wb 197   ∨ wo 865   = wceq 1637   ∈ wcel 2157  ∃wrex 3108  Vcvv 3402   ∪ cun 3778   ⊆ wss 3780  ∅c0 4127  {csn 4381  {cpr 4383  ⟨cop 4387   class class class wbr 4855   ↦ cmpt 4934   Or wor 5244   × cxp 5322  ^◡ccnv 5323  ran crn 5325   ↾ cres 5326  Oncon0 5950   Fn wfn 6106  ⟶wf 6107  –1-1-onto→wf1o 6110  ‘cfv 6111  (class class class)co 6884   ↦ cmpt2 6886  1_𝑜c1o 7799  2_𝑜c2o 7800  supcsup 8595   +_𝑐 ccda 9284  0cc0 10231  ℝ^*cxr 10368   < clt 10369   ≤ cle 10370  Basecbs 16088  Scalarcsca 16176  distcds 16182  X_scprds 16331   ×_s cxps 16391  ∞Metcxmt 19959

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-rep 4977  ax-sep 4988  ax-nul 4996  ax-pow 5048  ax-pr 5109  ax-un 7189  ax-inf2 8795  ax-cnex 10287  ax-resscn 10288  ax-1cn 10289  ax-icn 10290  ax-addcl 10291  ax-addrcl 10292  ax-mulcl 10293  ax-mulrcl 10294  ax-mulcom 10295  ax-addass 10296  ax-mulass 10297  ax-distr 10298  ax-i2m1 10299  ax-1ne0 10300  ax-1rid 10301  ax-rnegex 10302  ax-rrecex 10303  ax-cnre 10304  ax-pre-lttri 10305  ax-pre-lttrn 10306  ax-pre-ltadd 10307  ax-pre-mulgt0 10308  ax-pre-sup 10309

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-nel 3093  df-ral 3112  df-rex 3113  df-reu 3114  df-rmo 3115  df-rab 3116  df-v 3404  df-sbc 3645  df-csb 3740  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-pss 3796  df-nul 4128  df-if 4291  df-pw 4364  df-sn 4382  df-pr 4384  df-tp 4386  df-op 4388  df-uni 4642  df-int 4681  df-iun 4725  df-iin 4726  df-br 4856  df-opab 4918  df-mpt 4935  df-tr 4958  df-id 5232  df-eprel 5237  df-po 5245  df-so 5246  df-fr 5283  df-se 5284  df-we 5285  df-xp 5330  df-rel 5331  df-cnv 5332  df-co 5333  df-dm 5334  df-rn 5335  df-res 5336  df-ima 5337  df-pred 5907  df-ord 5953  df-on 5954  df-lim 5955  df-suc 5956  df-iota 6074  df-fun 6113  df-fn 6114  df-f 6115  df-f1 6116  df-fo 6117  df-f1o 6118  df-fv 6119  df-isom 6120  df-riota 6845  df-ov 6887  df-oprab 6888  df-mpt2 6889  df-of 7137  df-om 7306  df-1st 7408  df-2nd 7409  df-supp 7540  df-wrecs 7652  df-recs 7714  df-rdg 7752  df-1o 7806  df-2o 7807  df-oadd 7810  df-er 7989  df-map 8104  df-ixp 8156  df-en 8203  df-dom 8204  df-sdom 8205  df-fin 8206  df-fsupp 8525  df-sup 8597  df-inf 8598  df-oi 8664  df-card 9058  df-cda 9285  df-pnf 10371  df-mnf 10372  df-xr 10373  df-ltxr 10374  df-le 10375  df-sub 10563  df-neg 10564  df-div 10980  df-nn 11316  df-2 11376  df-3 11377  df-4 11378  df-5 11379  df-6 11380  df-7 11381  df-8 11382  df-9 11383  df-n0 11580  df-z 11664  df-dec 11780  df-uz 11925  df-rp 12067  df-xneg 12182  df-xadd 12183  df-xmul 12184  df-icc 12420  df-fz 12570  df-fzo 12710  df-seq 13045  df-hash 13358  df-struct 16090  df-ndx 16091  df-slot 16092  df-base 16094  df-sets 16095  df-ress 16096  df-plusg 16186  df-mulr 16187  df-sca 16189  df-vsca 16190  df-ip 16191  df-tset 16192  df-ple 16193  df-ds 16195  df-hom 16197  df-cco 16198  df-0g 16327  df-gsum 16328  df-prds 16333  df-xrs 16387  df-imas 16393  df-xps 16395  df-mre 16471  df-mrc 16472  df-acs 16474  df-mgm 17467  df-sgrp 17509  df-mnd 17520  df-submnd 17561  df-mulg 17766  df-cntz 17971  df-cmn 18416  df-xmet 19967

This theorem is referenced by:  tmsxpsval  22577