Metamath Proof Explorer

Theorem prdsms

Description: The indexed product structure is a metric space when the index set is finite. (Contributed by Mario Carneiro, 28-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 prdsxms.y ⊒ π‘Œ = ( 𝑆 Xs 𝑅 )
2 msxms ⊒ ( π‘₯ ∈ MetSp β†’ π‘₯ ∈ ∞MetSp )
3 2 ssriv ⊒ MetSp βŠ† ∞MetSp
4 fss ⊒ ( ( 𝑅 : 𝐼 ⟢ MetSp ∧ MetSp βŠ† ∞MetSp ) β†’ 𝑅 : 𝐼 ⟢ ∞MetSp )
5 3 4 mpan2 ⊒ ( 𝑅 : 𝐼 ⟢ MetSp β†’ 𝑅 : 𝐼 ⟢ ∞MetSp )
6 1 prdsxms ⊒ ( ( 𝑆 ∈ π‘Š ∧ 𝐼 ∈ Fin ∧ 𝑅 : 𝐼 ⟢ ∞MetSp ) β†’ π‘Œ ∈ ∞MetSp )
7 5 6 syl3an3 ⊒ ( ( 𝑆 ∈ π‘Š ∧ 𝐼 ∈ Fin ∧ 𝑅 : 𝐼 ⟢ MetSp ) β†’ π‘Œ ∈ ∞MetSp )
8 simp1 ⊒ ( ( 𝑆 ∈ π‘Š ∧ 𝐼 ∈ Fin ∧ 𝑅 : 𝐼 ⟢ MetSp ) β†’ 𝑆 ∈ π‘Š )
9 simp2 ⊒ ( ( 𝑆 ∈ π‘Š ∧ 𝐼 ∈ Fin ∧ 𝑅 : 𝐼 ⟢ MetSp ) β†’ 𝐼 ∈ Fin )
10 eqid ⊒ ( dist β€˜ π‘Œ ) = ( dist β€˜ π‘Œ )
11 eqid ⊒ ( Base β€˜ π‘Œ ) = ( Base β€˜ π‘Œ )
12 simp3 ⊒ ( ( 𝑆 ∈ π‘Š ∧ 𝐼 ∈ Fin ∧ 𝑅 : 𝐼 ⟢ MetSp ) β†’ 𝑅 : 𝐼 ⟢ MetSp )
13 1 8 9 10 11 12 prdsmslem1 ⊒ ( ( 𝑆 ∈ π‘Š ∧ 𝐼 ∈ Fin ∧ 𝑅 : 𝐼 ⟢ MetSp ) β†’ ( dist β€˜ π‘Œ ) ∈ ( Met β€˜ ( Base β€˜ π‘Œ ) ) )
14 ssid ⊒ ( Base β€˜ π‘Œ ) βŠ† ( Base β€˜ π‘Œ )
15 metres2 ⊒ ( ( ( dist β€˜ π‘Œ ) ∈ ( Met β€˜ ( Base β€˜ π‘Œ ) ) ∧ ( Base β€˜ π‘Œ ) βŠ† ( Base β€˜ π‘Œ ) ) β†’ ( ( dist β€˜ π‘Œ ) β†Ύ ( ( Base β€˜ π‘Œ ) Γ— ( Base β€˜ π‘Œ ) ) ) ∈ ( Met β€˜ ( Base β€˜ π‘Œ ) ) )
16 13 14 15 sylancl ⊒ ( ( 𝑆 ∈ π‘Š ∧ 𝐼 ∈ Fin ∧ 𝑅 : 𝐼 ⟢ MetSp ) β†’ ( ( dist β€˜ π‘Œ ) β†Ύ ( ( Base β€˜ π‘Œ ) Γ— ( Base β€˜ π‘Œ ) ) ) ∈ ( Met β€˜ ( Base β€˜ π‘Œ ) ) )
17 eqid ⊒ ( TopOpen β€˜ π‘Œ ) = ( TopOpen β€˜ π‘Œ )
18 eqid ⊒ ( ( dist β€˜ π‘Œ ) β†Ύ ( ( Base β€˜ π‘Œ ) Γ— ( Base β€˜ π‘Œ ) ) ) = ( ( dist β€˜ π‘Œ ) β†Ύ ( ( Base β€˜ π‘Œ ) Γ— ( Base β€˜ π‘Œ ) ) )
19 17 11 18 isms ⊒ ( π‘Œ ∈ MetSp ↔ ( π‘Œ ∈ ∞MetSp ∧ ( ( dist β€˜ π‘Œ ) β†Ύ ( ( Base β€˜ π‘Œ ) Γ— ( Base β€˜ π‘Œ ) ) ) ∈ ( Met β€˜ ( Base β€˜ π‘Œ ) ) ) )
20 7 16 19 sylanbrc ⊒ ( ( 𝑆 ∈ π‘Š ∧ 𝐼 ∈ Fin ∧ 𝑅 : 𝐼 ⟢ MetSp ) β†’ π‘Œ ∈ MetSp )