Metamath Proof Explorer


Theorem prdsds

Description: Structure product distance function. (Contributed by Mario Carneiro, 15-Aug-2015) (Revised by Thierry Arnoux, 16-Jun-2019) (Revised by Zhi Wang, 18-Aug-2024)

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 prdsds φD=fB,gBsupranxIfxdistRxgx0*<

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 BaseS=BaseS
8 1 2 3 4 5 prdsbas φB=xIBaseRx
9 eqid +P=+P
10 1 2 3 4 5 9 prdsplusg φ+P=fB,gBxIfx+Rxgx
11 eqid P=P
12 1 2 3 4 5 11 prdsmulr φP=fB,gBxIfxRxgx
13 eqid P=P
14 1 2 3 4 5 7 13 prdsvsca φP=fBaseS,gBxIfRxgx
15 eqidd φfB,gBSxIfx𝑖Rxgx=fB,gBSxIfx𝑖Rxgx
16 eqidd φ𝑡TopOpenR=𝑡TopOpenR
17 eqid P=P
18 1 2 3 4 5 17 prdsle φP=fg|fgBxIfxRxgx
19 eqidd φfB,gBsupranxIfxdistRxgx0*<=fB,gBsupranxIfxdistRxgx0*<
20 eqidd φfB,gBxIfxHomRxgx=fB,gBxIfxHomRxgx
21 eqidd φaB×B,cBd2ndafB,gBxIfxHomRxgxc,efB,gBxIfxHomRxgxaxIdx1stax2ndaxcompRxcxex=aB×B,cBd2ndafB,gBxIfxHomRxgxc,efB,gBxIfxHomRxgxaxIdx1stax2ndaxcompRxcxex
22 1 7 5 8 10 12 14 15 16 18 19 20 21 2 3 prdsval φP=BasendxB+ndx+PndxPScalarndxSndxP𝑖ndxfB,gBSxIfx𝑖RxgxTopSetndx𝑡TopOpenRndxPdistndxfB,gBsupranxIfxdistRxgx0*<HomndxfB,gBxIfxHomRxgxcompndxaB×B,cBd2ndafB,gBxIfxHomRxgxc,efB,gBxIfxHomRxgxaxIdx1stax2ndaxcompRxcxex
23 dsid dist=Slotdistndx
24 4 fvexi BV
25 xrex *V
26 25 uniex *V
27 26 pwex 𝒫*V
28 df-sup supranxIfxdistRxgx0*<=y*|zranxIfxdistRxgx0¬y<zz*z<ywranxIfxdistRxgx0z<w
29 ssrab2 y*|zranxIfxdistRxgx0¬y<zz*z<ywranxIfxdistRxgx0z<w*
30 29 unissi y*|zranxIfxdistRxgx0¬y<zz*z<ywranxIfxdistRxgx0z<w*
31 26 30 elpwi2 y*|zranxIfxdistRxgx0¬y<zz*z<ywranxIfxdistRxgx0z<w𝒫*
32 28 31 eqeltri supranxIfxdistRxgx0*<𝒫*
33 32 rgen2w fBgBsupranxIfxdistRxgx0*<𝒫*
34 24 24 27 33 mpoexw fB,gBsupranxIfxdistRxgx0*<V
35 34 a1i φfB,gBsupranxIfxdistRxgx0*<V
36 snsstp3 distndxfB,gBsupranxIfxdistRxgx0*<TopSetndx𝑡TopOpenRndxPdistndxfB,gBsupranxIfxdistRxgx0*<
37 ssun1 TopSetndx𝑡TopOpenRndxPdistndxfB,gBsupranxIfxdistRxgx0*<TopSetndx𝑡TopOpenRndxPdistndxfB,gBsupranxIfxdistRxgx0*<HomndxfB,gBxIfxHomRxgxcompndxaB×B,cBd2ndafB,gBxIfxHomRxgxc,efB,gBxIfxHomRxgxaxIdx1stax2ndaxcompRxcxex
38 36 37 sstri distndxfB,gBsupranxIfxdistRxgx0*<TopSetndx𝑡TopOpenRndxPdistndxfB,gBsupranxIfxdistRxgx0*<HomndxfB,gBxIfxHomRxgxcompndxaB×B,cBd2ndafB,gBxIfxHomRxgxc,efB,gBxIfxHomRxgxaxIdx1stax2ndaxcompRxcxex
39 ssun2 TopSetndx𝑡TopOpenRndxPdistndxfB,gBsupranxIfxdistRxgx0*<HomndxfB,gBxIfxHomRxgxcompndxaB×B,cBd2ndafB,gBxIfxHomRxgxc,efB,gBxIfxHomRxgxaxIdx1stax2ndaxcompRxcxexBasendxB+ndx+PndxPScalarndxSndxP𝑖ndxfB,gBSxIfx𝑖RxgxTopSetndx𝑡TopOpenRndxPdistndxfB,gBsupranxIfxdistRxgx0*<HomndxfB,gBxIfxHomRxgxcompndxaB×B,cBd2ndafB,gBxIfxHomRxgxc,efB,gBxIfxHomRxgxaxIdx1stax2ndaxcompRxcxex
40 38 39 sstri distndxfB,gBsupranxIfxdistRxgx0*<BasendxB+ndx+PndxPScalarndxSndxP𝑖ndxfB,gBSxIfx𝑖RxgxTopSetndx𝑡TopOpenRndxPdistndxfB,gBsupranxIfxdistRxgx0*<HomndxfB,gBxIfxHomRxgxcompndxaB×B,cBd2ndafB,gBxIfxHomRxgxc,efB,gBxIfxHomRxgxaxIdx1stax2ndaxcompRxcxex
41 22 6 23 35 40 prdsbaslem φD=fB,gBsupranxIfxdistRxgx0*<