P. 232 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 23101-23200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lmclim 23101	Relate a limit on the metric space of complex numbers to our complex number limit notation. (Contributed by NM, 9-Dec-2006.) (Revised by Mario Carneiro, 1-May-2014.)
|- J = ( TopOpen ` ℂfld )   &    |- Z = ( ZZ>= ` M )   =>    |- ( ( M e. ZZ /\ Z C_ dom F ) -> ( F ( ~~> t ` J ) P <-> ( F e. ( CC ^pm CC ) /\ F ~~> P ) ) )
Theorem	lmclimf 23102	Relate a limit on the metric space of complex numbers to our complex number limit notation. (Contributed by NM, 24-Jul-2007.) (Revised by Mario Carneiro, 1-May-2014.)
|- J = ( TopOpen ` ℂfld )   &    |- Z = ( ZZ>= ` M )   =>    |- ( ( M e. ZZ /\ F : Z --> CC ) -> ( F ( ~~> t ` J ) P <-> F ~~> P ) )
Theorem	metelcls 23103*	A point belongs to the closure of a subset iff there is a sequence in the subset converging to it. Theorem 1.4-6(a) of [Kreyszig] p. 30. This proof uses countable choice ax-cc 9257. The statement can be generalized to first-countable spaces, not just metrizable spaces. (Contributed by NM, 8-Nov-2007.) (Proof shortened by Mario Carneiro, 1-May-2015.)
|- J = ( MetOpen ` D )   &    |- ( ph -> D e. ( *Met ` X ) )   &    |- ( ph -> S C_ X )   =>    |- ( ph -> ( P e. ( ( cls ` J ) ` S ) <-> E. f ( f : NN --> S /\ f ( ~~> t ` J ) P ) ) )
Theorem	metcld 23104*	A subset of a metric space is closed iff every convergent sequence on it converges to a point in the subset. Theorem 1.4-6(b) of [Kreyszig] p. 30. (Contributed by NM, 11-Nov-2007.) (Revised by Mario Carneiro, 1-May-2014.)
|- J = ( MetOpen ` D )   =>    |- ( ( D e. ( *Met ` X ) /\ S C_ X ) -> ( S e. ( Clsd ` J ) <-> A. x A. f ( ( f : NN --> S /\ f ( ~~> t ` J ) x ) -> x e. S ) ) )
Theorem	metcld2 23105	A subset of a metric space is closed iff every convergent sequence on it converges to a point in the subset. Theorem 1.4-6(b) of [Kreyszig] p. 30. (Contributed by Mario Carneiro, 1-May-2014.)
|- J = ( MetOpen ` D )   =>    |- ( ( D e. ( *Met ` X ) /\ S C_ X ) -> ( S e. ( Clsd ` J ) <-> ( ( ~~> t ` J ) " ( S ^m NN ) ) C_ S ) )
Theorem	caubl 23106*	Sufficient condition to ensure a sequence of nested balls is Cauchy. (Contributed by Mario Carneiro, 18-Jan-2014.) (Revised by Mario Carneiro, 1-May-2014.)
|- ( ph -> D e. ( *Met ` X ) )   &    |- ( ph -> F : NN --> ( X X. RR+ ) )   &    |- ( ph -> A. n e. NN ( ( ball ` D ) ` ( F ` ( n + 1 ) ) ) C_ ( ( ball ` D ) ` ( F ` n ) ) )   &    |- ( ph -> A. r e. RR+ E. n e. NN ( 2nd ` ( F ` n ) ) < r )   =>    |- ( ph -> ( 1st o. F ) e. ( Cau ` D ) )
Theorem	caublcls 23107*	The convergent point of a sequence of nested balls is in the closures of any of the balls (i.e. it is in the intersection of the closures). Indeed, it is the only point in the intersection because a metric space is Hausdorff, but we don't prove this here. (Contributed by Mario Carneiro, 21-Jan-2014.) (Revised by Mario Carneiro, 1-May-2014.)
|- ( ph -> D e. ( *Met ` X ) )   &    |- ( ph -> F : NN --> ( X X. RR+ ) )   &    |- ( ph -> A. n e. NN ( ( ball ` D ) ` ( F ` ( n + 1 ) ) ) C_ ( ( ball ` D ) ` ( F ` n ) ) )   &    |- J = ( MetOpen ` D )   =>    |- ( ( ph /\ ( 1st o. F ) ( ~~> t ` J ) P /\ A e. NN ) -> P e. ( ( cls ` J ) ` ( ( ball ` D ) ` ( F ` A ) ) ) )
Theorem	metcnp4 23108*	Two ways to say a mapping from metric C to metric D is continuous at point P. Theorem 14-4.3 of [Gleason] p. 240. (Contributed by NM, 17-May-2007.) (Revised by Mario Carneiro, 4-May-2014.)
|- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   &    |- ( ph -> C e. ( *Met ` X ) )   &    |- ( ph -> D e. ( *Met ` Y ) )   &    |- ( ph -> P e. X )   =>    |- ( ph -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. f ( ( f : NN --> X /\ f ( ~~> t ` J ) P ) -> ( F o. f ) ( ~~> t ` K ) ( F ` P ) ) ) ) )
Theorem	metcn4 23109*	Two ways to say a mapping from metric C to metric D is continuous. Theorem 10.3 of [Munkres] p. 128. (Contributed by NM, 13-Jun-2007.) (Revised by Mario Carneiro, 4-May-2014.)
|- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   &    |- ( ph -> C e. ( *Met ` X ) )   &    |- ( ph -> D e. ( *Met ` Y ) )   &    |- ( ph -> F : X --> Y )   =>    |- ( ph -> ( F e. ( J Cn K ) <-> A. f ( f : NN --> X -> A. x ( f ( ~~> t ` J ) x -> ( F o. f ) ( ~~> t ` K ) ( F ` x ) ) ) ) )
Theorem	iscmet3i 23110*	Properties that determine a complete metric space. (Contributed by NM, 15-Apr-2007.) (Revised by Mario Carneiro, 5-May-2014.)
|- J = ( MetOpen ` D )   &    |- D e. ( Met ` X )   &    |- ( ( f e. ( Cau ` D ) /\ f : NN --> X ) -> f e. dom ( ~~> t ` J ) )   =>    |- D e. ( CMet ` X )
Theorem	lmcau 23111	Every convergent sequence in a metric space is a Cauchy sequence. Theorem 1.4-5 of [Kreyszig] p. 28. (Contributed by NM, 29-Jan-2008.) (Proof shortened by Mario Carneiro, 5-May-2014.)
|- J = ( MetOpen ` D )   =>    |- ( D e. ( *Met ` X ) -> dom ( ~~> t ` J ) C_ ( Cau ` D ) )
Theorem	flimcfil 23112	Every convergent filter in a metric space is a Cauchy filter. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- J = ( MetOpen ` D )   =>    |- ( ( D e. ( *Met ` X ) /\ A e. ( J fLim F ) ) -> F e. (CauFil ` D ) )
Theorem	cmetss 23113	A subspace of a complete metric space is complete iff it is closed in the parent space. Theorem 1.4-7 of [Kreyszig] p. 30. (Contributed by NM, 28-Jan-2008.) (Revised by Mario Carneiro, 15-Oct-2015.)
|- J = ( MetOpen ` D )   =>    |- ( D e. ( CMet ` X ) -> ( ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) <-> Y e. ( Clsd ` J ) ) )
Theorem	equivcmet 23114*	If two metrics are strongly equivalent, one is complete iff the other is. Unlike equivcau 23098, metss2 22317, this theorem does not have a one-directional form - it is possible for a metric C that is strongly finer than the complete metric D to be incomplete and vice versa. Consider D = the metric on RR induced by the usual homeomorphism from ( 0 , 1 ) against the usual metric C on RR and against the discrete metric E on RR. Then both C and E are complete but D is not, and C is strongly finer than D, which is strongly finer than E. (Contributed by Mario Carneiro, 15-Sep-2015.)
|- ( ph -> C e. ( Met ` X ) )   &    |- ( ph -> D e. ( Met ` X ) )   &    |- ( ph -> R e. RR+ )   &    |- ( ph -> S e. RR+ )   &    |- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x C y ) <_ ( R x. ( x D y ) ) )   &    |- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x D y ) <_ ( S x. ( x C y ) ) )   =>    |- ( ph -> ( C e. ( CMet ` X ) <-> D e. ( CMet ` X ) ) )
Theorem	relcmpcmet 23115*	If D is a metric space such that all the balls of some fixed size are relatively compact, then D is complete. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- J = ( MetOpen ` D )   &    |- ( ph -> D e. ( Met ` X ) )   &    |- ( ph -> R e. RR+ )   &    |- ( ( ph /\ x e. X ) -> ( J ↾t ( ( cls ` J ) ` ( x ( ball ` D ) R ) ) ) e. Comp )   =>    |- ( ph -> D e. ( CMet ` X ) )
Theorem	cmpcmet 23116	A compact metric space is complete. One half of heibor 33620. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- J = ( MetOpen ` D )   &    |- ( ph -> D e. ( Met ` X ) )   &    |- ( ph -> J e. Comp )   =>    |- ( ph -> D e. ( CMet ` X ) )
Theorem	cfilucfil3 23117	Given a metric D and a uniform structure generated by that metric, Cauchy filter bases on that uniform structure are exactly the Cauchy filters for the metric. (Contributed by Thierry Arnoux, 15-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
|- ( ( X =/= (/) /\ D e. ( *Met ` X ) ) -> ( ( C e. ( Fil ` X ) /\ C e. (CauFilu ` (metUnif ` D ) ) ) <-> C e. (CauFil ` D ) ) )
Theorem	cfilucfil4 23118	Given a metric D and a uniform structure generated by that metric, Cauchy filter bases on that uniform structure are exactly the Cauchy filters for the metric. (Contributed by Thierry Arnoux, 15-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
|- ( ( X =/= (/) /\ D e. ( *Met ` X ) /\ C e. ( Fil ` X ) ) -> ( C e. (CauFilu ` (metUnif ` D ) ) <-> C e. (CauFil ` D ) ) )
Theorem	cncmet 23119	The set of complex numbers is a complete metric space under the absolute value metric. (Contributed by NM, 20-Dec-2006.) (Revised by Mario Carneiro, 15-Oct-2015.)
|- D = ( abs o. - )   =>    |- D e. ( CMet ` CC )
Theorem	recmet 23120	The real numbers are a complete metric space. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.)
|- ( ( abs o. - ) |` ( RR X. RR ) ) e. ( CMet ` RR )
12.5.6  Baire's Category Theorem
Theorem	bcthlem1 23121*	Lemma for bcth 23126. Substitutions for the function F. (Contributed by Mario Carneiro, 9-Jan-2014.)
|- J = ( MetOpen ` D )   &    |- ( ph -> D e. ( CMet ` X ) )   &    |- F = ( k e. NN , z e. ( X X. RR+ ) |-> { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) } )   =>    |- ( ( ph /\ ( A e. NN /\ B e. ( X X. RR+ ) ) ) -> ( C e. ( A F B ) <-> ( C e. ( X X. RR+ ) /\ ( 2nd ` C ) < ( 1 / A ) /\ ( ( cls ` J ) ` ( ( ball ` D ) ` C ) ) C_ ( ( ( ball ` D ) ` B ) \ ( M ` A ) ) ) ) )
Theorem	bcthlem2 23122*	Lemma for bcth 23126. The balls in the sequence form an inclusion chain. (Contributed by Mario Carneiro, 7-Jan-2014.)
|- J = ( MetOpen ` D )   &    |- ( ph -> D e. ( CMet ` X ) )   &    |- F = ( k e. NN , z e. ( X X. RR+ ) |-> { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) } )   &    |- ( ph -> M : NN --> ( Clsd ` J ) )   &    |- ( ph -> R e. RR+ )   &    |- ( ph -> C e. X )   &    |- ( ph -> g : NN --> ( X X. RR+ ) )   &    |- ( ph -> ( g ` 1 ) = <. C , R >. )   &    |- ( ph -> A. k e. NN ( g ` ( k + 1 ) ) e. ( k F ( g ` k ) ) )   =>    |- ( ph -> A. n e. NN ( ( ball ` D ) ` ( g ` ( n + 1 ) ) ) C_ ( ( ball ` D ) ` ( g ` n ) ) )
Theorem	bcthlem3 23123*	Lemma for bcth 23126. The limit point of the centers in the sequence is in the intersection of every ball in the sequence. (Contributed by Mario Carneiro, 7-Jan-2014.)
|- J = ( MetOpen ` D )   &    |- ( ph -> D e. ( CMet ` X ) )   &    |- F = ( k e. NN , z e. ( X X. RR+ ) |-> { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) } )   &    |- ( ph -> M : NN --> ( Clsd ` J ) )   &    |- ( ph -> R e. RR+ )   &    |- ( ph -> C e. X )   &    |- ( ph -> g : NN --> ( X X. RR+ ) )   &    |- ( ph -> ( g ` 1 ) = <. C , R >. )   &    |- ( ph -> A. k e. NN ( g ` ( k + 1 ) ) e. ( k F ( g ` k ) ) )   =>    |- ( ( ph /\ ( 1st o. g ) ( ~~> t ` J ) x /\ A e. NN ) -> x e. ( ( ball ` D ) ` ( g ` A ) ) )
Theorem	bcthlem4 23124*	Lemma for bcth 23126. Given any open ball ( C ( ball ` D ) R ) as starting point (and in particular, a ball in int ( U. ran M )), the limit point x of the centers of the induced sequence of balls g is outside U. ran M. Note that a set A has empty interior iff every nonempty open set U contains points outside A, i.e. ( U \ A ) =/= (/). (Contributed by Mario Carneiro, 7-Jan-2014.)
|- J = ( MetOpen ` D )   &    |- ( ph -> D e. ( CMet ` X ) )   &    |- F = ( k e. NN , z e. ( X X. RR+ ) |-> { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) } )   &    |- ( ph -> M : NN --> ( Clsd ` J ) )   &    |- ( ph -> R e. RR+ )   &    |- ( ph -> C e. X )   &    |- ( ph -> g : NN --> ( X X. RR+ ) )   &    |- ( ph -> ( g ` 1 ) = <. C , R >. )   &    |- ( ph -> A. k e. NN ( g ` ( k + 1 ) ) e. ( k F ( g ` k ) ) )   =>    |- ( ph -> ( ( C ( ball ` D ) R ) \ U. ran M ) =/= (/) )
Theorem	bcthlem5 23125*	Lemma for bcth 23126. The proof makes essential use of the Axiom of Dependent Choice axdc4uz 12783, which in the form used here accepts a "selection" function F from each element of K to a nonempty subset of K, and the result function g maps g ( n + 1 ) to an element of F ( n , g ( n ) ). The trick here is thus in the choice of F and K: we let K be the set of all tagged nonempty open sets (tagged here meaning that we have a point and an open set, in an ordered pair), and F ( k , <. x , z >. ) gives the set of all balls of size less than 1 / k, tagged by their centers, whose closures fit within the given open set z and miss M ( k ). Since M ( k ) is closed, z \ M ( k ) is open and also nonempty, since z is nonempty and M ( k ) has empty interior. Then there is some ball contained in it, and hence our function F is valid (it never maps to the empty set). Now starting at a point in the interior of U. ran M, DC gives us the function g all whose elements are constrained by F acting on the previous value. (This is all proven in this lemma.) Now g is a sequence of tagged open balls, forming an inclusion chain (see bcthlem2 23122) and whose sizes tend to zero, since they are bounded above by 1 / k. Thus, the centers of these balls form a Cauchy sequence, and converge to a point x (see bcthlem4 23124). Since the inclusion chain also ensures the closure of each ball is in the previous ball, the point x must be in all these balls (see bcthlem3 23123) and hence misses each M ( k ), contradicting the fact that x is in the interior of U. ran M (which was the starting point). (Contributed by Mario Carneiro, 6-Jan-2014.)
|- J = ( MetOpen ` D )   &    |- ( ph -> D e. ( CMet ` X ) )   &    |- F = ( k e. NN , z e. ( X X. RR+ ) |-> { <. x , r >. | ( ( x e. X /\ r e. RR+ ) /\ ( r < ( 1 / k ) /\ ( ( cls ` J ) ` ( x ( ball ` D ) r ) ) C_ ( ( ( ball ` D ) ` z ) \ ( M ` k ) ) ) ) } )   &    |- ( ph -> M : NN --> ( Clsd ` J ) )   &    |- ( ph -> A. k e. NN ( ( int ` J ) ` ( M ` k ) ) = (/) )   =>    |- ( ph -> ( ( int ` J ) ` U. ran M ) = (/) )
Theorem	bcth 23126*	Baire's Category Theorem. If a nonempty metric space is complete, it is nonmeager in itself. In other words, no open set in the metric space can be the countable union of rare closed subsets (where rare means having a closure with empty interior), so some subset M ` k must have a nonempty interior. Theorem 4.7-2 of [Kreyszig] p. 247. (The terminology "meager" and "nonmeager" is used by Kreyszig to replace Baire's "of the first category" and "of the second category." The latter terms are going out of favor to avoid confusion with category theory.) See bcthlem5 23125 for an overview of the proof. (Contributed by NM, 28-Oct-2007.) (Proof shortened by Mario Carneiro, 6-Jan-2014.)
|- J = ( MetOpen ` D )   =>    |- ( ( D e. ( CMet ` X ) /\ M : NN --> ( Clsd ` J ) /\ ( ( int ` J ) ` U. ran M ) =/= (/) ) -> E. k e. NN ( ( int ` J ) ` ( M ` k ) ) =/= (/) )
Theorem	bcth2 23127*	Baire's Category Theorem, version 2: If countably many closed sets cover X, then one of them has an interior. (Contributed by Mario Carneiro, 10-Jan-2014.)
|- J = ( MetOpen ` D )   =>    |- ( ( ( D e. ( CMet ` X ) /\ X =/= (/) ) /\ ( M : NN --> ( Clsd ` J ) /\ U. ran M = X ) ) -> E. k e. NN ( ( int ` J ) ` ( M ` k ) ) =/= (/) )
Theorem	bcth3 23128*	Baire's Category Theorem, version 3: The intersection of countably many dense open sets is dense. (Contributed by Mario Carneiro, 10-Jan-2014.)
|- J = ( MetOpen ` D )   =>    |- ( ( D e. ( CMet ` X ) /\ M : NN --> J /\ A. k e. NN ( ( cls ` J ) ` ( M ` k ) ) = X ) -> ( ( cls ` J ) ` |^| ran M ) = X )
12.5.7  Banach spaces and subcomplex Hilbert spaces
Syntax	ccms 23129	Extend class notation with the class of all complete normed groups.
class CMetSp
Syntax	cbn 23130	Extend class notation with the class of all Banach spaces.
class Ban
Syntax	chl 23131	Extend class notation with the class of all subcomplex Hilbert spaces.
class CHil
Definition	df-cms 23132*	Define the class of all complete metric spaces. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- CMetSp = { w e. MetSp | [. ( Base ` w ) / b ]. ( ( dist ` w ) |` ( b X. b ) ) e. ( CMet ` b ) }
Definition	df-bn 23133	Define the class of all Banach spaces. A Banach space is a normed vector space such that both the vector space and the scalar field are complete under their respective norm-induced metrics. (Contributed by NM, 5-Dec-2006.) (Revised by Mario Carneiro, 15-Oct-2015.)
|- Ban = { w e. (NrmVec i^i CMetSp ) | (Scalar ` w ) e. CMetSp }
Definition	df-hl 23134	Define the class of all subcomplex Hilbert spaces. A subcomplex Hilbert space is a Banach space which is also an inner product space over a quadratically closed subfield of the field of complex numbers. (Contributed by Steve Rodriguez, 28-Apr-2007.)
|- CHil = (Ban i^i CPreHil )
Theorem	isbn 23135	A Banach space is a normed vector space with a complete induced metric. (Contributed by NM, 5-Dec-2006.) (Revised by Mario Carneiro, 15-Oct-2015.)
|- F = (Scalar ` W )   =>    |- ( W e. Ban <-> ( W e. NrmVec /\ W e. CMetSp /\ F e. CMetSp ) )
Theorem	bnsca 23136	The scalar field of a Banach space is complete. (Contributed by NM, 8-Sep-2007.) (Revised by Mario Carneiro, 15-Oct-2015.)
|- F = (Scalar ` W )   =>    |- ( W e. Ban -> F e. CMetSp )
Theorem	bnnvc 23137	A Banach space is a normed vector space. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- ( W e. Ban -> W e. NrmVec )
Theorem	bnnlm 23138	A Banach space is a normed module. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- ( W e. Ban -> W e. NrmMod )
Theorem	bnngp 23139	A Banach space is a normed group. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- ( W e. Ban -> W e. NrmGrp )
Theorem	bnlmod 23140	A Banach space is a left module. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- ( W e. Ban -> W e. LMod )
Theorem	bncms 23141	A Banach space is a complete metric space. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- ( W e. Ban -> W e. CMetSp )
Theorem	iscms 23142	A complete metric space is a metric space with a complete metric. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- X = ( Base ` M )   &    |- D = ( ( dist ` M ) |` ( X X. X ) )   =>    |- ( M e. CMetSp <-> ( M e. MetSp /\ D e. ( CMet ` X ) ) )
Theorem	cmscmet 23143	The induced metric on a complete normed group is complete. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- X = ( Base ` M )   &    |- D = ( ( dist ` M ) |` ( X X. X ) )   =>    |- ( M e. CMetSp -> D e. ( CMet ` X ) )
Theorem	bncmet 23144	The induced metric on Banach space is complete. (Contributed by NM, 8-Sep-2007.) (Revised by Mario Carneiro, 15-Oct-2015.)
|- X = ( Base ` M )   &    |- D = ( ( dist ` M ) |` ( X X. X ) )   =>    |- ( M e. Ban -> D e. ( CMet ` X ) )
Theorem	cmsms 23145	A complete metric space is a metric space. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- ( G e. CMetSp -> G e. MetSp )
Theorem	cmspropd 23146	Property deduction for a complete metric space. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ph -> ( ( dist ` K ) |` ( B X. B ) ) = ( ( dist ` L ) |` ( B X. B ) ) )   &    |- ( ph -> ( TopOpen ` K ) = ( TopOpen ` L ) )   =>    |- ( ph -> ( K e. CMetSp <-> L e. CMetSp ) )
Theorem	cmsss 23147	The restriction of a complete metric space is complete iff it is closed. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- K = ( M ↾s A )   &    |- X = ( Base ` M )   &    |- J = ( TopOpen ` M )   =>    |- ( ( M e. CMetSp /\ A C_ X ) -> ( K e. CMetSp <-> A e. ( Clsd ` J ) ) )
Theorem	lssbn 23148	A subspace of a Banach space is a Banach space iff it is closed. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- X = ( W ↾s U )   &    |- S = ( LSubSp ` W )   &    |- J = ( TopOpen ` W )   =>    |- ( ( W e. Ban /\ U e. S ) -> ( X e. Ban <-> U e. ( Clsd ` J ) ) )
Theorem	cmetcusp1 23149	If the uniform set of a complete metric space is the uniform structure generated by its metric, then it is a complete uniform space. (Contributed by Thierry Arnoux, 15-Dec-2017.)
|- X = ( Base ` F )   &    |- D = ( ( dist ` F ) |` ( X X. X ) )   &    |- U = (UnifSt ` F )   =>    |- ( ( X =/= (/) /\ F e. CMetSp /\ U = (metUnif ` D ) ) -> F e. CUnifSp )
Theorem	cmetcusp 23150	The uniform space generated by a complete metric is a complete uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.)
|- ( ( X =/= (/) /\ D e. ( CMet ` X ) ) -> (toUnifSp ` (metUnif ` D ) ) e. CUnifSp )
Theorem	cncms 23151	The field of complex numbers is a complete metric space. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- ℂfld e. CMetSp
Theorem	cnflduss 23152	The uniform structure of the complex numbers. (Contributed by Thierry Arnoux, 17-Dec-2017.) (Revised by Thierry Arnoux, 11-Mar-2018.)
|- U = (UnifSt ` ℂfld )   =>    |- U = (metUnif ` ( abs o. - ) )
Theorem	cnfldcusp 23153	The field of complex numbers is a complete uniform space. (Contributed by Thierry Arnoux, 17-Dec-2017.)
|- ℂfld e. CUnifSp
Theorem	resscdrg 23154	The real numbers are a subset of any complete subfield in the complex numbers. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- F = (ℂfld ↾s K )   =>    |- ( ( K e. (SubRing ` ℂfld ) /\ F e. DivRing /\ F e. CMetSp ) -> RR C_ K )
Theorem	cncdrg 23155	The only complete subfields of the complex numbers are RR and CC. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- F = (ℂfld ↾s K )   =>    |- ( ( K e. (SubRing ` ℂfld ) /\ F e. DivRing /\ F e. CMetSp ) -> K e. { RR , CC } )
Theorem	srabn 23156	The subring algebra over a complete normed ring is a Banach space iff the subring is a closed division ring. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- A = ( (subringAlg ` W ) ` S )   &    |- J = ( TopOpen ` W )   =>    |- ( ( W e. NrmRing /\ W e. CMetSp /\ S e. (SubRing ` W ) ) -> ( A e. Ban <-> ( S e. ( Clsd ` J ) /\ ( W ↾s S ) e. DivRing ) ) )
Theorem	rlmbn 23157	The ring module over a complete normed division ring is a Banach space. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- ( ( R e. NrmRing /\ R e. DivRing /\ R e. CMetSp ) -> (ringLMod ` R ) e. Ban )
Theorem	ishl 23158	The predicate "is a subcomplex Hilbert space." A Hilbert space is a Banach space which is also an inner product space, i.e. whose norm satisfies the parallelogram law. (Contributed by Steve Rodriguez, 28-Apr-2007.) (Revised by Mario Carneiro, 15-Oct-2015.)
|- ( W e. CHil <-> ( W e. Ban /\ W e. CPreHil ) )
Theorem	hlbn 23159	Every subcomplex Hilbert space is a Banach space. (Contributed by Steve Rodriguez, 28-Apr-2007.)
|- ( W e. CHil -> W e. Ban )
Theorem	hlcph 23160	Every subcomplex Hilbert space is a subcomplex pre-Hilbert space. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- ( W e. CHil -> W e. CPreHil )
Theorem	hlphl 23161	Every subcomplex Hilbert space is an inner product space (also called a pre-Hilbert space). (Contributed by NM, 28-Apr-2007.) (Revised by Mario Carneiro, 15-Oct-2015.)
|- ( W e. CHil -> W e. PreHil )
Theorem	hlcms 23162	Every subcomplex Hilbert space is a complete metric space. (Contributed by Mario Carneiro, 17-Oct-2015.)
|- ( W e. CHil -> W e. CMetSp )
Theorem	hlprlem 23163	Lemma for hlpr 23165. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( W e. CHil -> ( K e. (SubRing ` ℂfld ) /\ (ℂfld ↾s K ) e. DivRing /\ (ℂfld ↾s K ) e. CMetSp ) )
Theorem	hlress 23164	The scalar field of a subcomplex Hilbert space contains RR. (Contributed by Mario Carneiro, 8-Oct-2015.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( W e. CHil -> RR C_ K )
Theorem	hlpr 23165	The scalar field of a subcomplex Hilbert space is either RR or CC. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( W e. CHil -> K e. { RR , CC } )
Theorem	ishl2 23166	A Hilbert space is a complete subcomplex pre-Hilbert space over RR or CC. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( W e. CHil <-> ( W e. CMetSp /\ W e. CPreHil /\ K e. { RR , CC } ) )
12.5.7.1  The complete ordered field of the real numbers
Theorem	retopn 23167	The topology of the real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019.)
|- ( topGen ` ran (,) ) = ( TopOpen ` RRfld )
Theorem	recms 23168	The real numbers form a complete metric space. (Contributed by Thierry Arnoux, 1-Nov-2017.)
|- RRfld e. CMetSp
Theorem	reust 23169	The Uniform structure of the real numbers. (Contributed by Thierry Arnoux, 14-Feb-2018.)
|- (UnifSt ` RRfld ) = (metUnif ` ( ( dist ` RRfld ) |` ( RR X. RR ) ) )
Theorem	recusp 23170	The real numbers form a complete uniform space. (Contributed by Thierry Arnoux, 17-Dec-2017.)
|- RRfld e. CUnifSp
12.5.8  Euclidean spaces
Syntax	crrx 23171	Extend class notation with generalized real Euclidean spaces.
class ℝ^
Syntax	cehl 23172	Extend class notation with real Euclidean spaces.
class 𝔼hil
Definition	df-rrx 23173	Define the function associating with a set the free real vector space on that set, equipped with the natural inner product. This is the direct sum of copies of the field of real numbers indexed by that set. We call it here a "generalized real Euclidean space", but note that it need not be complete (for instance if the given set is infinite countable). (Contributed by Thierry Arnoux, 16-Jun-2019.)
|- ℝ^ = ( i e. _V |-> (toCHil ` (RRfld freeLMod i ) ) )
Definition	df-ehl 23174	Define a function generating the real Euclidean spaces of finite dimension. The case n = 0 corresponds to a space of dimension 0, that is, limited to a neutral element. Members of this family of spaces are Hilbert spaces, as shown in - ehlhl . (Contributed by Thierry Arnoux, 16-Jun-2019.)
|- 𝔼hil = ( n e. NN0 |-> (ℝ^ ` ( 1 ... n ) ) )
Theorem	rrxval 23175	Value of the generalized Euclidean space. (Contributed by Thierry Arnoux, 16-Jun-2019.)
|- H = (ℝ^ ` I )   =>    |- ( I e. V -> H = (toCHil ` (RRfld freeLMod I ) ) )
Theorem	rrxbase 23176*	The base of the generalized real Euclidean space is the set of functions with finite support. (Contributed by Thierry Arnoux, 16-Jun-2019.) (Proof shortened by AV, 22-Jul-2019.)
|- H = (ℝ^ ` I )   &    |- B = ( Base ` H )   =>    |- ( I e. V -> B = { f e. ( RR ^m I ) | f finSupp 0 } )
Theorem	rrxprds 23177	Expand the definition of the generalized real Euclidean spaces. (Contributed by Thierry Arnoux, 16-Jun-2019.)
|- H = (ℝ^ ` I )   &    |- B = ( Base ` H )   =>    |- ( I e. V -> H = (toCHil ` ( (RRfld X_s ( I X. { ( (subringAlg ` RRfld ) ` RR ) } ) ) ↾s B ) ) )
Theorem	rrxip 23178*	The inner product of the generalized real Euclidean spaces. (Contributed by Thierry Arnoux, 16-Jun-2019.)
|- H = (ℝ^ ` I )   &    |- B = ( Base ` H )   =>    |- ( I e. V -> ( f e. ( RR ^m I ) , g e. ( RR ^m I ) |-> (RRfld gsumg ( x e. I |-> ( ( f ` x ) x. ( g ` x ) ) ) ) ) = ( .i ` H ) )
Theorem	rrxnm 23179*	The norm of the generalized real Euclidean spaces. (Contributed by Thierry Arnoux, 16-Jun-2019.)
|- H = (ℝ^ ` I )   &    |- B = ( Base ` H )   =>    |- ( I e. V -> ( f e. B |-> ( sqr ` (RRfld gsumg ( x e. I |-> ( ( f ` x ) ^ 2 ) ) ) ) ) = ( norm ` H ) )
Theorem	rrxcph 23180	Generalized Euclidean real spaces are pre-Hilbert spaces. (Contributed by Thierry Arnoux, 23-Jun-2019.) (Proof shortened by AV, 22-Jul-2019.)
|- H = (ℝ^ ` I )   &    |- B = ( Base ` H )   =>    |- ( I e. V -> H e. CPreHil )
Theorem	rrxds 23181*	The distance over generalized Euclidean spaces. Compare with df-rrn 33625. (Contributed by Thierry Arnoux, 20-Jun-2019.) (Proof shortened by AV, 20-Jul-2019.)
|- H = (ℝ^ ` I )   &    |- B = ( Base ` H )   =>    |- ( I e. V -> ( f e. B , g e. B |-> ( sqr ` (RRfld gsumg ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) ) ) ) = ( dist ` H ) )
Theorem	csbren 23182*	Cauchy-Schwarz-Bunjakovsky inequality for R^n. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 4-Jun-2014.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. RR )   &    |- ( ( ph /\ k e. A ) -> C e. RR )   =>    |- ( ph -> ( sum_ k e. A ( B x. C ) ^ 2 ) <_ ( sum_ k e. A ( B ^ 2 ) x. sum_ k e. A ( C ^ 2 ) ) )
Theorem	trirn 23183*	Triangle inequality in R^n. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 4-Jun-2014.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. RR )   &    |- ( ( ph /\ k e. A ) -> C e. RR )   =>    |- ( ph -> ( sqr ` sum_ k e. A ( ( B + C ) ^ 2 ) ) <_ ( ( sqr ` sum_ k e. A ( B ^ 2 ) ) + ( sqr ` sum_ k e. A ( C ^ 2 ) ) ) )
Theorem	rrxf 23184*	Euclidean vectors as functions. (Contributed by Thierry Arnoux, 7-Jul-2019.)
|- X = { h e. ( RR ^m I ) | h finSupp 0 }   &    |- ( ph -> F e. X )   =>    |- ( ph -> F : I --> RR )
Theorem	rrxfsupp 23185*	Euclidean vectors are of finite support. (Contributed by Thierry Arnoux, 7-Jul-2019.)
|- X = { h e. ( RR ^m I ) | h finSupp 0 }   &    |- ( ph -> F e. X )   =>    |- ( ph -> ( F supp 0 ) e. Fin )
Theorem	rrxsuppss 23186*	Support of Euclidean vectors. (Contributed by Thierry Arnoux, 7-Jul-2019.)
|- X = { h e. ( RR ^m I ) | h finSupp 0 }   &    |- ( ph -> F e. X )   =>    |- ( ph -> ( F supp 0 ) C_ I )
Theorem	rrxmvallem 23187*	Support of the function used for building the distance . (Contributed by Thierry Arnoux, 30-Jun-2019.)
|- X = { h e. ( RR ^m I ) | h finSupp 0 }   =>    |- ( ( I e. V /\ F e. X /\ G e. X ) -> ( ( k e. I |-> ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) supp 0 ) C_ ( ( F supp 0 ) u. ( G supp 0 ) ) )
Theorem	rrxmval 23188*	The value of the Euclidean metric. Compare with rrnmval 33627. (Contributed by Thierry Arnoux, 30-Jun-2019.)
|- X = { h e. ( RR ^m I ) | h finSupp 0 }   &    |- D = ( dist ` (ℝ^ ` I ) )   =>    |- ( ( I e. V /\ F e. X /\ G e. X ) -> ( F D G ) = ( sqr ` sum_ k e. ( ( F supp 0 ) u. ( G supp 0 ) ) ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) )
Theorem	rrxmfval 23189*	The value of the Euclidean metric. Compare with rrnval 33626. (Contributed by Thierry Arnoux, 30-Jun-2019.)
|- X = { h e. ( RR ^m I ) | h finSupp 0 }   &    |- D = ( dist ` (ℝ^ ` I ) )   =>    |- ( I e. V -> D = ( f e. X , g e. X |-> ( sqr ` sum_ k e. ( ( f supp 0 ) u. ( g supp 0 ) ) ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) ) )
Theorem	rrxmetlem 23190*	Lemma for rrxmet 23191. (Contributed by Thierry Arnoux, 5-Jul-2019.)
|- X = { h e. ( RR ^m I ) | h finSupp 0 }   &    |- D = ( dist ` (ℝ^ ` I ) )   &    |- ( ph -> I e. V )   &    |- ( ph -> F e. X )   &    |- ( ph -> G e. X )   &    |- ( ph -> A C_ I )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> ( ( F supp 0 ) u. ( G supp 0 ) ) C_ A )   =>    |- ( ph -> sum_ k e. ( ( F supp 0 ) u. ( G supp 0 ) ) ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) = sum_ k e. A ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) )
Theorem	rrxmet 23191*	Euclidean space is a metric space. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 5-Jun-2014.) (Revised by Thierry Arnoux, 30-Jun-2019.)
|- X = { h e. ( RR ^m I ) | h finSupp 0 }   &    |- D = ( dist ` (ℝ^ ` I ) )   =>    |- ( I e. V -> D e. ( Met ` X ) )
Theorem	rrxdstprj1 23192*	The distance between two points in Euclidean space is greater than the distance between the projections onto one coordinate. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Sep-2015.) (Revised by Thierry Arnoux, 7-Jul-2019.)
|- X = { h e. ( RR ^m I ) | h finSupp 0 }   &    |- D = ( dist ` (ℝ^ ` I ) )   &    |- M = ( ( abs o. - ) |` ( RR X. RR ) )   =>    |- ( ( ( I e. V /\ A e. I ) /\ ( F e. X /\ G e. X ) ) -> ( ( F ` A ) M ( G ` A ) ) <_ ( F D G ) )
Theorem	ehlval 23193	Value of the Euclidean space of dimension N. (Contributed by Thierry Arnoux, 16-Jun-2019.)
|- E = (𝔼hil ` N )   =>    |- ( N e. NN0 -> E = (ℝ^ ` ( 1 ... N ) ) )
Theorem	ehlbase 23194	The base of the Euclidean space is the set of n-tuples of real numbers. (Contributed by Thierry Arnoux, 16-Jun-2019.)
|- E = (𝔼hil ` N )   =>    |- ( N e. NN0 -> ( RR ^m ( 1 ... N ) ) = ( Base ` E ) )
12.5.9  Minimizing Vector Theorem
Theorem	minveclem1 23195*	Lemma for minvec 23207. The set of all distances from points of Y to A are a nonempty set of nonnegative reals. (Contributed by Mario Carneiro, 8-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.)
|- X = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- N = ( norm ` U )   &    |- ( ph -> U e. CPreHil )   &    |- ( ph -> Y e. ( LSubSp ` U ) )   &    |- ( ph -> ( U ↾s Y ) e. CMetSp )   &    |- ( ph -> A e. X )   &    |- J = ( TopOpen ` U )   &    |- R = ran ( y e. Y |-> ( N ` ( A .- y ) ) )   =>    |- ( ph -> ( R C_ RR /\ R =/= (/) /\ A. w e. R 0 <_ w ) )
Theorem	minveclem4c 23196*	Lemma for minvec 23207. The infimum of the distances to A is a real number. (Contributed by Mario Carneiro, 16-Jun-2014.) (Revised by Mario Carneiro, 15-Oct-2015.) (Revised by AV, 3-Oct-2020.)
|- X = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- N = ( norm ` U )   &    |- ( ph -> U e. CPreHil )   &    |- ( ph -> Y e. ( LSubSp ` U ) )   &    |- ( ph -> ( U ↾s Y ) e. CMetSp )   &    |- ( ph -> A e. X )   &    |- J = ( TopOpen ` U )   &    |- R = ran ( y e. Y |-> ( N ` ( A .- y ) ) )   &    |- S = inf ( R , RR , < )   =>    |- ( ph -> S e. RR )
Theorem	minveclem2 23197*	Lemma for minvec 23207. Any two points K and L in Y are close to each other if they are close to the infimum of distance to A. (Contributed by Mario Carneiro, 9-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.) (Revised by AV, 3-Oct-2020.)
|- X = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- N = ( norm ` U )   &    |- ( ph -> U e. CPreHil )   &    |- ( ph -> Y e. ( LSubSp ` U ) )   &    |- ( ph -> ( U ↾s Y ) e. CMetSp )   &    |- ( ph -> A e. X )   &    |- J = ( TopOpen ` U )   &    |- R = ran ( y e. Y |-> ( N ` ( A .- y ) ) )   &    |- S = inf ( R , RR , < )   &    |- D = ( ( dist ` U ) |` ( X X. X ) )   &    |- ( ph -> B e. RR )   &    |- ( ph -> 0 <_ B )   &    |- ( ph -> K e. Y )   &    |- ( ph -> L e. Y )   &    |- ( ph -> ( ( A D K ) ^ 2 ) <_ ( ( S ^ 2 ) + B ) )   &    |- ( ph -> ( ( A D L ) ^ 2 ) <_ ( ( S ^ 2 ) + B ) )   =>    |- ( ph -> ( ( K D L ) ^ 2 ) <_ ( 4 x. B ) )
Theorem	minveclem3a 23198*	Lemma for minvec 23207. D is a complete metric when restricted to Y. (Contributed by Mario Carneiro, 7-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.)
|- X = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- N = ( norm ` U )   &    |- ( ph -> U e. CPreHil )   &    |- ( ph -> Y e. ( LSubSp ` U ) )   &    |- ( ph -> ( U ↾s Y ) e. CMetSp )   &    |- ( ph -> A e. X )   &    |- J = ( TopOpen ` U )   &    |- R = ran ( y e. Y |-> ( N ` ( A .- y ) ) )   &    |- S = inf ( R , RR , < )   &    |- D = ( ( dist ` U ) |` ( X X. X ) )   =>    |- ( ph -> ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) )
Theorem	minveclem3b 23199*	Lemma for minvec 23207. The set of vectors within a fixed distance of the infimum forms a filter base. (Contributed by Mario Carneiro, 15-Oct-2015.) (Revised by AV, 3-Oct-2020.)
|- X = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- N = ( norm ` U )   &    |- ( ph -> U e. CPreHil )   &    |- ( ph -> Y e. ( LSubSp ` U ) )   &    |- ( ph -> ( U ↾s Y ) e. CMetSp )   &    |- ( ph -> A e. X )   &    |- J = ( TopOpen ` U )   &    |- R = ran ( y e. Y |-> ( N ` ( A .- y ) ) )   &    |- S = inf ( R , RR , < )   &    |- D = ( ( dist ` U ) |` ( X X. X ) )   &    |- F = ran ( r e. RR+ |-> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } )   =>    |- ( ph -> F e. ( fBas ` Y ) )
Theorem	minveclem3 23200*	Lemma for minvec 23207. The filter formed by taking elements successively closer to the infimum is Cauchy. (Contributed by Mario Carneiro, 8-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.)
|- X = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- N = ( norm ` U )   &    |- ( ph -> U e. CPreHil )   &    |- ( ph -> Y e. ( LSubSp ` U ) )   &    |- ( ph -> ( U ↾s Y ) e. CMetSp )   &    |- ( ph -> A e. X )   &    |- J = ( TopOpen ` U )   &    |- R = ran ( y e. Y |-> ( N ` ( A .- y ) ) )   &    |- S = inf ( R , RR , < )   &    |- D = ( ( dist ` U ) |` ( X X. X ) )   &    |- F = ran ( r e. RR+ |-> { y e. Y | ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + r ) } )   =>    |- ( ph -> ( Y filGen F ) e. (CauFil ` ( D |` ( Y X. Y ) ) ) )