| 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 2737 |
. . 3
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) |
| 7 | | eqid 2737 |
. . 3
⊢
(Scalar‘𝑅) =
(Scalar‘𝑅) |
| 8 | | eqid 2737 |
. . 3
⊢
((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉}) = ((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉}) |
| 9 | 1, 2, 3, 4, 5, 6, 7, 8 | xpsval 17615 |
. 2
⊢ (𝜑 → 𝑇 = (◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})
“s ((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉}))) |
| 10 | 1, 2, 3, 4, 5, 6, 7, 8 | xpsrnbas 17616 |
. 2
⊢ (𝜑 → ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) =
(Base‘((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉}))) |
| 11 | 6 | xpsff1o2 17614 |
. . 3
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}):(𝑋 × 𝑌)–1-1-onto→ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) |
| 12 | | f1ocnv 6860 |
. . 3
⊢ ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}):(𝑋 × 𝑌)–1-1-onto→ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})–1-1-onto→(𝑋 × 𝑌)) |
| 13 | 11, 12 | mp1i 13 |
. 2
⊢ (𝜑 → ◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}):ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})–1-1-onto→(𝑋 × 𝑌)) |
| 14 | | ovexd 7466 |
. 2
⊢ (𝜑 → ((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉}) ∈
V) |
| 15 | | eqid 2737 |
. 2
⊢
((dist‘((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉})) ↾ (ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) × ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}))) =
((dist‘((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉})) ↾ (ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) × ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}))) |
| 16 | | xpsds.p |
. 2
⊢ 𝑃 = (dist‘𝑇) |
| 17 | | eqid 2737 |
. . . . 5
⊢
((Scalar‘𝑅)Xs(𝑘 ∈ 2o ↦
({〈∅, 𝑅〉,
〈1o, 𝑆〉}‘𝑘))) = ((Scalar‘𝑅)Xs(𝑘 ∈ 2o ↦
({〈∅, 𝑅〉,
〈1o, 𝑆〉}‘𝑘))) |
| 18 | | eqid 2737 |
. . . . 5
⊢
(Base‘((Scalar‘𝑅)Xs(𝑘 ∈ 2o ↦
({〈∅, 𝑅〉,
〈1o, 𝑆〉}‘𝑘)))) = (Base‘((Scalar‘𝑅)Xs(𝑘 ∈ 2o ↦
({〈∅, 𝑅〉,
〈1o, 𝑆〉}‘𝑘)))) |
| 19 | | eqid 2737 |
. . . . 5
⊢
(Base‘({〈∅, 𝑅〉, 〈1o, 𝑆〉}‘𝑘)) = (Base‘({〈∅, 𝑅〉, 〈1o,
𝑆〉}‘𝑘)) |
| 20 | | eqid 2737 |
. . . . 5
⊢
((dist‘({〈∅, 𝑅〉, 〈1o, 𝑆〉}‘𝑘)) ↾ ((Base‘({〈∅,
𝑅〉,
〈1o, 𝑆〉}‘𝑘)) × (Base‘({〈∅, 𝑅〉, 〈1o,
𝑆〉}‘𝑘)))) =
((dist‘({〈∅, 𝑅〉, 〈1o, 𝑆〉}‘𝑘)) ↾ ((Base‘({〈∅,
𝑅〉,
〈1o, 𝑆〉}‘𝑘)) × (Base‘({〈∅, 𝑅〉, 〈1o,
𝑆〉}‘𝑘)))) |
| 21 | | eqid 2737 |
. . . . 5
⊢
(dist‘((Scalar‘𝑅)Xs(𝑘 ∈ 2o ↦
({〈∅, 𝑅〉,
〈1o, 𝑆〉}‘𝑘)))) = (dist‘((Scalar‘𝑅)Xs(𝑘 ∈ 2o ↦
({〈∅, 𝑅〉,
〈1o, 𝑆〉}‘𝑘)))) |
| 22 | | fvexd 6921 |
. . . . 5
⊢ (𝜑 → (Scalar‘𝑅) ∈ V) |
| 23 | | 2onn 8680 |
. . . . . 6
⊢
2o ∈ ω |
| 24 | | nnfi 9207 |
. . . . . 6
⊢
(2o ∈ ω → 2o ∈
Fin) |
| 25 | 23, 24 | mp1i 13 |
. . . . 5
⊢ (𝜑 → 2o ∈
Fin) |
| 26 | | fvexd 6921 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 2o) →
({〈∅, 𝑅〉,
〈1o, 𝑆〉}‘𝑘) ∈ V) |
| 27 | | elpri 4649 |
. . . . . . 7
⊢ (𝑘 ∈ {∅, 1o}
→ (𝑘 = ∅ ∨
𝑘 =
1o)) |
| 28 | | df2o3 8514 |
. . . . . . 7
⊢
2o = {∅, 1o} |
| 29 | 27, 28 | eleq2s 2859 |
. . . . . 6
⊢ (𝑘 ∈ 2o →
(𝑘 = ∅ ∨ 𝑘 =
1o)) |
| 30 | | xpsmet.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ (Met‘𝑋)) |
| 31 | 30 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 = ∅) → 𝑀 ∈ (Met‘𝑋)) |
| 32 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑘 = ∅ →
({〈∅, 𝑅〉,
〈1o, 𝑆〉}‘𝑘) = ({〈∅, 𝑅〉, 〈1o, 𝑆〉}‘∅)) |
| 33 | | fvpr0o 17604 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ 𝑉 → ({〈∅, 𝑅〉, 〈1o, 𝑆〉}‘∅) = 𝑅) |
| 34 | 4, 33 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ({〈∅, 𝑅〉, 〈1o,
𝑆〉}‘∅) =
𝑅) |
| 35 | 32, 34 | sylan9eqr 2799 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 = ∅) → ({〈∅, 𝑅〉, 〈1o,
𝑆〉}‘𝑘) = 𝑅) |
| 36 | 35 | fveq2d 6910 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 = ∅) →
(dist‘({〈∅, 𝑅〉, 〈1o, 𝑆〉}‘𝑘)) = (dist‘𝑅)) |
| 37 | 35 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 = ∅) →
(Base‘({〈∅, 𝑅〉, 〈1o, 𝑆〉}‘𝑘)) = (Base‘𝑅)) |
| 38 | 37, 2 | eqtr4di 2795 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 = ∅) →
(Base‘({〈∅, 𝑅〉, 〈1o, 𝑆〉}‘𝑘)) = 𝑋) |
| 39 | 38 | sqxpeqd 5717 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 = ∅) →
((Base‘({〈∅, 𝑅〉, 〈1o, 𝑆〉}‘𝑘)) × (Base‘({〈∅, 𝑅〉, 〈1o,
𝑆〉}‘𝑘))) = (𝑋 × 𝑋)) |
| 40 | 36, 39 | reseq12d 5998 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 = ∅) →
((dist‘({〈∅, 𝑅〉, 〈1o, 𝑆〉}‘𝑘)) ↾ ((Base‘({〈∅,
𝑅〉,
〈1o, 𝑆〉}‘𝑘)) × (Base‘({〈∅, 𝑅〉, 〈1o,
𝑆〉}‘𝑘)))) = ((dist‘𝑅) ↾ (𝑋 × 𝑋))) |
| 41 | | xpsds.m |
. . . . . . . . 9
⊢ 𝑀 = ((dist‘𝑅) ↾ (𝑋 × 𝑋)) |
| 42 | 40, 41 | eqtr4di 2795 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 = ∅) →
((dist‘({〈∅, 𝑅〉, 〈1o, 𝑆〉}‘𝑘)) ↾ ((Base‘({〈∅,
𝑅〉,
〈1o, 𝑆〉}‘𝑘)) × (Base‘({〈∅, 𝑅〉, 〈1o,
𝑆〉}‘𝑘)))) = 𝑀) |
| 43 | 38 | fveq2d 6910 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 = ∅) →
(Met‘(Base‘({〈∅, 𝑅〉, 〈1o, 𝑆〉}‘𝑘))) = (Met‘𝑋)) |
| 44 | 31, 42, 43 | 3eltr4d 2856 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 = ∅) →
((dist‘({〈∅, 𝑅〉, 〈1o, 𝑆〉}‘𝑘)) ↾ ((Base‘({〈∅,
𝑅〉,
〈1o, 𝑆〉}‘𝑘)) × (Base‘({〈∅, 𝑅〉, 〈1o,
𝑆〉}‘𝑘)))) ∈
(Met‘(Base‘({〈∅, 𝑅〉, 〈1o, 𝑆〉}‘𝑘)))) |
| 45 | | xpsmet.4 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ (Met‘𝑌)) |
| 46 | 45 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 = 1o) → 𝑁 ∈ (Met‘𝑌)) |
| 47 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑘 = 1o →
({〈∅, 𝑅〉,
〈1o, 𝑆〉}‘𝑘) = ({〈∅, 𝑅〉, 〈1o, 𝑆〉}‘1o)) |
| 48 | | fvpr1o 17605 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ 𝑊 → ({〈∅, 𝑅〉, 〈1o, 𝑆〉}‘1o) =
𝑆) |
| 49 | 5, 48 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ({〈∅, 𝑅〉, 〈1o,
𝑆〉}‘1o) = 𝑆) |
| 50 | 47, 49 | sylan9eqr 2799 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 = 1o) → ({〈∅,
𝑅〉,
〈1o, 𝑆〉}‘𝑘) = 𝑆) |
| 51 | 50 | fveq2d 6910 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 = 1o) →
(dist‘({〈∅, 𝑅〉, 〈1o, 𝑆〉}‘𝑘)) = (dist‘𝑆)) |
| 52 | 50 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 = 1o) →
(Base‘({〈∅, 𝑅〉, 〈1o, 𝑆〉}‘𝑘)) = (Base‘𝑆)) |
| 53 | 52, 3 | eqtr4di 2795 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 = 1o) →
(Base‘({〈∅, 𝑅〉, 〈1o, 𝑆〉}‘𝑘)) = 𝑌) |
| 54 | 53 | sqxpeqd 5717 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 = 1o) →
((Base‘({〈∅, 𝑅〉, 〈1o, 𝑆〉}‘𝑘)) × (Base‘({〈∅, 𝑅〉, 〈1o,
𝑆〉}‘𝑘))) = (𝑌 × 𝑌)) |
| 55 | 51, 54 | reseq12d 5998 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 = 1o) →
((dist‘({〈∅, 𝑅〉, 〈1o, 𝑆〉}‘𝑘)) ↾ ((Base‘({〈∅,
𝑅〉,
〈1o, 𝑆〉}‘𝑘)) × (Base‘({〈∅, 𝑅〉, 〈1o,
𝑆〉}‘𝑘)))) = ((dist‘𝑆) ↾ (𝑌 × 𝑌))) |
| 56 | | xpsds.n |
. . . . . . . . 9
⊢ 𝑁 = ((dist‘𝑆) ↾ (𝑌 × 𝑌)) |
| 57 | 55, 56 | eqtr4di 2795 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 = 1o) →
((dist‘({〈∅, 𝑅〉, 〈1o, 𝑆〉}‘𝑘)) ↾ ((Base‘({〈∅,
𝑅〉,
〈1o, 𝑆〉}‘𝑘)) × (Base‘({〈∅, 𝑅〉, 〈1o,
𝑆〉}‘𝑘)))) = 𝑁) |
| 58 | 53 | fveq2d 6910 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 = 1o) →
(Met‘(Base‘({〈∅, 𝑅〉, 〈1o, 𝑆〉}‘𝑘))) = (Met‘𝑌)) |
| 59 | 46, 57, 58 | 3eltr4d 2856 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 = 1o) →
((dist‘({〈∅, 𝑅〉, 〈1o, 𝑆〉}‘𝑘)) ↾ ((Base‘({〈∅,
𝑅〉,
〈1o, 𝑆〉}‘𝑘)) × (Base‘({〈∅, 𝑅〉, 〈1o,
𝑆〉}‘𝑘)))) ∈
(Met‘(Base‘({〈∅, 𝑅〉, 〈1o, 𝑆〉}‘𝑘)))) |
| 60 | 44, 59 | jaodan 960 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑘 = ∅ ∨ 𝑘 = 1o)) →
((dist‘({〈∅, 𝑅〉, 〈1o, 𝑆〉}‘𝑘)) ↾ ((Base‘({〈∅,
𝑅〉,
〈1o, 𝑆〉}‘𝑘)) × (Base‘({〈∅, 𝑅〉, 〈1o,
𝑆〉}‘𝑘)))) ∈
(Met‘(Base‘({〈∅, 𝑅〉, 〈1o, 𝑆〉}‘𝑘)))) |
| 61 | 29, 60 | sylan2 593 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 2o) →
((dist‘({〈∅, 𝑅〉, 〈1o, 𝑆〉}‘𝑘)) ↾ ((Base‘({〈∅,
𝑅〉,
〈1o, 𝑆〉}‘𝑘)) × (Base‘({〈∅, 𝑅〉, 〈1o,
𝑆〉}‘𝑘)))) ∈
(Met‘(Base‘({〈∅, 𝑅〉, 〈1o, 𝑆〉}‘𝑘)))) |
| 62 | 17, 18, 19, 20, 21, 22, 25, 26, 61 | prdsmet 24380 |
. . . 4
⊢ (𝜑 →
(dist‘((Scalar‘𝑅)Xs(𝑘 ∈ 2o ↦
({〈∅, 𝑅〉,
〈1o, 𝑆〉}‘𝑘)))) ∈
(Met‘(Base‘((Scalar‘𝑅)Xs(𝑘 ∈ 2o ↦
({〈∅, 𝑅〉,
〈1o, 𝑆〉}‘𝑘)))))) |
| 63 | | fnpr2o 17602 |
. . . . . . . 8
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → {〈∅, 𝑅〉, 〈1o, 𝑆〉} Fn
2o) |
| 64 | 4, 5, 63 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → {〈∅, 𝑅〉, 〈1o,
𝑆〉} Fn
2o) |
| 65 | | dffn5 6967 |
. . . . . . 7
⊢
({〈∅, 𝑅〉, 〈1o, 𝑆〉} Fn 2o ↔
{〈∅, 𝑅〉,
〈1o, 𝑆〉} = (𝑘 ∈ 2o ↦
({〈∅, 𝑅〉,
〈1o, 𝑆〉}‘𝑘))) |
| 66 | 64, 65 | sylib 218 |
. . . . . 6
⊢ (𝜑 → {〈∅, 𝑅〉, 〈1o,
𝑆〉} = (𝑘 ∈ 2o ↦
({〈∅, 𝑅〉,
〈1o, 𝑆〉}‘𝑘))) |
| 67 | 66 | oveq2d 7447 |
. . . . 5
⊢ (𝜑 → ((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉}) = ((Scalar‘𝑅)Xs(𝑘 ∈ 2o ↦
({〈∅, 𝑅〉,
〈1o, 𝑆〉}‘𝑘)))) |
| 68 | 67 | fveq2d 6910 |
. . . 4
⊢ (𝜑 →
(dist‘((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉})) =
(dist‘((Scalar‘𝑅)Xs(𝑘 ∈ 2o ↦
({〈∅, 𝑅〉,
〈1o, 𝑆〉}‘𝑘))))) |
| 69 | 67 | fveq2d 6910 |
. . . . . 6
⊢ (𝜑 →
(Base‘((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉})) =
(Base‘((Scalar‘𝑅)Xs(𝑘 ∈ 2o ↦
({〈∅, 𝑅〉,
〈1o, 𝑆〉}‘𝑘))))) |
| 70 | 10, 69 | eqtrd 2777 |
. . . . 5
⊢ (𝜑 → ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) =
(Base‘((Scalar‘𝑅)Xs(𝑘 ∈ 2o ↦
({〈∅, 𝑅〉,
〈1o, 𝑆〉}‘𝑘))))) |
| 71 | 70 | fveq2d 6910 |
. . . 4
⊢ (𝜑 → (Met‘ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})) =
(Met‘(Base‘((Scalar‘𝑅)Xs(𝑘 ∈ 2o ↦
({〈∅, 𝑅〉,
〈1o, 𝑆〉}‘𝑘)))))) |
| 72 | 62, 68, 71 | 3eltr4d 2856 |
. . 3
⊢ (𝜑 →
(dist‘((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉})) ∈ (Met‘ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}))) |
| 73 | | ssid 4006 |
. . 3
⊢ ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) ⊆ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) |
| 74 | | metres2 24373 |
. . 3
⊢
(((dist‘((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉})) ∈ (Met‘ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})) ∧ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) ⊆ ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉})) →
((dist‘((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉})) ↾ (ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) × ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}))) ∈ (Met‘ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}))) |
| 75 | 72, 73, 74 | sylancl 586 |
. 2
⊢ (𝜑 →
((dist‘((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉})) ↾ (ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) × ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}))) ∈ (Met‘ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}))) |
| 76 | 9, 10, 13, 14, 15, 16, 75 | imasf1omet 24386 |
1
⊢ (𝜑 → 𝑃 ∈ (Met‘(𝑋 × 𝑌))) |