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 2622 |
. . . . 5
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) |
7 | | eqid 2622 |
. . . . 5
⊢
(Scalar‘𝑅) =
(Scalar‘𝑅) |
8 | | eqid 2622 |
. . . . 5
⊢
((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})) = ((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | xpsval 16232 |
. . . 4
⊢ (𝜑 → 𝑇 = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) “s
((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))) |
10 | 1, 2, 3, 4, 5, 6, 7, 8 | xpslem 16233 |
. . . 4
⊢ (𝜑 → ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) = (Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))) |
11 | 6 | xpsff1o2 16231 |
. . . . 5
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) |
12 | | f1ocnv 6149 |
. . . . 5
⊢ ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))–1-1-onto→(𝑋 × 𝑌)) |
13 | 11, 12 | mp1i 13 |
. . . 4
⊢ (𝜑 → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))–1-1-onto→(𝑋 × 𝑌)) |
14 | | ovexd 6680 |
. . . 4
⊢ (𝜑 → ((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})) ∈ V) |
15 | | eqid 2622 |
. . . 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 22184 |
. . . . 5
⊢ (𝜑 →
(dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ∈ (∞Met‘ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))) |
22 | | ssid 3624 |
. . . . 5
⊢ ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) ⊆ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) |
23 | | xmetres2 22166 |
. . . . 5
⊢
(((dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ∈ (∞Met‘ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) ∧ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) ⊆ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) → ((dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ↾ (ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) × ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))) ∈ (∞Met‘ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))) |
24 | 21, 22, 23 | sylancl 694 |
. . . 4
⊢ (𝜑 →
((dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ↾ (ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) × ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))) ∈ (∞Met‘ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))) |
25 | | df-ov 6653 |
. . . . . 6
⊢ (𝐴(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))𝐵) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐴, 𝐵〉) |
26 | | xpsds.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑋) |
27 | | xpsds.b |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ 𝑌) |
28 | 6 | xpsfval 16227 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → (𝐴(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))𝐵) = ◡({𝐴} +𝑐 {𝐵})) |
29 | 26, 27, 28 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → (𝐴(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))𝐵) = ◡({𝐴} +𝑐 {𝐵})) |
30 | 25, 29 | syl5eqr 2670 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐴, 𝐵〉) = ◡({𝐴} +𝑐 {𝐵})) |
31 | | opelxpi 5148 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → 〈𝐴, 𝐵〉 ∈ (𝑋 × 𝑌)) |
32 | 26, 27, 31 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → 〈𝐴, 𝐵〉 ∈ (𝑋 × 𝑌)) |
33 | | f1of 6137 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)⟶ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) |
34 | 11, 33 | ax-mp 5 |
. . . . . . 7
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)⟶ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) |
35 | 34 | ffvelrni 6358 |
. . . . . 6
⊢
(〈𝐴, 𝐵〉 ∈ (𝑋 × 𝑌) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐴, 𝐵〉) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) |
36 | 32, 35 | syl 17 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐴, 𝐵〉) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) |
37 | 30, 36 | eqeltrrd 2702 |
. . . 4
⊢ (𝜑 → ◡({𝐴} +𝑐 {𝐵}) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) |
38 | | df-ov 6653 |
. . . . . 6
⊢ (𝐶(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))𝐷) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐶, 𝐷〉) |
39 | | xpsds.c |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ 𝑋) |
40 | | xpsds.d |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ 𝑌) |
41 | 6 | xpsfval 16227 |
. . . . . . 7
⊢ ((𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) → (𝐶(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))𝐷) = ◡({𝐶} +𝑐 {𝐷})) |
42 | 39, 40, 41 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → (𝐶(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))𝐷) = ◡({𝐶} +𝑐 {𝐷})) |
43 | 38, 42 | syl5eqr 2670 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐶, 𝐷〉) = ◡({𝐶} +𝑐 {𝐷})) |
44 | | opelxpi 5148 |
. . . . . . 7
⊢ ((𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) → 〈𝐶, 𝐷〉 ∈ (𝑋 × 𝑌)) |
45 | 39, 40, 44 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → 〈𝐶, 𝐷〉 ∈ (𝑋 × 𝑌)) |
46 | 34 | ffvelrni 6358 |
. . . . . 6
⊢
(〈𝐶, 𝐷〉 ∈ (𝑋 × 𝑌) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐶, 𝐷〉) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) |
47 | 45, 46 | syl 17 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐶, 𝐷〉) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) |
48 | 43, 47 | eqeltrrd 2702 |
. . . 4
⊢ (𝜑 → ◡({𝐶} +𝑐 {𝐷}) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) |
49 | 9, 10, 13, 14, 15, 16, 24, 37, 48 | imasdsf1o 22179 |
. . 3
⊢ (𝜑 → ((◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐴} +𝑐 {𝐵}))𝑃(◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐶} +𝑐 {𝐷}))) = (◡({𝐴} +𝑐 {𝐵})((dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ↾ (ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) × ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))))◡({𝐶} +𝑐 {𝐷}))) |
50 | 37, 48 | ovresd 6801 |
. . 3
⊢ (𝜑 → (◡({𝐴} +𝑐 {𝐵})((dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ↾ (ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) × ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))))◡({𝐶} +𝑐 {𝐷})) = (◡({𝐴} +𝑐 {𝐵})(dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))◡({𝐶} +𝑐 {𝐷}))) |
51 | 49, 50 | eqtrd 2656 |
. 2
⊢ (𝜑 → ((◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐴} +𝑐 {𝐵}))𝑃(◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐶} +𝑐 {𝐷}))) = (◡({𝐴} +𝑐 {𝐵})(dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))◡({𝐶} +𝑐 {𝐷}))) |
52 | | f1ocnvfv 6534 |
. . . . 5
⊢ (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) ∧ 〈𝐴, 𝐵〉 ∈ (𝑋 × 𝑌)) → (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐴, 𝐵〉) = ◡({𝐴} +𝑐 {𝐵}) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐴} +𝑐 {𝐵})) = 〈𝐴, 𝐵〉)) |
53 | 11, 32, 52 | sylancr 695 |
. . . 4
⊢ (𝜑 → (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐴, 𝐵〉) = ◡({𝐴} +𝑐 {𝐵}) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐴} +𝑐 {𝐵})) = 〈𝐴, 𝐵〉)) |
54 | 30, 53 | mpd 15 |
. . 3
⊢ (𝜑 → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐴} +𝑐 {𝐵})) = 〈𝐴, 𝐵〉) |
55 | | f1ocnvfv 6534 |
. . . . 5
⊢ (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) ∧ 〈𝐶, 𝐷〉 ∈ (𝑋 × 𝑌)) → (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐶, 𝐷〉) = ◡({𝐶} +𝑐 {𝐷}) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐶} +𝑐 {𝐷})) = 〈𝐶, 𝐷〉)) |
56 | 11, 45, 55 | sylancr 695 |
. . . 4
⊢ (𝜑 → (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐶, 𝐷〉) = ◡({𝐶} +𝑐 {𝐷}) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐶} +𝑐 {𝐷})) = 〈𝐶, 𝐷〉)) |
57 | 43, 56 | mpd 15 |
. . 3
⊢ (𝜑 → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐶} +𝑐 {𝐷})) = 〈𝐶, 𝐷〉) |
58 | 54, 57 | oveq12d 6668 |
. 2
⊢ (𝜑 → ((◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐴} +𝑐 {𝐵}))𝑃(◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐶} +𝑐 {𝐷}))) = (〈𝐴, 𝐵〉𝑃〈𝐶, 𝐷〉)) |
59 | | eqid 2622 |
. . . 4
⊢
(Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) = (Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) |
60 | | fvexd 6203 |
. . . 4
⊢ (𝜑 → (Scalar‘𝑅) ∈ V) |
61 | | 2on 7568 |
. . . . 5
⊢
2𝑜 ∈ On |
62 | 61 | a1i 11 |
. . . 4
⊢ (𝜑 → 2𝑜
∈ On) |
63 | | xpscfn 16219 |
. . . . 5
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → ◡({𝑅} +𝑐 {𝑆}) Fn
2𝑜) |
64 | 4, 5, 63 | syl2anc 693 |
. . . 4
⊢ (𝜑 → ◡({𝑅} +𝑐 {𝑆}) Fn
2𝑜) |
65 | 37, 10 | eleqtrd 2703 |
. . . 4
⊢ (𝜑 → ◡({𝐴} +𝑐 {𝐵}) ∈ (Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))) |
66 | 48, 10 | eleqtrd 2703 |
. . . 4
⊢ (𝜑 → ◡({𝐶} +𝑐 {𝐷}) ∈ (Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))) |
67 | | eqid 2622 |
. . . 4
⊢
(dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) = (dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) |
68 | 8, 59, 60, 62, 64, 65, 66, 67 | prdsdsval 16138 |
. . 3
⊢ (𝜑 → (◡({𝐴} +𝑐 {𝐵})(dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))◡({𝐶} +𝑐 {𝐷})) = sup((ran (𝑘 ∈ 2𝑜 ↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))) ∪ {0}), ℝ*, <
)) |
69 | | df2o3 7573 |
. . . . . . . . . . 11
⊢
2𝑜 = {∅,
1𝑜} |
70 | 69 | rexeqi 3143 |
. . . . . . . . . 10
⊢
(∃𝑘 ∈
2𝑜 𝑥 =
((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)) ↔ ∃𝑘 ∈ {∅, 1𝑜}𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))) |
71 | | 0ex 4790 |
. . . . . . . . . . 11
⊢ ∅
∈ V |
72 | | 1on 7567 |
. . . . . . . . . . . 12
⊢
1𝑜 ∈ On |
73 | 72 | elexi 3213 |
. . . . . . . . . . 11
⊢
1𝑜 ∈ V |
74 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = ∅ → (◡({𝑅} +𝑐 {𝑆})‘𝑘) = (◡({𝑅} +𝑐 {𝑆})‘∅)) |
75 | 74 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝑘 = ∅ →
(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) = (dist‘(◡({𝑅} +𝑐 {𝑆})‘∅))) |
76 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ (𝑘 = ∅ → (◡({𝐴} +𝑐 {𝐵})‘𝑘) = (◡({𝐴} +𝑐 {𝐵})‘∅)) |
77 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ (𝑘 = ∅ → (◡({𝐶} +𝑐 {𝐷})‘𝑘) = (◡({𝐶} +𝑐 {𝐷})‘∅)) |
78 | 75, 76, 77 | oveq123d 6671 |
. . . . . . . . . . . 12
⊢ (𝑘 = ∅ → ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)) = ((◡({𝐴} +𝑐 {𝐵})‘∅)(dist‘(◡({𝑅} +𝑐 {𝑆})‘∅))(◡({𝐶} +𝑐 {𝐷})‘∅))) |
79 | 78 | eqeq2d 2632 |
. . . . . . . . . . 11
⊢ (𝑘 = ∅ → (𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)) ↔ 𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘∅)(dist‘(◡({𝑅} +𝑐 {𝑆})‘∅))(◡({𝐶} +𝑐 {𝐷})‘∅)))) |
80 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 1𝑜 →
(◡({𝑅} +𝑐 {𝑆})‘𝑘) = (◡({𝑅} +𝑐 {𝑆})‘1𝑜)) |
81 | 80 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 1𝑜 →
(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) = (dist‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜))) |
82 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 1𝑜 →
(◡({𝐴} +𝑐 {𝐵})‘𝑘) = (◡({𝐴} +𝑐 {𝐵})‘1𝑜)) |
83 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 1𝑜 →
(◡({𝐶} +𝑐 {𝐷})‘𝑘) = (◡({𝐶} +𝑐 {𝐷})‘1𝑜)) |
84 | 81, 82, 83 | oveq123d 6671 |
. . . . . . . . . . . 12
⊢ (𝑘 = 1𝑜 →
((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)) = ((◡({𝐴} +𝑐 {𝐵})‘1𝑜)(dist‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜))(◡({𝐶} +𝑐 {𝐷})‘1𝑜))) |
85 | 84 | eqeq2d 2632 |
. . . . . . . . . . 11
⊢ (𝑘 = 1𝑜 →
(𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)) ↔ 𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘1𝑜)(dist‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜))(◡({𝐶} +𝑐 {𝐷})‘1𝑜)))) |
86 | 71, 73, 79, 85 | rexpr 4239 |
. . . . . . . . . 10
⊢
(∃𝑘 ∈
{∅, 1𝑜}𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)) ↔ (𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘∅)(dist‘(◡({𝑅} +𝑐 {𝑆})‘∅))(◡({𝐶} +𝑐 {𝐷})‘∅)) ∨ 𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘1𝑜)(dist‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜))(◡({𝐶} +𝑐 {𝐷})‘1𝑜)))) |
87 | 70, 86 | bitri 264 |
. . . . . . . . 9
⊢
(∃𝑘 ∈
2𝑜 𝑥 =
((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)) ↔ (𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘∅)(dist‘(◡({𝑅} +𝑐 {𝑆})‘∅))(◡({𝐶} +𝑐 {𝐷})‘∅)) ∨ 𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘1𝑜)(dist‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜))(◡({𝐶} +𝑐 {𝐷})‘1𝑜)))) |
88 | | xpsc0 16220 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ 𝑉 → (◡({𝑅} +𝑐 {𝑆})‘∅) = 𝑅) |
89 | 4, 88 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (◡({𝑅} +𝑐 {𝑆})‘∅) = 𝑅) |
90 | 89 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (dist‘(◡({𝑅} +𝑐 {𝑆})‘∅)) = (dist‘𝑅)) |
91 | | xpsc0 16220 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ 𝑋 → (◡({𝐴} +𝑐 {𝐵})‘∅) = 𝐴) |
92 | 26, 91 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (◡({𝐴} +𝑐 {𝐵})‘∅) = 𝐴) |
93 | | xpsc0 16220 |
. . . . . . . . . . . . . 14
⊢ (𝐶 ∈ 𝑋 → (◡({𝐶} +𝑐 {𝐷})‘∅) = 𝐶) |
94 | 39, 93 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (◡({𝐶} +𝑐 {𝐷})‘∅) = 𝐶) |
95 | 90, 92, 94 | oveq123d 6671 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((◡({𝐴} +𝑐 {𝐵})‘∅)(dist‘(◡({𝑅} +𝑐 {𝑆})‘∅))(◡({𝐶} +𝑐 {𝐷})‘∅)) = (𝐴(dist‘𝑅)𝐶)) |
96 | 17 | oveqi 6663 |
. . . . . . . . . . . . 13
⊢ (𝐴𝑀𝐶) = (𝐴((dist‘𝑅) ↾ (𝑋 × 𝑋))𝐶) |
97 | 26, 39 | ovresd 6801 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴((dist‘𝑅) ↾ (𝑋 × 𝑋))𝐶) = (𝐴(dist‘𝑅)𝐶)) |
98 | 96, 97 | syl5eq 2668 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴𝑀𝐶) = (𝐴(dist‘𝑅)𝐶)) |
99 | 95, 98 | eqtr4d 2659 |
. . . . . . . . . . 11
⊢ (𝜑 → ((◡({𝐴} +𝑐 {𝐵})‘∅)(dist‘(◡({𝑅} +𝑐 {𝑆})‘∅))(◡({𝐶} +𝑐 {𝐷})‘∅)) = (𝐴𝑀𝐶)) |
100 | 99 | eqeq2d 2632 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘∅)(dist‘(◡({𝑅} +𝑐 {𝑆})‘∅))(◡({𝐶} +𝑐 {𝐷})‘∅)) ↔ 𝑥 = (𝐴𝑀𝐶))) |
101 | | xpsc1 16221 |
. . . . . . . . . . . . . . 15
⊢ (𝑆 ∈ 𝑊 → (◡({𝑅} +𝑐 {𝑆})‘1𝑜) = 𝑆) |
102 | 5, 101 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (◡({𝑅} +𝑐 {𝑆})‘1𝑜) = 𝑆) |
103 | 102 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (dist‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜)) =
(dist‘𝑆)) |
104 | | xpsc1 16221 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ 𝑌 → (◡({𝐴} +𝑐 {𝐵})‘1𝑜) = 𝐵) |
105 | 27, 104 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (◡({𝐴} +𝑐 {𝐵})‘1𝑜) = 𝐵) |
106 | | xpsc1 16221 |
. . . . . . . . . . . . . 14
⊢ (𝐷 ∈ 𝑌 → (◡({𝐶} +𝑐 {𝐷})‘1𝑜) = 𝐷) |
107 | 40, 106 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (◡({𝐶} +𝑐 {𝐷})‘1𝑜) = 𝐷) |
108 | 103, 105,
107 | oveq123d 6671 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((◡({𝐴} +𝑐 {𝐵})‘1𝑜)(dist‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜))(◡({𝐶} +𝑐 {𝐷})‘1𝑜)) = (𝐵(dist‘𝑆)𝐷)) |
109 | 18 | oveqi 6663 |
. . . . . . . . . . . . 13
⊢ (𝐵𝑁𝐷) = (𝐵((dist‘𝑆) ↾ (𝑌 × 𝑌))𝐷) |
110 | 27, 40 | ovresd 6801 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐵((dist‘𝑆) ↾ (𝑌 × 𝑌))𝐷) = (𝐵(dist‘𝑆)𝐷)) |
111 | 109, 110 | syl5eq 2668 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵𝑁𝐷) = (𝐵(dist‘𝑆)𝐷)) |
112 | 108, 111 | eqtr4d 2659 |
. . . . . . . . . . 11
⊢ (𝜑 → ((◡({𝐴} +𝑐 {𝐵})‘1𝑜)(dist‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜))(◡({𝐶} +𝑐 {𝐷})‘1𝑜)) = (𝐵𝑁𝐷)) |
113 | 112 | eqeq2d 2632 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘1𝑜)(dist‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜))(◡({𝐶} +𝑐 {𝐷})‘1𝑜)) ↔ 𝑥 = (𝐵𝑁𝐷))) |
114 | 100, 113 | orbi12d 746 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘∅)(dist‘(◡({𝑅} +𝑐 {𝑆})‘∅))(◡({𝐶} +𝑐 {𝐷})‘∅)) ∨ 𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘1𝑜)(dist‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜))(◡({𝐶} +𝑐 {𝐷})‘1𝑜))) ↔ (𝑥 = (𝐴𝑀𝐶) ∨ 𝑥 = (𝐵𝑁𝐷)))) |
115 | 87, 114 | syl5bb 272 |
. . . . . . . 8
⊢ (𝜑 → (∃𝑘 ∈ 2𝑜 𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)) ↔ (𝑥 = (𝐴𝑀𝐶) ∨ 𝑥 = (𝐵𝑁𝐷)))) |
116 | | vex 3203 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
117 | | eqid 2622 |
. . . . . . . . . 10
⊢ (𝑘 ∈ 2𝑜
↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))) = (𝑘 ∈ 2𝑜 ↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))) |
118 | 117 | elrnmpt 5372 |
. . . . . . . . 9
⊢ (𝑥 ∈ V → (𝑥 ∈ ran (𝑘 ∈ 2𝑜 ↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))) ↔ ∃𝑘 ∈ 2𝑜 𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)))) |
119 | 116, 118 | ax-mp 5 |
. . . . . . . 8
⊢ (𝑥 ∈ ran (𝑘 ∈ 2𝑜 ↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))) ↔ ∃𝑘 ∈ 2𝑜 𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))) |
120 | 116 | elpr 4198 |
. . . . . . . 8
⊢ (𝑥 ∈ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ↔ (𝑥 = (𝐴𝑀𝐶) ∨ 𝑥 = (𝐵𝑁𝐷))) |
121 | 115, 119,
120 | 3bitr4g 303 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ ran (𝑘 ∈ 2𝑜 ↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))) ↔ 𝑥 ∈ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)})) |
122 | 121 | eqrdv 2620 |
. . . . . 6
⊢ (𝜑 → ran (𝑘 ∈ 2𝑜 ↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))) = {(𝐴𝑀𝐶), (𝐵𝑁𝐷)}) |
123 | 122 | uneq1d 3766 |
. . . . 5
⊢ (𝜑 → (ran (𝑘 ∈ 2𝑜 ↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))) ∪ {0}) = ({(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ∪ {0})) |
124 | | uncom 3757 |
. . . . 5
⊢ ({(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ∪ {0}) = ({0} ∪ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)}) |
125 | 123, 124 | syl6eq 2672 |
. . . 4
⊢ (𝜑 → (ran (𝑘 ∈ 2𝑜 ↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))) ∪ {0}) = ({0} ∪ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)})) |
126 | 125 | supeq1d 8352 |
. . 3
⊢ (𝜑 → sup((ran (𝑘 ∈ 2𝑜
↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))) ∪ {0}), ℝ*, < ) =
sup(({0} ∪ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)}), ℝ*, <
)) |
127 | | 0xr 10086 |
. . . . . 6
⊢ 0 ∈
ℝ* |
128 | 127 | a1i 11 |
. . . . 5
⊢ (𝜑 → 0 ∈
ℝ*) |
129 | 128 | snssd 4340 |
. . . 4
⊢ (𝜑 → {0} ⊆
ℝ*) |
130 | | xmetcl 22136 |
. . . . . 6
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (𝐴𝑀𝐶) ∈
ℝ*) |
131 | 19, 26, 39, 130 | syl3anc 1326 |
. . . . 5
⊢ (𝜑 → (𝐴𝑀𝐶) ∈
ℝ*) |
132 | | xmetcl 22136 |
. . . . . 6
⊢ ((𝑁 ∈ (∞Met‘𝑌) ∧ 𝐵 ∈ 𝑌 ∧ 𝐷 ∈ 𝑌) → (𝐵𝑁𝐷) ∈
ℝ*) |
133 | 20, 27, 40, 132 | syl3anc 1326 |
. . . . 5
⊢ (𝜑 → (𝐵𝑁𝐷) ∈
ℝ*) |
134 | | prssi 4353 |
. . . . 5
⊢ (((𝐴𝑀𝐶) ∈ ℝ* ∧ (𝐵𝑁𝐷) ∈ ℝ*) → {(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ⊆
ℝ*) |
135 | 131, 133,
134 | syl2anc 693 |
. . . 4
⊢ (𝜑 → {(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ⊆
ℝ*) |
136 | | xrltso 11974 |
. . . . . 6
⊢ < Or
ℝ* |
137 | | supsn 8378 |
. . . . . 6
⊢ (( <
Or ℝ* ∧ 0 ∈ ℝ*) → sup({0},
ℝ*, < ) = 0) |
138 | 136, 127,
137 | mp2an 708 |
. . . . 5
⊢ sup({0},
ℝ*, < ) = 0 |
139 | | supxrcl 12145 |
. . . . . . 7
⊢ ({(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ⊆ ℝ* →
sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ) ∈
ℝ*) |
140 | 135, 139 | syl 17 |
. . . . . 6
⊢ (𝜑 → sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ) ∈
ℝ*) |
141 | | xmetge0 22149 |
. . . . . . 7
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → 0 ≤ (𝐴𝑀𝐶)) |
142 | 19, 26, 39, 141 | syl3anc 1326 |
. . . . . 6
⊢ (𝜑 → 0 ≤ (𝐴𝑀𝐶)) |
143 | | ovex 6678 |
. . . . . . . 8
⊢ (𝐴𝑀𝐶) ∈ V |
144 | 143 | prid1 4297 |
. . . . . . 7
⊢ (𝐴𝑀𝐶) ∈ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)} |
145 | | supxrub 12154 |
. . . . . . 7
⊢ (({(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ⊆ ℝ* ∧ (𝐴𝑀𝐶) ∈ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)}) → (𝐴𝑀𝐶) ≤ sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, <
)) |
146 | 135, 144,
145 | sylancl 694 |
. . . . . 6
⊢ (𝜑 → (𝐴𝑀𝐶) ≤ sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, <
)) |
147 | 128, 131,
140, 142, 146 | xrletrd 11993 |
. . . . 5
⊢ (𝜑 → 0 ≤ sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, <
)) |
148 | 138, 147 | syl5eqbr 4688 |
. . . 4
⊢ (𝜑 → sup({0},
ℝ*, < ) ≤ sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, <
)) |
149 | | supxrun 12146 |
. . . 4
⊢ (({0}
⊆ ℝ* ∧ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ⊆ ℝ* ∧
sup({0}, ℝ*, < ) ≤ sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < )) →
sup(({0} ∪ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)}), ℝ*, < ) =
sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, <
)) |
150 | 129, 135,
148, 149 | syl3anc 1326 |
. . 3
⊢ (𝜑 → sup(({0} ∪ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)}), ℝ*, < ) =
sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, <
)) |
151 | 68, 126, 150 | 3eqtrd 2660 |
. 2
⊢ (𝜑 → (◡({𝐴} +𝑐 {𝐵})(dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))◡({𝐶} +𝑐 {𝐷})) = sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, <
)) |
152 | 51, 58, 151 | 3eqtr3d 2664 |
1
⊢ (𝜑 → (〈𝐴, 𝐵〉𝑃〈𝐶, 𝐷〉) = sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, <
)) |