Metamath Proof Explorer

Theorem cnpwstotbnd

Description: A subset of A ^ I , where A C_ CC , is totally bounded iff it is bounded. (Contributed by Mario Carneiro, 14-Sep-2015)

Ref Expression
Hypotheses cnpwstotbnd.y 
|- Y = ( ( CCfld |`s A ) ^s I )
cnpwstotbnd.d 
|- D = ( ( dist ` Y ) |` ( X X. X ) )
Assertion cnpwstotbnd 
|- ( ( A C_ CC /\ I e. Fin ) -> ( D e. ( TotBnd ` X ) <-> D e. ( Bnd ` X ) ) )

Proof

Step Hyp Ref Expression
1 cnpwstotbnd.y 
 |-  Y = ( ( CCfld |`s A ) ^s I )
2 cnpwstotbnd.d 
 |-  D = ( ( dist ` Y ) |` ( X X. X ) )
3 eqid 
 |-  ( ( Scalar ` ( CCfld |`s A ) ) Xs_ ( I X. { ( CCfld |`s A ) } ) ) = ( ( Scalar ` ( CCfld |`s A ) ) Xs_ ( I X. { ( CCfld |`s A ) } ) )
4 eqid 
 |-  ( Base ` ( ( Scalar ` ( CCfld |`s A ) ) Xs_ ( I X. { ( CCfld |`s A ) } ) ) ) = ( Base ` ( ( Scalar ` ( CCfld |`s A ) ) Xs_ ( I X. { ( CCfld |`s A ) } ) ) )
5 eqid 
 |-  ( Base ` ( ( I X. { ( CCfld |`s A ) } ) ` x ) ) = ( Base ` ( ( I X. { ( CCfld |`s A ) } ) ` x ) )
6 eqid 
 |-  ( ( dist ` ( ( I X. { ( CCfld |`s A ) } ) ` x ) ) |` ( ( Base ` ( ( I X. { ( CCfld |`s A ) } ) ` x ) ) X. ( Base ` ( ( I X. { ( CCfld |`s A ) } ) ` x ) ) ) ) = ( ( dist ` ( ( I X. { ( CCfld |`s A ) } ) ` x ) ) |` ( ( Base ` ( ( I X. { ( CCfld |`s A ) } ) ` x ) ) X. ( Base ` ( ( I X. { ( CCfld |`s A ) } ) ` x ) ) ) )
7 eqid 
 |-  ( dist ` ( ( Scalar ` ( CCfld |`s A ) ) Xs_ ( I X. { ( CCfld |`s A ) } ) ) ) = ( dist ` ( ( Scalar ` ( CCfld |`s A ) ) Xs_ ( I X. { ( CCfld |`s A ) } ) ) )
8 fvexd 
 |-  ( ( A C_ CC /\ I e. Fin ) -> ( Scalar ` ( CCfld |`s A ) ) e. _V )
9 simpr 
 |-  ( ( A C_ CC /\ I e. Fin ) -> I e. Fin )
10 ovex 
 |-  ( CCfld |`s A ) e. _V
11 fnconstg 
 |-  ( ( CCfld |`s A ) e. _V -> ( I X. { ( CCfld |`s A ) } ) Fn I )
12 10 11 mp1i 
 |-  ( ( A C_ CC /\ I e. Fin ) -> ( I X. { ( CCfld |`s A ) } ) Fn I )
13 eqid 
 |-  ( ( dist ` ( ( Scalar ` ( CCfld |`s A ) ) Xs_ ( I X. { ( CCfld |`s A ) } ) ) ) |` ( X X. X ) ) = ( ( dist ` ( ( Scalar ` ( CCfld |`s A ) ) Xs_ ( I X. { ( CCfld |`s A ) } ) ) ) |` ( X X. X ) )
14 cnfldms 
 |-  CCfld e. MetSp
15 cnex 
 |-  CC e. _V
16 15 ssex 
 |-  ( A C_ CC -> A e. _V )
17 16 ad2antrr 
 |-  ( ( ( A C_ CC /\ I e. Fin ) /\ x e. I ) -> A e. _V )
18 ressms 
 |-  ( ( CCfld e. MetSp /\ A e. _V ) -> ( CCfld |`s A ) e. MetSp )
19 14 17 18 sylancr 
 |-  ( ( ( A C_ CC /\ I e. Fin ) /\ x e. I ) -> ( CCfld |`s A ) e. MetSp )
20 eqid 
 |-  ( Base ` ( CCfld |`s A ) ) = ( Base ` ( CCfld |`s A ) )
