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

Theorem xpsdsval 23640
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 17378 . . . 4 (𝜑𝑇 = ((𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) “s ((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})))
101, 2, 3, 4, 5, 6, 7, 8xpsrnbas 17379 . . . 4 (𝜑 → ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) = (Base‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})))
116xpsff1o2 17377 . . . . 5 (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}):(𝑋 × 𝑌)–1-1-onto→ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})
12 f1ocnv 6779 . . . . 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 7372 . . . 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 23638 . . . . 5 (𝜑 → (dist‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})) ∈ (∞Met‘ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})))
22 ssid 3954 . . . . 5 ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) ⊆ ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})
23 xmetres2 23620 . . . . 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 7340 . . . . . 6 (𝐴(𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})𝐵) = ((𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})‘⟨𝐴, 𝐵⟩)
26 xpsds.a . . . . . . 7 (𝜑𝐴𝑋)
27 xpsds.b . . . . . . 7 (𝜑𝐵𝑌)
286xpsfval 17374 . . . . . . 7 ((𝐴𝑋𝐵𝑌) → (𝐴(𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})𝐵) = {⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩})
2926, 27, 28syl2anc 584 . . . . . 6 (𝜑 → (𝐴(𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})𝐵) = {⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩})
3025, 29eqtr3id 2790 . . . . 5 (𝜑 → ((𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})‘⟨𝐴, 𝐵⟩) = {⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩})
3126, 27opelxpd 5658 . . . . . 6 (𝜑 → ⟨𝐴, 𝐵⟩ ∈ (𝑋 × 𝑌))
32 f1of 6767 . . . . . . . 8 ((𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}):(𝑋 × 𝑌)–1-1-onto→ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) → (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}):(𝑋 × 𝑌)⟶ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}))
3311, 32ax-mp 5 . . . . . . 7 (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}):(𝑋 × 𝑌)⟶ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})
3433ffvelcdmi 7016 . . . . . 6 (⟨𝐴, 𝐵⟩ ∈ (𝑋 × 𝑌) → ((𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})‘⟨𝐴, 𝐵⟩) ∈ ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}))
3531, 34syl 17 . . . . 5 (𝜑 → ((𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})‘⟨𝐴, 𝐵⟩) ∈ ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}))
3630, 35eqeltrrd 2838 . . . 4 (𝜑 → {⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩} ∈ ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}))
37 df-ov 7340 . . . . . 6 (𝐶(𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})𝐷) = ((𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})‘⟨𝐶, 𝐷⟩)
38 xpsds.c . . . . . . 7 (𝜑𝐶𝑋)
39 xpsds.d . . . . . . 7 (𝜑𝐷𝑌)
406xpsfval 17374 . . . . . . 7 ((𝐶𝑋𝐷𝑌) → (𝐶(𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})𝐷) = {⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩})
4138, 39, 40syl2anc 584 . . . . . 6 (𝜑 → (𝐶(𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})𝐷) = {⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩})
4237, 41eqtr3id 2790 . . . . 5 (𝜑 → ((𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})‘⟨𝐶, 𝐷⟩) = {⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩})
4338, 39opelxpd 5658 . . . . . 6 (𝜑 → ⟨𝐶, 𝐷⟩ ∈ (𝑋 × 𝑌))
4433ffvelcdmi 7016 . . . . . 6 (⟨𝐶, 𝐷⟩ ∈ (𝑋 × 𝑌) → ((𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})‘⟨𝐶, 𝐷⟩) ∈ ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}))
4543, 44syl 17 . . . . 5 (𝜑 → ((𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})‘⟨𝐶, 𝐷⟩) ∈ ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}))
4642, 45eqeltrrd 2838 . . . 4 (𝜑 → {⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩} ∈ ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}))
479, 10, 13, 14, 15, 16, 24, 36, 46imasdsf1o 23633 . . 3 (𝜑 → (((𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})‘{⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩})𝑃((𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})‘{⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩})) = ({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩} ((dist‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})) ↾ (ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) × ran (𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}))){⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}))
4836, 46ovresd 7501 . . 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 7206 . . . . 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 7206 . . . . 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 7355 . 2 (𝜑 → (((𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})‘{⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩})𝑃((𝑥𝑋, 𝑦𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})‘{⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩})) = (⟨𝐴, 𝐵𝑃𝐶, 𝐷⟩))
57 eqid 2736 . . . 4 (Base‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})) = (Base‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}))
58 fvexd 6840 . . . 4 (𝜑 → (Scalar‘𝑅) ∈ V)
59 2on 8381 . . . . 5 2o ∈ On
6059a1i 11 . . . 4 (𝜑 → 2o ∈ On)
61 fnpr2o 17365 . . . . 5 ((𝑅𝑉𝑆𝑊) → {⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩} Fn 2o)
624, 5, 61syl2anc 584 . . . 4 (𝜑 → {⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩} Fn 2o)
6336, 10eleqtrd 2839 . . . 4 (𝜑 → {⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩} ∈ (Base‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})))
6446, 10eleqtrd 2839 . . . 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 17286 . . 3 (𝜑 → ({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩} (dist‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})){⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}) = sup((ran (𝑘 ∈ 2o ↦ (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘𝑘)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘𝑘))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘𝑘))) ∪ {0}), ℝ*, < ))
67 df2o3 8375 . . . . . . . . . . 11 2o = {∅, 1o}
6867rexeqi 3308 . . . . . . . . . 10 (∃𝑘 ∈ 2o 𝑥 = (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘𝑘)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘𝑘))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘𝑘)) ↔ ∃𝑘 ∈ {∅, 1o}𝑥 = (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘𝑘)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘𝑘))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘𝑘)))
69 0ex 5251 . . . . . . . . . . 11 ∅ ∈ V
70 1oex 8377 . . . . . . . . . . 11 1o ∈ V
71 2fveq3 6830 . . . . . . . . . . . . 13 (𝑘 = ∅ → (dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘𝑘)) = (dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘∅)))
72 fveq2 6825 . . . . . . . . . . . . 13 (𝑘 = ∅ → ({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘𝑘) = ({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘∅))
73 fveq2 6825 . . . . . . . . . . . . 13 (𝑘 = ∅ → ({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘𝑘) = ({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘∅))
7471, 72, 73oveq123d 7358 . . . . . . . . . . . 12 (𝑘 = ∅ → (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘𝑘)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘𝑘))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘𝑘)) = (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘∅)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘∅))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘∅)))
7574eqeq2d 2747 . . . . . . . . . . 11 (𝑘 = ∅ → (𝑥 = (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘𝑘)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘𝑘))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘𝑘)) ↔ 𝑥 = (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘∅)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘∅))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘∅))))
76 2fveq3 6830 . . . . . . . . . . . . 13 (𝑘 = 1o → (dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘𝑘)) = (dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘1o)))
77 fveq2 6825 . . . . . . . . . . . . 13 (𝑘 = 1o → ({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘𝑘) = ({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘1o))
78 fveq2 6825 . . . . . . . . . . . . 13 (𝑘 = 1o → ({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘𝑘) = ({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘1o))
7976, 77, 78oveq123d 7358 . . . . . . . . . . . 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 4649 . . . . . . . . . 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 17367 . . . . . . . . . . . . . . 15 (𝑅𝑉 → ({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘∅) = 𝑅)
844, 83syl 17 . . . . . . . . . . . . . 14 (𝜑 → ({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘∅) = 𝑅)
8584fveq2d 6829 . . . . . . . . . . . . 13 (𝜑 → (dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘∅)) = (dist‘𝑅))
86 fvpr0o 17367 . . . . . . . . . . . . . 14 (𝐴𝑋 → ({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘∅) = 𝐴)
8726, 86syl 17 . . . . . . . . . . . . 13 (𝜑 → ({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘∅) = 𝐴)
88 fvpr0o 17367 . . . . . . . . . . . . . 14 (𝐶𝑋 → ({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘∅) = 𝐶)
8938, 88syl 17 . . . . . . . . . . . . 13 (𝜑 → ({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘∅) = 𝐶)
9085, 87, 89oveq123d 7358 . . . . . . . . . . . 12 (𝜑 → (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘∅)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘∅))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘∅)) = (𝐴(dist‘𝑅)𝐶))
9117oveqi 7350 . . . . . . . . . . . . 13 (𝐴𝑀𝐶) = (𝐴((dist‘𝑅) ↾ (𝑋 × 𝑋))𝐶)
9226, 38ovresd 7501 . . . . . . . . . . . . 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 17368 . . . . . . . . . . . . . . 15 (𝑆𝑊 → ({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘1o) = 𝑆)
975, 96syl 17 . . . . . . . . . . . . . 14 (𝜑 → ({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘1o) = 𝑆)
9897fveq2d 6829 . . . . . . . . . . . . 13 (𝜑 → (dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘1o)) = (dist‘𝑆))
99 fvpr1o 17368 . . . . . . . . . . . . . 14 (𝐵𝑌 → ({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘1o) = 𝐵)
10027, 99syl 17 . . . . . . . . . . . . 13 (𝜑 → ({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘1o) = 𝐵)
101 fvpr1o 17368 . . . . . . . . . . . . . 14 (𝐷𝑌 → ({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘1o) = 𝐷)
10239, 101syl 17 . . . . . . . . . . . . 13 (𝜑 → ({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘1o) = 𝐷)
10398, 100, 102oveq123d 7358 . . . . . . . . . . . 12 (𝜑 → (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘1o)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘1o))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘1o)) = (𝐵(dist‘𝑆)𝐷))
10418oveqi 7350 . . . . . . . . . . . . 13 (𝐵𝑁𝐷) = (𝐵((dist‘𝑆) ↾ (𝑌 × 𝑌))𝐷)
10527, 39ovresd 7501 . . . . . . . . . . . . 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 916 . . . . . . . . 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 5897 . . . . . . . . 9 (𝑥 ∈ V → (𝑥 ∈ ran (𝑘 ∈ 2o ↦ (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘𝑘)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘𝑘))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘𝑘))) ↔ ∃𝑘 ∈ 2o 𝑥 = (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘𝑘)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘𝑘))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘𝑘))))
113112elv 3447 . . . . . . . 8 (𝑥 ∈ ran (𝑘 ∈ 2o ↦ (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘𝑘)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘𝑘))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘𝑘))) ↔ ∃𝑘 ∈ 2o 𝑥 = (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘𝑘)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘𝑘))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘𝑘)))
114 vex 3445 . . . . . . . . 9 𝑥 ∈ V
115114elpr 4596 . . . . . . . 8 (𝑥 ∈ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ↔ (𝑥 = (𝐴𝑀𝐶) ∨ 𝑥 = (𝐵𝑁𝐷)))
116110, 113, 1153bitr4g 313 . . . . . . 7 (𝜑 → (𝑥 ∈ ran (𝑘 ∈ 2o ↦ (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘𝑘)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘𝑘))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘𝑘))) ↔ 𝑥 ∈ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)}))
117116eqrdv 2734 . . . . . 6 (𝜑 → ran (𝑘 ∈ 2o ↦ (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘𝑘)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘𝑘))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘𝑘))) = {(𝐴𝑀𝐶), (𝐵𝑁𝐷)})
118117uneq1d 4109 . . . . 5 (𝜑 → (ran (𝑘 ∈ 2o ↦ (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘𝑘)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘𝑘))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘𝑘))) ∪ {0}) = ({(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ∪ {0}))
119 uncom 4100 . . . . 5 ({(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ∪ {0}) = ({0} ∪ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)})
120118, 119eqtrdi 2792 . . . 4 (𝜑 → (ran (𝑘 ∈ 2o ↦ (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘𝑘)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘𝑘))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘𝑘))) ∪ {0}) = ({0} ∪ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)}))
121120supeq1d 9303 . . 3 (𝜑 → sup((ran (𝑘 ∈ 2o ↦ (({⟨∅, 𝐴⟩, ⟨1o, 𝐵⟩}‘𝑘)(dist‘({⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩}‘𝑘))({⟨∅, 𝐶⟩, ⟨1o, 𝐷⟩}‘𝑘))) ∪ {0}), ℝ*, < ) = sup(({0} ∪ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)}), ℝ*, < ))
122 0xr 11123 . . . . . 6 0 ∈ ℝ*
123122a1i 11 . . . . 5 (𝜑 → 0 ∈ ℝ*)
124123snssd 4756 . . . 4 (𝜑 → {0} ⊆ ℝ*)
125 xmetcl 23590 . . . . . 6 ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝐴𝑋𝐶𝑋) → (𝐴𝑀𝐶) ∈ ℝ*)
12619, 26, 38, 125syl3anc 1370 . . . . 5 (𝜑 → (𝐴𝑀𝐶) ∈ ℝ*)
127 xmetcl 23590 . . . . . 6 ((𝑁 ∈ (∞Met‘𝑌) ∧ 𝐵𝑌𝐷𝑌) → (𝐵𝑁𝐷) ∈ ℝ*)
12820, 27, 39, 127syl3anc 1370 . . . . 5 (𝜑 → (𝐵𝑁𝐷) ∈ ℝ*)
129126, 128prssd 4769 . . . 4 (𝜑 → {(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ⊆ ℝ*)
130 xrltso 12976 . . . . . 6 < Or ℝ*
131 supsn 9329 . . . . . 6 (( < Or ℝ* ∧ 0 ∈ ℝ*) → sup({0}, ℝ*, < ) = 0)
132130, 122, 131mp2an 689 . . . . 5 sup({0}, ℝ*, < ) = 0
133 supxrcl 13150 . . . . . . 7 ({(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ⊆ ℝ* → sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ) ∈ ℝ*)
134129, 133syl 17 . . . . . 6 (𝜑 → sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ) ∈ ℝ*)
135 xmetge0 23603 . . . . . . 7 ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝐴𝑋𝐶𝑋) → 0 ≤ (𝐴𝑀𝐶))
13619, 26, 38, 135syl3anc 1370 . . . . . 6 (𝜑 → 0 ≤ (𝐴𝑀𝐶))
137 ovex 7370 . . . . . . . 8 (𝐴𝑀𝐶) ∈ V
138137prid1 4710 . . . . . . 7 (𝐴𝑀𝐶) ∈ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)}
139 supxrub 13159 . . . . . . 7 (({(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ⊆ ℝ* ∧ (𝐴𝑀𝐶) ∈ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)}) → (𝐴𝑀𝐶) ≤ sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ))
140129, 138, 139sylancl 586 . . . . . 6 (𝜑 → (𝐴𝑀𝐶) ≤ sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ))
141123, 126, 134, 136, 140xrletrd 12997 . . . . 5 (𝜑 → 0 ≤ sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ))
142132, 141eqbrtrid 5127 . . . 4 (𝜑 → sup({0}, ℝ*, < ) ≤ sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ))
143 supxrun 13151 . . . 4 (({0} ⊆ ℝ* ∧ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ⊆ ℝ* ∧ sup({0}, ℝ*, < ) ≤ sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < )) → sup(({0} ∪ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)}), ℝ*, < ) = sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ))
144124, 129, 142, 143syl3anc 1370 . . 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 844   = wceq 1540  wcel 2105  wrex 3070  Vcvv 3441  cun 3896  wss 3898  c0 4269  {csn 4573  {cpr 4575  cop 4579   class class class wbr 5092  cmpt 5175   Or wor 5531   × cxp 5618  ccnv 5619  ran crn 5621  cres 5622  Oncon0 6302   Fn wfn 6474  wf 6475  1-1-ontowf1o 6478  cfv 6479  (class class class)co 7337  cmpo 7339  1oc1o 8360  2oc2o 8361  supcsup 9297  0cc0 10972  *cxr 11109   < clt 11110  cle 11111  Basecbs 17009  Scalarcsca 17062  distcds 17068  Xscprds 17253   ×s cxps 17314  ∞Metcxmet 20688
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5229  ax-sep 5243  ax-nul 5250  ax-pow 5308  ax-pr 5372  ax-un 7650  ax-cnex 11028  ax-resscn 11029  ax-1cn 11030  ax-icn 11031  ax-addcl 11032  ax-addrcl 11033  ax-mulcl 11034  ax-mulrcl 11035  ax-mulcom 11036  ax-addass 11037  ax-mulass 11038  ax-distr 11039  ax-i2m1 11040  ax-1ne0 11041  ax-1rid 11042  ax-rnegex 11043  ax-rrecex 11044  ax-cnre 11045  ax-pre-lttri 11046  ax-pre-lttrn 11047  ax-pre-ltadd 11048  ax-pre-mulgt0 11049  ax-pre-sup 11050
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3917  df-nul 4270  df-if 4474  df-pw 4549  df-sn 4574  df-pr 4576  df-tp 4578  df-op 4580  df-uni 4853  df-int 4895  df-iun 4943  df-iin 4944  df-br 5093  df-opab 5155  df-mpt 5176  df-tr 5210  df-id 5518  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5575  df-se 5576  df-we 5577  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-pred 6238  df-ord 6305  df-on 6306  df-lim 6307  df-suc 6308  df-iota 6431  df-fun 6481  df-fn 6482  df-f 6483  df-f1 6484  df-fo 6485  df-f1o 6486  df-fv 6487  df-isom 6488  df-riota 7293  df-ov 7340  df-oprab 7341  df-mpo 7342  df-of 7595  df-om 7781  df-1st 7899  df-2nd 7900  df-supp 8048  df-frecs 8167  df-wrecs 8198  df-recs 8272  df-rdg 8311  df-1o 8367  df-2o 8368  df-er 8569  df-map 8688  df-ixp 8757  df-en 8805  df-dom 8806  df-sdom 8807  df-fin 8808  df-fsupp 9227  df-sup 9299  df-inf 9300  df-oi 9367  df-card 9796  df-pnf 11112  df-mnf 11113  df-xr 11114  df-ltxr 11115  df-le 11116  df-sub 11308  df-neg 11309  df-div 11734  df-nn 12075  df-2 12137  df-3 12138  df-4 12139  df-5 12140  df-6 12141  df-7 12142  df-8 12143  df-9 12144  df-n0 12335  df-z 12421  df-dec 12539  df-uz 12684  df-rp 12832  df-xneg 12949  df-xadd 12950  df-xmul 12951  df-icc 13187  df-fz 13341  df-fzo 13484  df-seq 13823  df-hash 14146  df-struct 16945  df-sets 16962  df-slot 16980  df-ndx 16992  df-base 17010  df-ress 17039  df-plusg 17072  df-mulr 17073  df-sca 17075  df-vsca 17076  df-ip 17077  df-tset 17078  df-ple 17079  df-ds 17081  df-hom 17083  df-cco 17084  df-0g 17249  df-gsum 17250  df-prds 17255  df-xrs 17310  df-imas 17316  df-xps 17318  df-mre 17392  df-mrc 17393  df-acs 17395  df-mgm 18423  df-sgrp 18472  df-mnd 18483  df-submnd 18528  df-mulg 18797  df-cntz 19019  df-cmn 19483  df-xmet 20696
This theorem is referenced by:  tmsxpsval  23800
  Copyright terms: Public domain W3C validator