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 2610 |
. . 3
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) |
7 | | eqid 2610 |
. . 3
⊢
(Scalar‘𝑅) =
(Scalar‘𝑅) |
8 | | eqid 2610 |
. . 3
⊢
((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})) = ((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | xpsval 16055 |
. 2
⊢ (𝜑 → 𝑇 = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) “s
((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))) |
10 | 1, 2, 3, 4, 5, 6, 7, 8 | xpslem 16056 |
. 2
⊢ (𝜑 → ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) = (Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))) |
11 | 6 | xpsff1o2 16054 |
. . 3
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) |
12 | | f1ocnv 6062 |
. . 3
⊢ ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):(𝑋 × 𝑌)–1-1-onto→ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))–1-1-onto→(𝑋 × 𝑌)) |
13 | 11, 12 | mp1i 13 |
. 2
⊢ (𝜑 → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))–1-1-onto→(𝑋 × 𝑌)) |
14 | | ovex 6577 |
. . 3
⊢
((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})) ∈ V |
15 | 14 | a1i 11 |
. 2
⊢ (𝜑 → ((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})) ∈ V) |
16 | | eqid 2610 |
. 2
⊢
((dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ↾ (ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) × ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))) = ((dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ↾ (ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) × ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))) |
17 | | xpsds.p |
. 2
⊢ 𝑃 = (dist‘𝑇) |
18 | | eqid 2610 |
. . . . 5
⊢
((Scalar‘𝑅)Xs(𝑘 ∈ 2𝑜 ↦ (◡({𝑅} +𝑐 {𝑆})‘𝑘))) = ((Scalar‘𝑅)Xs(𝑘 ∈ 2𝑜 ↦ (◡({𝑅} +𝑐 {𝑆})‘𝑘))) |
19 | | eqid 2610 |
. . . . 5
⊢
(Base‘((Scalar‘𝑅)Xs(𝑘 ∈ 2𝑜 ↦ (◡({𝑅} +𝑐 {𝑆})‘𝑘)))) = (Base‘((Scalar‘𝑅)Xs(𝑘 ∈ 2𝑜 ↦ (◡({𝑅} +𝑐 {𝑆})‘𝑘)))) |
20 | | eqid 2610 |
. . . . 5
⊢
(Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) = (Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) |
21 | | eqid 2610 |
. . . . 5
⊢
((dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) ↾ ((Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) × (Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)))) = ((dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) ↾ ((Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) × (Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)))) |
22 | | eqid 2610 |
. . . . 5
⊢
(dist‘((Scalar‘𝑅)Xs(𝑘 ∈ 2𝑜 ↦ (◡({𝑅} +𝑐 {𝑆})‘𝑘)))) = (dist‘((Scalar‘𝑅)Xs(𝑘 ∈ 2𝑜 ↦ (◡({𝑅} +𝑐 {𝑆})‘𝑘)))) |
23 | | fvex 6113 |
. . . . . 6
⊢
(Scalar‘𝑅)
∈ V |
24 | 23 | a1i 11 |
. . . . 5
⊢ (𝜑 → (Scalar‘𝑅) ∈ V) |
25 | | 2onn 7607 |
. . . . . 6
⊢
2𝑜 ∈ ω |
26 | | nnfi 8038 |
. . . . . 6
⊢
(2𝑜 ∈ ω → 2𝑜
∈ Fin) |
27 | 25, 26 | mp1i 13 |
. . . . 5
⊢ (𝜑 → 2𝑜
∈ Fin) |
28 | | fvex 6113 |
. . . . . 6
⊢ (◡({𝑅} +𝑐 {𝑆})‘𝑘) ∈ V |
29 | 28 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → (◡({𝑅} +𝑐 {𝑆})‘𝑘) ∈ V) |
30 | | elpri 4145 |
. . . . . . 7
⊢ (𝑘 ∈ {∅,
1𝑜} → (𝑘 = ∅ ∨ 𝑘 = 1𝑜)) |
31 | | df2o3 7460 |
. . . . . . 7
⊢
2𝑜 = {∅,
1𝑜} |
32 | 30, 31 | eleq2s 2706 |
. . . . . 6
⊢ (𝑘 ∈ 2𝑜
→ (𝑘 = ∅ ∨
𝑘 =
1𝑜)) |
33 | | xpsmet.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ (Met‘𝑋)) |
34 | 33 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 = ∅) → 𝑀 ∈ (Met‘𝑋)) |
35 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑘 = ∅ → (◡({𝑅} +𝑐 {𝑆})‘𝑘) = (◡({𝑅} +𝑐 {𝑆})‘∅)) |
36 | | xpsc0 16043 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ 𝑉 → (◡({𝑅} +𝑐 {𝑆})‘∅) = 𝑅) |
37 | 4, 36 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (◡({𝑅} +𝑐 {𝑆})‘∅) = 𝑅) |
38 | 35, 37 | sylan9eqr 2666 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 = ∅) → (◡({𝑅} +𝑐 {𝑆})‘𝑘) = 𝑅) |
39 | 38 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 = ∅) → (dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) = (dist‘𝑅)) |
40 | 38 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 = ∅) → (Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) = (Base‘𝑅)) |
41 | 40, 2 | syl6eqr 2662 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 = ∅) → (Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) = 𝑋) |
42 | 41 | sqxpeqd 5065 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 = ∅) → ((Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) × (Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))) = (𝑋 × 𝑋)) |
43 | 39, 42 | reseq12d 5318 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 = ∅) → ((dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) ↾ ((Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) × (Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)))) = ((dist‘𝑅) ↾ (𝑋 × 𝑋))) |
44 | | xpsds.m |
. . . . . . . . 9
⊢ 𝑀 = ((dist‘𝑅) ↾ (𝑋 × 𝑋)) |
45 | 43, 44 | syl6eqr 2662 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 = ∅) → ((dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) ↾ ((Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) × (Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)))) = 𝑀) |
46 | 41 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 = ∅) →
(Met‘(Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))) = (Met‘𝑋)) |
47 | 34, 45, 46 | 3eltr4d 2703 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 = ∅) → ((dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) ↾ ((Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) × (Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)))) ∈ (Met‘(Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)))) |
48 | | xpsmet.4 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ (Met‘𝑌)) |
49 | 48 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 = 1𝑜) → 𝑁 ∈ (Met‘𝑌)) |
50 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑘 = 1𝑜 →
(◡({𝑅} +𝑐 {𝑆})‘𝑘) = (◡({𝑅} +𝑐 {𝑆})‘1𝑜)) |
51 | | xpsc1 16044 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ 𝑊 → (◡({𝑅} +𝑐 {𝑆})‘1𝑜) = 𝑆) |
52 | 5, 51 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (◡({𝑅} +𝑐 {𝑆})‘1𝑜) = 𝑆) |
53 | 50, 52 | sylan9eqr 2666 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 = 1𝑜) → (◡({𝑅} +𝑐 {𝑆})‘𝑘) = 𝑆) |
54 | 53 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 = 1𝑜) →
(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) = (dist‘𝑆)) |
55 | 53 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 = 1𝑜) →
(Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) = (Base‘𝑆)) |
56 | 55, 3 | syl6eqr 2662 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 = 1𝑜) →
(Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) = 𝑌) |
57 | 56 | sqxpeqd 5065 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 = 1𝑜) →
((Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) × (Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))) = (𝑌 × 𝑌)) |
58 | 54, 57 | reseq12d 5318 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 = 1𝑜) →
((dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) ↾ ((Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) × (Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)))) = ((dist‘𝑆) ↾ (𝑌 × 𝑌))) |
59 | | xpsds.n |
. . . . . . . . 9
⊢ 𝑁 = ((dist‘𝑆) ↾ (𝑌 × 𝑌)) |
60 | 58, 59 | syl6eqr 2662 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 = 1𝑜) →
((dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) ↾ ((Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) × (Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)))) = 𝑁) |
61 | 56 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 = 1𝑜) →
(Met‘(Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))) = (Met‘𝑌)) |
62 | 49, 60, 61 | 3eltr4d 2703 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 = 1𝑜) →
((dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) ↾ ((Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) × (Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)))) ∈ (Met‘(Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)))) |
63 | 47, 62 | jaodan 822 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑘 = ∅ ∨ 𝑘 = 1𝑜)) →
((dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) ↾ ((Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) × (Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)))) ∈ (Met‘(Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)))) |
64 | 32, 63 | sylan2 490 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) →
((dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) ↾ ((Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) × (Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)))) ∈ (Met‘(Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)))) |
65 | 18, 19, 20, 21, 22, 24, 27, 29, 64 | prdsmet 21985 |
. . . 4
⊢ (𝜑 →
(dist‘((Scalar‘𝑅)Xs(𝑘 ∈ 2𝑜 ↦ (◡({𝑅} +𝑐 {𝑆})‘𝑘)))) ∈
(Met‘(Base‘((Scalar‘𝑅)Xs(𝑘 ∈ 2𝑜 ↦ (◡({𝑅} +𝑐 {𝑆})‘𝑘)))))) |
66 | | xpscfn 16042 |
. . . . . . . 8
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → ◡({𝑅} +𝑐 {𝑆}) Fn
2𝑜) |
67 | 4, 5, 66 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → ◡({𝑅} +𝑐 {𝑆}) Fn
2𝑜) |
68 | | dffn5 6151 |
. . . . . . 7
⊢ (◡({𝑅} +𝑐 {𝑆}) Fn 2𝑜 ↔ ◡({𝑅} +𝑐 {𝑆}) = (𝑘 ∈ 2𝑜 ↦ (◡({𝑅} +𝑐 {𝑆})‘𝑘))) |
69 | 67, 68 | sylib 207 |
. . . . . 6
⊢ (𝜑 → ◡({𝑅} +𝑐 {𝑆}) = (𝑘 ∈ 2𝑜 ↦ (◡({𝑅} +𝑐 {𝑆})‘𝑘))) |
70 | 69 | oveq2d 6565 |
. . . . 5
⊢ (𝜑 → ((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})) = ((Scalar‘𝑅)Xs(𝑘 ∈ 2𝑜 ↦ (◡({𝑅} +𝑐 {𝑆})‘𝑘)))) |
71 | 70 | fveq2d 6107 |
. . . 4
⊢ (𝜑 →
(dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) = (dist‘((Scalar‘𝑅)Xs(𝑘 ∈ 2𝑜 ↦ (◡({𝑅} +𝑐 {𝑆})‘𝑘))))) |
72 | 70 | fveq2d 6107 |
. . . . . 6
⊢ (𝜑 →
(Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) = (Base‘((Scalar‘𝑅)Xs(𝑘 ∈ 2𝑜 ↦ (◡({𝑅} +𝑐 {𝑆})‘𝑘))))) |
73 | 10, 72 | eqtrd 2644 |
. . . . 5
⊢ (𝜑 → ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) = (Base‘((Scalar‘𝑅)Xs(𝑘 ∈ 2𝑜 ↦ (◡({𝑅} +𝑐 {𝑆})‘𝑘))))) |
74 | 73 | fveq2d 6107 |
. . . 4
⊢ (𝜑 → (Met‘ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) =
(Met‘(Base‘((Scalar‘𝑅)Xs(𝑘 ∈ 2𝑜 ↦ (◡({𝑅} +𝑐 {𝑆})‘𝑘)))))) |
75 | 65, 71, 74 | 3eltr4d 2703 |
. . 3
⊢ (𝜑 →
(dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ∈ (Met‘ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))) |
76 | | ssid 3587 |
. . 3
⊢ ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) ⊆ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) |
77 | | metres2 21978 |
. . 3
⊢
(((dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ∈ (Met‘ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) ∧ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) ⊆ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) → ((dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ↾ (ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) × ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))) ∈ (Met‘ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))) |
78 | 75, 76, 77 | sylancl 693 |
. 2
⊢ (𝜑 →
((dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ↾ (ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) × ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))) ∈ (Met‘ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))) |
79 | 9, 10, 13, 15, 16, 17, 78 | imasf1omet 21991 |
1
⊢ (𝜑 → 𝑃 ∈ (Met‘(𝑋 × 𝑌))) |