21 eqid 
 |-  ( ( dist ` ( CCfld |`s A ) ) |` ( ( Base ` ( CCfld |`s A ) ) X. ( Base ` ( CCfld |`s A ) ) ) ) = ( ( dist ` ( CCfld |`s A ) ) |` ( ( Base ` ( CCfld |`s A ) ) X. ( Base ` ( CCfld |`s A ) ) ) )
22 20 21 msmet 
 |-  ( ( CCfld |`s A ) e. MetSp -> ( ( dist ` ( CCfld |`s A ) ) |` ( ( Base ` ( CCfld |`s A ) ) X. ( Base ` ( CCfld |`s A ) ) ) ) e. ( Met ` ( Base ` ( CCfld |`s A ) ) ) )
23 19 22 syl 
 |-  ( ( ( A C_ CC /\ I e. Fin ) /\ x e. I ) -> ( ( dist ` ( CCfld |`s A ) ) |` ( ( Base ` ( CCfld |`s A ) ) X. ( Base ` ( CCfld |`s A ) ) ) ) e. ( Met ` ( Base ` ( CCfld |`s A ) ) ) )
24 10 fvconst2 
 |-  ( x e. I -> ( ( I X. { ( CCfld |`s A ) } ) ` x ) = ( CCfld |`s A ) )
