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 Y = S 𝑠 R
prdsxms.s φ S W
prdsxms.i φ I Fin
prdsxms.d D = dist Y
prdsxms.b B = Base Y
prdsms.r φ R : I MetSp
Assertion prdsmslem1 φ D Met B

Proof

Step Hyp Ref Expression
1 prdsxms.y Y = S 𝑠 R
2 prdsxms.s φ S W
3 prdsxms.i φ I Fin
4 prdsxms.d D = dist Y
5 prdsxms.b B = Base Y
6 prdsms.r φ R : I MetSp
7 eqid S 𝑠 k I R k = S 𝑠 k I R k
8 eqid Base S 𝑠 k I R k = Base S 𝑠 k I R k
9 eqid Base R k = Base R k
10 eqid dist R k Base R k × Base R k = dist R k Base R k × Base R k
11 eqid dist S 𝑠 k I R k = dist S 𝑠 k I R k
12 6 ffvelrnda φ k I R k MetSp
13 9 10 msmet R k MetSp dist R k Base R k × Base R k Met Base R k
14 12 13 syl φ k I dist R k Base R k × Base R k Met Base R k
15 7 8 9 10 11 2 3 12 14 prdsmet φ dist S 𝑠 k I R k Met Base S 𝑠 k I R k
16 6 feqmptd φ R = k I R k
17 16 oveq2d φ S 𝑠 R = S 𝑠 k I R k
18 1 17 eqtrid φ Y = S 𝑠 k I R k
19 18 fveq2d φ dist Y = dist S 𝑠 k I R k
20 4 19 eqtrid φ D = dist S 𝑠 k I R k
21 18 fveq2d φ Base Y = Base S 𝑠 k I R k
22 5 21 eqtrid φ B = Base S 𝑠 k I R k
23 22 fveq2d φ Met B = Met Base S 𝑠 k I R k
24 15 20 23 3eltr4d φ D Met B