Theorem xpsdsval 22594

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 2777	. . . . 5 ⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))
7		eqid 2777	. . . . 5 ⊢ (Scalar‘𝑅) = (Scalar‘𝑅)
8		eqid 2777	. . . . 5 ⊢ ((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})) = ((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))
9	1, 2, 3, 4, 5, 6, 7, 8	xpsval 16618	. . . 4 ⊢ (𝜑 → 𝑇 = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) “s ((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))))
10	1, 2, 3, 4, 5, 6, 7, 8	xpslem 16619	. . . 4 ⊢ (𝜑 → ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) = (Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))))
11	6	xpsff1o2 16617	. . . . 5 ⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))
12		f1ocnv 6403	. . . . 5 ⊢ ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))–1-1-onto→(𝑋 × 𝑌))
13	11, 12	mp1i 13	. . . 4 ⊢ (𝜑 → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))–1-1-onto→(𝑋 × 𝑌))
14		ovexd 6956	. . . 4 ⊢ (𝜑 → ((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})) ∈ V)
15		eqid 2777	. . . 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 22592	. . . . 5 ⊢ (𝜑 → (dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ∈ (∞Met‘ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))))
22		ssid 3841	. . . . 5 ⊢ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) ⊆ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))
23		xmetres2 22574	. . . . 5 ⊢ (((dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ∈ (∞Met‘ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) ∧ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) ⊆ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) → ((dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ↾ (ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) × ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))) ∈ (∞Met‘ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))))
24	21, 22, 23	sylancl 580	. . . 4 ⊢ (𝜑 → ((dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ↾ (ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) × ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))) ∈ (∞Met‘ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))))
25		df-ov 6925	. . . . . 6 ⊢ (𝐴(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))𝐵) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘⟨𝐴, 𝐵⟩)
26		xpsds.a	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ 𝑋)
27		xpsds.b	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ 𝑌)
28	6	xpsfval 16613	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → (𝐴(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))𝐵) = ◡({𝐴} +𝑐 {𝐵}))
29	26, 27, 28	syl2anc 579	. . . . . 6 ⊢ (𝜑 → (𝐴(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))𝐵) = ◡({𝐴} +𝑐 {𝐵}))
30	25, 29	syl5eqr 2827	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘⟨𝐴, 𝐵⟩) = ◡({𝐴} +𝑐 {𝐵}))
31		opelxpi 5392	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → ⟨𝐴, 𝐵⟩ ∈ (𝑋 × 𝑌))
32	26, 27, 31	syl2anc 579	. . . . . 6 ⊢ (𝜑 → ⟨𝐴, 𝐵⟩ ∈ (𝑋 × 𝑌))
33		f1of 6391	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)⟶ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))
34	11, 33	ax-mp 5	. . . . . . 7 ⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)⟶ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))
35	34	ffvelrni 6622	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝑋 × 𝑌) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘⟨𝐴, 𝐵⟩) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))
36	32, 35	syl 17	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘⟨𝐴, 𝐵⟩) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))
37	30, 36	eqeltrrd 2859	. . . 4 ⊢ (𝜑 → ◡({𝐴} +𝑐 {𝐵}) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))
38		df-ov 6925	. . . . . 6 ⊢ (𝐶(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))𝐷) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘⟨𝐶, 𝐷⟩)
39		xpsds.c	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ 𝑋)
40		xpsds.d	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ 𝑌)
41	6	xpsfval 16613	. . . . . . 7 ⊢ ((𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) → (𝐶(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))𝐷) = ◡({𝐶} +𝑐 {𝐷}))
42	39, 40, 41	syl2anc 579	. . . . . 6 ⊢ (𝜑 → (𝐶(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))𝐷) = ◡({𝐶} +𝑐 {𝐷}))
43	38, 42	syl5eqr 2827	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘⟨𝐶, 𝐷⟩) = ◡({𝐶} +𝑐 {𝐷}))
44		opelxpi 5392	. . . . . . 7 ⊢ ((𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) → ⟨𝐶, 𝐷⟩ ∈ (𝑋 × 𝑌))
45	39, 40, 44	syl2anc 579	. . . . . 6 ⊢ (𝜑 → ⟨𝐶, 𝐷⟩ ∈ (𝑋 × 𝑌))
46	34	ffvelrni 6622	. . . . . 6 ⊢ (⟨𝐶, 𝐷⟩ ∈ (𝑋 × 𝑌) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘⟨𝐶, 𝐷⟩) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))
47	45, 46	syl 17	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘⟨𝐶, 𝐷⟩) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))
48	43, 47	eqeltrrd 2859	. . . 4 ⊢ (𝜑 → ◡({𝐶} +𝑐 {𝐷}) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))
49	9, 10, 13, 14, 15, 16, 24, 37, 48	imasdsf1o 22587	. . 3 ⊢ (𝜑 → ((◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐴} +𝑐 {𝐵}))𝑃(◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐶} +𝑐 {𝐷}))) = (◡({𝐴} +𝑐 {𝐵})((dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ↾ (ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) × ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))))◡({𝐶} +𝑐 {𝐷})))
50	37, 48	ovresd 7078	. . 3 ⊢ (𝜑 → (◡({𝐴} +𝑐 {𝐵})((dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ↾ (ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) × ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))))◡({𝐶} +𝑐 {𝐷})) = (◡({𝐴} +𝑐 {𝐵})(dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))◡({𝐶} +𝑐 {𝐷})))
51	49, 50	eqtrd 2813	. 2 ⊢ (𝜑 → ((◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐴} +𝑐 {𝐵}))𝑃(◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐶} +𝑐 {𝐷}))) = (◡({𝐴} +𝑐 {𝐵})(dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))◡({𝐶} +𝑐 {𝐷})))
52		f1ocnvfv 6806	. . . . 5 ⊢ (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) ∧ ⟨𝐴, 𝐵⟩ ∈ (𝑋 × 𝑌)) → (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘⟨𝐴, 𝐵⟩) = ◡({𝐴} +𝑐 {𝐵}) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐴} +𝑐 {𝐵})) = ⟨𝐴, 𝐵⟩))
53	11, 32, 52	sylancr 581	. . . 4 ⊢ (𝜑 → (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘⟨𝐴, 𝐵⟩) = ◡({𝐴} +𝑐 {𝐵}) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐴} +𝑐 {𝐵})) = ⟨𝐴, 𝐵⟩))
54	30, 53	mpd 15	. . 3 ⊢ (𝜑 → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐴} +𝑐 {𝐵})) = ⟨𝐴, 𝐵⟩)
55		f1ocnvfv 6806	. . . . 5 ⊢ (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) ∧ ⟨𝐶, 𝐷⟩ ∈ (𝑋 × 𝑌)) → (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘⟨𝐶, 𝐷⟩) = ◡({𝐶} +𝑐 {𝐷}) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐶} +𝑐 {𝐷})) = ⟨𝐶, 𝐷⟩))
56	11, 45, 55	sylancr 581	. . . 4 ⊢ (𝜑 → (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘⟨𝐶, 𝐷⟩) = ◡({𝐶} +𝑐 {𝐷}) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐶} +𝑐 {𝐷})) = ⟨𝐶, 𝐷⟩))
57	43, 56	mpd 15	. . 3 ⊢ (𝜑 → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐶} +𝑐 {𝐷})) = ⟨𝐶, 𝐷⟩)
58	54, 57	oveq12d 6940	. 2 ⊢ (𝜑 → ((◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐴} +𝑐 {𝐵}))𝑃(◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐶} +𝑐 {𝐷}))) = (⟨𝐴, 𝐵⟩𝑃⟨𝐶, 𝐷⟩))
59		eqid 2777	. . . 4 ⊢ (Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) = (Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))
60		fvexd 6461	. . . 4 ⊢ (𝜑 → (Scalar‘𝑅) ∈ V)
61		2on 7852	. . . . 5 ⊢ 2o ∈ On
62	61	a1i 11	. . . 4 ⊢ (𝜑 → 2o ∈ On)
63		xpscfn 16605	. . . . 5 ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → ◡({𝑅} +𝑐 {𝑆}) Fn 2o)
64	4, 5, 63	syl2anc 579	. . . 4 ⊢ (𝜑 → ◡({𝑅} +𝑐 {𝑆}) Fn 2o)
65	37, 10	eleqtrd 2860	. . . 4 ⊢ (𝜑 → ◡({𝐴} +𝑐 {𝐵}) ∈ (Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))))
66	48, 10	eleqtrd 2860	. . . 4 ⊢ (𝜑 → ◡({𝐶} +𝑐 {𝐷}) ∈ (Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))))
67		eqid 2777	. . . 4 ⊢ (dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) = (dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))
68	8, 59, 60, 62, 64, 65, 66, 67	prdsdsval 16524	. . 3 ⊢ (𝜑 → (◡({𝐴} +𝑐 {𝐵})(dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))◡({𝐶} +𝑐 {𝐷})) = sup((ran (𝑘 ∈ 2o ↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))) ∪ {0}), ℝ*, < ))
69		df2o3 7857	. . . . . . . . . . 11 ⊢ 2o = {∅, 1o}
70	69	rexeqi 3338	. . . . . . . . . 10 ⊢ (∃𝑘 ∈ 2o 𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)) ↔ ∃𝑘 ∈ {∅, 1o}𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)))
71		0ex 5026	. . . . . . . . . . 11 ⊢ ∅ ∈ V
72		1oex 7851	. . . . . . . . . . 11 ⊢ 1o ∈ V
73		2fveq3 6451	. . . . . . . . . . . . 13 ⊢ (𝑘 = ∅ → (dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) = (dist‘(◡({𝑅} +𝑐 {𝑆})‘∅)))
74		fveq2 6446	. . . . . . . . . . . . 13 ⊢ (𝑘 = ∅ → (◡({𝐴} +𝑐 {𝐵})‘𝑘) = (◡({𝐴} +𝑐 {𝐵})‘∅))
75		fveq2 6446	. . . . . . . . . . . . 13 ⊢ (𝑘 = ∅ → (◡({𝐶} +𝑐 {𝐷})‘𝑘) = (◡({𝐶} +𝑐 {𝐷})‘∅))
76	73, 74, 75	oveq123d 6943	. . . . . . . . . . . 12 ⊢ (𝑘 = ∅ → ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)) = ((◡({𝐴} +𝑐 {𝐵})‘∅)(dist‘(◡({𝑅} +𝑐 {𝑆})‘∅))(◡({𝐶} +𝑐 {𝐷})‘∅)))
77	76	eqeq2d 2787	. . . . . . . . . . 11 ⊢ (𝑘 = ∅ → (𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)) ↔ 𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘∅)(dist‘(◡({𝑅} +𝑐 {𝑆})‘∅))(◡({𝐶} +𝑐 {𝐷})‘∅))))
78		2fveq3 6451	. . . . . . . . . . . . 13 ⊢ (𝑘 = 1o → (dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) = (dist‘(◡({𝑅} +𝑐 {𝑆})‘1o)))
79		fveq2 6446	. . . . . . . . . . . . 13 ⊢ (𝑘 = 1o → (◡({𝐴} +𝑐 {𝐵})‘𝑘) = (◡({𝐴} +𝑐 {𝐵})‘1o))
80		fveq2 6446	. . . . . . . . . . . . 13 ⊢ (𝑘 = 1o → (◡({𝐶} +𝑐 {𝐷})‘𝑘) = (◡({𝐶} +𝑐 {𝐷})‘1o))
81	78, 79, 80	oveq123d 6943	. . . . . . . . . . . 12 ⊢ (𝑘 = 1o → ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)) = ((◡({𝐴} +𝑐 {𝐵})‘1o)(dist‘(◡({𝑅} +𝑐 {𝑆})‘1o))(◡({𝐶} +𝑐 {𝐷})‘1o)))
82	81	eqeq2d 2787	. . . . . . . . . . 11 ⊢ (𝑘 = 1o → (𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)) ↔ 𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘1o)(dist‘(◡({𝑅} +𝑐 {𝑆})‘1o))(◡({𝐶} +𝑐 {𝐷})‘1o))))
83	71, 72, 77, 82	rexpr 4467	. . . . . . . . . 10 ⊢ (∃𝑘 ∈ {∅, 1o}𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)) ↔ (𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘∅)(dist‘(◡({𝑅} +𝑐 {𝑆})‘∅))(◡({𝐶} +𝑐 {𝐷})‘∅)) ∨ 𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘1o)(dist‘(◡({𝑅} +𝑐 {𝑆})‘1o))(◡({𝐶} +𝑐 {𝐷})‘1o))))
84	70, 83	bitri 267	. . . . . . . . 9 ⊢ (∃𝑘 ∈ 2o 𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)) ↔ (𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘∅)(dist‘(◡({𝑅} +𝑐 {𝑆})‘∅))(◡({𝐶} +𝑐 {𝐷})‘∅)) ∨ 𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘1o)(dist‘(◡({𝑅} +𝑐 {𝑆})‘1o))(◡({𝐶} +𝑐 {𝐷})‘1o))))
85		xpsc0 16606	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ 𝑉 → (◡({𝑅} +𝑐 {𝑆})‘∅) = 𝑅)
86	4, 85	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (◡({𝑅} +𝑐 {𝑆})‘∅) = 𝑅)
87	86	fveq2d 6450	. . . . . . . . . . . . 13 ⊢ (𝜑 → (dist‘(◡({𝑅} +𝑐 {𝑆})‘∅)) = (dist‘𝑅))
88		xpsc0 16606	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ 𝑋 → (◡({𝐴} +𝑐 {𝐵})‘∅) = 𝐴)
89	26, 88	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (◡({𝐴} +𝑐 {𝐵})‘∅) = 𝐴)
90		xpsc0 16606	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∈ 𝑋 → (◡({𝐶} +𝑐 {𝐷})‘∅) = 𝐶)
91	39, 90	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (◡({𝐶} +𝑐 {𝐷})‘∅) = 𝐶)
92	87, 89, 91	oveq123d 6943	. . . . . . . . . . . 12 ⊢ (𝜑 → ((◡({𝐴} +𝑐 {𝐵})‘∅)(dist‘(◡({𝑅} +𝑐 {𝑆})‘∅))(◡({𝐶} +𝑐 {𝐷})‘∅)) = (𝐴(dist‘𝑅)𝐶))
93	17	oveqi 6935	. . . . . . . . . . . . 13 ⊢ (𝐴𝑀𝐶) = (𝐴((dist‘𝑅) ↾ (𝑋 × 𝑋))𝐶)
94	26, 39	ovresd 7078	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴((dist‘𝑅) ↾ (𝑋 × 𝑋))𝐶) = (𝐴(dist‘𝑅)𝐶))
95	93, 94	syl5eq 2825	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴𝑀𝐶) = (𝐴(dist‘𝑅)𝐶))
96	92, 95	eqtr4d 2816	. . . . . . . . . . 11 ⊢ (𝜑 → ((◡({𝐴} +𝑐 {𝐵})‘∅)(dist‘(◡({𝑅} +𝑐 {𝑆})‘∅))(◡({𝐶} +𝑐 {𝐷})‘∅)) = (𝐴𝑀𝐶))
97	96	eqeq2d 2787	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘∅)(dist‘(◡({𝑅} +𝑐 {𝑆})‘∅))(◡({𝐶} +𝑐 {𝐷})‘∅)) ↔ 𝑥 = (𝐴𝑀𝐶)))
98		xpsc1 16607	. . . . . . . . . . . . . . 15 ⊢ (𝑆 ∈ 𝑊 → (◡({𝑅} +𝑐 {𝑆})‘1o) = 𝑆)
99	5, 98	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (◡({𝑅} +𝑐 {𝑆})‘1o) = 𝑆)
100	99	fveq2d 6450	. . . . . . . . . . . . 13 ⊢ (𝜑 → (dist‘(◡({𝑅} +𝑐 {𝑆})‘1o)) = (dist‘𝑆))
101		xpsc1 16607	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ 𝑌 → (◡({𝐴} +𝑐 {𝐵})‘1o) = 𝐵)
102	27, 101	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (◡({𝐴} +𝑐 {𝐵})‘1o) = 𝐵)
103		xpsc1 16607	. . . . . . . . . . . . . 14 ⊢ (𝐷 ∈ 𝑌 → (◡({𝐶} +𝑐 {𝐷})‘1o) = 𝐷)
104	40, 103	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (◡({𝐶} +𝑐 {𝐷})‘1o) = 𝐷)
105	100, 102, 104	oveq123d 6943	. . . . . . . . . . . 12 ⊢ (𝜑 → ((◡({𝐴} +𝑐 {𝐵})‘1o)(dist‘(◡({𝑅} +𝑐 {𝑆})‘1o))(◡({𝐶} +𝑐 {𝐷})‘1o)) = (𝐵(dist‘𝑆)𝐷))
106	18	oveqi 6935	. . . . . . . . . . . . 13 ⊢ (𝐵𝑁𝐷) = (𝐵((dist‘𝑆) ↾ (𝑌 × 𝑌))𝐷)
107	27, 40	ovresd 7078	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵((dist‘𝑆) ↾ (𝑌 × 𝑌))𝐷) = (𝐵(dist‘𝑆)𝐷))
108	106, 107	syl5eq 2825	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐵𝑁𝐷) = (𝐵(dist‘𝑆)𝐷))
109	105, 108	eqtr4d 2816	. . . . . . . . . . 11 ⊢ (𝜑 → ((◡({𝐴} +𝑐 {𝐵})‘1o)(dist‘(◡({𝑅} +𝑐 {𝑆})‘1o))(◡({𝐶} +𝑐 {𝐷})‘1o)) = (𝐵𝑁𝐷))
110	109	eqeq2d 2787	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘1o)(dist‘(◡({𝑅} +𝑐 {𝑆})‘1o))(◡({𝐶} +𝑐 {𝐷})‘1o)) ↔ 𝑥 = (𝐵𝑁𝐷)))
111	97, 110	orbi12d 905	. . . . . . . . 9 ⊢ (𝜑 → ((𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘∅)(dist‘(◡({𝑅} +𝑐 {𝑆})‘∅))(◡({𝐶} +𝑐 {𝐷})‘∅)) ∨ 𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘1o)(dist‘(◡({𝑅} +𝑐 {𝑆})‘1o))(◡({𝐶} +𝑐 {𝐷})‘1o))) ↔ (𝑥 = (𝐴𝑀𝐶) ∨ 𝑥 = (𝐵𝑁𝐷))))
112	84, 111	syl5bb 275	. . . . . . . 8 ⊢ (𝜑 → (∃𝑘 ∈ 2o 𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)) ↔ (𝑥 = (𝐴𝑀𝐶) ∨ 𝑥 = (𝐵𝑁𝐷))))
113		vex 3400	. . . . . . . . 9 ⊢ 𝑥 ∈ V
114		eqid 2777	. . . . . . . . . 10 ⊢ (𝑘 ∈ 2o ↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))) = (𝑘 ∈ 2o ↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)))
115	114	elrnmpt 5618	. . . . . . . . 9 ⊢ (𝑥 ∈ V → (𝑥 ∈ ran (𝑘 ∈ 2o ↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))) ↔ ∃𝑘 ∈ 2o 𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))))
116	113, 115	ax-mp 5	. . . . . . . 8 ⊢ (𝑥 ∈ ran (𝑘 ∈ 2o ↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))) ↔ ∃𝑘 ∈ 2o 𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)))
117	113	elpr 4420	. . . . . . . 8 ⊢ (𝑥 ∈ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ↔ (𝑥 = (𝐴𝑀𝐶) ∨ 𝑥 = (𝐵𝑁𝐷)))
118	112, 116, 117	3bitr4g 306	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ ran (𝑘 ∈ 2o ↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))) ↔ 𝑥 ∈ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)}))
119	118	eqrdv 2775	. . . . . 6 ⊢ (𝜑 → ran (𝑘 ∈ 2o ↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))) = {(𝐴𝑀𝐶), (𝐵𝑁𝐷)})
120	119	uneq1d 3988	. . . . 5 ⊢ (𝜑 → (ran (𝑘 ∈ 2o ↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))) ∪ {0}) = ({(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ∪ {0}))
121		uncom 3979	. . . . 5 ⊢ ({(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ∪ {0}) = ({0} ∪ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)})
122	120, 121	syl6eq 2829	. . . 4 ⊢ (𝜑 → (ran (𝑘 ∈ 2o ↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))) ∪ {0}) = ({0} ∪ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)}))
123	122	supeq1d 8640	. . 3 ⊢ (𝜑 → sup((ran (𝑘 ∈ 2o ↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))) ∪ {0}), ℝ*, < ) = sup(({0} ∪ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)}), ℝ*, < ))
124		0xr 10423	. . . . . 6 ⊢ 0 ∈ ℝ*
125	124	a1i 11	. . . . 5 ⊢ (𝜑 → 0 ∈ ℝ*)
126	125	snssd 4571	. . . 4 ⊢ (𝜑 → {0} ⊆ ℝ*)
127		xmetcl 22544	. . . . . 6 ⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (𝐴𝑀𝐶) ∈ ℝ*)
128	19, 26, 39, 127	syl3anc 1439	. . . . 5 ⊢ (𝜑 → (𝐴𝑀𝐶) ∈ ℝ*)
129		xmetcl 22544	. . . . . 6 ⊢ ((𝑁 ∈ (∞Met‘𝑌) ∧ 𝐵 ∈ 𝑌 ∧ 𝐷 ∈ 𝑌) → (𝐵𝑁𝐷) ∈ ℝ*)
130	20, 27, 40, 129	syl3anc 1439	. . . . 5 ⊢ (𝜑 → (𝐵𝑁𝐷) ∈ ℝ*)
131		prssi 4583	. . . . 5 ⊢ (((𝐴𝑀𝐶) ∈ ℝ* ∧ (𝐵𝑁𝐷) ∈ ℝ*) → {(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ⊆ ℝ*)
132	128, 130, 131	syl2anc 579	. . . 4 ⊢ (𝜑 → {(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ⊆ ℝ*)
133		xrltso 12284	. . . . . 6 ⊢ < Or ℝ*
134		supsn 8666	. . . . . 6 ⊢ (( < Or ℝ* ∧ 0 ∈ ℝ*) → sup({0}, ℝ*, < ) = 0)
135	133, 124, 134	mp2an 682	. . . . 5 ⊢ sup({0}, ℝ*, < ) = 0
136		supxrcl 12457	. . . . . . 7 ⊢ ({(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ⊆ ℝ* → sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ) ∈ ℝ*)
137	132, 136	syl 17	. . . . . 6 ⊢ (𝜑 → sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ) ∈ ℝ*)
138		xmetge0 22557	. . . . . . 7 ⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → 0 ≤ (𝐴𝑀𝐶))
139	19, 26, 39, 138	syl3anc 1439	. . . . . 6 ⊢ (𝜑 → 0 ≤ (𝐴𝑀𝐶))
140		ovex 6954	. . . . . . . 8 ⊢ (𝐴𝑀𝐶) ∈ V
141	140	prid1 4528	. . . . . . 7 ⊢ (𝐴𝑀𝐶) ∈ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)}
142		supxrub 12466	. . . . . . 7 ⊢ (({(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ⊆ ℝ* ∧ (𝐴𝑀𝐶) ∈ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)}) → (𝐴𝑀𝐶) ≤ sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ))
143	132, 141, 142	sylancl 580	. . . . . 6 ⊢ (𝜑 → (𝐴𝑀𝐶) ≤ sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ))
144	125, 128, 137, 139, 143	xrletrd 12305	. . . . 5 ⊢ (𝜑 → 0 ≤ sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ))
145	135, 144	syl5eqbr 4921	. . . 4 ⊢ (𝜑 → sup({0}, ℝ*, < ) ≤ sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ))
146		supxrun 12458	. . . 4 ⊢ (({0} ⊆ ℝ* ∧ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ⊆ ℝ* ∧ sup({0}, ℝ*, < ) ≤ sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < )) → sup(({0} ∪ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)}), ℝ*, < ) = sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ))
147	126, 132, 145, 146	syl3anc 1439	. . 3 ⊢ (𝜑 → sup(({0} ∪ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)}), ℝ*, < ) = sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ))
148	68, 123, 147	3eqtrd 2817	. 2 ⊢ (𝜑 → (◡({𝐴} +𝑐 {𝐵})(dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))◡({𝐶} +𝑐 {𝐷})) = sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ))
149	51, 58, 148	3eqtr3d 2821	1 ⊢ (𝜑 → (⟨𝐴, 𝐵⟩𝑃⟨𝐶, 𝐷⟩) = sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ))

