Metamath Proof Explorer

Theorem prdsxms

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)

Ref Expression
Hypothesis prdsxms.y ⊒ π‘Œ = ( 𝑆 Xs 𝑅 )
Assertion prdsxms ( ( 𝑆 ∈ π‘Š ∧ 𝐼 ∈ Fin ∧ 𝑅 : 𝐼 ⟢ ∞MetSp ) β†’ π‘Œ ∈ ∞MetSp )

Proof

Step Hyp Ref Expression
1 prdsxms.y ⊒ π‘Œ = ( 𝑆 Xs 𝑅 )
2 simp1 ⊒ ( ( 𝑆 ∈ π‘Š ∧ 𝐼 ∈ Fin ∧ 𝑅 : 𝐼 ⟢ ∞MetSp ) β†’ 𝑆 ∈ π‘Š )
3 simp2 ⊒ ( ( 𝑆 ∈ π‘Š ∧ 𝐼 ∈ Fin ∧ 𝑅 : 𝐼 ⟢ ∞MetSp ) β†’ 𝐼 ∈ Fin )
4 eqid ⊒ ( dist β€˜ π‘Œ ) = ( dist β€˜ π‘Œ )
5 eqid ⊒ ( Base β€˜ π‘Œ ) = ( Base β€˜ π‘Œ )
6 simp3 ⊒ ( ( 𝑆 ∈ π‘Š ∧ 𝐼 ∈ Fin ∧ 𝑅 : 𝐼 ⟢ ∞MetSp ) β†’ 𝑅 : 𝐼 ⟢ ∞MetSp )
7 1 2 3 4 5 6 prdsxmslem1 ⊒ ( ( 𝑆 ∈ π‘Š ∧ 𝐼 ∈ Fin ∧ 𝑅 : 𝐼 ⟢ ∞MetSp ) β†’ ( dist β€˜ π‘Œ ) ∈ ( ∞Met β€˜ ( Base β€˜ π‘Œ ) ) )
8 ssid ⊒ ( Base β€˜ π‘Œ ) βŠ† ( Base β€˜ π‘Œ )
9 xmetres2 ⊒ ( ( ( dist β€˜ π‘Œ ) ∈ ( ∞Met β€˜ ( Base β€˜ π‘Œ ) ) ∧ ( Base β€˜ π‘Œ ) βŠ† ( Base β€˜ π‘Œ ) ) β†’ ( ( dist β€˜ π‘Œ ) β†Ύ ( ( Base β€˜ π‘Œ ) Γ— ( Base β€˜ π‘Œ ) ) ) ∈ ( ∞Met β€˜ ( Base β€˜ π‘Œ ) ) )
10 7 8 9 sylancl ⊒ ( ( 𝑆 ∈ π‘Š ∧ 𝐼 ∈ Fin ∧ 𝑅 : 𝐼 ⟢ ∞MetSp ) β†’ ( ( dist β€˜ π‘Œ ) β†Ύ ( ( Base β€˜ π‘Œ ) Γ— ( Base β€˜ π‘Œ ) ) ) ∈ ( ∞Met β€˜ ( Base β€˜ π‘Œ ) ) )
11 eqid ⊒ ( TopOpen β€˜ π‘Œ ) = ( TopOpen β€˜ π‘Œ )
12 eqid ⊒ ( Base β€˜ ( 𝑅 β€˜ π‘˜ ) ) = ( Base β€˜ ( 𝑅 β€˜ π‘˜ ) )
13 eqid ⊒ ( ( dist β€˜ ( 𝑅 β€˜ π‘˜ ) ) β†Ύ ( ( Base β€˜ ( 𝑅 β€˜ π‘˜ ) ) Γ— ( Base β€˜ ( 𝑅 β€˜ π‘˜ ) ) ) ) = ( ( dist β€˜ ( 𝑅 β€˜ π‘˜ ) ) β†Ύ ( ( Base β€˜ ( 𝑅 β€˜ π‘˜ ) ) Γ— ( Base β€˜ ( 𝑅 β€˜ π‘˜ ) ) ) )
14 eqid ⊒ ( TopOpen β€˜ ( 𝑅 β€˜ π‘˜ ) ) = ( TopOpen β€˜ ( 𝑅 β€˜ π‘˜ ) )
15 eqid ⊒ { π‘₯ ∣ βˆƒ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ βˆ€ π‘˜ ∈ 𝐼 ( 𝑔 β€˜ π‘˜ ) ∈ ( ( TopOpen ∘ 𝑅 ) β€˜ π‘˜ ) ∧ βˆƒ 𝑧 ∈ Fin βˆ€ π‘˜ ∈ ( 𝐼 βˆ– 𝑧 ) ( 𝑔 β€˜ π‘˜ ) = βˆͺ ( ( TopOpen ∘ 𝑅 ) β€˜ π‘˜ ) ) ∧ π‘₯ = X π‘˜ ∈ 𝐼 ( 𝑔 β€˜ π‘˜ ) ) } = { π‘₯ ∣ βˆƒ 𝑔 ( ( 𝑔 Fn 𝐼 ∧ βˆ€ π‘˜ ∈ 𝐼 ( 𝑔 β€˜ π‘˜ ) ∈ ( ( TopOpen ∘ 𝑅 ) β€˜ π‘˜ ) ∧ βˆƒ 𝑧 ∈ Fin βˆ€ π‘˜ ∈ ( 𝐼 βˆ– 𝑧 ) ( 𝑔 β€˜ π‘˜ ) = βˆͺ ( ( TopOpen ∘ 𝑅 ) β€˜ π‘˜ ) ) ∧ π‘₯ = X π‘˜ ∈ 𝐼 ( 𝑔 β€˜ π‘˜ ) ) }
16 1 2 3 4 5 6 11 12 13 14 15 prdsxmslem2 ⊒ ( ( 𝑆 ∈ π‘Š ∧ 𝐼 ∈ Fin ∧ 𝑅 : 𝐼 ⟢ ∞MetSp ) β†’ ( TopOpen β€˜ π‘Œ ) = ( MetOpen β€˜ ( dist β€˜ π‘Œ ) ) )
17 xmetf ⊒ ( ( dist β€˜ π‘Œ ) ∈ ( ∞Met β€˜ ( Base β€˜ π‘Œ ) ) β†’ ( dist β€˜ π‘Œ ) : ( ( Base β€˜ π‘Œ ) Γ— ( Base β€˜ π‘Œ ) ) ⟢ ℝ* )
18 ffn ⊒ ( ( dist β€˜ π‘Œ ) : ( ( Base β€˜ π‘Œ ) Γ— ( Base β€˜ π‘Œ ) ) ⟢ ℝ* β†’ ( dist β€˜ π‘Œ ) Fn ( ( Base β€˜ π‘Œ ) Γ— ( Base β€˜ π‘Œ ) ) )
19 fnresdm ⊒ ( ( dist β€˜ π‘Œ ) Fn ( ( Base β€˜ π‘Œ ) Γ— ( Base β€˜ π‘Œ ) ) β†’ ( ( dist β€˜ π‘Œ ) β†Ύ ( ( Base β€˜ π‘Œ ) Γ— ( Base β€˜ π‘Œ ) ) ) = ( dist β€˜ π‘Œ ) )
20 7 17 18 19 4syl ⊒ ( ( 𝑆 ∈ π‘Š ∧ 𝐼 ∈ Fin ∧ 𝑅 : 𝐼 ⟢ ∞MetSp ) β†’ ( ( dist β€˜ π‘Œ ) β†Ύ ( ( Base β€˜ π‘Œ ) Γ— ( Base β€˜ π‘Œ ) ) ) = ( dist β€˜ π‘Œ ) )
21 20 fveq2d ⊒ ( ( 𝑆 ∈ π‘Š ∧ 𝐼 ∈ Fin ∧ 𝑅 : 𝐼 ⟢ ∞MetSp ) β†’ ( MetOpen β€˜ ( ( dist β€˜ π‘Œ ) β†Ύ ( ( Base β€˜ π‘Œ ) Γ— ( Base β€˜ π‘Œ ) ) ) ) = ( MetOpen β€˜ ( dist β€˜ π‘Œ ) ) )
22 16 21 eqtr4d ⊒ ( ( 𝑆 ∈ π‘Š ∧ 𝐼 ∈ Fin ∧ 𝑅 : 𝐼 ⟢ ∞MetSp ) β†’ ( TopOpen β€˜ π‘Œ ) = ( MetOpen β€˜ ( ( dist β€˜ π‘Œ ) β†Ύ ( ( Base β€˜ π‘Œ ) Γ— ( Base β€˜ π‘Œ ) ) ) ) )
23 eqid ⊒ ( ( dist β€˜ π‘Œ ) β†Ύ ( ( Base β€˜ π‘Œ ) Γ— ( Base β€˜ π‘Œ ) ) ) = ( ( dist β€˜ π‘Œ ) β†Ύ ( ( Base β€˜ π‘Œ ) Γ— ( Base β€˜ π‘Œ ) ) )
24 11 5 23 isxms2 ⊒ ( π‘Œ ∈ ∞MetSp ↔ ( ( ( dist β€˜ π‘Œ ) β†Ύ ( ( Base β€˜ π‘Œ ) Γ— ( Base β€˜ π‘Œ ) ) ) ∈ ( ∞Met β€˜ ( Base β€˜ π‘Œ ) ) ∧ ( TopOpen β€˜ π‘Œ ) = ( MetOpen β€˜ ( ( dist β€˜ π‘Œ ) β†Ύ ( ( Base β€˜ π‘Œ ) Γ— ( Base β€˜ π‘Œ ) ) ) ) ) )
25 10 22 24 sylanbrc ⊒ ( ( 𝑆 ∈ π‘Š ∧ 𝐼 ∈ Fin ∧ 𝑅 : 𝐼 ⟢ ∞MetSp ) β†’ π‘Œ ∈ ∞MetSp )