Metamath Proof Explorer

Definition df-cplmet

Description: A function which completes the given metric space. (Contributed by Mario Carneiro, 2-Dec-2014)

Ref Expression
Assertion df-cplmet 
|- cplMetSp = ( w e. _V |-> [_ ( ( w ^s NN ) |`s ( Cau ` ( dist ` w ) ) ) / r ]_ [_ ( Base ` r ) / v ]_ [_ { <. f , g >. | ( { f , g } C_ v /\ A. x e. RR+ E. j e. ZZ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( g ` j ) ( ball ` ( dist ` w ) ) x ) ) } / e ]_ ( ( r /s e ) sSet { <. ( dist ` ndx ) , { <. <. x , y >. , z >. | E. p e. v E. q e. v ( ( x = [ p ] e /\ y = [ q ] e ) /\ ( p oF ( dist ` r ) q ) ~~> z ) } >. } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccpms 
 |-  cplMetSp
1 vw 
 |-  w
2 cvv 
 |-  _V
3 1 cv 
 |-  w
4 cpws 
 |-  ^s
5 cn 
 |-  NN
6 3 5 4 co 
 |-  ( w ^s NN )
7 cress 
 |-  |`s
8 ccau 
 |-  Cau
9 cds 
 |-  dist
10 3 9 cfv 
 |-  ( dist ` w )
11 10 8 cfv 
 |-  ( Cau ` ( dist ` w ) )
12 6 11 7 co 
 |-  ( ( w ^s NN ) |`s ( Cau ` ( dist ` w ) ) )
13 vr 
 |-  r
14 cbs 
 |-  Base
15 13 cv 
 |-  r
16 15 14 cfv 
 |-  ( Base ` r )
17 vv 
 |-  v
18 vf 
 |-  f
19 vg 
 |-  g
20 18 cv 
 |-  f
21 19 cv 
 |-  g
22 20 21 cpr 
 |-  { f , g }
23 17 cv 
 |-  v
24 22 23 wss 
 |-  { f , g } C_ v
25 vx 
 |-  x
26 crp 
 |-  RR+
27 vj 
 |-  j
28 cz 
 |-  ZZ
29 cuz 
 |-  ZZ>=
30 27 cv 
 |-  j
31 30 29 cfv 
 |-  ( ZZ>= ` j )
32 20 31 cres 
 |-  ( f |` ( ZZ>= ` j ) )
33 30 21 cfv 
 |-  ( g ` j )
34 cbl 
 |-  ball
35 10 34 cfv 
 |-  ( ball ` ( dist ` w ) )
36 25 cv 
 |-  x
37 33 36 35 co 
 |-  ( ( g ` j ) ( ball ` ( dist ` w ) ) x )
38 31 37 32 wf 
 |-  ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( g ` j ) ( ball ` ( dist ` w ) ) x )
39 38 27 28 wrex 
 |-  E. j e. ZZ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( g ` j ) ( ball ` ( dist ` w ) ) x )
40 39 25 26 wral 
 |-  A. x e. RR+ E. j e. ZZ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( g ` j ) ( ball ` ( dist ` w ) ) x )
41 24 40 wa 
 |-  ( { f , g } C_ v /\ A. x e. RR+ E. j e. ZZ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( g ` j ) ( ball ` ( dist ` w ) ) x ) )
42 41 18 19 copab 
 |-  { <. f , g >. | ( { f , g } C_ v /\ A. x e. RR+ E. j e. ZZ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( g ` j ) ( ball ` ( dist ` w ) ) x ) ) }
43 ve 
 |-  e
44 cqus 
 |-  /s
45 43 cv 
 |-  e
46 15 45 44 co 
 |-  ( r /s e )
47 csts 
 |-  sSet
48 cnx 
 |-  ndx
49 48 9 cfv 
 |-  ( dist ` ndx )
50 vy 
 |-  y
51 vz 
 |-  z
52 vp 
 |-  p
53 vq 
 |-  q
54 52 cv 
 |-  p
55 54 45 cec 
 |-  [ p ] e
56 36 55 wceq 
 |-  x = [ p ] e
57 50 cv 
 |-  y
58 53 cv 
 |-  q
59 58 45 cec 
 |-  [ q ] e
60 57 59 wceq 
 |-  y = [ q ] e
61 56 60 wa 
 |-  ( x = [ p ] e /\ y = [ q ] e )
62 15 9 cfv 
 |-  ( dist ` r )
63 62 cof 
 |-  oF ( dist ` r )
64 54 58 63 co 
 |-  ( p oF ( dist ` r ) q )
65 cli 
 |-  ~~>
66 51 cv 
 |-  z
67 64 66 65 wbr 
 |-  ( p oF ( dist ` r ) q ) ~~> z
68 61 67 wa 
 |-  ( ( x = [ p ] e /\ y = [ q ] e ) /\ ( p oF ( dist ` r ) q ) ~~> z )
69 68 53 23 wrex 
 |-  E. q e. v ( ( x = [ p ] e /\ y = [ q ] e ) /\ ( p oF ( dist ` r ) q ) ~~> z )
70 69 52 23 wrex 
 |-  E. p e. v E. q e. v ( ( x = [ p ] e /\ y = [ q ] e ) /\ ( p oF ( dist ` r ) q ) ~~> z )
71 70 25 50 51 coprab 
 |-  { <. <. x , y >. , z >. | E. p e. v E. q e. v ( ( x = [ p ] e /\ y = [ q ] e ) /\ ( p oF ( dist ` r ) q ) ~~> z ) }
72 49 71 cop 
 |-  <. ( dist ` ndx ) , { <. <. x , y >. , z >. | E. p e. v E. q e. v ( ( x = [ p ] e /\ y = [ q ] e ) /\ ( p oF ( dist ` r ) q ) ~~> z ) } >.
73 72 csn 
 |-  { <. ( dist ` ndx ) , { <. <. x , y >. , z >. | E. p e. v E. q e. v ( ( x = [ p ] e /\ y = [ q ] e ) /\ ( p oF ( dist ` r ) q ) ~~> z ) } >. }
74 46 73 47 co 
 |-  ( ( r /s e ) sSet { <. ( dist ` ndx ) , { <. <. x , y >. , z >. | E. p e. v E. q e. v ( ( x = [ p ] e /\ y = [ q ] e ) /\ ( p oF ( dist ` r ) q ) ~~> z ) } >. } )
