Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > prdsmslem1 | Structured version Visualization version GIF version |
Description: Lemma for prdsms 23453. The distance function of a product structure is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.) |
Ref | Expression |
---|---|
prdsxms.y | ⊢ 𝑌 = (𝑆Xs𝑅) |
prdsxms.s | ⊢ (𝜑 → 𝑆 ∈ 𝑊) |
prdsxms.i | ⊢ (𝜑 → 𝐼 ∈ Fin) |
prdsxms.d | ⊢ 𝐷 = (dist‘𝑌) |
prdsxms.b | ⊢ 𝐵 = (Base‘𝑌) |
prdsms.r | ⊢ (𝜑 → 𝑅:𝐼⟶MetSp) |
Ref | Expression |
---|---|
prdsmslem1 | ⊢ (𝜑 → 𝐷 ∈ (Met‘𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2738 | . . 3 ⊢ (𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘))) = (𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘))) | |
2 | eqid 2738 | . . 3 ⊢ (Base‘(𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘)))) = (Base‘(𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘)))) | |
3 | eqid 2738 | . . 3 ⊢ (Base‘(𝑅‘𝑘)) = (Base‘(𝑅‘𝑘)) | |
4 | eqid 2738 | . . 3 ⊢ ((dist‘(𝑅‘𝑘)) ↾ ((Base‘(𝑅‘𝑘)) × (Base‘(𝑅‘𝑘)))) = ((dist‘(𝑅‘𝑘)) ↾ ((Base‘(𝑅‘𝑘)) × (Base‘(𝑅‘𝑘)))) | |
5 | eqid 2738 | . . 3 ⊢ (dist‘(𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘)))) = (dist‘(𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘)))) | |
6 | prdsxms.s | . . 3 ⊢ (𝜑 → 𝑆 ∈ 𝑊) | |
7 | prdsxms.i | . . 3 ⊢ (𝜑 → 𝐼 ∈ Fin) | |
8 | prdsms.r | . . . 4 ⊢ (𝜑 → 𝑅:𝐼⟶MetSp) | |
9 | 8 | ffvelrnda 6923 | . . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑅‘𝑘) ∈ MetSp) |
10 | 3, 4 | msmet 23379 | . . . 4 ⊢ ((𝑅‘𝑘) ∈ MetSp → ((dist‘(𝑅‘𝑘)) ↾ ((Base‘(𝑅‘𝑘)) × (Base‘(𝑅‘𝑘)))) ∈ (Met‘(Base‘(𝑅‘𝑘)))) |
11 | 9, 10 | syl 17 | . . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → ((dist‘(𝑅‘𝑘)) ↾ ((Base‘(𝑅‘𝑘)) × (Base‘(𝑅‘𝑘)))) ∈ (Met‘(Base‘(𝑅‘𝑘)))) |
12 | 1, 2, 3, 4, 5, 6, 7, 9, 11 | prdsmet 23292 | . 2 ⊢ (𝜑 → (dist‘(𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘)))) ∈ (Met‘(Base‘(𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘)))))) |
13 | prdsxms.d | . . 3 ⊢ 𝐷 = (dist‘𝑌) | |
14 | prdsxms.y | . . . . 5 ⊢ 𝑌 = (𝑆Xs𝑅) | |
15 | 8 | feqmptd 6799 | . . . . . 6 ⊢ (𝜑 → 𝑅 = (𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘))) |
16 | 15 | oveq2d 7248 | . . . . 5 ⊢ (𝜑 → (𝑆Xs𝑅) = (𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘)))) |
17 | 14, 16 | syl5eq 2791 | . . . 4 ⊢ (𝜑 → 𝑌 = (𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘)))) |
18 | 17 | fveq2d 6740 | . . 3 ⊢ (𝜑 → (dist‘𝑌) = (dist‘(𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘))))) |
19 | 13, 18 | syl5eq 2791 | . 2 ⊢ (𝜑 → 𝐷 = (dist‘(𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘))))) |
20 | prdsxms.b | . . . 4 ⊢ 𝐵 = (Base‘𝑌) | |
21 | 17 | fveq2d 6740 | . . . 4 ⊢ (𝜑 → (Base‘𝑌) = (Base‘(𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘))))) |
22 | 20, 21 | syl5eq 2791 | . . 3 ⊢ (𝜑 → 𝐵 = (Base‘(𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘))))) |
23 | 22 | fveq2d 6740 | . 2 ⊢ (𝜑 → (Met‘𝐵) = (Met‘(Base‘(𝑆Xs(𝑘 ∈ 𝐼 ↦ (𝑅‘𝑘)))))) |
24 | 12, 19, 23 | 3eltr4d 2854 | 1 ⊢ (𝜑 → 𝐷 ∈ (Met‘𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 = wceq 1543 ∈ wcel 2111 ↦ cmpt 5150 × cxp 5564 ↾ cres 5568 ⟶wf 6394 ‘cfv 6398 (class class class)co 7232 Fincfn 8647 Basecbs 16785 distcds 16836 Xscprds 16975 Metcmet 20374 MetSpcms 23240 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2159 ax-12 2176 ax-ext 2709 ax-rep 5194 ax-sep 5207 ax-nul 5214 ax-pow 5273 ax-pr 5337 ax-un 7542 ax-cnex 10810 ax-resscn 10811 ax-1cn 10812 ax-icn 10813 ax-addcl 10814 ax-addrcl 10815 ax-mulcl 10816 ax-mulrcl 10817 ax-mulcom 10818 ax-addass 10819 ax-mulass 10820 ax-distr 10821 ax-i2m1 10822 ax-1ne0 10823 ax-1rid 10824 ax-rnegex 10825 ax-rrecex 10826 ax-cnre 10827 ax-pre-lttri 10828 ax-pre-lttrn 10829 ax-pre-ltadd 10830 ax-pre-mulgt0 10831 ax-pre-sup 10832 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2072 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2887 df-ne 2942 df-nel 3048 df-ral 3067 df-rex 3068 df-reu 3069 df-rmo 3070 df-rab 3071 df-v 3423 df-sbc 3710 df-csb 3827 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-pss 3900 df-nul 4253 df-if 4455 df-pw 4530 df-sn 4557 df-pr 4559 df-tp 4561 df-op 4563 df-uni 4835 df-iun 4921 df-br 5069 df-opab 5131 df-mpt 5151 df-tr 5177 df-id 5470 df-eprel 5475 df-po 5483 df-so 5484 df-fr 5524 df-we 5526 df-xp 5572 df-rel 5573 df-cnv 5574 df-co 5575 df-dm 5576 df-rn 5577 df-res 5578 df-ima 5579 df-pred 6176 df-ord 6234 df-on 6235 df-lim 6236 df-suc 6237 df-iota 6356 df-fun 6400 df-fn 6401 df-f 6402 df-f1 6403 df-fo 6404 df-f1o 6405 df-fv 6406 df-riota 7189 df-ov 7235 df-oprab 7236 df-mpo 7237 df-om 7664 df-1st 7780 df-2nd 7781 df-wrecs 8068 df-recs 8129 df-rdg 8167 df-1o 8223 df-er 8412 df-map 8531 df-ixp 8600 df-en 8648 df-dom 8649 df-sdom 8650 df-fin 8651 df-sup 9083 df-inf 9084 df-pnf 10894 df-mnf 10895 df-xr 10896 df-ltxr 10897 df-le 10898 df-sub 11089 df-neg 11090 df-div 11515 df-nn 11856 df-2 11918 df-3 11919 df-4 11920 df-5 11921 df-6 11922 df-7 11923 df-8 11924 df-9 11925 df-n0 12116 df-z 12202 df-dec 12319 df-uz 12464 df-q 12570 df-rp 12612 df-xneg 12729 df-xadd 12730 df-xmul 12731 df-icc 12967 df-fz 13121 df-struct 16725 df-slot 16760 df-ndx 16770 df-base 16786 df-plusg 16840 df-mulr 16841 df-sca 16843 df-vsca 16844 df-ip 16845 df-tset 16846 df-ple 16847 df-ds 16849 df-hom 16851 df-cco 16852 df-topgen 16973 df-prds 16977 df-psmet 20380 df-xmet 20381 df-met 20382 df-bl 20383 df-mopn 20384 df-top 21815 df-topon 21832 df-topsp 21854 df-bases 21867 df-xms 23242 df-ms 23243 |
This theorem is referenced by: prdsms 23453 |
Copyright terms: Public domain | W3C validator |