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 2610 |
. . . . 5
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) |
7 | | eqid 2610 |
. . . . 5
⊢
(Scalar‘𝑅) =
(Scalar‘𝑅) |
8 | | eqid 2610 |
. . . . 5
⊢
((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})) = ((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | xpsval 16055 |
. . . 4
⊢ (𝜑 → 𝑇 = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) “s
((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))) |
10 | 1, 2, 3, 4, 5, 6, 7, 8 | xpslem 16056 |
. . . 4
⊢ (𝜑 → ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) = (Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))) |
11 | 6 | xpsff1o2 16054 |
. . . . 5
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) |
12 | | f1ocnv 6062 |
. . . . 5
⊢ ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))–1-1-onto→(𝑋 × 𝑌)) |
13 | 11, 12 | mp1i 13 |
. . . 4
⊢ (𝜑 → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))–1-1-onto→(𝑋 × 𝑌)) |
14 | | ovex 6577 |
. . . . 5
⊢
((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})) ∈ V |
15 | 14 | a1i 11 |
. . . 4
⊢ (𝜑 → ((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})) ∈ V) |
16 | | eqid 2610 |
. . . 4
⊢
((dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ↾ (ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) × ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))) = ((dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ↾ (ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) × ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))) |
17 | | xpsds.p |
. . . 4
⊢ 𝑃 = (dist‘𝑇) |
18 | | xpsds.m |
. . . . . 6
⊢ 𝑀 = ((dist‘𝑅) ↾ (𝑋 × 𝑋)) |
19 | | xpsds.n |
. . . . . 6
⊢ 𝑁 = ((dist‘𝑆) ↾ (𝑌 × 𝑌)) |
20 | | xpsds.3 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ (∞Met‘𝑋)) |
21 | | xpsds.4 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ (∞Met‘𝑌)) |
22 | 1, 2, 3, 4, 5, 17,
18, 19, 20, 21 | xpsxmetlem 21994 |
. . . . 5
⊢ (𝜑 →
(dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ∈ (∞Met‘ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))) |
23 | | ssid 3587 |
. . . . 5
⊢ ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) ⊆ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) |
24 | | xmetres2 21976 |
. . . . 5
⊢
(((dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ∈ (∞Met‘ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) ∧ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) ⊆ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) → ((dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ↾ (ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) × ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))) ∈ (∞Met‘ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))) |
25 | 22, 23, 24 | sylancl 693 |
. . . 4
⊢ (𝜑 →
((dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ↾ (ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) × ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))) ∈ (∞Met‘ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))) |
26 | | df-ov 6552 |
. . . . . 6
⊢ (𝐴(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))𝐵) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐴, 𝐵〉) |
27 | | xpsds.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑋) |
28 | | xpsds.b |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ 𝑌) |
29 | 6 | xpsfval 16050 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → (𝐴(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))𝐵) = ◡({𝐴} +𝑐 {𝐵})) |
30 | 27, 28, 29 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → (𝐴(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))𝐵) = ◡({𝐴} +𝑐 {𝐵})) |
31 | 26, 30 | syl5eqr 2658 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐴, 𝐵〉) = ◡({𝐴} +𝑐 {𝐵})) |
32 | | opelxpi 5072 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → 〈𝐴, 𝐵〉 ∈ (𝑋 × 𝑌)) |
33 | 27, 28, 32 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → 〈𝐴, 𝐵〉 ∈ (𝑋 × 𝑌)) |
34 | | f1of 6050 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)⟶ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) |
35 | 11, 34 | ax-mp 5 |
. . . . . . 7
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)⟶ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) |
36 | 35 | ffvelrni 6266 |
. . . . . 6
⊢
(〈𝐴, 𝐵〉 ∈ (𝑋 × 𝑌) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐴, 𝐵〉) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) |
37 | 33, 36 | syl 17 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐴, 𝐵〉) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) |
38 | 31, 37 | eqeltrrd 2689 |
. . . 4
⊢ (𝜑 → ◡({𝐴} +𝑐 {𝐵}) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) |
39 | | df-ov 6552 |
. . . . . 6
⊢ (𝐶(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))𝐷) = ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐶, 𝐷〉) |
40 | | xpsds.c |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ 𝑋) |
41 | | xpsds.d |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ 𝑌) |
42 | 6 | xpsfval 16050 |
. . . . . . 7
⊢ ((𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) → (𝐶(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))𝐷) = ◡({𝐶} +𝑐 {𝐷})) |
43 | 40, 41, 42 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → (𝐶(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))𝐷) = ◡({𝐶} +𝑐 {𝐷})) |
44 | 39, 43 | syl5eqr 2658 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐶, 𝐷〉) = ◡({𝐶} +𝑐 {𝐷})) |
45 | | opelxpi 5072 |
. . . . . . 7
⊢ ((𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) → 〈𝐶, 𝐷〉 ∈ (𝑋 × 𝑌)) |
46 | 40, 41, 45 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → 〈𝐶, 𝐷〉 ∈ (𝑋 × 𝑌)) |
47 | 35 | ffvelrni 6266 |
. . . . . 6
⊢
(〈𝐶, 𝐷〉 ∈ (𝑋 × 𝑌) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐶, 𝐷〉) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) |
48 | 46, 47 | syl 17 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐶, 𝐷〉) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) |
49 | 44, 48 | eqeltrrd 2689 |
. . . 4
⊢ (𝜑 → ◡({𝐶} +𝑐 {𝐷}) ∈ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) |
50 | 9, 10, 13, 15, 16, 17, 25, 38, 49 | imasdsf1o 21989 |
. . 3
⊢ (𝜑 → ((◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐴} +𝑐 {𝐵}))𝑃(◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐶} +𝑐 {𝐷}))) = (◡({𝐴} +𝑐 {𝐵})((dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ↾ (ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) × ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))))◡({𝐶} +𝑐 {𝐷}))) |
51 | 38, 49 | ovresd 6699 |
. . 3
⊢ (𝜑 → (◡({𝐴} +𝑐 {𝐵})((dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ↾ (ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) × ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))))◡({𝐶} +𝑐 {𝐷})) = (◡({𝐴} +𝑐 {𝐵})(dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))◡({𝐶} +𝑐 {𝐷}))) |
52 | 50, 51 | eqtrd 2644 |
. 2
⊢ (𝜑 → ((◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐴} +𝑐 {𝐵}))𝑃(◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐶} +𝑐 {𝐷}))) = (◡({𝐴} +𝑐 {𝐵})(dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))◡({𝐶} +𝑐 {𝐷}))) |
53 | | f1ocnvfv 6434 |
. . . . 5
⊢ (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) ∧ 〈𝐴, 𝐵〉 ∈ (𝑋 × 𝑌)) → (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐴, 𝐵〉) = ◡({𝐴} +𝑐 {𝐵}) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐴} +𝑐 {𝐵})) = 〈𝐴, 𝐵〉)) |
54 | 11, 33, 53 | sylancr 694 |
. . . 4
⊢ (𝜑 → (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐴, 𝐵〉) = ◡({𝐴} +𝑐 {𝐵}) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐴} +𝑐 {𝐵})) = 〈𝐴, 𝐵〉)) |
55 | 31, 54 | mpd 15 |
. . 3
⊢ (𝜑 → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐴} +𝑐 {𝐵})) = 〈𝐴, 𝐵〉) |
56 | | f1ocnvfv 6434 |
. . . . 5
⊢ (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) ∧ 〈𝐶, 𝐷〉 ∈ (𝑋 × 𝑌)) → (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐶, 𝐷〉) = ◡({𝐶} +𝑐 {𝐷}) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐶} +𝑐 {𝐷})) = 〈𝐶, 𝐷〉)) |
57 | 11, 46, 56 | sylancr 694 |
. . . 4
⊢ (𝜑 → (((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘〈𝐶, 𝐷〉) = ◡({𝐶} +𝑐 {𝐷}) → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐶} +𝑐 {𝐷})) = 〈𝐶, 𝐷〉)) |
58 | 44, 57 | mpd 15 |
. . 3
⊢ (𝜑 → (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐶} +𝑐 {𝐷})) = 〈𝐶, 𝐷〉) |
59 | 55, 58 | oveq12d 6567 |
. 2
⊢ (𝜑 → ((◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐴} +𝑐 {𝐵}))𝑃(◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))‘◡({𝐶} +𝑐 {𝐷}))) = (〈𝐴, 𝐵〉𝑃〈𝐶, 𝐷〉)) |
60 | | eqid 2610 |
. . . 4
⊢
(Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) = (Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) |
61 | | fvex 6113 |
. . . . 5
⊢
(Scalar‘𝑅)
∈ V |
62 | 61 | a1i 11 |
. . . 4
⊢ (𝜑 → (Scalar‘𝑅) ∈ V) |
63 | | 2on 7455 |
. . . . 5
⊢
2𝑜 ∈ On |
64 | 63 | a1i 11 |
. . . 4
⊢ (𝜑 → 2𝑜
∈ On) |
65 | | xpscfn 16042 |
. . . . 5
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → ◡({𝑅} +𝑐 {𝑆}) Fn
2𝑜) |
66 | 4, 5, 65 | syl2anc 691 |
. . . 4
⊢ (𝜑 → ◡({𝑅} +𝑐 {𝑆}) Fn
2𝑜) |
67 | 38, 10 | eleqtrd 2690 |
. . . 4
⊢ (𝜑 → ◡({𝐴} +𝑐 {𝐵}) ∈ (Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))) |
68 | 49, 10 | eleqtrd 2690 |
. . . 4
⊢ (𝜑 → ◡({𝐶} +𝑐 {𝐷}) ∈ (Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))) |
69 | | eqid 2610 |
. . . 4
⊢
(dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) = (dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) |
70 | 8, 60, 62, 64, 66, 67, 68, 69 | prdsdsval 15961 |
. . 3
⊢ (𝜑 → (◡({𝐴} +𝑐 {𝐵})(dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))◡({𝐶} +𝑐 {𝐷})) = sup((ran (𝑘 ∈ 2𝑜 ↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))) ∪ {0}), ℝ*, <
)) |
71 | | df2o3 7460 |
. . . . . . . . . . 11
⊢
2𝑜 = {∅,
1𝑜} |
72 | 71 | rexeqi 3120 |
. . . . . . . . . 10
⊢
(∃𝑘 ∈
2𝑜 𝑥 =
((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)) ↔ ∃𝑘 ∈ {∅, 1𝑜}𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))) |
73 | | 0ex 4718 |
. . . . . . . . . . 11
⊢ ∅
∈ V |
74 | | 1on 7454 |
. . . . . . . . . . . 12
⊢
1𝑜 ∈ On |
75 | 74 | elexi 3186 |
. . . . . . . . . . 11
⊢
1𝑜 ∈ V |
76 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = ∅ → (◡({𝑅} +𝑐 {𝑆})‘𝑘) = (◡({𝑅} +𝑐 {𝑆})‘∅)) |
77 | 76 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑘 = ∅ →
(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) = (dist‘(◡({𝑅} +𝑐 {𝑆})‘∅))) |
78 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑘 = ∅ → (◡({𝐴} +𝑐 {𝐵})‘𝑘) = (◡({𝐴} +𝑐 {𝐵})‘∅)) |
79 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑘 = ∅ → (◡({𝐶} +𝑐 {𝐷})‘𝑘) = (◡({𝐶} +𝑐 {𝐷})‘∅)) |
80 | 77, 78, 79 | oveq123d 6570 |
. . . . . . . . . . . 12
⊢ (𝑘 = ∅ → ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)) = ((◡({𝐴} +𝑐 {𝐵})‘∅)(dist‘(◡({𝑅} +𝑐 {𝑆})‘∅))(◡({𝐶} +𝑐 {𝐷})‘∅))) |
81 | 80 | eqeq2d 2620 |
. . . . . . . . . . 11
⊢ (𝑘 = ∅ → (𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)) ↔ 𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘∅)(dist‘(◡({𝑅} +𝑐 {𝑆})‘∅))(◡({𝐶} +𝑐 {𝐷})‘∅)))) |
82 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 1𝑜 →
(◡({𝑅} +𝑐 {𝑆})‘𝑘) = (◡({𝑅} +𝑐 {𝑆})‘1𝑜)) |
83 | 82 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 1𝑜 →
(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) = (dist‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜))) |
84 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 1𝑜 →
(◡({𝐴} +𝑐 {𝐵})‘𝑘) = (◡({𝐴} +𝑐 {𝐵})‘1𝑜)) |
85 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 1𝑜 →
(◡({𝐶} +𝑐 {𝐷})‘𝑘) = (◡({𝐶} +𝑐 {𝐷})‘1𝑜)) |
86 | 83, 84, 85 | oveq123d 6570 |
. . . . . . . . . . . 12
⊢ (𝑘 = 1𝑜 →
((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)) = ((◡({𝐴} +𝑐 {𝐵})‘1𝑜)(dist‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜))(◡({𝐶} +𝑐 {𝐷})‘1𝑜))) |
87 | 86 | eqeq2d 2620 |
. . . . . . . . . . 11
⊢ (𝑘 = 1𝑜 →
(𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)) ↔ 𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘1𝑜)(dist‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜))(◡({𝐶} +𝑐 {𝐷})‘1𝑜)))) |
88 | 73, 75, 81, 87 | rexpr 4186 |
. . . . . . . . . 10
⊢
(∃𝑘 ∈
{∅, 1𝑜}𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)) ↔ (𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘∅)(dist‘(◡({𝑅} +𝑐 {𝑆})‘∅))(◡({𝐶} +𝑐 {𝐷})‘∅)) ∨ 𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘1𝑜)(dist‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜))(◡({𝐶} +𝑐 {𝐷})‘1𝑜)))) |
89 | 72, 88 | bitri 263 |
. . . . . . . . 9
⊢
(∃𝑘 ∈
2𝑜 𝑥 =
((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)) ↔ (𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘∅)(dist‘(◡({𝑅} +𝑐 {𝑆})‘∅))(◡({𝐶} +𝑐 {𝐷})‘∅)) ∨ 𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘1𝑜)(dist‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜))(◡({𝐶} +𝑐 {𝐷})‘1𝑜)))) |
90 | | xpsc0 16043 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ 𝑉 → (◡({𝑅} +𝑐 {𝑆})‘∅) = 𝑅) |
91 | 4, 90 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (◡({𝑅} +𝑐 {𝑆})‘∅) = 𝑅) |
92 | 91 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (dist‘(◡({𝑅} +𝑐 {𝑆})‘∅)) = (dist‘𝑅)) |
93 | | xpsc0 16043 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ 𝑋 → (◡({𝐴} +𝑐 {𝐵})‘∅) = 𝐴) |
94 | 27, 93 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (◡({𝐴} +𝑐 {𝐵})‘∅) = 𝐴) |
95 | | xpsc0 16043 |
. . . . . . . . . . . . . 14
⊢ (𝐶 ∈ 𝑋 → (◡({𝐶} +𝑐 {𝐷})‘∅) = 𝐶) |
96 | 40, 95 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (◡({𝐶} +𝑐 {𝐷})‘∅) = 𝐶) |
97 | 92, 94, 96 | oveq123d 6570 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((◡({𝐴} +𝑐 {𝐵})‘∅)(dist‘(◡({𝑅} +𝑐 {𝑆})‘∅))(◡({𝐶} +𝑐 {𝐷})‘∅)) = (𝐴(dist‘𝑅)𝐶)) |
98 | 18 | oveqi 6562 |
. . . . . . . . . . . . 13
⊢ (𝐴𝑀𝐶) = (𝐴((dist‘𝑅) ↾ (𝑋 × 𝑋))𝐶) |
99 | 27, 40 | ovresd 6699 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴((dist‘𝑅) ↾ (𝑋 × 𝑋))𝐶) = (𝐴(dist‘𝑅)𝐶)) |
100 | 98, 99 | syl5eq 2656 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴𝑀𝐶) = (𝐴(dist‘𝑅)𝐶)) |
101 | 97, 100 | eqtr4d 2647 |
. . . . . . . . . . 11
⊢ (𝜑 → ((◡({𝐴} +𝑐 {𝐵})‘∅)(dist‘(◡({𝑅} +𝑐 {𝑆})‘∅))(◡({𝐶} +𝑐 {𝐷})‘∅)) = (𝐴𝑀𝐶)) |
102 | 101 | eqeq2d 2620 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘∅)(dist‘(◡({𝑅} +𝑐 {𝑆})‘∅))(◡({𝐶} +𝑐 {𝐷})‘∅)) ↔ 𝑥 = (𝐴𝑀𝐶))) |
103 | | xpsc1 16044 |
. . . . . . . . . . . . . . 15
⊢ (𝑆 ∈ 𝑊 → (◡({𝑅} +𝑐 {𝑆})‘1𝑜) = 𝑆) |
104 | 5, 103 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (◡({𝑅} +𝑐 {𝑆})‘1𝑜) = 𝑆) |
105 | 104 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (dist‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜)) =
(dist‘𝑆)) |
106 | | xpsc1 16044 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ 𝑌 → (◡({𝐴} +𝑐 {𝐵})‘1𝑜) = 𝐵) |
107 | 28, 106 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (◡({𝐴} +𝑐 {𝐵})‘1𝑜) = 𝐵) |
108 | | xpsc1 16044 |
. . . . . . . . . . . . . 14
⊢ (𝐷 ∈ 𝑌 → (◡({𝐶} +𝑐 {𝐷})‘1𝑜) = 𝐷) |
109 | 41, 108 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (◡({𝐶} +𝑐 {𝐷})‘1𝑜) = 𝐷) |
110 | 105, 107,
109 | oveq123d 6570 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((◡({𝐴} +𝑐 {𝐵})‘1𝑜)(dist‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜))(◡({𝐶} +𝑐 {𝐷})‘1𝑜)) = (𝐵(dist‘𝑆)𝐷)) |
111 | 19 | oveqi 6562 |
. . . . . . . . . . . . 13
⊢ (𝐵𝑁𝐷) = (𝐵((dist‘𝑆) ↾ (𝑌 × 𝑌))𝐷) |
112 | 28, 41 | ovresd 6699 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐵((dist‘𝑆) ↾ (𝑌 × 𝑌))𝐷) = (𝐵(dist‘𝑆)𝐷)) |
113 | 111, 112 | syl5eq 2656 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵𝑁𝐷) = (𝐵(dist‘𝑆)𝐷)) |
114 | 110, 113 | eqtr4d 2647 |
. . . . . . . . . . 11
⊢ (𝜑 → ((◡({𝐴} +𝑐 {𝐵})‘1𝑜)(dist‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜))(◡({𝐶} +𝑐 {𝐷})‘1𝑜)) = (𝐵𝑁𝐷)) |
115 | 114 | eqeq2d 2620 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘1𝑜)(dist‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜))(◡({𝐶} +𝑐 {𝐷})‘1𝑜)) ↔ 𝑥 = (𝐵𝑁𝐷))) |
116 | 102, 115 | orbi12d 742 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘∅)(dist‘(◡({𝑅} +𝑐 {𝑆})‘∅))(◡({𝐶} +𝑐 {𝐷})‘∅)) ∨ 𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘1𝑜)(dist‘(◡({𝑅} +𝑐 {𝑆})‘1𝑜))(◡({𝐶} +𝑐 {𝐷})‘1𝑜))) ↔ (𝑥 = (𝐴𝑀𝐶) ∨ 𝑥 = (𝐵𝑁𝐷)))) |
117 | 89, 116 | syl5bb 271 |
. . . . . . . 8
⊢ (𝜑 → (∃𝑘 ∈ 2𝑜 𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)) ↔ (𝑥 = (𝐴𝑀𝐶) ∨ 𝑥 = (𝐵𝑁𝐷)))) |
118 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
119 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑘 ∈ 2𝑜
↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))) = (𝑘 ∈ 2𝑜 ↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))) |
120 | 119 | elrnmpt 5293 |
. . . . . . . . 9
⊢ (𝑥 ∈ V → (𝑥 ∈ ran (𝑘 ∈ 2𝑜 ↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))) ↔ ∃𝑘 ∈ 2𝑜 𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘)))) |
121 | 118, 120 | ax-mp 5 |
. . . . . . . 8
⊢ (𝑥 ∈ ran (𝑘 ∈ 2𝑜 ↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))) ↔ ∃𝑘 ∈ 2𝑜 𝑥 = ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))) |
122 | 118 | elpr 4146 |
. . . . . . . 8
⊢ (𝑥 ∈ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ↔ (𝑥 = (𝐴𝑀𝐶) ∨ 𝑥 = (𝐵𝑁𝐷))) |
123 | 117, 121,
122 | 3bitr4g 302 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ ran (𝑘 ∈ 2𝑜 ↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))) ↔ 𝑥 ∈ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)})) |
124 | 123 | eqrdv 2608 |
. . . . . 6
⊢ (𝜑 → ran (𝑘 ∈ 2𝑜 ↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))) = {(𝐴𝑀𝐶), (𝐵𝑁𝐷)}) |
125 | 124 | uneq1d 3728 |
. . . . 5
⊢ (𝜑 → (ran (𝑘 ∈ 2𝑜 ↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))) ∪ {0}) = ({(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ∪ {0})) |
126 | | uncom 3719 |
. . . . 5
⊢ ({(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ∪ {0}) = ({0} ∪ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)}) |
127 | 125, 126 | syl6eq 2660 |
. . . 4
⊢ (𝜑 → (ran (𝑘 ∈ 2𝑜 ↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))) ∪ {0}) = ({0} ∪ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)})) |
128 | 127 | supeq1d 8235 |
. . 3
⊢ (𝜑 → sup((ran (𝑘 ∈ 2𝑜
↦ ((◡({𝐴} +𝑐 {𝐵})‘𝑘)(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))(◡({𝐶} +𝑐 {𝐷})‘𝑘))) ∪ {0}), ℝ*, < ) =
sup(({0} ∪ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)}), ℝ*, <
)) |
129 | | 0xr 9965 |
. . . . . 6
⊢ 0 ∈
ℝ* |
130 | 129 | a1i 11 |
. . . . 5
⊢ (𝜑 → 0 ∈
ℝ*) |
131 | 130 | snssd 4281 |
. . . 4
⊢ (𝜑 → {0} ⊆
ℝ*) |
132 | | xmetcl 21946 |
. . . . . 6
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (𝐴𝑀𝐶) ∈
ℝ*) |
133 | 20, 27, 40, 132 | syl3anc 1318 |
. . . . 5
⊢ (𝜑 → (𝐴𝑀𝐶) ∈
ℝ*) |
134 | | xmetcl 21946 |
. . . . . 6
⊢ ((𝑁 ∈ (∞Met‘𝑌) ∧ 𝐵 ∈ 𝑌 ∧ 𝐷 ∈ 𝑌) → (𝐵𝑁𝐷) ∈
ℝ*) |
135 | 21, 28, 41, 134 | syl3anc 1318 |
. . . . 5
⊢ (𝜑 → (𝐵𝑁𝐷) ∈
ℝ*) |
136 | | prssi 4293 |
. . . . 5
⊢ (((𝐴𝑀𝐶) ∈ ℝ* ∧ (𝐵𝑁𝐷) ∈ ℝ*) → {(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ⊆
ℝ*) |
137 | 133, 135,
136 | syl2anc 691 |
. . . 4
⊢ (𝜑 → {(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ⊆
ℝ*) |
138 | | xrltso 11850 |
. . . . . 6
⊢ < Or
ℝ* |
139 | | supsn 8261 |
. . . . . 6
⊢ (( <
Or ℝ* ∧ 0 ∈ ℝ*) → sup({0},
ℝ*, < ) = 0) |
140 | 138, 129,
139 | mp2an 704 |
. . . . 5
⊢ sup({0},
ℝ*, < ) = 0 |
141 | | supxrcl 12017 |
. . . . . . 7
⊢ ({(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ⊆ ℝ* →
sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ) ∈
ℝ*) |
142 | 137, 141 | syl 17 |
. . . . . 6
⊢ (𝜑 → sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ) ∈
ℝ*) |
143 | | xmetge0 21959 |
. . . . . . 7
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → 0 ≤ (𝐴𝑀𝐶)) |
144 | 20, 27, 40, 143 | syl3anc 1318 |
. . . . . 6
⊢ (𝜑 → 0 ≤ (𝐴𝑀𝐶)) |
145 | | ovex 6577 |
. . . . . . . 8
⊢ (𝐴𝑀𝐶) ∈ V |
146 | 145 | prid1 4241 |
. . . . . . 7
⊢ (𝐴𝑀𝐶) ∈ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)} |
147 | | supxrub 12026 |
. . . . . . 7
⊢ (({(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ⊆ ℝ* ∧ (𝐴𝑀𝐶) ∈ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)}) → (𝐴𝑀𝐶) ≤ sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, <
)) |
148 | 137, 146,
147 | sylancl 693 |
. . . . . 6
⊢ (𝜑 → (𝐴𝑀𝐶) ≤ sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, <
)) |
149 | 130, 133,
142, 144, 148 | xrletrd 11869 |
. . . . 5
⊢ (𝜑 → 0 ≤ sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, <
)) |
150 | 140, 149 | syl5eqbr 4618 |
. . . 4
⊢ (𝜑 → sup({0},
ℝ*, < ) ≤ sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, <
)) |
151 | | supxrun 12018 |
. . . 4
⊢ (({0}
⊆ ℝ* ∧ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)} ⊆ ℝ* ∧
sup({0}, ℝ*, < ) ≤ sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < )) →
sup(({0} ∪ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)}), ℝ*, < ) =
sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, <
)) |
152 | 131, 137,
150, 151 | syl3anc 1318 |
. . 3
⊢ (𝜑 → sup(({0} ∪ {(𝐴𝑀𝐶), (𝐵𝑁𝐷)}), ℝ*, < ) =
sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, <
)) |
153 | 70, 128, 152 | 3eqtrd 2648 |
. 2
⊢ (𝜑 → (◡({𝐴} +𝑐 {𝐵})(dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))◡({𝐶} +𝑐 {𝐷})) = sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, <
)) |
154 | 52, 59, 153 | 3eqtr3d 2652 |
1
⊢ (𝜑 → (〈𝐴, 𝐵〉𝑃〈𝐶, 𝐷〉) = sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, <
)) |