75 43 42 74 csb 
 |-  [_ { <. f , g >. | ( { f , g } C_ v /\ A. x e. RR+ E. j e. ZZ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( g ` j ) ( ball ` ( dist ` w ) ) x ) ) } / e ]_ ( ( r /s e ) sSet { <. ( dist ` ndx ) , { <. <. x , y >. , z >. | E. p e. v E. q e. v ( ( x = [ p ] e /\ y = [ q ] e ) /\ ( p oF ( dist ` r ) q ) ~~> z ) } >. } )
76 17 16 75 csb 
 |-  [_ ( Base ` r ) / v ]_ [_ { <. f , g >. | ( { f , g } C_ v /\ A. x e. RR+ E. j e. ZZ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( g ` j ) ( ball ` ( dist ` w ) ) x ) ) } / e ]_ ( ( r /s e ) sSet { <. ( dist ` ndx ) , { <. <. x , y >. , z >. | E. p e. v E. q e. v ( ( x = [ p ] e /\ y = [ q ] e ) /\ ( p oF ( dist ` r ) q ) ~~> z ) } >. } )
77 13 12 76 csb 
 |-  [_ ( ( w ^s NN ) |`s ( Cau ` ( dist ` w ) ) ) / r ]_ [_ ( Base ` r ) / v ]_ [_ { <. f , g >. | ( { f , g } C_ v /\ A. x e. RR+ E. j e. ZZ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( g ` j ) ( ball ` ( dist ` w ) ) x ) ) } / e ]_ ( ( r /s e ) sSet { <. ( dist ` ndx ) , { <. <. x , y >. , z >. | E. p e. v E. q e. v ( ( x = [ p ] e /\ y = [ q ] e ) /\ ( p oF ( dist ` r ) q ) ~~> z ) } >. } )
78 1 2 77 cmpt 
 |-  ( w e. _V |-> [_ ( ( w ^s NN ) |`s ( Cau ` ( dist ` w ) ) ) / r ]_ [_ ( Base ` r ) / v ]_ [_ { <. f , g >. | ( { f , g } C_ v /\ A. x e. RR+ E. j e. ZZ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( g ` j ) ( ball ` ( dist ` w ) ) x ) ) } / e ]_ ( ( r /s e ) sSet { <. ( dist ` ndx ) , { <. <. x , y >. , z >. | E. p e. v E. q e. v ( ( x = [ p ] e /\ y = [ q ] e ) /\ ( p oF ( dist ` r ) q ) ~~> z ) } >. } ) )
79 0 78 wceq 
 |-  cplMetSp = ( w e. _V |-> [_ ( ( w ^s NN ) |`s ( Cau ` ( dist ` w ) ) ) / r ]_ [_ ( Base ` r ) / v ]_ [_ { <. f , g >. | ( { f , g } C_ v /\ A. x e. RR+ E. j e. ZZ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( g ` j ) ( ball ` ( dist ` w ) ) x ) ) } / e ]_ ( ( r /s e ) sSet { <. ( dist ` ndx ) , { <. <. x , y >. , z >. | E. p e. v E. q e. v ( ( x = [ p ] e /\ y = [ q ] e ) /\ ( p oF ( dist ` r ) q ) ~~> z ) } >. } ) )