Syntax hints:   → wi 4   ↔ wb 198   ∨ wo 836   = wceq 1601   ∈ wcel 2106  ∃wrex 3090  Vcvv 3397   ∪ cun 3789   ⊆ wss 3791  ∅c0 4140  {csn 4397  {cpr 4399  ⟨cop 4403   class class class wbr 4886   ↦ cmpt 4965   Or wor 5273   × cxp 5353  ^◡ccnv 5354  ran crn 5356   ↾ cres 5357  Oncon0 5976   Fn wfn 6130  ⟶wf 6131  –1-1-onto→wf1o 6134  ‘cfv 6135  (class class class)co 6922   ↦ cmpt2 6924  1_oc1o 7836  2_oc2o 7837  supcsup 8634   +_𝑐 ccda 9324  0cc0 10272  ℝ^*cxr 10410   < clt 10411   ≤ cle 10412  Basecbs 16255  Scalarcsca 16341  distcds 16347  X_scprds 16492   ×_s cxps 16552  ∞Metcxmet 20127

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-8 2108  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753  ax-rep 5006  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-inf2 8835  ax-cnex 10328  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-addrcl 10333  ax-mulcl 10334  ax-mulrcl 10335  ax-mulcom 10336  ax-addass 10337  ax-mulass 10338  ax-distr 10339  ax-i2m1 10340  ax-1ne0 10341  ax-1rid 10342  ax-rnegex 10343  ax-rrecex 10344  ax-cnre 10345  ax-pre-lttri 10346  ax-pre-lttrn 10347  ax-pre-ltadd 10348  ax-pre-mulgt0 10349  ax-pre-sup 10350

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2550  df-eu 2586  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-ne 2969  df-nel 3075  df-ral 3094  df-rex 3095  df-reu 3096  df-rmo 3097  df-rab 3098  df-v 3399  df-sbc 3652  df-csb 3751  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-pss 3807  df-nul 4141  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4672  df-int 4711  df-iun 4755  df-iin 4756  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-se 5315  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-pred 5933  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-isom 6144  df-riota 6883  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-of 7174  df-om 7344  df-1st 7445  df-2nd 7446  df-supp 7577  df-wrecs 7689  df-recs 7751  df-rdg 7789  df-1o 7843  df-2o 7844  df-oadd 7847  df-er 8026  df-map 8142  df-ixp 8195  df-en 8242  df-dom 8243  df-sdom 8244  df-fin 8245  df-fsupp 8564  df-sup 8636  df-inf 8637  df-oi 8704  df-card 9098  df-cda 9325  df-pnf 10413  df-mnf 10414  df-xr 10415  df-ltxr 10416  df-le 10417  df-sub 10608  df-neg 10609  df-div 11033  df-nn 11375  df-2 11438  df-3 11439  df-4 11440  df-5 11441  df-6 11442  df-7 11443  df-8 11444  df-9 11445  df-n0 11643  df-z 11729  df-dec 11846  df-uz 11993  df-rp 12138  df-xneg 12257  df-xadd 12258  df-xmul 12259  df-icc 12494  df-fz 12644  df-fzo 12785  df-seq 13120  df-hash 13436  df-struct 16257  df-ndx 16258  df-slot 16259  df-base 16261  df-sets 16262  df-ress 16263  df-plusg 16351  df-mulr 16352  df-sca 16354  df-vsca 16355  df-ip 16356  df-tset 16357  df-ple 16358  df-ds 16360  df-hom 16362  df-cco 16363  df-0g 16488  df-gsum 16489  df-prds 16494  df-xrs 16548  df-imas 16554  df-xps 16556  df-mre 16632  df-mrc 16633  df-acs 16635  df-mgm 17628  df-sgrp 17670  df-mnd 17681  df-submnd 17722  df-mulg 17928  df-cntz 18133  df-cmn 18581  df-xmet 20135

This theorem is referenced by:  tmsxpsval  22751