Metamath Proof Explorer

Theorem prdsmslem1

Description: Lemma for prdsms . The distance function of a product structure is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015)

Ref Expression
Hypotheses prdsxms.y ⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
prdsxms.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑊 )
prdsxms.i ⊢ ( 𝜑 → 𝐼 ∈ Fin )
prdsxms.d ⊢ 𝐷 = ( dist ‘ 𝑌 )
prdsxms.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
prdsms.r ⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ MetSp )
Assertion prdsmslem1 ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 prdsxms.y ⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
2 prdsxms.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑊 )
3 prdsxms.i ⊢ ( 𝜑 → 𝐼 ∈ Fin )
4 prdsxms.d ⊢ 𝐷 = ( dist ‘ 𝑌 )
5 prdsxms.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
6 prdsms.r ⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ MetSp )
7 eqid ⊢ ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) = ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) )
8 eqid ⊢ ( Base ‘ ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) ) = ( Base ‘ ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) )
9 eqid ⊢ ( Base ‘ ( 𝑅 ‘ 𝑘 ) ) = ( Base ‘ ( 𝑅 ‘ 𝑘 ) )
10 eqid ⊢ ( ( dist ‘ ( 𝑅 ‘ 𝑘 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑘 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑘 ) ) ) ) = ( ( dist ‘ ( 𝑅 ‘ 𝑘 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑘 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑘 ) ) ) )
11 eqid ⊢ ( dist ‘ ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) ) = ( dist ‘ ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) )
12 6 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑘 ) ∈ MetSp )
13 9 10 msmet ⊢ ( ( 𝑅 ‘ 𝑘 ) ∈ MetSp → ( ( dist ‘ ( 𝑅 ‘ 𝑘 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑘 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑘 ) ) ) ) ∈ ( Met ‘ ( Base ‘ ( 𝑅 ‘ 𝑘 ) ) ) )
14 12 13 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( ( dist ‘ ( 𝑅 ‘ 𝑘 ) ) ↾ ( ( Base ‘ ( 𝑅 ‘ 𝑘 ) ) × ( Base ‘ ( 𝑅 ‘ 𝑘 ) ) ) ) ∈ ( Met ‘ ( Base ‘ ( 𝑅 ‘ 𝑘 ) ) ) )
15 7 8 9 10 11 2 3 12 14 prdsmet ⊢ ( 𝜑 → ( dist ‘ ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) ) ∈ ( Met ‘ ( Base ‘ ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) ) ) )
16 6 feqmptd ⊢ ( 𝜑 → 𝑅 = ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) )
17 16 oveq2d ⊢ ( 𝜑 → ( 𝑆 Xs 𝑅 ) = ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) )
18 1 17 syl5eq ⊢ ( 𝜑 → 𝑌 = ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) )
19 18 fveq2d ⊢ ( 𝜑 → ( dist ‘ 𝑌 ) = ( dist ‘ ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) ) )
20 4 19 syl5eq ⊢ ( 𝜑 → 𝐷 = ( dist ‘ ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) ) )
21 18 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝑌 ) = ( Base ‘ ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) ) )
22 5 21 syl5eq ⊢ ( 𝜑 → 𝐵 = ( Base ‘ ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) ) )
23 22 fveq2d ⊢ ( 𝜑 → ( Met ‘ 𝐵 ) = ( Met ‘ ( Base ‘ ( 𝑆 Xs ( 𝑘 ∈ 𝐼 ↦ ( 𝑅 ‘ 𝑘 ) ) ) ) ) )
24 15 20 23 3eltr4d ⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝐵 ) )