Step | Hyp | Ref
| Expression |
1 | | xpsds.t |
. . 3
⊢ 𝑇 = (𝑅 ×s 𝑆) |
2 | | xpsds.x |
. . 3
⊢ 𝑋 = (Base‘𝑅) |
3 | | xpsds.y |
. . 3
⊢ 𝑌 = (Base‘𝑆) |
4 | | xpsds.1 |
. . 3
⊢ (𝜑 → 𝑅 ∈ 𝑉) |
5 | | xpsds.2 |
. . 3
⊢ (𝜑 → 𝑆 ∈ 𝑊) |
6 | | eqid 2825 |
. . 3
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) |
7 | | eqid 2825 |
. . 3
⊢
(Scalar‘𝑅) =
(Scalar‘𝑅) |
8 | | eqid 2825 |
. . 3
⊢
((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})) = ((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | xpsval 16592 |
. 2
⊢ (𝜑 → 𝑇 = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) “s
((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))) |
10 | 1, 2, 3, 4, 5, 6, 7, 8 | xpslem 16593 |
. 2
⊢ (𝜑 → ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) = (Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))) |
11 | 6 | xpsff1o2 16591 |
. . 3
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) |
12 | | f1ocnv 6394 |
. . 3
⊢ ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))–1-1-onto→(𝑋 × 𝑌)) |
13 | 11, 12 | mp1i 13 |
. 2
⊢ (𝜑 → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))–1-1-onto→(𝑋 × 𝑌)) |
14 | | ovexd 6944 |
. 2
⊢ (𝜑 → ((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})) ∈ V) |
15 | | eqid 2825 |
. 2
⊢
((dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ↾ (ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) × ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))) = ((dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ↾ (ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) × ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))) |
16 | | xpsds.p |
. 2
⊢ 𝑃 = (dist‘𝑇) |
17 | | eqid 2825 |
. . . . 5
⊢
((Scalar‘𝑅)Xs(𝑘 ∈ 2o ↦ (◡({𝑅} +𝑐 {𝑆})‘𝑘))) = ((Scalar‘𝑅)Xs(𝑘 ∈ 2o ↦ (◡({𝑅} +𝑐 {𝑆})‘𝑘))) |
18 | | eqid 2825 |
. . . . 5
⊢
(Base‘((Scalar‘𝑅)Xs(𝑘 ∈ 2o ↦ (◡({𝑅} +𝑐 {𝑆})‘𝑘)))) = (Base‘((Scalar‘𝑅)Xs(𝑘 ∈ 2o ↦ (◡({𝑅} +𝑐 {𝑆})‘𝑘)))) |
19 | | eqid 2825 |
. . . . 5
⊢
(Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) = (Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) |
20 | | eqid 2825 |
. . . . 5
⊢
((dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) ↾ ((Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) × (Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)))) = ((dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) ↾ ((Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) × (Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)))) |
21 | | eqid 2825 |
. . . . 5
⊢
(dist‘((Scalar‘𝑅)Xs(𝑘 ∈ 2o ↦ (◡({𝑅} +𝑐 {𝑆})‘𝑘)))) = (dist‘((Scalar‘𝑅)Xs(𝑘 ∈ 2o ↦ (◡({𝑅} +𝑐 {𝑆})‘𝑘)))) |
22 | | fvexd 6452 |
. . . . 5
⊢ (𝜑 → (Scalar‘𝑅) ∈ V) |
23 | | 2onn 7992 |
. . . . . 6
⊢
2o ∈ ω |
24 | | nnfi 8428 |
. . . . . 6
⊢
(2o ∈ ω → 2o ∈
Fin) |
25 | 23, 24 | mp1i 13 |
. . . . 5
⊢ (𝜑 → 2o ∈
Fin) |
26 | | fvexd 6452 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 2o) → (◡({𝑅} +𝑐 {𝑆})‘𝑘) ∈ V) |
27 | | elpri 4421 |
. . . . . . 7
⊢ (𝑘 ∈ {∅, 1o}
→ (𝑘 = ∅ ∨
𝑘 =
1o)) |
28 | | df2o3 7845 |
. . . . . . 7
⊢
2o = {∅, 1o} |
29 | 27, 28 | eleq2s 2924 |
. . . . . 6
⊢ (𝑘 ∈ 2o →
(𝑘 = ∅ ∨ 𝑘 =
1o)) |
30 | | xpsmet.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ (Met‘𝑋)) |
31 | 30 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 = ∅) → 𝑀 ∈ (Met‘𝑋)) |
32 | | fveq2 6437 |
. . . . . . . . . . . 12
⊢ (𝑘 = ∅ → (◡({𝑅} +𝑐 {𝑆})‘𝑘) = (◡({𝑅} +𝑐 {𝑆})‘∅)) |
33 | | xpsc0 16580 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ 𝑉 → (◡({𝑅} +𝑐 {𝑆})‘∅) = 𝑅) |
34 | 4, 33 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (◡({𝑅} +𝑐 {𝑆})‘∅) = 𝑅) |
35 | 32, 34 | sylan9eqr 2883 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 = ∅) → (◡({𝑅} +𝑐 {𝑆})‘𝑘) = 𝑅) |
36 | 35 | fveq2d 6441 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 = ∅) → (dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) = (dist‘𝑅)) |
37 | 35 | fveq2d 6441 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 = ∅) → (Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) = (Base‘𝑅)) |
38 | 37, 2 | syl6eqr 2879 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 = ∅) → (Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) = 𝑋) |
39 | 38 | sqxpeqd 5378 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 = ∅) → ((Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) × (Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))) = (𝑋 × 𝑋)) |
40 | 36, 39 | reseq12d 5634 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 = ∅) → ((dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) ↾ ((Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) × (Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)))) = ((dist‘𝑅) ↾ (𝑋 × 𝑋))) |
41 | | xpsds.m |
. . . . . . . . 9
⊢ 𝑀 = ((dist‘𝑅) ↾ (𝑋 × 𝑋)) |
42 | 40, 41 | syl6eqr 2879 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 = ∅) → ((dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) ↾ ((Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) × (Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)))) = 𝑀) |
43 | 38 | fveq2d 6441 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 = ∅) →
(Met‘(Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))) = (Met‘𝑋)) |
44 | 31, 42, 43 | 3eltr4d 2921 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 = ∅) → ((dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) ↾ ((Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) × (Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)))) ∈ (Met‘(Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)))) |
45 | | xpsmet.4 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ (Met‘𝑌)) |
46 | 45 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 = 1o) → 𝑁 ∈ (Met‘𝑌)) |
47 | | fveq2 6437 |
. . . . . . . . . . . 12
⊢ (𝑘 = 1o → (◡({𝑅} +𝑐 {𝑆})‘𝑘) = (◡({𝑅} +𝑐 {𝑆})‘1o)) |
48 | | xpsc1 16581 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ 𝑊 → (◡({𝑅} +𝑐 {𝑆})‘1o) = 𝑆) |
49 | 5, 48 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (◡({𝑅} +𝑐 {𝑆})‘1o) = 𝑆) |
50 | 47, 49 | sylan9eqr 2883 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 = 1o) → (◡({𝑅} +𝑐 {𝑆})‘𝑘) = 𝑆) |
51 | 50 | fveq2d 6441 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 = 1o) → (dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) = (dist‘𝑆)) |
52 | 50 | fveq2d 6441 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 = 1o) → (Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) = (Base‘𝑆)) |
53 | 52, 3 | syl6eqr 2879 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 = 1o) → (Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) = 𝑌) |
54 | 53 | sqxpeqd 5378 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 = 1o) → ((Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) × (Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))) = (𝑌 × 𝑌)) |
55 | 51, 54 | reseq12d 5634 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 = 1o) → ((dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) ↾ ((Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) × (Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)))) = ((dist‘𝑆) ↾ (𝑌 × 𝑌))) |
56 | | xpsds.n |
. . . . . . . . 9
⊢ 𝑁 = ((dist‘𝑆) ↾ (𝑌 × 𝑌)) |
57 | 55, 56 | syl6eqr 2879 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 = 1o) → ((dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) ↾ ((Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) × (Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)))) = 𝑁) |
58 | 53 | fveq2d 6441 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 = 1o) →
(Met‘(Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))) = (Met‘𝑌)) |
59 | 46, 57, 58 | 3eltr4d 2921 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 = 1o) → ((dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) ↾ ((Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) × (Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)))) ∈ (Met‘(Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)))) |
60 | 44, 59 | jaodan 985 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑘 = ∅ ∨ 𝑘 = 1o)) → ((dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) ↾ ((Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) × (Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)))) ∈ (Met‘(Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)))) |
61 | 29, 60 | sylan2 586 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 2o) →
((dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) ↾ ((Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) × (Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)))) ∈ (Met‘(Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)))) |
62 | 17, 18, 19, 20, 21, 22, 25, 26, 61 | prdsmet 22552 |
. . . 4
⊢ (𝜑 →
(dist‘((Scalar‘𝑅)Xs(𝑘 ∈ 2o ↦ (◡({𝑅} +𝑐 {𝑆})‘𝑘)))) ∈
(Met‘(Base‘((Scalar‘𝑅)Xs(𝑘 ∈ 2o ↦ (◡({𝑅} +𝑐 {𝑆})‘𝑘)))))) |
63 | | xpscfn 16579 |
. . . . . . . 8
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → ◡({𝑅} +𝑐 {𝑆}) Fn 2o) |
64 | 4, 5, 63 | syl2anc 579 |
. . . . . . 7
⊢ (𝜑 → ◡({𝑅} +𝑐 {𝑆}) Fn 2o) |
65 | | dffn5 6492 |
. . . . . . 7
⊢ (◡({𝑅} +𝑐 {𝑆}) Fn 2o ↔ ◡({𝑅} +𝑐 {𝑆}) = (𝑘 ∈ 2o ↦ (◡({𝑅} +𝑐 {𝑆})‘𝑘))) |
66 | 64, 65 | sylib 210 |
. . . . . 6
⊢ (𝜑 → ◡({𝑅} +𝑐 {𝑆}) = (𝑘 ∈ 2o ↦ (◡({𝑅} +𝑐 {𝑆})‘𝑘))) |
67 | 66 | oveq2d 6926 |
. . . . 5
⊢ (𝜑 → ((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})) = ((Scalar‘𝑅)Xs(𝑘 ∈ 2o ↦ (◡({𝑅} +𝑐 {𝑆})‘𝑘)))) |
68 | 67 | fveq2d 6441 |
. . . 4
⊢ (𝜑 →
(dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) = (dist‘((Scalar‘𝑅)Xs(𝑘 ∈ 2o ↦ (◡({𝑅} +𝑐 {𝑆})‘𝑘))))) |
69 | 67 | fveq2d 6441 |
. . . . . 6
⊢ (𝜑 →
(Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) = (Base‘((Scalar‘𝑅)Xs(𝑘 ∈ 2o ↦ (◡({𝑅} +𝑐 {𝑆})‘𝑘))))) |
70 | 10, 69 | eqtrd 2861 |
. . . . 5
⊢ (𝜑 → ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) = (Base‘((Scalar‘𝑅)Xs(𝑘 ∈ 2o ↦ (◡({𝑅} +𝑐 {𝑆})‘𝑘))))) |
71 | 70 | fveq2d 6441 |
. . . 4
⊢ (𝜑 → (Met‘ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) =
(Met‘(Base‘((Scalar‘𝑅)Xs(𝑘 ∈ 2o ↦ (◡({𝑅} +𝑐 {𝑆})‘𝑘)))))) |
72 | 62, 68, 71 | 3eltr4d 2921 |
. . 3
⊢ (𝜑 →
(dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ∈ (Met‘ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))) |
73 | | ssid 3848 |
. . 3
⊢ ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) ⊆ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) |
74 | | metres2 22545 |
. . 3
⊢
(((dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ∈ (Met‘ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) ∧ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) ⊆ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) → ((dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ↾ (ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) × ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))) ∈ (Met‘ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))) |
75 | 72, 73, 74 | sylancl 580 |
. 2
⊢ (𝜑 →
((dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ↾ (ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) × ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))) ∈ (Met‘ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))) |
76 | 9, 10, 13, 14, 15, 16, 75 | imasf1omet 22558 |
1
⊢ (𝜑 → 𝑃 ∈ (Met‘(𝑋 × 𝑌))) |