Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . 3
⊢
((Scalar‘𝑅)Xs(𝑘 ∈ 2𝑜 ↦ (◡({𝑅} +𝑐 {𝑆})‘𝑘))) = ((Scalar‘𝑅)Xs(𝑘 ∈ 2𝑜 ↦ (◡({𝑅} +𝑐 {𝑆})‘𝑘))) |
2 | | eqid 2610 |
. . 3
⊢
(Base‘((Scalar‘𝑅)Xs(𝑘 ∈ 2𝑜 ↦ (◡({𝑅} +𝑐 {𝑆})‘𝑘)))) = (Base‘((Scalar‘𝑅)Xs(𝑘 ∈ 2𝑜 ↦ (◡({𝑅} +𝑐 {𝑆})‘𝑘)))) |
3 | | eqid 2610 |
. . 3
⊢
(Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) = (Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) |
4 | | eqid 2610 |
. . 3
⊢
((dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) ↾ ((Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) × (Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)))) = ((dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) ↾ ((Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) × (Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)))) |
5 | | eqid 2610 |
. . 3
⊢
(dist‘((Scalar‘𝑅)Xs(𝑘 ∈ 2𝑜 ↦ (◡({𝑅} +𝑐 {𝑆})‘𝑘)))) = (dist‘((Scalar‘𝑅)Xs(𝑘 ∈ 2𝑜 ↦ (◡({𝑅} +𝑐 {𝑆})‘𝑘)))) |
6 | | fvex 6113 |
. . . 4
⊢
(Scalar‘𝑅)
∈ V |
7 | 6 | a1i 11 |
. . 3
⊢ (𝜑 → (Scalar‘𝑅) ∈ V) |
8 | | 2on 7455 |
. . . 4
⊢
2𝑜 ∈ On |
9 | 8 | a1i 11 |
. . 3
⊢ (𝜑 → 2𝑜
∈ On) |
10 | | fvex 6113 |
. . . 4
⊢ (◡({𝑅} +𝑐 {𝑆})‘𝑘) ∈ V |
11 | 10 | a1i 11 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) → (◡({𝑅} +𝑐 {𝑆})‘𝑘) ∈ V) |
12 | | elpri 4145 |
. . . . 5
⊢ (𝑘 ∈ {∅,
1𝑜} → (𝑘 = ∅ ∨ 𝑘 = 1𝑜)) |
13 | | df2o3 7460 |
. . . . 5
⊢
2𝑜 = {∅,
1𝑜} |
14 | 12, 13 | eleq2s 2706 |
. . . 4
⊢ (𝑘 ∈ 2𝑜
→ (𝑘 = ∅ ∨
𝑘 =
1𝑜)) |
15 | | xpsds.3 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ (∞Met‘𝑋)) |
16 | 15 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 = ∅) → 𝑀 ∈ (∞Met‘𝑋)) |
17 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑘 = ∅ → (◡({𝑅} +𝑐 {𝑆})‘𝑘) = (◡({𝑅} +𝑐 {𝑆})‘∅)) |
18 | | xpsds.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈ 𝑉) |
19 | | xpsc0 16043 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ 𝑉 → (◡({𝑅} +𝑐 {𝑆})‘∅) = 𝑅) |
20 | 18, 19 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (◡({𝑅} +𝑐 {𝑆})‘∅) = 𝑅) |
21 | 17, 20 | sylan9eqr 2666 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 = ∅) → (◡({𝑅} +𝑐 {𝑆})‘𝑘) = 𝑅) |
22 | 21 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 = ∅) → (dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) = (dist‘𝑅)) |
23 | 21 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 = ∅) → (Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) = (Base‘𝑅)) |
24 | | xpsds.x |
. . . . . . . . . 10
⊢ 𝑋 = (Base‘𝑅) |
25 | 23, 24 | syl6eqr 2662 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 = ∅) → (Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) = 𝑋) |
26 | 25 | sqxpeqd 5065 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 = ∅) → ((Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) × (Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))) = (𝑋 × 𝑋)) |
27 | 22, 26 | reseq12d 5318 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 = ∅) → ((dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) ↾ ((Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) × (Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)))) = ((dist‘𝑅) ↾ (𝑋 × 𝑋))) |
28 | | xpsds.m |
. . . . . . 7
⊢ 𝑀 = ((dist‘𝑅) ↾ (𝑋 × 𝑋)) |
29 | 27, 28 | syl6eqr 2662 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 = ∅) → ((dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) ↾ ((Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) × (Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)))) = 𝑀) |
30 | 25 | fveq2d 6107 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 = ∅) →
(∞Met‘(Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))) = (∞Met‘𝑋)) |
31 | 16, 29, 30 | 3eltr4d 2703 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 = ∅) → ((dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) ↾ ((Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) × (Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)))) ∈
(∞Met‘(Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)))) |
32 | | xpsds.4 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ (∞Met‘𝑌)) |
33 | 32 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 = 1𝑜) → 𝑁 ∈ (∞Met‘𝑌)) |
34 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑘 = 1𝑜 →
(◡({𝑅} +𝑐 {𝑆})‘𝑘) = (◡({𝑅} +𝑐 {𝑆})‘1𝑜)) |
35 | | xpsds.2 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ∈ 𝑊) |
36 | | xpsc1 16044 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ 𝑊 → (◡({𝑅} +𝑐 {𝑆})‘1𝑜) = 𝑆) |
37 | 35, 36 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (◡({𝑅} +𝑐 {𝑆})‘1𝑜) = 𝑆) |
38 | 34, 37 | sylan9eqr 2666 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 = 1𝑜) → (◡({𝑅} +𝑐 {𝑆})‘𝑘) = 𝑆) |
39 | 38 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 = 1𝑜) →
(dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) = (dist‘𝑆)) |
40 | 38 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 = 1𝑜) →
(Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) = (Base‘𝑆)) |
41 | | xpsds.y |
. . . . . . . . . 10
⊢ 𝑌 = (Base‘𝑆) |
42 | 40, 41 | syl6eqr 2662 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 = 1𝑜) →
(Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) = 𝑌) |
43 | 42 | sqxpeqd 5065 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 = 1𝑜) →
((Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) × (Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))) = (𝑌 × 𝑌)) |
44 | 39, 43 | reseq12d 5318 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 = 1𝑜) →
((dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) ↾ ((Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) × (Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)))) = ((dist‘𝑆) ↾ (𝑌 × 𝑌))) |
45 | | xpsds.n |
. . . . . . 7
⊢ 𝑁 = ((dist‘𝑆) ↾ (𝑌 × 𝑌)) |
46 | 44, 45 | syl6eqr 2662 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 = 1𝑜) →
((dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) ↾ ((Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) × (Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)))) = 𝑁) |
47 | 42 | fveq2d 6107 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 = 1𝑜) →
(∞Met‘(Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘))) = (∞Met‘𝑌)) |
48 | 33, 46, 47 | 3eltr4d 2703 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 = 1𝑜) →
((dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) ↾ ((Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) × (Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)))) ∈
(∞Met‘(Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)))) |
49 | 31, 48 | jaodan 822 |
. . . 4
⊢ ((𝜑 ∧ (𝑘 = ∅ ∨ 𝑘 = 1𝑜)) →
((dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) ↾ ((Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) × (Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)))) ∈
(∞Met‘(Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)))) |
50 | 14, 49 | sylan2 490 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 2𝑜) →
((dist‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) ↾ ((Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)) × (Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)))) ∈
(∞Met‘(Base‘(◡({𝑅} +𝑐 {𝑆})‘𝑘)))) |
51 | 1, 2, 3, 4, 5, 7, 9, 11, 50 | prdsxmet 21984 |
. 2
⊢ (𝜑 →
(dist‘((Scalar‘𝑅)Xs(𝑘 ∈ 2𝑜 ↦ (◡({𝑅} +𝑐 {𝑆})‘𝑘)))) ∈
(∞Met‘(Base‘((Scalar‘𝑅)Xs(𝑘 ∈ 2𝑜 ↦ (◡({𝑅} +𝑐 {𝑆})‘𝑘)))))) |
52 | | xpscfn 16042 |
. . . . . 6
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → ◡({𝑅} +𝑐 {𝑆}) Fn
2𝑜) |
53 | 18, 35, 52 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → ◡({𝑅} +𝑐 {𝑆}) Fn
2𝑜) |
54 | | dffn5 6151 |
. . . . 5
⊢ (◡({𝑅} +𝑐 {𝑆}) Fn 2𝑜 ↔ ◡({𝑅} +𝑐 {𝑆}) = (𝑘 ∈ 2𝑜 ↦ (◡({𝑅} +𝑐 {𝑆})‘𝑘))) |
55 | 53, 54 | sylib 207 |
. . . 4
⊢ (𝜑 → ◡({𝑅} +𝑐 {𝑆}) = (𝑘 ∈ 2𝑜 ↦ (◡({𝑅} +𝑐 {𝑆})‘𝑘))) |
56 | 55 | oveq2d 6565 |
. . 3
⊢ (𝜑 → ((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})) = ((Scalar‘𝑅)Xs(𝑘 ∈ 2𝑜 ↦ (◡({𝑅} +𝑐 {𝑆})‘𝑘)))) |
57 | 56 | fveq2d 6107 |
. 2
⊢ (𝜑 →
(dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) = (dist‘((Scalar‘𝑅)Xs(𝑘 ∈ 2𝑜 ↦ (◡({𝑅} +𝑐 {𝑆})‘𝑘))))) |
58 | | xpsds.t |
. . . . 5
⊢ 𝑇 = (𝑅 ×s 𝑆) |
59 | | eqid 2610 |
. . . . 5
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) |
60 | | eqid 2610 |
. . . . 5
⊢
(Scalar‘𝑅) =
(Scalar‘𝑅) |
61 | | eqid 2610 |
. . . . 5
⊢
((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})) = ((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})) |
62 | 58, 24, 41, 18, 35, 59, 60, 61 | xpslem 16056 |
. . . 4
⊢ (𝜑 → ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) = (Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆})))) |
63 | 56 | fveq2d 6107 |
. . . 4
⊢ (𝜑 →
(Base‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) = (Base‘((Scalar‘𝑅)Xs(𝑘 ∈ 2𝑜 ↦ (◡({𝑅} +𝑐 {𝑆})‘𝑘))))) |
64 | 62, 63 | eqtrd 2644 |
. . 3
⊢ (𝜑 → ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})) = (Base‘((Scalar‘𝑅)Xs(𝑘 ∈ 2𝑜 ↦ (◡({𝑅} +𝑐 {𝑆})‘𝑘))))) |
65 | 64 | fveq2d 6107 |
. 2
⊢ (𝜑 → (∞Met‘ran
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦}))) =
(∞Met‘(Base‘((Scalar‘𝑅)Xs(𝑘 ∈ 2𝑜 ↦ (◡({𝑅} +𝑐 {𝑆})‘𝑘)))))) |
66 | 51, 57, 65 | 3eltr4d 2703 |
1
⊢ (𝜑 →
(dist‘((Scalar‘𝑅)Xs◡({𝑅} +𝑐 {𝑆}))) ∈ (∞Met‘ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ◡({𝑥} +𝑐 {𝑦})))) |