This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem prdsdsfn

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

Ref Expression
Hypotheses prdsbas.p 
|- P = ( S Xs_ R )
prdsbas.s 
|- ( ph -> S e. V )
prdsbas.r 
|- ( ph -> R e. W )
prdsbas.b 
|- B = ( Base ` P )
prdsbas.i 
|- ( ph -> dom R = I )
prdsds.l 
|- D = ( dist ` P )
Assertion prdsdsfn 
|- ( ph -> D Fn ( B X. B ) )

Proof

Step Hyp Ref Expression
1 prdsbas.p 
 |-  P = ( S Xs_ R )
2 prdsbas.s 
 |-  ( ph -> S e. V )
3 prdsbas.r 
 |-  ( ph -> R e. W )
4 prdsbas.b 
 |-  B = ( Base ` P )
5 prdsbas.i 
 |-  ( ph -> dom R = I )
6 prdsds.l 
 |-  D = ( dist ` P )
7 eqid 
 |-  ( f e. B , g e. B |-> sup ( ( ran ( x e. I |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) = ( f e. B , g e. B |-> sup ( ( ran ( x e. I |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) )
8 xrltso 
 |-  < Or RR*
9 8 supex 
 |-  sup ( ( ran ( x e. I |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) e. _V
10 7 9 fnmpoi 
 |-  ( f e. B , g e. B |-> sup ( ( ran ( x e. I |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) Fn ( B X. B )
11 1 2 3 4 5 6 prdsds 
 |-  ( ph -> D = ( f e. B , g e. B |-> sup ( ( ran ( x e. I |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) )
12 11 fneq1d 
 |-  ( ph -> ( D Fn ( B X. B ) <-> ( f e. B , g e. B |-> sup ( ( ran ( x e. I |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) Fn ( B X. B ) ) )
13 10 12 mpbiri 
 |-  ( ph -> D Fn ( B X. B ) )