Metamath Proof Explorer


Theorem prdsdsfn

Description: Structure product distance function. (Contributed by Mario Carneiro, 15-Sep-2015)

Ref Expression
Hypotheses prdsbas.p P=S𝑠R
prdsbas.s φSV
prdsbas.r φRW
prdsbas.b B=BaseP
prdsbas.i φdomR=I
prdsds.l D=distP
Assertion prdsdsfn φDFnB×B

Proof

Step Hyp Ref Expression
1 prdsbas.p P=S𝑠R
2 prdsbas.s φSV
3 prdsbas.r φRW
4 prdsbas.b B=BaseP
5 prdsbas.i φdomR=I
6 prdsds.l D=distP
7 eqid fB,gBsupranxIfxdistRxgx0*<=fB,gBsupranxIfxdistRxgx0*<
8 xrltso <Or*
9 8 supex supranxIfxdistRxgx0*<V
10 7 9 fnmpoi fB,gBsupranxIfxdistRxgx0*<FnB×B
11 1 2 3 4 5 6 prdsds φD=fB,gBsupranxIfxdistRxgx0*<
12 11 fneq1d φDFnB×BfB,gBsupranxIfxdistRxgx0*<FnB×B
13 10 12 mpbiri φDFnB×B