MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xpsdsval Structured version   Visualization version   GIF version

Theorem xpsdsval 22109
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.
StepHypRef 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 2621 . . . . 5 (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})) = (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))
7 eqid 2621 . . . . 5 (Scalar‘𝑅) = (Scalar‘𝑅)
8 eqid 2621 . . . . 5 ((Scalar‘𝑅)Xs({𝑅} +𝑐 {𝑆})) = ((Scalar‘𝑅)Xs({𝑅} +𝑐 {𝑆}))
91, 2, 3, 4, 5, 6, 7, 8xpsval 16164 . . . 4 (𝜑𝑇 = ((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})) “s ((Scalar‘𝑅)Xs({𝑅} +𝑐 {𝑆}))))
101, 2, 3, 4, 5, 6, 7, 8xpslem 16165 . . . 4 (𝜑 → ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})) = (Base‘((Scalar‘𝑅)Xs({𝑅} +𝑐 {𝑆}))))
116xpsff1o2 16163 . . . . 5 (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))
12 f1ocnv 6111 . . . . 5 ((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})) → (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})):ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))–1-1-onto→(𝑋 × 𝑌))
1311, 12mp1i 13 . . . 4 (𝜑(𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})):ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))–1-1-onto→(𝑋 × 𝑌))
14 ovexd 6640 . . . 4 (𝜑 → ((Scalar‘𝑅)Xs({𝑅} +𝑐 {𝑆})) ∈ V)
15 eqid 2621 . . . 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‘𝑌))
211, 2, 3, 4, 5, 16, 17, 18, 19, 20xpsxmetlem 22107 . . . . 5 (𝜑 → (dist‘((Scalar‘𝑅)Xs({𝑅} +𝑐 {𝑆}))) ∈ (∞Met‘ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))))
22 ssid 3608 . . . . 5 ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})) ⊆ ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))
23 xmetres2 22089 . . . . 5 (((dist‘((Scalar‘𝑅)Xs({𝑅} +𝑐 {𝑆}))) ∈ (∞Met‘ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))) ∧ ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})) ⊆ ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))) → ((dist‘((Scalar‘𝑅)Xs({𝑅} +𝑐 {𝑆}))) ↾ (ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})) × ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})))) ∈ (∞Met‘ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))))
2421, 22, 23sylancl 693 . . . 4 (𝜑 → ((dist‘((Scalar‘𝑅)Xs({𝑅} +𝑐 {𝑆}))) ↾ (ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})) × ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})))) ∈ (∞Met‘ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))))
25 df-ov 6613 . . . . . 6 (𝐴(𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))𝐵) = ((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘⟨𝐴, 𝐵⟩)
26 xpsds.a . . . . . . 7 (𝜑𝐴𝑋)
27 xpsds.b . . . . . . 7 (𝜑𝐵𝑌)
286xpsfval 16159 . . . . . . 7 ((𝐴𝑋𝐵𝑌) → (𝐴(𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))𝐵) = ({𝐴} +𝑐 {𝐵}))
2926, 27, 28syl2anc 692 . . . . . 6 (𝜑 → (𝐴(𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))𝐵) = ({𝐴} +𝑐 {𝐵}))
3025, 29syl5eqr 2669 . . . . 5 (𝜑 → ((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘⟨𝐴, 𝐵⟩) = ({𝐴} +𝑐 {𝐵}))
31 opelxpi 5113 . . . . . . 7 ((𝐴𝑋𝐵𝑌) → ⟨𝐴, 𝐵⟩ ∈ (𝑋 × 𝑌))
3226, 27, 31syl2anc 692 . . . . . 6 (𝜑 → ⟨𝐴, 𝐵⟩ ∈ (𝑋 × 𝑌))
33 f1of 6099 . . . . . . . 8 ((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})) → (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)⟶ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})))
3411, 33ax-mp 5 . . . . . . 7 (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)⟶ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))
3534ffvelrni 6319 . . . . . 6 (⟨𝐴, 𝐵⟩ ∈ (𝑋 × 𝑌) → ((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘⟨𝐴, 𝐵⟩) ∈ ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})))
3632, 35syl 17 . . . . 5 (𝜑 → ((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘⟨𝐴, 𝐵⟩) ∈ ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})))
3730, 36eqeltrrd 2699 . . . 4 (𝜑({𝐴} +𝑐 {𝐵}) ∈ ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})))
38 df-ov 6613 . . . . . 6 (𝐶(𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))𝐷) = ((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘⟨𝐶, 𝐷⟩)
39 xpsds.c . . . . . . 7 (𝜑𝐶𝑋)
40 xpsds.d . . . . . . 7 (𝜑𝐷𝑌)
416xpsfval 16159 . . . . . . 7 ((𝐶𝑋𝐷𝑌) → (𝐶(𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))𝐷) = ({𝐶} +𝑐 {𝐷}))
4239, 40, 41syl2anc 692 . . . . . 6 (𝜑 → (𝐶(𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))𝐷) = ({𝐶} +𝑐 {𝐷}))
4338, 42syl5eqr 2669 . . . . 5 (𝜑 → ((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘⟨𝐶, 𝐷⟩) = ({𝐶} +𝑐 {𝐷}))
44 opelxpi 5113 . . . . . . 7 ((𝐶𝑋𝐷𝑌) → ⟨𝐶, 𝐷⟩ ∈ (𝑋 × 𝑌))
4539, 40, 44syl2anc 692 . . . . . 6 (𝜑 → ⟨𝐶, 𝐷⟩ ∈ (𝑋 × 𝑌))
4634ffvelrni 6319 . . . . . 6 (⟨𝐶, 𝐷⟩ ∈ (𝑋 × 𝑌) → ((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘⟨𝐶, 𝐷⟩) ∈ ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})))
4745, 46syl 17 . . . . 5 (𝜑 → ((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘⟨𝐶, 𝐷⟩) ∈ ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})))
4843, 47eqeltrrd 2699 . . . 4 (𝜑({𝐶} +𝑐 {𝐷}) ∈ ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})))
499, 10, 13, 14, 15, 16, 24, 37, 48imasdsf1o 22102 . . 3 (𝜑 → (((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘({𝐴} +𝑐 {𝐵}))𝑃((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘({𝐶} +𝑐 {𝐷}))) = (({𝐴} +𝑐 {𝐵})((dist‘((Scalar‘𝑅)Xs({𝑅} +𝑐 {𝑆}))) ↾ (ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})) × ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))))({𝐶} +𝑐 {𝐷})))
5037, 48ovresd 6761 . . 3 (𝜑 → (({𝐴} +𝑐 {𝐵})((dist‘((Scalar‘𝑅)Xs({𝑅} +𝑐 {𝑆}))) ↾ (ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})) × ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))))({𝐶} +𝑐 {𝐷})) = (({𝐴} +𝑐 {𝐵})(dist‘((Scalar‘𝑅)Xs({𝑅} +𝑐 {𝑆})))({𝐶} +𝑐 {𝐷})))
5149, 50eqtrd 2655 . 2 (𝜑 → (((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘({𝐴} +𝑐 {𝐵}))𝑃((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘({𝐶} +𝑐 {𝐷}))) = (({𝐴} +𝑐 {𝐵})(dist‘((Scalar‘𝑅)Xs({𝑅} +𝑐 {𝑆})))({𝐶} +𝑐 {𝐷})))
52 f1ocnvfv 6494 . . . . 5 (((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})) ∧ ⟨𝐴, 𝐵⟩ ∈ (𝑋 × 𝑌)) → (((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘⟨𝐴, 𝐵⟩) = ({𝐴} +𝑐 {𝐵}) → ((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘({𝐴} +𝑐 {𝐵})) = ⟨𝐴, 𝐵⟩))
5311, 32, 52sylancr 694 . . . 4 (𝜑 → (((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘⟨𝐴, 𝐵⟩) = ({𝐴} +𝑐 {𝐵}) → ((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘({𝐴} +𝑐 {𝐵})) = ⟨𝐴, 𝐵⟩))
5430, 53mpd 15 . . 3 (𝜑 → ((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘({𝐴} +𝑐 {𝐵})) = ⟨𝐴, 𝐵⟩)
55 f1ocnvfv 6494 . . . . 5 (((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran (𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦})) ∧ ⟨𝐶, 𝐷⟩ ∈ (𝑋 × 𝑌)) → (((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘⟨𝐶, 𝐷⟩) = ({𝐶} +𝑐 {𝐷}) → ((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘({𝐶} +𝑐 {𝐷})) = ⟨𝐶, 𝐷⟩))
5611, 45, 55sylancr 694 . . . 4 (𝜑 → (((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘⟨𝐶, 𝐷⟩) = ({𝐶} +𝑐 {𝐷}) → ((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘({𝐶} +𝑐 {𝐷})) = ⟨𝐶, 𝐷⟩))
5743, 56mpd 15 . . 3 (𝜑 → ((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘({𝐶} +𝑐 {𝐷})) = ⟨𝐶, 𝐷⟩)
5854, 57oveq12d 6628 . 2 (𝜑 → (((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘({𝐴} +𝑐 {𝐵}))𝑃((𝑥𝑋, 𝑦𝑌({𝑥} +𝑐 {𝑦}))‘({𝐶} +𝑐 {𝐷}))) = (⟨𝐴, 𝐵𝑃𝐶, 𝐷⟩))
59 eqid 2621 . . . 4 (Base‘((Scalar‘𝑅)Xs({𝑅} +𝑐 {𝑆}))) = (Base‘((Scalar‘𝑅)Xs({𝑅} +𝑐 {𝑆})))
60 fvex 6163 . . . . 5 (Scalar‘𝑅) ∈ V
6160a1i 11 . . . 4 (𝜑 → (Scalar‘𝑅) ∈ V)
62 2on 7520 . . . . 5 2𝑜 ∈ On
6362a1i 11 . . . 4 (𝜑 → 2𝑜 ∈ On)
64 xpscfn 16151 . . . . 5 ((𝑅𝑉𝑆𝑊) → ({𝑅} +𝑐 {𝑆}) Fn 2𝑜)
654, 5, 64syl2anc 692 . . . 4 (𝜑({𝑅} +𝑐 {𝑆}) Fn 2𝑜)
6637, 10eleqtrd 2700 . . . 4 (𝜑({𝐴} +𝑐 {𝐵}) ∈ (Base‘((Scalar‘𝑅)Xs({𝑅} +𝑐 {𝑆}))))
6748, 10eleqtrd 2700 . . . 4 (𝜑({𝐶} +𝑐 {𝐷}) ∈ (Base‘((Scalar‘𝑅)Xs({𝑅} +𝑐 {𝑆}))))
68 eqid 2621 . . . 4 (dist‘((Scalar‘𝑅)Xs({𝑅} +𝑐 {𝑆}))) = (dist‘((Scalar‘𝑅)Xs({𝑅} +𝑐 {𝑆})))
698, 59, 61, 63, 65, 66, 67, 68prdsdsval 16070 . . 3 (𝜑 → (({𝐴} +𝑐 {𝐵})(dist‘((Scalar‘𝑅)Xs({𝑅} +𝑐 {𝑆})))({𝐶} +𝑐 {𝐷})) = sup((ran (𝑘 ∈ 2𝑜 ↦ ((({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(({𝑅} +𝑐 {𝑆})‘𝑘))(({𝐶} +𝑐 {𝐷})‘𝑘))) ∪ {0}), ℝ*, < ))
70 df2o3 7525 . . . . . . . . . . 11 2𝑜 = {∅, 1𝑜}
7170rexeqi 3135 . . . . . . . . . 10 (∃𝑘 ∈ 2𝑜 𝑥 = ((({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(({𝑅} +𝑐 {𝑆})‘𝑘))(({𝐶} +𝑐 {𝐷})‘𝑘)) ↔ ∃𝑘 ∈ {∅, 1𝑜}𝑥 = ((({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(({𝑅} +𝑐 {𝑆})‘𝑘))(({𝐶} +𝑐 {𝐷})‘𝑘)))
72 0ex 4755 . . . . . . . . . . 11 ∅ ∈ V
73 1on 7519 . . . . . . . . . . . 12 1𝑜 ∈ On
7473elexi 3202 . . . . . . . . . . 11 1𝑜 ∈ V
75 fveq2 6153 . . . . . . . . . . . . . 14 (𝑘 = ∅ → (({𝑅} +𝑐 {𝑆})‘𝑘) = (({𝑅} +𝑐 {𝑆})‘∅))
7675fveq2d 6157 . . . . . . . . . . . . 13 (𝑘 = ∅ → (dist‘(({𝑅} +𝑐 {𝑆})‘𝑘)) = (dist‘(({𝑅} +𝑐 {𝑆})‘∅)))
77 fveq2 6153 . . . . . . . . . . . . 13 (𝑘 = ∅ → (({𝐴} +𝑐 {𝐵})‘𝑘) = (({𝐴} +𝑐 {𝐵})‘∅))
78 fveq2 6153 . . . . . . . . . . . . 13 (𝑘 = ∅ → (({𝐶} +𝑐 {𝐷})‘𝑘) = (({𝐶} +𝑐 {𝐷})‘∅))
7976, 77, 78oveq123d 6631 . . . . . . . . . . . 12 (𝑘 = ∅ → ((({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(({𝑅} +𝑐 {𝑆})‘𝑘))(({𝐶} +𝑐 {𝐷})‘𝑘)) = ((({𝐴} +𝑐 {𝐵})‘∅)(dist‘(({𝑅} +𝑐 {𝑆})‘∅))(({𝐶} +𝑐 {𝐷})‘∅)))
8079eqeq2d 2631 . . . . . . . . . . 11 (𝑘 = ∅ → (𝑥 = ((({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(({𝑅} +𝑐 {𝑆})‘𝑘))(({𝐶} +𝑐 {𝐷})‘𝑘)) ↔ 𝑥 = ((({𝐴} +𝑐 {𝐵})‘∅)(dist‘(({𝑅} +𝑐 {𝑆})‘∅))(({𝐶} +𝑐 {𝐷})‘∅))))
81 fveq2 6153 . . . . . . . . . . . . . 14 (𝑘 = 1𝑜 → (({𝑅} +𝑐 {𝑆})‘𝑘) = (({𝑅} +𝑐 {𝑆})‘1𝑜))
8281fveq2d 6157 . . . . . . . . . . . . 13 (𝑘 = 1𝑜 → (dist‘(({𝑅} +𝑐 {𝑆})‘𝑘)) = (dist‘(({𝑅} +𝑐 {𝑆})‘1𝑜)))
83 fveq2 6153 . . . . . . . . . . . . 13 (𝑘 = 1𝑜 → (({𝐴} +𝑐 {𝐵})‘𝑘) = (({𝐴} +𝑐 {𝐵})‘1𝑜))
84 fveq2 6153 . . . . . . . . . . . . 13 (𝑘 = 1𝑜 → (({𝐶} +𝑐 {𝐷})‘𝑘) = (({𝐶} +𝑐 {𝐷})‘1𝑜))
8582, 83, 84oveq123d 6631 . . . . . . . . . . . 12 (𝑘 = 1𝑜 → ((({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(({𝑅} +𝑐 {𝑆})‘𝑘))(({𝐶} +𝑐 {𝐷})‘𝑘)) = ((({𝐴} +𝑐 {𝐵})‘1𝑜)(dist‘(({𝑅} +𝑐 {𝑆})‘1𝑜))(({𝐶} +𝑐 {𝐷})‘1𝑜)))
8685eqeq2d 2631 . . . . . . . . . . 11 (𝑘 = 1𝑜 → (𝑥 = ((({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(({𝑅} +𝑐 {𝑆})‘𝑘))(({𝐶} +𝑐 {𝐷})‘𝑘)) ↔ 𝑥 = ((({𝐴} +𝑐 {𝐵})‘1𝑜)(dist‘(({𝑅} +𝑐 {𝑆})‘1𝑜))(({𝐶} +𝑐 {𝐷})‘1𝑜))))
8772, 74, 80, 86rexpr 4215 . . . . . . . . . 10 (∃𝑘 ∈ {∅, 1𝑜}𝑥 = ((({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(({𝑅} +𝑐 {𝑆})‘𝑘))(({𝐶} +𝑐 {𝐷})‘𝑘)) ↔ (𝑥 = ((({𝐴} +𝑐 {𝐵})‘∅)(dist‘(({𝑅} +𝑐 {𝑆})‘∅))(({𝐶} +𝑐 {𝐷})‘∅)) ∨ 𝑥 = ((({𝐴} +𝑐 {𝐵})‘1𝑜)(dist‘(({𝑅} +𝑐 {𝑆})‘1𝑜))(({𝐶} +𝑐 {𝐷})‘1𝑜))))
8871, 87bitri 264 . . . . . . . . 9 (∃𝑘 ∈ 2𝑜 𝑥 = ((({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(({𝑅} +𝑐 {𝑆})‘𝑘))(({𝐶} +𝑐 {𝐷})‘𝑘)) ↔ (𝑥 = ((({𝐴} +𝑐 {𝐵})‘∅)(dist‘(({𝑅} +𝑐 {𝑆})‘∅))(({𝐶} +𝑐 {𝐷})‘∅)) ∨ 𝑥 = ((({𝐴} +𝑐 {𝐵})‘1𝑜)(dist‘(({𝑅} +𝑐 {𝑆})‘1𝑜))(({𝐶} +𝑐 {𝐷})‘1𝑜))))
89 xpsc0 16152 . . . . . . . . . . . . . . 15 (𝑅𝑉 → (({𝑅} +𝑐 {𝑆})‘∅) = 𝑅)
904, 89syl 17 . . . . . . . . . . . . . 14 (𝜑 → (({𝑅} +𝑐 {𝑆})‘∅) = 𝑅)
9190fveq2d 6157 . . . . . . . . . . . . 13 (𝜑 → (dist‘(({𝑅} +𝑐 {𝑆})‘∅)) = (dist‘𝑅))
92 xpsc0 16152 . . . . . . . . . . . . . 14 (𝐴𝑋 → (({𝐴} +𝑐 {𝐵})‘∅) = 𝐴)
9326, 92syl 17 . . . . . . . . . . . . 13 (𝜑 → (({𝐴} +𝑐 {𝐵})‘∅) = 𝐴)
94 xpsc0 16152 . . . . . . . . . . . . . 14 (𝐶𝑋 → (({𝐶} +𝑐 {𝐷})‘∅) = 𝐶)
9539, 94syl 17 . . . . . . . . . . . . 13 (𝜑 → (({𝐶} +𝑐 {𝐷})‘∅) = 𝐶)
9691, 93, 95oveq123d 6631 . . . . . . . . . . . 12 (𝜑 → ((({𝐴} +𝑐 {𝐵})‘∅)(dist‘(({𝑅} +𝑐 {𝑆})‘∅))(({𝐶} +𝑐 {𝐷})‘∅)) = (𝐴(dist‘𝑅)𝐶))
9717oveqi 6623 . . . . . . . . . . . . 13 (𝐴𝑀𝐶) = (𝐴((dist‘𝑅) ↾ (𝑋 × 𝑋))𝐶)
9826, 39ovresd 6761 . . . . . . . . . . . . 13 (𝜑 → (𝐴((dist‘𝑅) ↾ (𝑋 × 𝑋))𝐶) = (𝐴(dist‘𝑅)𝐶))
9997, 98syl5eq 2667 . . . . . . . . . . . 12 (𝜑 → (𝐴𝑀𝐶) = (𝐴(dist‘𝑅)𝐶))
10096, 99eqtr4d 2658 . . . . . . . . . . 11 (𝜑 → ((({𝐴} +𝑐 {𝐵})‘∅)(dist‘(({𝑅} +𝑐 {𝑆})‘∅))(({𝐶} +𝑐 {𝐷})‘∅)) = (𝐴𝑀𝐶))
101100eqeq2d 2631 . . . . . . . . . 10 (𝜑 → (𝑥 = ((({𝐴} +𝑐 {𝐵})‘∅)(dist‘(({𝑅} +𝑐 {𝑆})‘∅))(({𝐶} +𝑐 {𝐷})‘∅)) ↔ 𝑥 = (𝐴𝑀𝐶)))
102 xpsc1 16153 . . . . . . . . . . . . . . 15 (𝑆𝑊 → (({𝑅} +𝑐 {𝑆})‘1𝑜) = 𝑆)
1035, 102syl 17 . . . . . . . . . . . . . 14 (𝜑 → (({𝑅} +𝑐 {𝑆})‘1𝑜) = 𝑆)
104103fveq2d 6157 . . . . . . . . . . . . 13 (𝜑 → (dist‘(({𝑅} +𝑐 {𝑆})‘1𝑜)) = (dist‘𝑆))
105 xpsc1 16153 . . . . . . . . . . . . . 14 (𝐵𝑌 → (({𝐴} +𝑐 {𝐵})‘1𝑜) = 𝐵)
10627, 105syl 17 . . . . . . . . . . . . 13 (𝜑 → (({𝐴} +𝑐 {𝐵})‘1𝑜) = 𝐵)
107 xpsc1 16153 . . . . . . . . . . . . . 14 (𝐷𝑌 → (({𝐶} +𝑐 {𝐷})‘1𝑜) = 𝐷)
10840, 107syl 17 . . . . . . . . . . . . 13 (𝜑 → (({𝐶} +𝑐 {𝐷})‘1𝑜) = 𝐷)
109104, 106, 108oveq123d 6631 . . . . . . . . . . . 12 (𝜑 → ((({𝐴} +𝑐 {𝐵})‘1𝑜)(dist‘(({𝑅} +𝑐 {𝑆})‘1𝑜))(({𝐶} +𝑐 {𝐷})‘1𝑜)) = (𝐵(dist‘𝑆)𝐷))
11018oveqi 6623 . . . . . . . . . . . . 13 (𝐵𝑁𝐷) = (𝐵((dist‘𝑆) ↾ (𝑌 × 𝑌))𝐷)
11127, 40ovresd 6761 . . . . . . . . . . . . 13 (𝜑 → (𝐵((dist‘𝑆) ↾ (𝑌 × 𝑌))𝐷) = (𝐵(dist‘𝑆)𝐷))
112110, 111syl5eq 2667 . . . . . . . . . . . 12 (𝜑 → (𝐵𝑁𝐷) = (𝐵(dist‘𝑆)𝐷))
113109, 112eqtr4d 2658 . . . . . . . . . . 11 (𝜑 → ((({𝐴} +𝑐 {𝐵})‘1𝑜)(dist‘(({𝑅} +𝑐 {𝑆})‘1𝑜))(({𝐶} +𝑐 {𝐷})‘1𝑜)) = (𝐵𝑁𝐷))
114113eqeq2d 2631 . . . . . . . . . 10 (𝜑 → (𝑥 = ((({𝐴} +𝑐 {𝐵})‘1𝑜)(dist‘(({𝑅} +𝑐 {𝑆})‘1𝑜))(({𝐶} +𝑐 {𝐷})‘1𝑜)) ↔ 𝑥 = (𝐵𝑁𝐷)))
115101, 114orbi12d 745 . . . . . . . . 9 (𝜑 → ((𝑥 = ((({𝐴} +𝑐 {𝐵})‘∅)(dist‘(({𝑅} +𝑐 {𝑆})‘∅))(({𝐶} +𝑐 {𝐷})‘∅)) ∨ 𝑥 = ((({𝐴} +𝑐 {𝐵})‘1𝑜)(dist‘(({𝑅} +𝑐 {𝑆})‘1𝑜))(({𝐶} +𝑐 {𝐷})‘1𝑜))) ↔ (𝑥 = (𝐴𝑀𝐶) ∨ 𝑥 = (𝐵𝑁𝐷))))
11688, 115syl5bb 272 . . . . . . . 8 (𝜑 → (∃𝑘 ∈ 2𝑜 𝑥 = ((({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(({𝑅} +𝑐 {𝑆})‘𝑘))(({𝐶} +𝑐 {𝐷})‘𝑘)) ↔ (𝑥 = (𝐴𝑀𝐶) ∨ 𝑥 = (𝐵𝑁𝐷))))
117 vex 3192 . . . . . . . . 9 𝑥 ∈ V
118 eqid 2621 . . . . . . . . . 10 (𝑘 ∈ 2𝑜 ↦ ((({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(({𝑅} +𝑐 {𝑆})‘𝑘))(({𝐶} +𝑐 {𝐷})‘𝑘))) = (𝑘 ∈ 2𝑜 ↦ ((({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(({𝑅} +𝑐 {𝑆})‘𝑘))(({𝐶} +𝑐 {𝐷})‘𝑘)))
119118elrnmpt 5337 . . . . . . . . 9 (𝑥 ∈ V → (𝑥 ∈ ran (𝑘 ∈ 2𝑜 ↦ ((({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(({𝑅} +𝑐 {𝑆})‘𝑘))(({𝐶} +𝑐 {𝐷})‘𝑘))) ↔ ∃𝑘 ∈ 2𝑜 𝑥 = ((({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(({𝑅} +𝑐 {𝑆})‘𝑘))(({𝐶} +𝑐 {𝐷})‘𝑘))))
120117, 119ax-mp 5 . . . . . . . 8 (𝑥 ∈ ran (𝑘 ∈ 2𝑜 ↦ ((({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(({𝑅} +𝑐 {𝑆})‘𝑘))(({𝐶} +𝑐 {𝐷})‘𝑘))) ↔ ∃𝑘 ∈ 2𝑜 𝑥 = ((({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(({𝑅} +𝑐 {𝑆})‘𝑘))(({𝐶} +𝑐 {𝐷})‘𝑘)))
121117elpr 4174 . . . . . . . 8 (𝑥 ∈ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ↔ (𝑥 = (𝐴𝑀𝐶) ∨ 𝑥 = (𝐵𝑁𝐷)))
122116, 120, 1213bitr4g 303 . . . . . . 7 (𝜑 → (𝑥 ∈ ran (𝑘 ∈ 2𝑜 ↦ ((({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(({𝑅} +𝑐 {𝑆})‘𝑘))(({𝐶} +𝑐 {𝐷})‘𝑘))) ↔ 𝑥 ∈ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)}))
123122eqrdv 2619 . . . . . 6 (𝜑 → ran (𝑘 ∈ 2𝑜 ↦ ((({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(({𝑅} +𝑐 {𝑆})‘𝑘))(({𝐶} +𝑐 {𝐷})‘𝑘))) = {(𝐴𝑀𝐶), (𝐵𝑁𝐷)})
124123uneq1d 3749 . . . . 5 (𝜑 → (ran (𝑘 ∈ 2𝑜 ↦ ((({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(({𝑅} +𝑐 {𝑆})‘𝑘))(({𝐶} +𝑐 {𝐷})‘𝑘))) ∪ {0}) = ({(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ∪ {0}))
125 uncom 3740 . . . . 5 ({(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ∪ {0}) = ({0} ∪ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)})
126124, 125syl6eq 2671 . . . 4 (𝜑 → (ran (𝑘 ∈ 2𝑜 ↦ ((({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(({𝑅} +𝑐 {𝑆})‘𝑘))(({𝐶} +𝑐 {𝐷})‘𝑘))) ∪ {0}) = ({0} ∪ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)}))
127126supeq1d 8304 . . 3 (𝜑 → sup((ran (𝑘 ∈ 2𝑜 ↦ ((({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(({𝑅} +𝑐 {𝑆})‘𝑘))(({𝐶} +𝑐 {𝐷})‘𝑘))) ∪ {0}), ℝ*, < ) = sup(({0} ∪ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)}), ℝ*, < ))
128 0xr 10038 . . . . . 6 0 ∈ ℝ*
129128a1i 11 . . . . 5 (𝜑 → 0 ∈ ℝ*)
130129snssd 4314 . . . 4 (𝜑 → {0} ⊆ ℝ*)
131 xmetcl 22059 . . . . . 6 ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝐴𝑋𝐶𝑋) → (𝐴𝑀𝐶) ∈ ℝ*)
13219, 26, 39, 131syl3anc 1323 . . . . 5 (𝜑 → (𝐴𝑀𝐶) ∈ ℝ*)
133 xmetcl 22059 . . . . . 6 ((𝑁 ∈ (∞Met‘𝑌) ∧ 𝐵𝑌𝐷𝑌) → (𝐵𝑁𝐷) ∈ ℝ*)
13420, 27, 40, 133syl3anc 1323 . . . . 5 (𝜑 → (𝐵𝑁𝐷) ∈ ℝ*)
135 prssi 4326 . . . . 5 (((𝐴𝑀𝐶) ∈ ℝ* ∧ (𝐵𝑁𝐷) ∈ ℝ*) → {(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ⊆ ℝ*)
136132, 134, 135syl2anc 692 . . . 4 (𝜑 → {(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ⊆ ℝ*)
137 xrltso 11926 . . . . . 6 < Or ℝ*
138 supsn 8330 . . . . . 6 (( < Or ℝ* ∧ 0 ∈ ℝ*) → sup({0}, ℝ*, < ) = 0)
139137, 128, 138mp2an 707 . . . . 5 sup({0}, ℝ*, < ) = 0
140 supxrcl 12096 . . . . . . 7 ({(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ⊆ ℝ* → sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ) ∈ ℝ*)
141136, 140syl 17 . . . . . 6 (𝜑 → sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ) ∈ ℝ*)
142 xmetge0 22072 . . . . . . 7 ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝐴𝑋𝐶𝑋) → 0 ≤ (𝐴𝑀𝐶))
14319, 26, 39, 142syl3anc 1323 . . . . . 6 (𝜑 → 0 ≤ (𝐴𝑀𝐶))
144 ovex 6638 . . . . . . . 8 (𝐴𝑀𝐶) ∈ V
145144prid1 4272 . . . . . . 7 (𝐴𝑀𝐶) ∈ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)}
146 supxrub 12105 . . . . . . 7 (({(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ⊆ ℝ* ∧ (𝐴𝑀𝐶) ∈ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)}) → (𝐴𝑀𝐶) ≤ sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ))
147136, 145, 146sylancl 693 . . . . . 6 (𝜑 → (𝐴𝑀𝐶) ≤ sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ))
148129, 132, 141, 143, 147xrletrd 11945 . . . . 5 (𝜑 → 0 ≤ sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ))
149139, 148syl5eqbr 4653 . . . 4 (𝜑 → sup({0}, ℝ*, < ) ≤ sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ))
150 supxrun 12097 . . . 4 (({0} ⊆ ℝ* ∧ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ⊆ ℝ* ∧ sup({0}, ℝ*, < ) ≤ sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < )) → sup(({0} ∪ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)}), ℝ*, < ) = sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ))
151130, 136, 149, 150syl3anc 1323 . . 3 (𝜑 → sup(({0} ∪ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)}), ℝ*, < ) = sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ))
15269, 127, 1513eqtrd 2659 . 2 (𝜑 → (({𝐴} +𝑐 {𝐵})(dist‘((Scalar‘𝑅)Xs({𝑅} +𝑐 {𝑆})))({𝐶} +𝑐 {𝐷})) = sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ))
15351, 58, 1523eqtr3d 2663 1 (𝜑 → (⟨𝐴, 𝐵𝑃𝐶, 𝐷⟩) = sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wo 383   = wceq 1480  wcel 1987  wrex 2908  Vcvv 3189  cun 3557  wss 3559  c0 3896  {csn 4153  {cpr 4155  cop 4159   class class class wbr 4618  cmpt 4678   Or wor 4999   × cxp 5077  ccnv 5078  ran crn 5080  cres 5081  Oncon0 5687   Fn wfn 5847  wf 5848  1-1-ontowf1o 5851  cfv 5852  (class class class)co 6610  cmpt2 6612  1𝑜c1o 7505  2𝑜c2o 7506  supcsup 8298   +𝑐 ccda 8941  0cc0 9888  *cxr 10025   < clt 10026  cle 10027  Basecbs 15792  Scalarcsca 15876  distcds 15882  Xscprds 16038   ×s cxps 16098  ∞Metcxmt 19663
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-inf2 8490  ax-cnex 9944  ax-resscn 9945  ax-1cn 9946  ax-icn 9947  ax-addcl 9948  ax-addrcl 9949  ax-mulcl 9950  ax-mulrcl 9951  ax-mulcom 9952  ax-addass 9953  ax-mulass 9954  ax-distr 9955  ax-i2m1 9956  ax-1ne0 9957  ax-1rid 9958  ax-rnegex 9959  ax-rrecex 9960  ax-cnre 9961  ax-pre-lttri 9962  ax-pre-lttrn 9963  ax-pre-ltadd 9964  ax-pre-mulgt0 9965  ax-pre-sup 9966
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-iin 4493  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-se 5039  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-isom 5861  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-of 6857  df-om 7020  df-1st 7120  df-2nd 7121  df-supp 7248  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-2o 7513  df-oadd 7516  df-er 7694  df-map 7811  df-ixp 7861  df-en 7908  df-dom 7909  df-sdom 7910  df-fin 7911  df-fsupp 8228  df-sup 8300  df-inf 8301  df-oi 8367  df-card 8717  df-cda 8942  df-pnf 10028  df-mnf 10029  df-xr 10030  df-ltxr 10031  df-le 10032  df-sub 10220  df-neg 10221  df-div 10637  df-nn 10973  df-2 11031  df-3 11032  df-4 11033  df-5 11034  df-6 11035  df-7 11036  df-8 11037  df-9 11038  df-n0 11245  df-z 11330  df-dec 11446  df-uz 11640  df-rp 11785  df-xneg 11898  df-xadd 11899  df-xmul 11900  df-icc 12132  df-fz 12277  df-fzo 12415  df-seq 12750  df-hash 13066  df-struct 15794  df-ndx 15795  df-slot 15796  df-base 15797  df-sets 15798  df-ress 15799  df-plusg 15886  df-mulr 15887  df-sca 15889  df-vsca 15890  df-ip 15891  df-tset 15892  df-ple 15893  df-ds 15896  df-hom 15898  df-cco 15899  df-0g 16034  df-gsum 16035  df-prds 16040  df-xrs 16094  df-imas 16100  df-xps 16102  df-mre 16178  df-mrc 16179  df-acs 16181  df-mgm 17174  df-sgrp 17216  df-mnd 17227  df-submnd 17268  df-mulg 17473  df-cntz 17682  df-cmn 18127  df-xmet 19671
This theorem is referenced by:  tmsxpsval  22266
  Copyright terms: Public domain W3C validator