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

Theorem xpsdsval 23734
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 2736 . . . . 5 (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) = (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})
7 eqid 2736 . . . . 5 (Scalar‘𝑅) = (Scalar‘𝑅)
8 eqid 2736 . . . . 5 ((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}) = ((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})
91, 2, 3, 4, 5, 6, 7, 8xpsval 17452 . . . 4 (𝜑𝑇 = ((𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) “s ((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})))
101, 2, 3, 4, 5, 6, 7, 8xpsrnbas 17453 . . . 4 (𝜑 → ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) = (Base‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})))
116xpsff1o2 17451 . . . . 5 (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}):(𝑋 × 𝑌)–1-1-onto→ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})
12 f1ocnv 6796 . . . . 5 ((𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}):(𝑋 × 𝑌)–1-1-onto→ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) → (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}):ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})–1-1-onto→(𝑋 × 𝑌))
1311, 12mp1i 13 . . . 4 (𝜑(𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}):ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})–1-1-onto→(𝑋 × 𝑌))
14 ovexd 7392 . . . 4 (𝜑 → ((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}) ∈ V)
15 eqid 2736 . . . 4 ((dist‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})) ↾ (ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) × ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}))) = ((dist‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})) ↾ (ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) × ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})))
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 23732 . . . . 5 (𝜑 → (dist‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})) ∈ (∞Met‘ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})))
22 ssid 3966 . . . . 5 ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) ⊆ ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})
23 xmetres2 23714 . . . . 5 (((dist‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})) ∈ (∞Met‘ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})) ∧ ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) ⊆ ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})) → ((dist‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})) ↾ (ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) × ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}))) ∈ (∞Met‘ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})))
2421, 22, 23sylancl 586 . . . 4 (𝜑 → ((dist‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})) ↾ (ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) × ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}))) ∈ (∞Met‘ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})))
25 df-ov 7360 . . . . . 6 (𝐴(𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})𝐵) = ((𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})‘⟨𝐴, 𝐵⟩)
26 xpsds.a . . . . . . 7 (𝜑𝐴𝑋)
27 xpsds.b . . . . . . 7 (𝜑𝐵𝑌)
286xpsfval 17448 . . . . . . 7 ((𝐴𝑋𝐵𝑌) → (𝐴(𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})𝐵) = {⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩})
2926, 27, 28syl2anc 584 . . . . . 6 (𝜑 → (𝐴(𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})𝐵) = {⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩})
3025, 29eqtr3id 2790 . . . . 5 (𝜑 → ((𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})‘⟨𝐴, 𝐵⟩) = {⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩})
3126, 27opelxpd 5671 . . . . . 6 (𝜑 → ⟨𝐴, 𝐵⟩ ∈ (𝑋 × 𝑌))
32 f1of 6784 . . . . . . . 8 ((𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}):(𝑋 × 𝑌)–1-1-onto→ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) → (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}):(𝑋 × 𝑌)⟶ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}))
3311, 32ax-mp 5 . . . . . . 7 (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}):(𝑋 × 𝑌)⟶ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})
3433ffvelcdmi 7034 . . . . . 6 (⟨𝐴, 𝐵⟩ ∈ (𝑋 × 𝑌) → ((𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})‘⟨𝐴, 𝐵⟩) ∈ ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}))
3531, 34syl 17 . . . . 5 (𝜑 → ((𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})‘⟨𝐴, 𝐵⟩) ∈ ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}))
3630, 35eqeltrrd 2839 . . . 4 (𝜑 → {⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩} ∈ ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}))
37 df-ov 7360 . . . . . 6 (𝐶(𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})𝐷) = ((𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})‘⟨𝐶, 𝐷⟩)
38 xpsds.c . . . . . . 7 (𝜑𝐶𝑋)
39 xpsds.d . . . . . . 7 (𝜑𝐷𝑌)
406xpsfval 17448 . . . . . . 7 ((𝐶𝑋𝐷𝑌) → (𝐶(𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})𝐷) = {⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩})
4138, 39, 40syl2anc 584 . . . . . 6 (𝜑 → (𝐶(𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})𝐷) = {⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩})
4237, 41eqtr3id 2790 . . . . 5 (𝜑 → ((𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})‘⟨𝐶, 𝐷⟩) = {⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩})
4338, 39opelxpd 5671 . . . . . 6 (𝜑 → ⟨𝐶, 𝐷⟩ ∈ (𝑋 × 𝑌))
4433ffvelcdmi 7034 . . . . . 6 (⟨𝐶, 𝐷⟩ ∈ (𝑋 × 𝑌) → ((𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})‘⟨𝐶, 𝐷⟩) ∈ ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}))
4543, 44syl 17 . . . . 5 (𝜑 → ((𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})‘⟨𝐶, 𝐷⟩) ∈ ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}))
4642, 45eqeltrrd 2839 . . . 4 (𝜑 → {⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩} ∈ ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}))
479, 10, 13, 14, 15, 16, 24, 36, 46imasdsf1o 23727 . . 3 (𝜑 → (((𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})‘{⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩})𝑃((𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})‘{⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩})) = ({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩} ((dist‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})) ↾ (ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) × ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}))){⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}))
4836, 46ovresd 7521 . . 3 (𝜑 → ({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩} ((dist‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})) ↾ (ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) × ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}))){⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}) = ({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩} (dist‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})){⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}))
4947, 48eqtrd 2776 . 2 (𝜑 → (((𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})‘{⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩})𝑃((𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})‘{⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩})) = ({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩} (dist‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})){⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}))
50 f1ocnvfv 7224 . . . . 5 (((𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}):(𝑋 × 𝑌)–1-1-onto→ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) ∧ ⟨𝐴, 𝐵⟩ ∈ (𝑋 × 𝑌)) → (((𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})‘⟨𝐴, 𝐵⟩) = {⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩} → ((𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})‘{⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}) = ⟨𝐴, 𝐵⟩))
5111, 31, 50sylancr 587 . . . 4 (𝜑 → (((𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})‘⟨𝐴, 𝐵⟩) = {⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩} → ((𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})‘{⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}) = ⟨𝐴, 𝐵⟩))
5230, 51mpd 15 . . 3 (𝜑 → ((𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})‘{⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}) = ⟨𝐴, 𝐵⟩)
53 f1ocnvfv 7224 . . . . 5 (((𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}):(𝑋 × 𝑌)–1-1-onto→ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) ∧ ⟨𝐶, 𝐷⟩ ∈ (𝑋 × 𝑌)) → (((𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})‘⟨𝐶, 𝐷⟩) = {⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩} → ((𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})‘{⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}) = ⟨𝐶, 𝐷⟩))
5411, 43, 53sylancr 587 . . . 4 (𝜑 → (((𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})‘⟨𝐶, 𝐷⟩) = {⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩} → ((𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})‘{⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}) = ⟨𝐶, 𝐷⟩))
5542, 54mpd 15 . . 3 (𝜑 → ((𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})‘{⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}) = ⟨𝐶, 𝐷⟩)
5652, 55oveq12d 7375 . 2 (𝜑 → (((𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})‘{⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩})𝑃((𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})‘{⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩})) = (⟨𝐴, 𝐵𝑃𝐶, 𝐷⟩))
57 eqid 2736 . . . 4 (Base‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})) = (Base‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}))
58 fvexd 6857 . . . 4 (𝜑 → (Scalar‘𝑅) ∈ V)
59 2on 8426 . . . . 5 2o ∈ On
6059a1i 11 . . . 4 (𝜑 → 2o ∈ On)
61 fnpr2o 17439 . . . . 5 ((𝑅𝑉𝑆𝑊) → {⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩} Fn 2o)
624, 5, 61syl2anc 584 . . . 4 (𝜑 → {⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩} Fn 2o)
6336, 10eleqtrd 2840 . . . 4 (𝜑 → {⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩} ∈ (Base‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})))
6446, 10eleqtrd 2840 . . . 4 (𝜑 → {⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩} ∈ (Base‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})))
65 eqid 2736 . . . 4 (dist‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})) = (dist‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}))
668, 57, 58, 60, 62, 63, 64, 65prdsdsval 17360 . . 3 (𝜑 → ({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩} (dist‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})){⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}) = sup((ran (𝑘 ∈ 2o ↦ (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘𝑘)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘𝑘))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘𝑘))) ∪ {0}), ℝ*, < ))
67 df2o3 8420 . . . . . . . . . . 11 2o = {∅, 1o}
6867rexeqi 3312 . . . . . . . . . 10 (∃𝑘 ∈ 2o 𝑥 = (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘𝑘)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘𝑘))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘𝑘)) ↔ ∃𝑘 ∈ {∅, 1o}𝑥 = (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘𝑘)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘𝑘))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘𝑘)))
69 0ex 5264 . . . . . . . . . . 11 ∅ ∈ V
70 1oex 8422 . . . . . . . . . . 11 1o ∈ V
71 2fveq3 6847 . . . . . . . . . . . . 13 (𝑘 = ∅ → (dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘𝑘)) = (dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘∅)))
72 fveq2 6842 . . . . . . . . . . . . 13 (𝑘 = ∅ → ({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘𝑘) = ({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘∅))
73 fveq2 6842 . . . . . . . . . . . . 13 (𝑘 = ∅ → ({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘𝑘) = ({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘∅))
7471, 72, 73oveq123d 7378 . . . . . . . . . . . 12 (𝑘 = ∅ → (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘𝑘)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘𝑘))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘𝑘)) = (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘∅)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘∅))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘∅)))
7574eqeq2d 2747 . . . . . . . . . . 11 (𝑘 = ∅ → (𝑥 = (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘𝑘)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘𝑘))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘𝑘)) ↔ 𝑥 = (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘∅)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘∅))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘∅))))
76 2fveq3 6847 . . . . . . . . . . . . 13 (𝑘 = 1o → (dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘𝑘)) = (dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘1o)))
77 fveq2 6842 . . . . . . . . . . . . 13 (𝑘 = 1o → ({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘𝑘) = ({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘1o))
78 fveq2 6842 . . . . . . . . . . . . 13 (𝑘 = 1o → ({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘𝑘) = ({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘1o))
7976, 77, 78oveq123d 7378 . . . . . . . . . . . 12 (𝑘 = 1o → (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘𝑘)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘𝑘))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘𝑘)) = (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘1o)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘1o))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘1o)))
8079eqeq2d 2747 . . . . . . . . . . 11 (𝑘 = 1o → (𝑥 = (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘𝑘)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘𝑘))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘𝑘)) ↔ 𝑥 = (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘1o)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘1o))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘1o))))
8169, 70, 75, 80rexpr 4662 . . . . . . . . . 10 (∃𝑘 ∈ {∅, 1o}𝑥 = (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘𝑘)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘𝑘))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘𝑘)) ↔ (𝑥 = (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘∅)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘∅))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘∅)) ∨ 𝑥 = (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘1o)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘1o))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘1o))))
8268, 81bitri 274 . . . . . . . . 9 (∃𝑘 ∈ 2o 𝑥 = (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘𝑘)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘𝑘))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘𝑘)) ↔ (𝑥 = (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘∅)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘∅))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘∅)) ∨ 𝑥 = (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘1o)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘1o))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘1o))))
83 fvpr0o 17441 . . . . . . . . . . . . . . 15 (𝑅𝑉 → ({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘∅) = 𝑅)
844, 83syl 17 . . . . . . . . . . . . . 14 (𝜑 → ({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘∅) = 𝑅)
8584fveq2d 6846 . . . . . . . . . . . . 13 (𝜑 → (dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘∅)) = (dist‘𝑅))
86 fvpr0o 17441 . . . . . . . . . . . . . 14 (𝐴𝑋 → ({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘∅) = 𝐴)
8726, 86syl 17 . . . . . . . . . . . . 13 (𝜑 → ({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘∅) = 𝐴)
88 fvpr0o 17441 . . . . . . . . . . . . . 14 (𝐶𝑋 → ({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘∅) = 𝐶)
8938, 88syl 17 . . . . . . . . . . . . 13 (𝜑 → ({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘∅) = 𝐶)
9085, 87, 89oveq123d 7378 . . . . . . . . . . . 12 (𝜑 → (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘∅)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘∅))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘∅)) = (𝐴(dist‘𝑅)𝐶))
9117oveqi 7370 . . . . . . . . . . . . 13 (𝐴𝑀𝐶) = (𝐴((dist‘𝑅) ↾ (𝑋 × 𝑋))𝐶)
9226, 38ovresd 7521 . . . . . . . . . . . . 13 (𝜑 → (𝐴((dist‘𝑅) ↾ (𝑋 × 𝑋))𝐶) = (𝐴(dist‘𝑅)𝐶))
9391, 92eqtrid 2788 . . . . . . . . . . . 12 (𝜑 → (𝐴𝑀𝐶) = (𝐴(dist‘𝑅)𝐶))
9490, 93eqtr4d 2779 . . . . . . . . . . 11 (𝜑 → (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘∅)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘∅))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘∅)) = (𝐴𝑀𝐶))
9594eqeq2d 2747 . . . . . . . . . 10 (𝜑 → (𝑥 = (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘∅)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘∅))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘∅)) ↔ 𝑥 = (𝐴𝑀𝐶)))
96 fvpr1o 17442 . . . . . . . . . . . . . . 15 (𝑆𝑊 → ({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘1o) = 𝑆)
975, 96syl 17 . . . . . . . . . . . . . 14 (𝜑 → ({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘1o) = 𝑆)
9897fveq2d 6846 . . . . . . . . . . . . 13 (𝜑 → (dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘1o)) = (dist‘𝑆))
99 fvpr1o 17442 . . . . . . . . . . . . . 14 (𝐵𝑌 → ({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘1o) = 𝐵)
10027, 99syl 17 . . . . . . . . . . . . 13 (𝜑 → ({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘1o) = 𝐵)
101 fvpr1o 17442 . . . . . . . . . . . . . 14 (𝐷𝑌 → ({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘1o) = 𝐷)
10239, 101syl 17 . . . . . . . . . . . . 13 (𝜑 → ({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘1o) = 𝐷)
10398, 100, 102oveq123d 7378 . . . . . . . . . . . 12 (𝜑 → (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘1o)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘1o))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘1o)) = (𝐵(dist‘𝑆)𝐷))
10418oveqi 7370 . . . . . . . . . . . . 13 (𝐵𝑁𝐷) = (𝐵((dist‘𝑆) ↾ (𝑌 × 𝑌))𝐷)
10527, 39ovresd 7521 . . . . . . . . . . . . 13 (𝜑 → (𝐵((dist‘𝑆) ↾ (𝑌 × 𝑌))𝐷) = (𝐵(dist‘𝑆)𝐷))
106104, 105eqtrid 2788 . . . . . . . . . . . 12 (𝜑 → (𝐵𝑁𝐷) = (𝐵(dist‘𝑆)𝐷))
107103, 106eqtr4d 2779 . . . . . . . . . . 11 (𝜑 → (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘1o)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘1o))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘1o)) = (𝐵𝑁𝐷))
108107eqeq2d 2747 . . . . . . . . . 10 (𝜑 → (𝑥 = (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘1o)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘1o))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘1o)) ↔ 𝑥 = (𝐵𝑁𝐷)))
10995, 108orbi12d 917 . . . . . . . . 9 (𝜑 → ((𝑥 = (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘∅)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘∅))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘∅)) ∨ 𝑥 = (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘1o)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘1o))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘1o))) ↔ (𝑥 = (𝐴𝑀𝐶) ∨ 𝑥 = (𝐵𝑁𝐷))))
11082, 109bitrid 282 . . . . . . . 8 (𝜑 → (∃𝑘 ∈ 2o 𝑥 = (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘𝑘)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘𝑘))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘𝑘)) ↔ (𝑥 = (𝐴𝑀𝐶) ∨ 𝑥 = (𝐵𝑁𝐷))))
111 eqid 2736 . . . . . . . . . 10 (𝑘 ∈ 2o ↦ (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘𝑘)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘𝑘))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘𝑘))) = (𝑘 ∈ 2o ↦ (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘𝑘)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘𝑘))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘𝑘)))
112111elrnmpt 5911 . . . . . . . . 9 (𝑥 ∈ V → (𝑥 ∈ ran (𝑘 ∈ 2o ↦ (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘𝑘)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘𝑘))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘𝑘))) ↔ ∃𝑘 ∈ 2o 𝑥 = (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘𝑘)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘𝑘))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘𝑘))))
113112elv 3451 . . . . . . . 8 (𝑥 ∈ ran (𝑘 ∈ 2o ↦ (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘𝑘)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘𝑘))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘𝑘))) ↔ ∃𝑘 ∈ 2o 𝑥 = (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘𝑘)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘𝑘))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘𝑘)))
114 vex 3449 . . . . . . . . 9 𝑥 ∈ V
115114elpr 4609 . . . . . . . 8 (𝑥 ∈ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ↔ (𝑥 = (𝐴𝑀𝐶) ∨ 𝑥 = (𝐵𝑁𝐷)))
116110, 113, 1153bitr4g 313 . . . . . . 7 (𝜑 → (𝑥 ∈ ran (𝑘 ∈ 2o ↦ (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘𝑘)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘𝑘))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘𝑘))) ↔ 𝑥 ∈ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)}))
117116eqrdv 2734 . . . . . 6 (𝜑 → ran (𝑘 ∈ 2o ↦ (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘𝑘)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘𝑘))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘𝑘))) = {(𝐴𝑀𝐶), (𝐵𝑁𝐷)})
118117uneq1d 4122 . . . . 5 (𝜑 → (ran (𝑘 ∈ 2o ↦ (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘𝑘)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘𝑘))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘𝑘))) ∪ {0}) = ({(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ∪ {0}))
119 uncom 4113 . . . . 5 ({(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ∪ {0}) = ({0} ∪ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)})
120118, 119eqtrdi 2792 . . . 4 (𝜑 → (ran (𝑘 ∈ 2o ↦ (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘𝑘)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘𝑘))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘𝑘))) ∪ {0}) = ({0} ∪ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)}))
121120supeq1d 9382 . . 3 (𝜑 → sup((ran (𝑘 ∈ 2o ↦ (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘𝑘)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘𝑘))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘𝑘))) ∪ {0}), ℝ*, < ) = sup(({0} ∪ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)}), ℝ*, < ))
122 0xr 11202 . . . . . 6 0 ∈ ℝ*
123122a1i 11 . . . . 5 (𝜑 → 0 ∈ ℝ*)
124123snssd 4769 . . . 4 (𝜑 → {0} ⊆ ℝ*)
125 xmetcl 23684 . . . . . 6 ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝐴𝑋𝐶𝑋) → (𝐴𝑀𝐶) ∈ ℝ*)
12619, 26, 38, 125syl3anc 1371 . . . . 5 (𝜑 → (𝐴𝑀𝐶) ∈ ℝ*)
127 xmetcl 23684 . . . . . 6 ((𝑁 ∈ (∞Met‘𝑌) ∧ 𝐵𝑌𝐷𝑌) → (𝐵𝑁𝐷) ∈ ℝ*)
12820, 27, 39, 127syl3anc 1371 . . . . 5 (𝜑 → (𝐵𝑁𝐷) ∈ ℝ*)
129126, 128prssd 4782 . . . 4 (𝜑 → {(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ⊆ ℝ*)
130 xrltso 13060 . . . . . 6 < Or ℝ*
131 supsn 9408 . . . . . 6 (( < Or ℝ* ∧ 0 ∈ ℝ*) → sup({0}, ℝ*, < ) = 0)
132130, 122, 131mp2an 690 . . . . 5 sup({0}, ℝ*, < ) = 0
133 supxrcl 13234 . . . . . . 7 ({(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ⊆ ℝ* → sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ) ∈ ℝ*)
134129, 133syl 17 . . . . . 6 (𝜑 → sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ) ∈ ℝ*)
135 xmetge0 23697 . . . . . . 7 ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝐴𝑋𝐶𝑋) → 0 ≤ (𝐴𝑀𝐶))
13619, 26, 38, 135syl3anc 1371 . . . . . 6 (𝜑 → 0 ≤ (𝐴𝑀𝐶))
137 ovex 7390 . . . . . . . 8 (𝐴𝑀𝐶) ∈ V
138137prid1 4723 . . . . . . 7 (𝐴𝑀𝐶) ∈ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)}
139 supxrub 13243 . . . . . . 7 (({(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ⊆ ℝ* ∧ (𝐴𝑀𝐶) ∈ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)}) → (𝐴𝑀𝐶) ≤ sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ))
140129, 138, 139sylancl 586 . . . . . 6 (𝜑 → (𝐴𝑀𝐶) ≤ sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ))
141123, 126, 134, 136, 140xrletrd 13081 . . . . 5 (𝜑 → 0 ≤ sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ))
142132, 141eqbrtrid 5140 . . . 4 (𝜑 → sup({0}, ℝ*, < ) ≤ sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ))
143 supxrun 13235 . . . 4 (({0} ⊆ ℝ* ∧ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ⊆ ℝ* ∧ sup({0}, ℝ*, < ) ≤ sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < )) → sup(({0} ∪ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)}), ℝ*, < ) = sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ))
144124, 129, 142, 143syl3anc 1371 . . 3 (𝜑 → sup(({0} ∪ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)}), ℝ*, < ) = sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ))
14566, 121, 1443eqtrd 2780 . 2 (𝜑 → ({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩} (dist‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})){⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}) = sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ))
14649, 56, 1453eqtr3d 2784 1 (𝜑 → (⟨𝐴, 𝐵𝑃𝐶, 𝐷⟩) = sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wo 845   = wceq 1541  wcel 2106  wrex 3073  Vcvv 3445  cun 3908  wss 3910  c0 4282  {csn 4586  {cpr 4588  cop 4592   class class class wbr 5105  cmpt 5188   Or wor 5544   × cxp 5631  ccnv 5632  ran crn 5634  cres 5635  Oncon0 6317   Fn wfn 6491  wf 6492  1-1-ontowf1o 6495  cfv 6496  (class class class)co 7357  cmpo 7359  1oc1o 8405  2oc2o 8406  supcsup 9376  0cc0 11051  *cxr 11188   < clt 11189  cle 11190  Basecbs 17083  Scalarcsca 17136  distcds 17142  Xscprds 17327   ×s cxps 17388  ∞Metcxmet 20781
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-iin 4957  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-of 7617  df-om 7803  df-1st 7921  df-2nd 7922  df-supp 8093  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-2o 8413  df-er 8648  df-map 8767  df-ixp 8836  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fsupp 9306  df-sup 9378  df-inf 9379  df-oi 9446  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-7 12221  df-8 12222  df-9 12223  df-n0 12414  df-z 12500  df-dec 12619  df-uz 12764  df-rp 12916  df-xneg 13033  df-xadd 13034  df-xmul 13035  df-icc 13271  df-fz 13425  df-fzo 13568  df-seq 13907  df-hash 14231  df-struct 17019  df-sets 17036  df-slot 17054  df-ndx 17066  df-base 17084  df-ress 17113  df-plusg 17146  df-mulr 17147  df-sca 17149  df-vsca 17150  df-ip 17151  df-tset 17152  df-ple 17153  df-ds 17155  df-hom 17157  df-cco 17158  df-0g 17323  df-gsum 17324  df-prds 17329  df-xrs 17384  df-imas 17390  df-xps 17392  df-mre 17466  df-mrc 17467  df-acs 17469  df-mgm 18497  df-sgrp 18546  df-mnd 18557  df-submnd 18602  df-mulg 18873  df-cntz 19097  df-cmn 19564  df-xmet 20789
This theorem is referenced by:  tmsxpsval  23894
  Copyright terms: Public domain W3C validator