25 24 adantl 
 |-  ( ( ( A C_ CC /\ I e. Fin ) /\ x e. I ) -> ( ( I X. { ( CCfld |`s A ) } ) ` x ) = ( CCfld |`s A ) )
26 25 fveq2d 
 |-  ( ( ( A C_ CC /\ I e. Fin ) /\ x e. I ) -> ( dist ` ( ( I X. { ( CCfld |`s A ) } ) ` x ) ) = ( dist ` ( CCfld |`s A ) ) )
27 25 fveq2d 
 |-  ( ( ( A C_ CC /\ I e. Fin ) /\ x e. I ) -> ( Base ` ( ( I X. { ( CCfld |`s A ) } ) ` x ) ) = ( Base ` ( CCfld |`s A ) ) )
28 27 sqxpeqd 
 |-  ( ( ( A C_ CC /\ I e. Fin ) /\ x e. I ) -> ( ( Base ` ( ( I X. { ( CCfld |`s A ) } ) ` x ) ) X. ( Base ` ( ( I X. { ( CCfld |`s A ) } ) ` x ) ) ) = ( ( Base ` ( CCfld |`s A ) ) X. ( Base ` ( CCfld |`s A ) ) ) )
29 26 28 reseq12d 
 |-  ( ( ( A C_ CC /\ I e. Fin ) /\ x e. I ) -> ( ( dist ` ( ( I X. { ( CCfld |`s A ) } ) ` x ) ) |` ( ( Base ` ( ( I X. { ( CCfld |`s A ) } ) ` x ) ) X. ( Base ` ( ( I X. { ( CCfld |`s A ) } ) ` x ) ) ) ) = ( ( dist ` ( CCfld |`s A ) ) |` ( ( Base ` ( CCfld |`s A ) ) X. ( Base ` ( CCfld |`s A ) ) ) ) )
30 27 fveq2d 
 |-  ( ( ( A C_ CC /\ I e. Fin ) /\ x e. I ) -> ( Met ` ( Base ` ( ( I X. { ( CCfld |`s A ) } ) ` x ) ) ) = ( Met ` ( Base ` ( CCfld |`s A ) ) ) )
31 23 29 30 3eltr4d 
 |-  ( ( ( A C_ CC /\ I e. Fin ) /\ x e. I ) -> ( ( dist ` ( ( I X. { ( CCfld |`s A ) } ) ` x ) ) |` ( ( Base ` ( ( I X. { ( CCfld |`s A ) } ) ` x ) ) X. ( Base ` ( ( I X. { ( CCfld |`s A ) } ) ` x ) ) ) ) e. ( Met ` ( Base ` ( ( I X. { ( CCfld |`s A ) } ) ` x ) ) ) )
32 totbndbnd 
 |-  ( ( ( ( dist ` ( CCfld |`s A ) ) |` ( ( Base ` ( CCfld |`s A ) ) X. ( Base ` ( CCfld |`s A ) ) ) ) |` ( y X. y ) ) e. ( TotBnd ` y ) -> ( ( ( dist ` ( CCfld |`s A ) ) |` ( ( Base ` ( CCfld |`s A ) ) X. ( Base ` ( CCfld |`s A ) ) ) ) |` ( y X. y ) ) e. ( Bnd ` y ) )
33 eqid 
 |-  ( CCfld |`s A ) = ( CCfld |`s A )
34 cnfldbas 
 |-  CC = ( Base ` CCfld )
35 33 34 ressbas2 
 |-  ( A C_ CC -> A = ( Base ` ( CCfld |`s A ) ) )
36 35 ad2antrr 
 |-  ( ( ( A C_ CC /\ I e. Fin ) /\ x e. I ) -> A = ( Base ` ( CCfld |`s A ) ) )
37 36 fveq2d 
 |-  ( ( ( A C_ CC /\ I e. Fin ) /\ x e. I ) -> ( Met ` A ) = ( Met ` ( Base ` ( CCfld |`s A ) ) ) )
38 23 37 eleqtrrd 
 |-  ( ( ( A C_ CC /\ I e. Fin ) /\ x e. I ) -> ( ( dist ` ( CCfld |`s A ) ) |` ( ( Base ` ( CCfld |`s A ) ) X. ( Base ` ( CCfld |`s A ) ) ) ) e. ( Met ` A ) )
39 eqid 
 |-  ( ( ( dist ` ( CCfld |`s A ) ) |` ( ( Base ` ( CCfld |`s A ) ) X. ( Base ` ( CCfld |`s A ) ) ) ) |` ( y X. y ) ) = ( ( ( dist ` ( CCfld |`s A ) ) |` ( ( Base ` ( CCfld |`s A ) ) X. ( Base ` ( CCfld |`s A ) ) ) ) |` ( y X. y ) )
40 39 bnd2lem 
 |-  ( ( ( ( dist ` ( CCfld |`s A ) ) |` ( ( Base ` ( CCfld |`s A ) ) X. ( Base ` ( CCfld |`s A ) ) ) ) e. ( Met ` A ) /\ ( ( ( dist ` ( CCfld |`s A ) ) |` ( ( Base ` ( CCfld |`s A ) ) X. ( Base ` ( CCfld |`s A ) ) ) ) |` ( y X. y ) ) e. ( Bnd ` y ) ) -> y C_ A )
41 40 ex 
 |-  ( ( ( dist ` ( CCfld |`s A ) ) |` ( ( Base ` ( CCfld |`s A ) ) X. ( Base ` ( CCfld |`s A ) ) ) ) e. ( Met ` A ) -> ( ( ( ( dist ` ( CCfld |`s A ) ) |` ( ( Base ` ( CCfld |`s A ) ) X. ( Base ` ( CCfld |`s A ) ) ) ) |` ( y X. y ) ) e. ( Bnd ` y ) -> y C_ A ) )
42 38 41 syl 
 |-  ( ( ( A C_ CC /\ I e. Fin ) /\ x e. I ) -> ( ( ( ( dist ` ( CCfld |`s A ) ) |` ( ( Base ` ( CCfld |`s A ) ) X. ( Base ` ( CCfld |`s A ) ) ) ) |` ( y X. y ) ) e. ( Bnd ` y ) -> y C_ A ) )
43 32 42 syl5 
 |-  ( ( ( A C_ CC /\ I e. Fin ) /\ x e. I ) -> ( ( ( ( dist ` ( CCfld |`s A ) ) |` ( ( Base ` ( CCfld |`s A ) ) X. ( Base ` ( CCfld |`s A ) ) ) ) |` ( y X. y ) ) e. ( TotBnd ` y ) -> y C_ A ) )
44 eqid 
 |-  ( ( abs o. - ) |` ( y X. y ) ) = ( ( abs o. - ) |` ( y X. y ) )
45 44 cntotbnd 
 |-  ( ( ( abs o. - ) |` ( y X. y ) ) e. ( TotBnd ` y ) <-> ( ( abs o. - ) |` ( y X. y ) ) e. ( Bnd ` y ) )
46 45 a1i 
 |-  ( ( ( ( A C_ CC /\ I e. Fin ) /\ x e. I ) /\ y C_ A ) -> ( ( ( abs o. - ) |` ( y X. y ) ) e. ( TotBnd ` y ) <-> ( ( abs o. - ) |` ( y X. y ) ) e. ( Bnd ` y ) ) )
47 36 sseq2d 
 |-  ( ( ( A C_ CC /\ I e. Fin ) /\ x e. I ) -> ( y C_ A <-> y C_ ( Base ` ( CCfld |`s A ) ) ) )
48 47 biimpa 
 |-  ( ( ( ( A C_ CC /\ I e. Fin ) /\ x e. I ) /\ y C_ A ) -> y C_ ( Base ` ( CCfld |`s A ) ) )
49 xpss12 
 |-  ( ( y C_ ( Base ` ( CCfld |`s A ) ) /\ y C_ ( Base ` ( CCfld |`s A ) ) ) -> ( y X. y ) C_ ( ( Base ` ( CCfld |`s A ) ) X. ( Base ` ( CCfld |`s A ) ) ) )
50 48 48 49 syl2anc 
 |-  ( ( ( ( A C_ CC /\ I e. Fin ) /\ x e. I ) /\ y C_ A ) -> ( y X. y ) C_ ( ( Base ` ( CCfld |`s A ) ) X. ( Base ` ( CCfld |`s A ) ) ) )
51 50 resabs1d 
 |-  ( ( ( ( A C_ CC /\ I e. Fin ) /\ x e. I ) /\ y C_ A ) -> ( ( ( dist ` ( CCfld |`s A ) ) |` ( ( Base ` ( CCfld |`s A ) ) X. ( Base ` ( CCfld |`s A ) ) ) ) |` ( y X. y ) ) = ( ( dist ` ( CCfld |`s A ) ) |` ( y X. y ) ) )
52 17 adantr 
 |-  ( ( ( ( A C_ CC /\ I e. Fin ) /\ x e. I ) /\ y C_ A ) -> A e. _V )
53 cnfldds 
 |-  ( abs o. - ) = ( dist ` CCfld )
54 33 53 ressds 
 |-  ( A e. _V -> ( abs o. - ) = ( dist ` ( CCfld |`s A ) ) )
55 52 54 syl 
 |-  ( ( ( ( A C_ CC /\ I e. Fin ) /\ x e. I ) /\ y C_ A ) -> ( abs o. - ) = ( dist ` ( CCfld |`s A ) ) )
56 55 reseq1d 
 |-  ( ( ( ( A C_ CC /\ I e. Fin ) /\ x e. I ) /\ y C_ A ) -> ( ( abs o. - ) |` ( y X. y ) ) = ( ( dist ` ( CCfld |`s A ) ) |` ( y X. y ) ) )
57 51 56 eqtr4d 
 |-  ( ( ( ( A C_ CC /\ I e. Fin ) /\ x e. I ) /\ y C_ A ) -> ( ( ( dist ` ( CCfld |`s A ) ) |` ( ( Base ` ( CCfld |`s A ) ) X. ( Base ` ( CCfld |`s A ) ) ) ) |` ( y X. y ) ) = ( ( abs o. - ) |` ( y X. y ) ) )
58 57 eleq1d 
 |-  ( ( ( ( A C_ CC /\ I e. Fin ) /\ x e. I ) /\ y C_ A ) -> ( ( ( ( dist ` ( CCfld |`s A ) ) |` ( ( Base ` ( CCfld |`s A ) ) X. ( Base ` ( CCfld |`s A ) ) ) ) |` ( y X. y ) ) e. ( TotBnd ` y ) <-> ( ( abs o. - ) |` ( y X. y ) ) e. ( TotBnd ` y ) ) )
59 57 eleq1d 
 |-  ( ( ( ( A C_ CC /\ I e. Fin ) /\ x e. I ) /\ y C_ A ) -> ( ( ( ( dist ` ( CCfld |`s A ) ) |` ( ( Base ` ( CCfld |`s A ) ) X. ( Base ` ( CCfld |`s A ) ) ) ) |` ( y X. y ) ) e. ( Bnd ` y ) <-> ( ( abs o. - ) |` ( y X. y ) ) e. ( Bnd ` y ) ) )
60 46 58 59 3bitr4d 
 |-  ( ( ( ( A C_ CC /\ I e. Fin ) /\ x e. I ) /\ y C_ A ) -> ( ( ( ( dist ` ( CCfld |`s A ) ) |` ( ( Base ` ( CCfld |`s A ) ) X. ( Base ` ( CCfld |`s A ) ) ) ) |` ( y X. y ) ) e. ( TotBnd ` y ) <-> ( ( ( dist ` ( CCfld |`s A ) ) |` ( ( Base ` ( CCfld |`s A ) ) X. ( Base ` ( CCfld |`s A ) ) ) ) |` ( y X. y ) ) e. ( Bnd ` y ) ) )
61 60 ex 
 |-  ( ( ( A C_ CC /\ I e. Fin ) /\ x e. I ) -> ( y C_ A -> ( ( ( ( dist ` ( CCfld |`s A ) ) |` ( ( Base ` ( CCfld |`s A ) ) X. ( Base ` ( CCfld |`s A ) ) ) ) |` ( y X. y ) ) e. ( TotBnd ` y ) <-> ( ( ( dist ` ( CCfld |`s A ) ) |` ( ( Base ` ( CCfld |`s A ) ) X. ( Base ` ( CCfld |`s A ) ) ) ) |` ( y X. y ) ) e. ( Bnd ` y ) ) ) )
62 43 42 61 pm5.21ndd 
 |-  ( ( ( A C_ CC /\ I e. Fin ) /\ x e. I ) -> ( ( ( ( dist ` ( CCfld |`s A ) ) |` ( ( Base ` ( CCfld |`s A ) ) X. ( Base ` ( CCfld |`s A ) ) ) ) |` ( y X. y ) ) e. ( TotBnd ` y ) <-> ( ( ( dist ` ( CCfld |`s A ) ) |` ( ( Base ` ( CCfld |`s A ) ) X. ( Base ` ( CCfld |`s A ) ) ) ) |` ( y X. y ) ) e. ( Bnd ` y ) ) )
63 29 reseq1d 
 |-  ( ( ( A C_ CC /\ I e. Fin ) /\ x e. I ) -> ( ( ( dist ` ( ( I X. { ( CCfld |`s A ) } ) ` x ) ) |` ( ( Base ` ( ( I X. { ( CCfld |`s A ) } ) ` x ) ) X. ( Base ` ( ( I X. { ( CCfld |`s A ) } ) ` x ) ) ) ) |` ( y X. y ) ) = ( ( ( dist ` ( CCfld |`s A ) ) |` ( ( Base ` ( CCfld |`s A ) ) X. ( Base ` ( CCfld |`s A ) ) ) ) |` ( y X. y ) ) )
64 63 eleq1d 
 |-  ( ( ( A C_ CC /\ I e. Fin ) /\ x e. I ) -> ( ( ( ( dist ` ( ( I X. { ( CCfld |`s A ) } ) ` x ) ) |` ( ( Base ` ( ( I X. { ( CCfld |`s A ) } ) ` x ) ) X. ( Base ` ( ( I X. { ( CCfld |`s A ) } ) ` x ) ) ) ) |` ( y X. y ) ) e. ( TotBnd ` y ) <-> ( ( ( dist ` ( CCfld |`s A ) ) |` ( ( Base ` ( CCfld |`s A ) ) X. ( Base ` ( CCfld |`s A ) ) ) ) |` ( y X. y ) ) e. ( TotBnd ` y ) ) )
65 63 eleq1d 
 |-  ( ( ( A C_ CC /\ I e. Fin ) /\ x e. I ) -> ( ( ( ( dist ` ( ( I X. { ( CCfld |`s A ) } ) ` x ) ) |` ( ( Base ` ( ( I X. { ( CCfld |`s A ) } ) ` x ) ) X. ( Base ` ( ( I X. { ( CCfld |`s A ) } ) ` x ) ) ) ) |` ( y X. y ) ) e. ( Bnd ` y ) <-> ( ( ( dist ` ( CCfld |`s A ) ) |` ( ( Base ` ( CCfld |`s A ) ) X. ( Base ` ( CCfld |`s A ) ) ) ) |` ( y X. y ) ) e. ( Bnd ` y ) ) )
66 62 64 65 3bitr4d 
 |-  ( ( ( A C_ CC /\ I e. Fin ) /\ x e. I ) -> ( ( ( ( dist ` ( ( I X. { ( CCfld |`s A ) } ) ` x ) ) |` ( ( Base ` ( ( I X. { ( CCfld |`s A ) } ) ` x ) ) X. ( Base ` ( ( I X. { ( CCfld |`s A ) } ) ` x ) ) ) ) |` ( y X. y ) ) e. ( TotBnd ` y ) <-> ( ( ( dist ` ( ( I X. { ( CCfld |`s A ) } ) ` x ) ) |` ( ( Base ` ( ( I X. { ( CCfld |`s A ) } ) ` x ) ) X. ( Base ` ( ( I X. { ( CCfld |`s A ) } ) ` x ) ) ) ) |` ( y X. y ) ) e. ( Bnd ` y ) ) )
67 3 4 5 6 7 8 9 12 13 31 66 prdsbnd2 
 |-  ( ( A C_ CC /\ I e. Fin ) -> ( ( ( dist ` ( ( Scalar ` ( CCfld |`s A ) ) Xs_ ( I X. { ( CCfld |`s A ) } ) ) ) |` ( X X. X ) ) e. ( TotBnd ` X ) <-> ( ( dist ` ( ( Scalar ` ( CCfld |`s A ) ) Xs_ ( I X. { ( CCfld |`s A ) } ) ) ) |` ( X X. X ) ) e. ( Bnd ` X ) ) )
68 eqid 
 |-  ( Scalar ` ( CCfld |`s A ) ) = ( Scalar ` ( CCfld |`s A ) )
