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({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, <
)) |