prdsxms - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > prdsxms		Structured version Visualization version GIF version

Theorem prdsxms 24487

Description: The indexed product structure is an extended metric space when the index set is finite. (Although the extended metric is still valid when the index set is infinite, it no longer agrees with the product topology, which is not metrizable in any case.) (Contributed by Mario Carneiro, 28-Aug-2015.)

**Hypothesis**
Ref	Expression
prdsxms.y	⊢ 𝑌 = (𝑆X_s𝑅)

**Assertion**
Ref	Expression
prdsxms	⊢ ((𝑆 ∈ 𝑊 ∧ 𝐼 ∈ Fin ∧ 𝑅:𝐼⟶∞MetSp) → 𝑌 ∈ ∞MetSp)

Proof of Theorem prdsxms Dummy variables 𝑔 𝑘 𝑥 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		prdsxms.y	. . . 4 ⊢ 𝑌 = (𝑆X_s𝑅)
2		simp1 1136	. . . 4 ⊢ ((𝑆 ∈ 𝑊 ∧ 𝐼 ∈ Fin ∧ 𝑅:𝐼⟶∞MetSp) → 𝑆 ∈ 𝑊)
3		simp2 1137	. . . 4 ⊢ ((𝑆 ∈ 𝑊 ∧ 𝐼 ∈ Fin ∧ 𝑅:𝐼⟶∞MetSp) → 𝐼 ∈ Fin)
4		eqid 2734	. . . 4 ⊢ (dist‘𝑌) = (dist‘𝑌)
5		eqid 2734	. . . 4 ⊢ (Base‘𝑌) = (Base‘𝑌)
6		simp3 1138	. . . 4 ⊢ ((𝑆 ∈ 𝑊 ∧ 𝐼 ∈ Fin ∧ 𝑅:𝐼⟶∞MetSp) → 𝑅:𝐼⟶∞MetSp)
7	1, 2, 3, 4, 5, 6	prdsxmslem1 24485	. . 3 ⊢ ((𝑆 ∈ 𝑊 ∧ 𝐼 ∈ Fin ∧ 𝑅:𝐼⟶∞MetSp) → (dist‘𝑌) ∈ (∞Met‘(Base‘𝑌)))
8		ssid 3986	. . 3 ⊢ (Base‘𝑌) ⊆ (Base‘𝑌)
9		xmetres2 24316	. . 3 ⊢ (((dist‘𝑌) ∈ (∞Met‘(Base‘𝑌)) ∧ (Base‘𝑌) ⊆ (Base‘𝑌)) → ((dist‘𝑌) ↾ ((Base‘𝑌) × (Base‘𝑌))) ∈ (∞Met‘(Base‘𝑌)))
10	7, 8, 9	sylancl 586	. 2 ⊢ ((𝑆 ∈ 𝑊 ∧ 𝐼 ∈ Fin ∧ 𝑅:𝐼⟶∞MetSp) → ((dist‘𝑌) ↾ ((Base‘𝑌) × (Base‘𝑌))) ∈ (∞Met‘(Base‘𝑌)))
11		eqid 2734	. . . 4 ⊢ (TopOpen‘𝑌) = (TopOpen‘𝑌)
12		eqid 2734	. . . 4 ⊢ (Base‘(𝑅‘𝑘)) = (Base‘(𝑅‘𝑘))
13		eqid 2734	. . . 4 ⊢ ((dist‘(𝑅‘𝑘)) ↾ ((Base‘(𝑅‘𝑘)) × (Base‘(𝑅‘𝑘)))) = ((dist‘(𝑅‘𝑘)) ↾ ((Base‘(𝑅‘𝑘)) × (Base‘(𝑅‘𝑘))))
14		eqid 2734	. . . 4 ⊢ (TopOpen‘(𝑅‘𝑘)) = (TopOpen‘(𝑅‘𝑘))
15		eqid 2734	. . . 4 ⊢ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘))} = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘))}
16	1, 2, 3, 4, 5, 6, 11, 12, 13, 14, 15	prdsxmslem2 24486	. . 3 ⊢ ((𝑆 ∈ 𝑊 ∧ 𝐼 ∈ Fin ∧ 𝑅:𝐼⟶∞MetSp) → (TopOpen‘𝑌) = (MetOpen‘(dist‘𝑌)))
17		xmetf 24284	. . . . 5 ⊢ ((dist‘𝑌) ∈ (∞Met‘(Base‘𝑌)) → (dist‘𝑌):((Base‘𝑌) × (Base‘𝑌))⟶ℝ^*)
18		ffn 6716	. . . . 5 ⊢ ((dist‘𝑌):((Base‘𝑌) × (Base‘𝑌))⟶ℝ^* → (dist‘𝑌) Fn ((Base‘𝑌) × (Base‘𝑌)))
19		fnresdm 6667	. . . . 5 ⊢ ((dist‘𝑌) Fn ((Base‘𝑌) × (Base‘𝑌)) → ((dist‘𝑌) ↾ ((Base‘𝑌) × (Base‘𝑌))) = (dist‘𝑌))
20	7, 17, 18, 19	4syl 19	. . . 4 ⊢ ((𝑆 ∈ 𝑊 ∧ 𝐼 ∈ Fin ∧ 𝑅:𝐼⟶∞MetSp) → ((dist‘𝑌) ↾ ((Base‘𝑌) × (Base‘𝑌))) = (dist‘𝑌))
21	20	fveq2d 6890	. . 3 ⊢ ((𝑆 ∈ 𝑊 ∧ 𝐼 ∈ Fin ∧ 𝑅:𝐼⟶∞MetSp) → (MetOpen‘((dist‘𝑌) ↾ ((Base‘𝑌) × (Base‘𝑌)))) = (MetOpen‘(dist‘𝑌)))
22	16, 21	eqtr4d 2772	. 2 ⊢ ((𝑆 ∈ 𝑊 ∧ 𝐼 ∈ Fin ∧ 𝑅:𝐼⟶∞MetSp) → (TopOpen‘𝑌) = (MetOpen‘((dist‘𝑌) ↾ ((Base‘𝑌) × (Base‘𝑌)))))
23		eqid 2734	. . 3 ⊢ ((dist‘𝑌) ↾ ((Base‘𝑌) × (Base‘𝑌))) = ((dist‘𝑌) ↾ ((Base‘𝑌) × (Base‘𝑌)))
24	11, 5, 23	isxms2 24403	. 2 ⊢ (𝑌 ∈ ∞MetSp ↔ (((dist‘𝑌) ↾ ((Base‘𝑌) × (Base‘𝑌))) ∈ (∞Met‘(Base‘𝑌)) ∧ (TopOpen‘𝑌) = (MetOpen‘((dist‘𝑌) ↾ ((Base‘𝑌) × (Base‘𝑌))))))
25	10, 22, 24	sylanbrc 583	1 ⊢ ((𝑆 ∈ 𝑊 ∧ 𝐼 ∈ Fin ∧ 𝑅:𝐼⟶∞MetSp) → 𝑌 ∈ ∞MetSp)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1539 ∃wex 1778 ∈ wcel 2107 {cab 2712 ∀wral 3050 ∃wrex 3059 ∖ cdif 3928 ⊆ wss 3931 ∪ cuni 4887 × cxp 5663 ↾ cres 5667 ∘ ccom 5669 Fn wfn 6536 ⟶wf 6537 ‘cfv 6541 (class class class)co 7413 Xcixp 8919 Fincfn 8967 ℝ^*cxr 11276 Basecbs 17229 distcds 17282 TopOpenctopn 17437 X_scprds 17461 ∞Metcxmet 21311 MetOpencmopn 21316 ∞MetSpcxms 24272

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2706 ax-rep 5259 ax-sep 5276 ax-nul 5286 ax-pow 5345 ax-pr 5412 ax-un 7737 ax-cnex 11193 ax-resscn 11194 ax-1cn 11195 ax-icn 11196 ax-addcl 11197 ax-addrcl 11198 ax-mulcl 11199 ax-mulrcl 11200 ax-mulcom 11201 ax-addass 11202 ax-mulass 11203 ax-distr 11204 ax-i2m1 11205 ax-1ne0 11206 ax-1rid 11207 ax-rnegex 11208 ax-rrecex 11209 ax-cnre 11210 ax-pre-lttri 11211 ax-pre-lttrn 11212 ax-pre-ltadd 11213 ax-pre-mulgt0 11214 ax-pre-sup 11215

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2808 df-nfc 2884 df-ne 2932 df-nel 3036 df-ral 3051 df-rex 3060 df-rmo 3363 df-reu 3364 df-rab 3420 df-v 3465 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-pss 3951 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-tp 4611 df-op 4613 df-uni 4888 df-int 4927 df-iun 4973 df-iin 4974 df-br 5124 df-opab 5186 df-mpt 5206 df-tr 5240 df-id 5558 df-eprel 5564 df-po 5572 df-so 5573 df-fr 5617 df-we 5619 df-xp 5671 df-rel 5672 df-cnv 5673 df-co 5674 df-dm 5675 df-rn 5676 df-res 5677 df-ima 5678 df-pred 6301 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-riota 7370 df-ov 7416 df-oprab 7417 df-mpo 7418 df-om 7870 df-1st 7996 df-2nd 7997 df-frecs 8288 df-wrecs 8319 df-recs 8393 df-rdg 8432 df-1o 8488 df-2o 8489 df-er 8727 df-map 8850 df-ixp 8920 df-en 8968 df-dom 8969 df-sdom 8970 df-fin 8971 df-fi 9433 df-sup 9464 df-inf 9465 df-pnf 11279 df-mnf 11280 df-xr 11281 df-ltxr 11282 df-le 11283 df-sub 11476 df-neg 11477 df-div 11903 df-nn 12249 df-2 12311 df-3 12312 df-4 12313 df-5 12314 df-6 12315 df-7 12316 df-8 12317 df-9 12318 df-n0 12510 df-z 12597 df-dec 12717 df-uz 12861 df-q 12973 df-rp 13017 df-xneg 13136 df-xadd 13137 df-xmul 13138 df-icc 13376 df-fz 13530 df-struct 17166 df-slot 17201 df-ndx 17213 df-base 17230 df-plusg 17286 df-mulr 17287 df-sca 17289 df-vsca 17290 df-ip 17291 df-tset 17292 df-ple 17293 df-ds 17295 df-hom 17297 df-cco 17298 df-rest 17438 df-topn 17439 df-topgen 17459 df-pt 17460 df-prds 17463 df-psmet 21318 df-xmet 21319 df-bl 21321 df-mopn 21322 df-top 22848 df-topon 22865 df-topsp 22887 df-bases 22900 df-xms 24275

This theorem is referenced by: prdsms 24488 pwsxms 24489 xpsxms 24491

W3C validator