69 1 68 pwsval 
 |-  ( ( ( CCfld |`s A ) e. _V /\ I e. Fin ) -> Y = ( ( Scalar ` ( CCfld |`s A ) ) Xs_ ( I X. { ( CCfld |`s A ) } ) ) )
70 10 9 69 sylancr 
 |-  ( ( A C_ CC /\ I e. Fin ) -> Y = ( ( Scalar ` ( CCfld |`s A ) ) Xs_ ( I X. { ( CCfld |`s A ) } ) ) )
71 70 fveq2d 
 |-  ( ( A C_ CC /\ I e. Fin ) -> ( dist ` Y ) = ( dist ` ( ( Scalar ` ( CCfld |`s A ) ) Xs_ ( I X. { ( CCfld |`s A ) } ) ) ) )
72 71 reseq1d 
 |-  ( ( A C_ CC /\ I e. Fin ) -> ( ( dist ` Y ) |` ( X X. X ) ) = ( ( dist ` ( ( Scalar ` ( CCfld |`s A ) ) Xs_ ( I X. { ( CCfld |`s A ) } ) ) ) |` ( X X. X ) ) )
73 2 72 syl5eq 
 |-  ( ( A C_ CC /\ I e. Fin ) -> D = ( ( dist ` ( ( Scalar ` ( CCfld |`s A ) ) Xs_ ( I X. { ( CCfld |`s A ) } ) ) ) |` ( X X. X ) ) )
74 73 eleq1d 
 |-  ( ( A C_ CC /\ I e. Fin ) -> ( D e. ( TotBnd ` X ) <-> ( ( dist ` ( ( Scalar ` ( CCfld |`s A ) ) Xs_ ( I X. { ( CCfld |`s A ) } ) ) ) |` ( X X. X ) ) e. ( TotBnd ` X ) ) )
75 73 eleq1d 
 |-  ( ( A C_ CC /\ I e. Fin ) -> ( D e. ( Bnd ` X ) <-> ( ( dist ` ( ( Scalar ` ( CCfld |`s A ) ) Xs_ ( I X. { ( CCfld |`s A ) } ) ) ) |` ( X X. X ) ) e. ( Bnd ` X ) ) )
76 67 74 75 3bitr4d 
 |-  ( ( A C_ CC /\ I e. Fin ) -> ( D e. ( TotBnd ` X ) <-> D e. ( Bnd ` X ) ) )