P. 231 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 23001-23100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cphorthcom 23001	Orthogonality (meaning inner product is 0) is commutative. Complex version of iporthcom 19980. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- ., = ( .i ` W )   &    |- V = ( Base ` W )   =>    |- ( ( W e. CPreHil /\ A e. V /\ B e. V ) -> ( ( A ., B ) = 0 <-> ( B ., A ) = 0 ) )
Theorem	cphip0l 23002	Inner product with a zero first argument. Part of proof of Theorem 6.44 of [Ponnusamy] p. 361. Complex version of ip0l 19981. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- ., = ( .i ` W )   &    |- V = ( Base ` W )   &    |- .0. = ( 0g ` W )   =>    |- ( ( W e. CPreHil /\ A e. V ) -> ( .0. ., A ) = 0 )
Theorem	cphip0r 23003	Inner product with a zero second argument. Complex version of ip0r 19982. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- ., = ( .i ` W )   &    |- V = ( Base ` W )   &    |- .0. = ( 0g ` W )   =>    |- ( ( W e. CPreHil /\ A e. V ) -> ( A ., .0. ) = 0 )
Theorem	cphipeq0 23004	The inner product of a vector with itself is zero iff the vector is zero. Part of Definition 3.1-1 of [Kreyszig] p. 129. Complex version of ipeq0 19983. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- ., = ( .i ` W )   &    |- V = ( Base ` W )   &    |- .0. = ( 0g ` W )   =>    |- ( ( W e. CPreHil /\ A e. V ) -> ( ( A ., A ) = 0 <-> A = .0. ) )
Theorem	cphdir 23005	Distributive law for inner product (right-distributivity). Equation I3 of [Ponnusamy] p. 362. Complex version of ipdir 19984. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- ., = ( .i ` W )   &    |- V = ( Base ` W )   &    |- .+ = ( +g ` W )   =>    |- ( ( W e. CPreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( A .+ B ) ., C ) = ( ( A ., C ) + ( B ., C ) ) )
Theorem	cphdi 23006	Distributive law for inner product (left-distributivity). Complex version of ipdi 19985. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- ., = ( .i ` W )   &    |- V = ( Base ` W )   &    |- .+ = ( +g ` W )   =>    |- ( ( W e. CPreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( A ., ( B .+ C ) ) = ( ( A ., B ) + ( A ., C ) ) )
Theorem	cph2di 23007	Distributive law for inner product. Complex version of ip2di 19986. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- ., = ( .i ` W )   &    |- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- ( ph -> W e. CPreHil )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. V )   &    |- ( ph -> C e. V )   &    |- ( ph -> D e. V )   =>    |- ( ph -> ( ( A .+ B ) ., ( C .+ D ) ) = ( ( ( A ., C ) + ( B ., D ) ) + ( ( A ., D ) + ( B ., C ) ) ) )
Theorem	cphsubdir 23008	Distributive law for inner product subtraction. Complex version of ipsubdir 19987. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- ., = ( .i ` W )   &    |- V = ( Base ` W )   &    |- .- = ( -g ` W )   =>    |- ( ( W e. CPreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( A .- B ) ., C ) = ( ( A ., C ) - ( B ., C ) ) )
Theorem	cphsubdi 23009	Distributive law for inner product subtraction. Complex version of ipsubdi 19988. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- ., = ( .i ` W )   &    |- V = ( Base ` W )   &    |- .- = ( -g ` W )   =>    |- ( ( W e. CPreHil /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( A ., ( B .- C ) ) = ( ( A ., B ) - ( A ., C ) ) )
Theorem	cph2subdi 23010	Distributive law for inner product subtraction. Complex version of ip2subdi 19989. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- ., = ( .i ` W )   &    |- V = ( Base ` W )   &    |- .- = ( -g ` W )   &    |- ( ph -> W e. CPreHil )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. V )   &    |- ( ph -> C e. V )   &    |- ( ph -> D e. V )   =>    |- ( ph -> ( ( A .- B ) ., ( C .- D ) ) = ( ( ( A ., C ) + ( B ., D ) ) - ( ( A ., D ) + ( B ., C ) ) ) )
Theorem	cphass 23011	Associative law for inner product. Equation I2 of [Ponnusamy] p. 363. See ipass 19990, his5 27943. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- ., = ( .i ` W )   &    |- V = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- .x. = ( .s ` W )   =>    |- ( ( W e. CPreHil /\ ( A e. K /\ B e. V /\ C e. V ) ) -> ( ( A .x. B ) ., C ) = ( A x. ( B ., C ) ) )
Theorem	cphassr 23012	"Associative" law for second argument of inner product (compare cphass 23011). See ipassr 19991, his52 . (Contributed by Mario Carneiro, 16-Oct-2015.)
|- ., = ( .i ` W )   &    |- V = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- .x. = ( .s ` W )   =>    |- ( ( W e. CPreHil /\ ( A e. K /\ B e. V /\ C e. V ) ) -> ( B ., ( A .x. C ) ) = ( ( * ` A ) x. ( B ., C ) ) )
Theorem	cph2ass 23013	Move scalar multiplication to outside of inner product. See his35 27945. (Contributed by Mario Carneiro, 17-Oct-2015.)
|- ., = ( .i ` W )   &    |- V = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- .x. = ( .s ` W )   =>    |- ( ( W e. CPreHil /\ ( A e. K /\ B e. K ) /\ ( C e. V /\ D e. V ) ) -> ( ( A .x. C ) ., ( B .x. D ) ) = ( ( A x. ( * ` B ) ) x. ( C ., D ) ) )
Theorem	cphassi 23014	Associative law for the first argument of an inner product with scalar _ i. (Contributed by AV, 17-Oct-2021.)
|- X = ( Base ` W )   &    |- .x. = ( .s ` W )   &    |- ., = ( .i ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( ( _i .x. B ) ., A ) = ( _i x. ( B ., A ) ) )
Theorem	cphassir 23015	"Associative" law for the second argument of an inner product with scalar _ i. (Contributed by AV, 17-Oct-2021.)
|- X = ( Base ` W )   &    |- .x. = ( .s ` W )   &    |- ., = ( .i ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( A ., ( _i .x. B ) ) = ( -u _i x. ( A ., B ) ) )
Theorem	tchex 23016*	Lemma for tchbas 23018 and similar theorems. (Contributed by Mario Carneiro, 7-Oct-2015.)
|- V = ( Base ` W )   =>    |- ( x e. V |-> ( sqr ` ( x ., x ) ) ) e. _V
Theorem	tchval 23017*	Define a function to augment a subcomplex pre-Hilbert space with norm. (Contributed by Mario Carneiro, 7-Oct-2015.)
|- G = (toCHil ` W )   &    |- V = ( Base ` W )   &    |- ., = ( .i ` W )   =>    |- G = ( W toNrmGrp ( x e. V |-> ( sqr ` ( x ., x ) ) ) )
Theorem	tchbas 23018	The base set of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.)
|- G = (toCHil ` W )   &    |- V = ( Base ` W )   =>    |- V = ( Base ` G )
Theorem	tchplusg 23019	The addition operation of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.)
|- G = (toCHil ` W )   &    |- .+ = ( +g ` W )   =>    |- .+ = ( +g ` G )
Theorem	tchsub 23020	The subtraction operation of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Thierry Arnoux, 30-Jun-2019.)
|- G = (toCHil ` W )   &    |- .- = ( -g ` W )   =>    |- .- = ( -g ` G )
Theorem	tchmulr 23021	The ring operation of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.)
|- G = (toCHil ` W )   &    |- .x. = ( .r ` W )   =>    |- .x. = ( .r ` G )
Theorem	tchsca 23022	The scalar field of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.)
|- G = (toCHil ` W )   &    |- F = (Scalar ` W )   =>    |- F = (Scalar ` G )
Theorem	tchvsca 23023	The scalar multiplication of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.)
|- G = (toCHil ` W )   &    |- .x. = ( .s ` W )   =>    |- .x. = ( .s ` G )
Theorem	tchip 23024	The inner product of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.)
|- G = (toCHil ` W )   &    |- .x. = ( .i ` W )   =>    |- .x. = ( .i ` G )
Theorem	tchtopn 23025	The topology of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.)
|- G = (toCHil ` W )   &    |- D = ( dist ` G )   &    |- J = ( TopOpen ` G )   =>    |- ( W e. V -> J = ( MetOpen ` D ) )
Theorem	tchphl 23026	Augmentation of a subcomplex pre-Hilbert space with a norm does not affect whether it is still a pre-Hilbert space because all the original components are the same. (Contributed by Mario Carneiro, 8-Oct-2015.)
|- G = (toCHil ` W )   =>    |- ( W e. PreHil <-> G e. PreHil )
Theorem	tchnmfval 23027*	The norm of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.)
|- G = (toCHil ` W )   &    |- N = ( norm ` G )   &    |- V = ( Base ` W )   &    |- ., = ( .i ` W )   =>    |- ( W e. Grp -> N = ( x e. V |-> ( sqr ` ( x ., x ) ) ) )
Theorem	tchnmval 23028	The norm of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.)
|- G = (toCHil ` W )   &    |- N = ( norm ` G )   &    |- V = ( Base ` W )   &    |- ., = ( .i ` W )   =>    |- ( ( W e. Grp /\ X e. V ) -> ( N ` X ) = ( sqr ` ( X ., X ) ) )
Theorem	cphtchnm 23029	The norm of a norm-augmented subcomplex pre-Hilbert space is the same as the original norm on it. (Contributed by Mario Carneiro, 11-Oct-2015.)
|- G = (toCHil ` W )   &    |- N = ( norm ` W )   =>    |- ( W e. CPreHil -> N = ( norm ` G ) )
Theorem	tchds 23030	The distance of a pre-Hilbert space augmented with norm. (Contributed by Thierry Arnoux, 30-Jun-2019.)
|- G = (toCHil ` W )   &    |- N = ( norm ` G )   &    |- .- = ( -g ` W )   =>    |- ( W e. Grp -> ( N o. .- ) = ( dist ` G ) )
Theorem	tchclm 23031	Lemma for tchcph 23036. (Contributed by Mario Carneiro, 16-Oct-2015.)
|- G = (toCHil ` W )   &    |- V = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- ( ph -> W e. PreHil )   &    |- ( ph -> F = (ℂfld ↾s K ) )   =>    |- ( ph -> W e. CMod )
Theorem	tchcphlem3 23032	Lemma for tchcph 23036: real closure of an inner product of a vector with itself. (Contributed by Mario Carneiro, 10-Oct-2015.)
|- G = (toCHil ` W )   &    |- V = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- ( ph -> W e. PreHil )   &    |- ( ph -> F = (ℂfld ↾s K ) )   &    |- ., = ( .i ` W )   =>    |- ( ( ph /\ X e. V ) -> ( X ., X ) e. RR )
Theorem	ipcau2 23033*	The Cauchy-Schwarz inequality for a subcomplex pre-Hilbert space. (Contributed by Mario Carneiro, 11-Oct-2015.)
|- G = (toCHil ` W )   &    |- V = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- ( ph -> W e. PreHil )   &    |- ( ph -> F = (ℂfld ↾s K ) )   &    |- ., = ( .i ` W )   &    |- ( ( ph /\ ( x e. K /\ x e. RR /\ 0 <_ x ) ) -> ( sqr ` x ) e. K )   &    |- ( ( ph /\ x e. V ) -> 0 <_ ( x ., x ) )   &    |- K = ( Base ` F )   &    |- N = ( norm ` G )   &    |- C = ( ( Y ., X ) / ( Y ., Y ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   =>    |- ( ph -> ( abs ` ( X ., Y ) ) <_ ( ( N ` X ) x. ( N ` Y ) ) )
Theorem	tchcphlem1 23034*	Lemma for tchcph 23036: the triangle inequality. (Contributed by Mario Carneiro, 8-Oct-2015.)
|- G = (toCHil ` W )   &    |- V = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- ( ph -> W e. PreHil )   &    |- ( ph -> F = (ℂfld ↾s K ) )   &    |- ., = ( .i ` W )   &    |- ( ( ph /\ ( x e. K /\ x e. RR /\ 0 <_ x ) ) -> ( sqr ` x ) e. K )   &    |- ( ( ph /\ x e. V ) -> 0 <_ ( x ., x ) )   &    |- K = ( Base ` F )   &    |- .- = ( -g ` W )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   =>    |- ( ph -> ( sqr ` ( ( X .- Y ) ., ( X .- Y ) ) ) <_ ( ( sqr ` ( X ., X ) ) + ( sqr ` ( Y ., Y ) ) ) )
Theorem	tchcphlem2 23035*	Lemma for tchcph 23036: homogeneity. (Contributed by Mario Carneiro, 8-Oct-2015.)
|- G = (toCHil ` W )   &    |- V = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- ( ph -> W e. PreHil )   &    |- ( ph -> F = (ℂfld ↾s K ) )   &    |- ., = ( .i ` W )   &    |- ( ( ph /\ ( x e. K /\ x e. RR /\ 0 <_ x ) ) -> ( sqr ` x ) e. K )   &    |- ( ( ph /\ x e. V ) -> 0 <_ ( x ., x ) )   &    |- K = ( Base ` F )   &    |- .x. = ( .s ` W )   &    |- ( ph -> X e. K )   &    |- ( ph -> Y e. V )   =>    |- ( ph -> ( sqr ` ( ( X .x. Y ) ., ( X .x. Y ) ) ) = ( ( abs ` X ) x. ( sqr ` ( Y ., Y ) ) ) )
Theorem	tchcph 23036*	The standard definition of a norm turns any pre-Hilbert space over a quadratically closed subfield of ℂfld into a subcomplex pre-Hilbert space (which allows access to a norm, metric, and topology). (Contributed by Mario Carneiro, 11-Oct-2015.)
|- G = (toCHil ` W )   &    |- V = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- ( ph -> W e. PreHil )   &    |- ( ph -> F = (ℂfld ↾s K ) )   &    |- ., = ( .i ` W )   &    |- ( ( ph /\ ( x e. K /\ x e. RR /\ 0 <_ x ) ) -> ( sqr ` x ) e. K )   &    |- ( ( ph /\ x e. V ) -> 0 <_ ( x ., x ) )   =>    |- ( ph -> G e. CPreHil )
Theorem	ipcau 23037	The Cauchy-Schwarz inequality for a subcomplex pre-Hilbert space. (Contributed by Mario Carneiro, 11-Oct-2015.)
|- V = ( Base ` W )   &    |- ., = ( .i ` W )   &    |- N = ( norm ` W )   =>    |- ( ( W e. CPreHil /\ X e. V /\ Y e. V ) -> ( abs ` ( X ., Y ) ) <_ ( ( N ` X ) x. ( N ` Y ) ) )
Theorem	nmparlem 23038	Lemma for nmpar 23039. (Contributed by Mario Carneiro, 7-Oct-2015.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- .- = ( -g ` W )   &    |- N = ( norm ` W )   &    |- ., = ( .i ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- ( ph -> W e. CPreHil )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. V )   =>    |- ( ph -> ( ( ( N ` ( A .+ B ) ) ^ 2 ) + ( ( N ` ( A .- B ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` A ) ^ 2 ) + ( ( N ` B ) ^ 2 ) ) ) )
Theorem	nmpar 23039	A subcomplex pre-Hilbert space satisfies the parallelogram law. (Contributed by Mario Carneiro, 7-Oct-2015.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- .- = ( -g ` W )   &    |- N = ( norm ` W )   =>    |- ( ( W e. CPreHil /\ A e. V /\ B e. V ) -> ( ( ( N ` ( A .+ B ) ) ^ 2 ) + ( ( N ` ( A .- B ) ) ^ 2 ) ) = ( 2 x. ( ( ( N ` A ) ^ 2 ) + ( ( N ` B ) ^ 2 ) ) ) )
Theorem	cphipval2 23040	Value of the inner product expressed by the norm defined by it. (Contributed by NM, 31-Jan-2007.) (Revised by AV, 18-Oct-2021.)
|- X = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- .x. = ( .s ` W )   &    |- N = ( norm ` W )   &    |- ., = ( .i ` W )   &    |- .- = ( -g ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( A ., B ) = ( ( ( ( ( N ` ( A .+ B ) ) ^ 2 ) - ( ( N ` ( A .- B ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( A .+ ( _i .x. B ) ) ) ^ 2 ) - ( ( N ` ( A .- ( _i .x. B ) ) ) ^ 2 ) ) ) ) / 4 ) )
Theorem	4cphipval2 23041	Four times the inner product value cphipval2 23040. (Contributed by NM, 1-Feb-2008.) (Revised by AV, 18-Oct-2021.)
|- X = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- .x. = ( .s ` W )   &    |- N = ( norm ` W )   &    |- ., = ( .i ` W )   &    |- .- = ( -g ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( 4 x. ( A ., B ) ) = ( ( ( ( N ` ( A .+ B ) ) ^ 2 ) - ( ( N ` ( A .- B ) ) ^ 2 ) ) + ( _i x. ( ( ( N ` ( A .+ ( _i .x. B ) ) ) ^ 2 ) - ( ( N ` ( A .- ( _i .x. B ) ) ) ^ 2 ) ) ) ) )
Theorem	cphipval 23042*	Value of the inner product expressed by a sum of terms with the norm defined by the inner product. Equation 6.45 of [Ponnusamy] p. 361. (Contributed by NM, 31-Jan-2007.) (Revised by AV, 18-Oct-2021.)
|- X = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- .x. = ( .s ` W )   &    |- N = ( norm ` W )   &    |- ., = ( .i ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   =>    |- ( ( ( W e. CPreHil /\ _i e. K ) /\ A e. X /\ B e. X ) -> ( A ., B ) = ( sum_ k e. ( 1 ... 4 ) ( ( _i ^ k ) x. ( ( N ` ( A .+ ( ( _i ^ k ) .x. B ) ) ) ^ 2 ) ) / 4 ) )
Theorem	ipcnlem2 23043	The inner product operation of a subcomplex pre-Hilbert space is continuous. (Contributed by Mario Carneiro, 13-Oct-2015.)
|- V = ( Base ` W )   &    |- ., = ( .i ` W )   &    |- D = ( dist ` W )   &    |- N = ( norm ` W )   &    |- T = ( ( R / 2 ) / ( ( N ` A ) + 1 ) )   &    |- U = ( ( R / 2 ) / ( ( N ` B ) + T ) )   &    |- ( ph -> W e. CPreHil )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. V )   &    |- ( ph -> R e. RR+ )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ph -> ( A D X ) < U )   &    |- ( ph -> ( B D Y ) < T )   =>    |- ( ph -> ( abs ` ( ( A ., B ) - ( X ., Y ) ) ) < R )
Theorem	ipcnlem1 23044*	The inner product operation of a subcomplex pre-Hilbert space is continuous. (Contributed by Mario Carneiro, 13-Oct-2015.)
|- V = ( Base ` W )   &    |- ., = ( .i ` W )   &    |- D = ( dist ` W )   &    |- N = ( norm ` W )   &    |- T = ( ( R / 2 ) / ( ( N ` A ) + 1 ) )   &    |- U = ( ( R / 2 ) / ( ( N ` B ) + T ) )   &    |- ( ph -> W e. CPreHil )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. V )   &    |- ( ph -> R e. RR+ )   =>    |- ( ph -> E. r e. RR+ A. x e. V A. y e. V ( ( ( A D x ) < r /\ ( B D y ) < r ) -> ( abs ` ( ( A ., B ) - ( x ., y ) ) ) < R ) )
Theorem	ipcn 23045	The inner product operation of a subcomplex pre-Hilbert space is continuous. (Contributed by Mario Carneiro, 13-Oct-2015.)
|- ., = ( .if ` W )   &    |- J = ( TopOpen ` W )   &    |- K = ( TopOpen ` ℂfld )   =>    |- ( W e. CPreHil -> ., e. ( ( J tX J ) Cn K ) )
Theorem	cnmpt1ip 23046*	Continuity of inner product; analogue of cnmpt12f 21469 which cannot be used directly because .i is not a function. (Contributed by Mario Carneiro, 13-Oct-2015.)
|- J = ( TopOpen ` W )   &    |- C = ( TopOpen ` ℂfld )   &    |- ., = ( .i ` W )   &    |- ( ph -> W e. CPreHil )   &    |- ( ph -> K e. (TopOn ` X ) )   &    |- ( ph -> ( x e. X |-> A ) e. ( K Cn J ) )   &    |- ( ph -> ( x e. X |-> B ) e. ( K Cn J ) )   =>    |- ( ph -> ( x e. X |-> ( A ., B ) ) e. ( K Cn C ) )
Theorem	cnmpt2ip 23047*	Continuity of inner product; analogue of cnmpt22f 21478 which cannot be used directly because .i is not a function. (Contributed by Mario Carneiro, 13-Oct-2015.)
|- J = ( TopOpen ` W )   &    |- C = ( TopOpen ` ℂfld )   &    |- ., = ( .i ` W )   &    |- ( ph -> W e. CPreHil )   &    |- ( ph -> K e. (TopOn ` X ) )   &    |- ( ph -> L e. (TopOn ` Y ) )   &    |- ( ph -> ( x e. X , y e. Y |-> A ) e. ( ( K tX L ) Cn J ) )   &    |- ( ph -> ( x e. X , y e. Y |-> B ) e. ( ( K tX L ) Cn J ) )   =>    |- ( ph -> ( x e. X , y e. Y |-> ( A ., B ) ) e. ( ( K tX L ) Cn C ) )
Theorem	csscld 23048	A "closed subspace" in a subcomplex pre-Hilbert space is actually closed in the topology induced by the norm, thus justifying the terminology "closed subspace". (Contributed by Mario Carneiro, 13-Oct-2015.)
|- C = ( CSubSp ` W )   &    |- J = ( TopOpen ` W )   =>    |- ( ( W e. CPreHil /\ S e. C ) -> S e. ( Clsd ` J ) )
Theorem	clsocv 23049	The orthogonal complement of the closure of a subset is the same as the orthogonal complement of the subset itself. (Contributed by Mario Carneiro, 13-Oct-2015.)
|- V = ( Base ` W )   &    |- O = ( ocv ` W )   &    |- J = ( TopOpen ` W )   =>    |- ( ( W e. CPreHil /\ S C_ V ) -> ( O ` ( ( cls ` J ) ` S ) ) = ( O ` S ) )
12.5.5  Convergence and completeness
Syntax	ccfil 23050	Extend class notation with the set of Cauchy filters.
class CauFil
Syntax	cca 23051	Extend class notation with a function on metric spaces whose value is the set of all Cauchy sequences of the space.
class Cau
Syntax	cms 23052	Extend class notation with class of complete metric spaces.
class CMet
Definition	df-cfil 23053*	Define the set of Cauchy filters on a metric space. A Cauchy filter is a filter on the set such that for every 0 < x there is an element of the filter whose metric diameter is less than x. (Contributed by Mario Carneiro, 13-Oct-2015.)
|- CauFil = ( d e. U. ran *Met |-> { f e. ( Fil ` dom dom d ) | A. x e. RR+ E. y e. f ( d " ( y X. y ) ) C_ ( 0 [,) x ) } )
Definition	df-cau 23054*	Define a function on metric spaces whose value is the set of Cauchy sequences of the space. (Contributed by NM, 8-Sep-2006.)
|- Cau = ( d e. U. ran *Met |-> { f e. ( dom dom d ^pm CC ) | A. x e. RR+ E. j e. ZZ ( f |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> ( ( f ` j ) ( ball ` d ) x ) } )
Definition	df-cmet 23055*	Define the class of complete metrics. (Contributed by Mario Carneiro, 1-May-2014.)
|- CMet = ( x e. _V |-> { d e. ( Met ` x ) | A. f e. (CauFil ` d ) ( ( MetOpen ` d ) fLim f ) =/= (/) } )
Theorem	lmmbr 23056*	Express the binary relation "sequence F converges to point P " in a metric space. Definition 1.4-1 of [Kreyszig] p. 25. The condition F C_ ( CC X. X ) allows us to use objects more general than sequences when convenient; see the comment in df-lm 21033. (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 1-May-2014.)
|- J = ( MetOpen ` D )   &    |- ( ph -> D e. ( *Met ` X ) )   =>    |- ( ph -> ( F ( ~~> t ` J ) P <-> ( F e. ( X ^pm CC ) /\ P e. X /\ A. x e. RR+ E. y e. ran ZZ>= ( F |` y ) : y --> ( P ( ball ` D ) x ) ) ) )
Theorem	lmmbr2 23057*	Express the binary relation "sequence F converges to point P " in a metric space. Definition 1.4-1 of [Kreyszig] p. 25. The condition F C_ ( CC X. X ) allows us to use objects more general than sequences when convenient; see the comment in df-lm 21033. (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 1-May-2014.)
|- J = ( MetOpen ` D )   &    |- ( ph -> D e. ( *Met ` X ) )   =>    |- ( ph -> ( F ( ~~> t ` J ) P <-> ( F e. ( X ^pm CC ) /\ P e. X /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D P ) < x ) ) ) )
Theorem	lmmbr3 23058*	Express the binary relation "sequence F converges to point P " in a metric space using an arbitrary upper set of integers. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 1-May-2014.)
|- J = ( MetOpen ` D )   &    |- ( ph -> D e. ( *Met ` X ) )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   =>    |- ( ph -> ( F ( ~~> t ` J ) P <-> ( F e. ( X ^pm CC ) /\ P e. X /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D P ) < x ) ) ) )
Theorem	lmmcvg 23059*	Convergence property of a converging sequence. (Contributed by NM, 1-Jun-2007.) (Revised by Mario Carneiro, 1-May-2014.)
|- J = ( MetOpen ` D )   &    |- ( ph -> D e. ( *Met ` X ) )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )   &    |- ( ph -> F ( ~~> t ` J ) P )   &    |- ( ph -> R e. RR+ )   =>    |- ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( A e. X /\ ( A D P ) < R ) )
Theorem	lmmbrf 23060*	Express the binary relation "sequence F converges to point P " in a metric space using an arbitrary upper set of integers. This version of lmmbr2 23057 presupposes that F is a function. (Contributed by NM, 20-Jul-2007.) (Revised by Mario Carneiro, 1-May-2014.)
|- J = ( MetOpen ` D )   &    |- ( ph -> D e. ( *Met ` X ) )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )   &    |- ( ph -> F : Z --> X )   =>    |- ( ph -> ( F ( ~~> t ` J ) P <-> ( P e. X /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( A D P ) < x ) ) )
Theorem	lmnn 23061*	A condition that implies convergence. (Contributed by NM, 8-Jun-2007.) (Revised by Mario Carneiro, 1-May-2014.)
|- J = ( MetOpen ` D )   &    |- ( ph -> D e. ( *Met ` X ) )   &    |- ( ph -> P e. X )   &    |- ( ph -> F : NN --> X )   &    |- ( ( ph /\ k e. NN ) -> ( ( F ` k ) D P ) < ( 1 / k ) )   =>    |- ( ph -> F ( ~~> t ` J ) P )
Theorem	cfilfval 23062*	The set of Cauchy filters on a metric space. (Contributed by Mario Carneiro, 13-Oct-2015.)
|- ( D e. ( *Met ` X ) -> (CauFil ` D ) = { f e. ( Fil ` X ) | A. x e. RR+ E. y e. f ( D " ( y X. y ) ) C_ ( 0 [,) x ) } )
Theorem	iscfil 23063*	The property of being a Cauchy filter. (Contributed by Mario Carneiro, 13-Oct-2015.)
|- ( D e. ( *Met ` X ) -> ( F e. (CauFil ` D ) <-> ( F e. ( Fil ` X ) /\ A. x e. RR+ E. y e. F ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) )
Theorem	iscfil2 23064*	The property of being a Cauchy filter. (Contributed by Mario Carneiro, 13-Oct-2015.)
|- ( D e. ( *Met ` X ) -> ( F e. (CauFil ` D ) <-> ( F e. ( Fil ` X ) /\ A. x e. RR+ E. y e. F A. z e. y A. w e. y ( z D w ) < x ) ) )
Theorem	cfilfil 23065	A Cauchy filter is a filter. (Contributed by Mario Carneiro, 13-Oct-2015.)
|- ( ( D e. ( *Met ` X ) /\ F e. (CauFil ` D ) ) -> F e. ( Fil ` X ) )
Theorem	cfili 23066*	Property of a Cauchy filter. (Contributed by Mario Carneiro, 13-Oct-2015.)
|- ( ( F e. (CauFil ` D ) /\ R e. RR+ ) -> E. x e. F A. y e. x A. z e. x ( y D z ) < R )
Theorem	cfil3i 23067*	A Cauchy filter contains balls of any pre-chosen size. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- ( ( D e. ( *Met ` X ) /\ F e. (CauFil ` D ) /\ R e. RR+ ) -> E. x e. X ( x ( ball ` D ) R ) e. F )
Theorem	cfilss 23068	A filter finer than a Cauchy filter is Cauchy. (Contributed by Mario Carneiro, 13-Oct-2015.)
|- ( ( ( D e. ( *Met ` X ) /\ F e. (CauFil ` D ) ) /\ ( G e. ( Fil ` X ) /\ F C_ G ) ) -> G e. (CauFil ` D ) )
Theorem	fgcfil 23069*	The Cauchy filter condition for a filter base. (Contributed by Mario Carneiro, 13-Oct-2015.)
|- ( ( D e. ( *Met ` X ) /\ B e. ( fBas ` X ) ) -> ( ( X filGen B ) e. (CauFil ` D ) <-> A. x e. RR+ E. y e. B A. z e. y A. w e. y ( z D w ) < x ) )
Theorem	fmcfil 23070*	The Cauchy filter condition for a filter map. (Contributed by Mario Carneiro, 13-Oct-2015.)
|- ( ( D e. ( *Met ` X ) /\ B e. ( fBas ` Y ) /\ F : Y --> X ) -> ( ( ( X FilMap F ) ` B ) e. (CauFil ` D ) <-> A. x e. RR+ E. y e. B A. z e. y A. w e. y ( ( F ` z ) D ( F ` w ) ) < x ) )
Theorem	iscfil3 23071*	A filter is Cauchy iff it contains a ball of any chosen size. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- ( D e. ( *Met ` X ) -> ( F e. (CauFil ` D ) <-> ( F e. ( Fil ` X ) /\ A. r e. RR+ E. x e. X ( x ( ball ` D ) r ) e. F ) ) )
Theorem	cfilfcls 23072	Similar to ultrafilters (uffclsflim 21835), the cluster points and limit points of a Cauchy filter coincide. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- J = ( MetOpen ` D )   &    |- X = dom dom D   =>    |- ( F e. (CauFil ` D ) -> ( J fClus F ) = ( J fLim F ) )
Theorem	caufval 23073*	The set of Cauchy sequences on a metric space. (Contributed by NM, 8-Sep-2006.) (Revised by Mario Carneiro, 5-Sep-2015.)
|- ( D e. ( *Met ` X ) -> ( Cau ` D ) = { f e. ( X ^pm CC ) | A. x e. RR+ E. k e. ZZ ( f |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( f ` k ) ( ball ` D ) x ) } )
Theorem	iscau 23074*	Express the property " F is a Cauchy sequence of metric D." Part of Definition 1.4-3 of [Kreyszig] p. 28. The condition F C_ ( CC X. X ) allows us to use objects more general than sequences when convenient; see the comment in df-lm 21033. (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 14-Nov-2013.)
|- ( D e. ( *Met ` X ) -> ( F e. ( Cau ` D ) <-> ( F e. ( X ^pm CC ) /\ A. x e. RR+ E. k e. ZZ ( F |` ( ZZ>= ` k ) ) : ( ZZ>= ` k ) --> ( ( F ` k ) ( ball ` D ) x ) ) ) )
Theorem	iscau2 23075*	Express the property " F is a Cauchy sequence of metric D," using an arbitrary upper set of integers. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 14-Nov-2013.)
|- ( D e. ( *Met ` X ) -> ( F e. ( Cau ` D ) <-> ( F e. ( X ^pm CC ) /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) ) )
Theorem	iscau3 23076*	Express the Cauchy sequence property in the more conventional three-quantifier form. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 14-Nov-2013.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> D e. ( *Met ` X ) )   &    |- ( ph -> M e. ZZ )   =>    |- ( ph -> ( F e. ( Cau ` D ) <-> ( F e. ( X ^pm CC ) /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ A. m e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` m ) ) < x ) ) ) )
Theorem	iscau4 23077*	Express the property " F is a Cauchy sequence of metric D," using an arbitrary upper set of integers. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 23-Dec-2013.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> D e. ( *Met ` X ) )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )   &    |- ( ( ph /\ j e. Z ) -> ( F ` j ) = B )   =>    |- ( ph -> ( F e. ( Cau ` D ) <-> ( F e. ( X ^pm CC ) /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ A e. X /\ ( A D B ) < x ) ) ) )
Theorem	iscauf 23078*	Express the property " F is a Cauchy sequence of metric D " presupposing F is a function. (Contributed by NM, 24-Jul-2007.) (Revised by Mario Carneiro, 23-Dec-2013.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> D e. ( *Met ` X ) )   &    |- ( ph -> M e. ZZ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )   &    |- ( ( ph /\ j e. Z ) -> ( F ` j ) = B )   &    |- ( ph -> F : Z --> X )   =>    |- ( ph -> ( F e. ( Cau ` D ) <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( B D A ) < x ) )
Theorem	caun0 23079	A metric with a Cauchy sequence cannot be empty. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 24-Dec-2013.)
|- ( ( D e. ( *Met ` X ) /\ F e. ( Cau ` D ) ) -> X =/= (/) )
Theorem	caufpm 23080	Inclusion of a Cauchy sequence, under our definition. (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 24-Dec-2013.)
|- ( ( D e. ( *Met ` X ) /\ F e. ( Cau ` D ) ) -> F e. ( X ^pm CC ) )
Theorem	caucfil 23081	A Cauchy sequence predicate can be expressed in terms of the Cauchy filter predicate for a suitably chosen filter. (Contributed by Mario Carneiro, 13-Oct-2015.)
|- Z = ( ZZ>= ` M )   &    |- L = ( ( X FilMap F ) ` ( ZZ>= " Z ) )   =>    |- ( ( D e. ( *Met ` X ) /\ M e. ZZ /\ F : Z --> X ) -> ( F e. ( Cau ` D ) <-> L e. (CauFil ` D ) ) )
Theorem	iscmet 23082*	The property " D is a complete metric." meaning all Cauchy filters converge to a point in the space. (Contributed by Mario Carneiro, 1-May-2014.) (Revised by Mario Carneiro, 13-Oct-2015.)
|- J = ( MetOpen ` D )   =>    |- ( D e. ( CMet ` X ) <-> ( D e. ( Met ` X ) /\ A. f e. (CauFil ` D ) ( J fLim f ) =/= (/) ) )
Theorem	cmetcvg 23083	The convergence of a Cauchy filter in a complete metric space. (Contributed by Mario Carneiro, 14-Oct-2015.)
|- J = ( MetOpen ` D )   =>    |- ( ( D e. ( CMet ` X ) /\ F e. (CauFil ` D ) ) -> ( J fLim F ) =/= (/) )
Theorem	cmetmet 23084	A complete metric space is a metric space. (Contributed by NM, 18-Dec-2006.) (Revised by Mario Carneiro, 29-Jan-2014.)
|- ( D e. ( CMet ` X ) -> D e. ( Met ` X ) )
Theorem	cmetmeti 23085	A complete metric space is a metric space. (Contributed by NM, 26-Oct-2007.)
|- D e. ( CMet ` X )   =>    |- D e. ( Met ` X )
Theorem	cmetcaulem 23086*	Lemma for cmetcau 23087. (Contributed by Mario Carneiro, 14-Oct-2015.)
|- J = ( MetOpen ` D )   &    |- ( ph -> D e. ( CMet ` X ) )   &    |- ( ph -> P e. X )   &    |- ( ph -> F e. ( Cau ` D ) )   &    |- G = ( x e. NN |-> if ( x e. dom F , ( F ` x ) , P ) )   =>    |- ( ph -> F e. dom ( ~~> t ` J ) )
Theorem	cmetcau 23087	The convergence of a Cauchy sequence in a complete metric space. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 14-Oct-2015.)
|- J = ( MetOpen ` D )   =>    |- ( ( D e. ( CMet ` X ) /\ F e. ( Cau ` D ) ) -> F e. dom ( ~~> t ` J ) )
Theorem	iscmet3lem3 23088*	Lemma for iscmet3 23091. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- Z = ( ZZ>= ` M )   =>    |- ( ( M e. ZZ /\ R e. RR+ ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( ( 1 / 2 ) ^ k ) < R )
Theorem	iscmet3lem1 23089*	Lemma for iscmet3 23091. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- Z = ( ZZ>= ` M )   &    |- J = ( MetOpen ` D )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> D e. ( Met ` X ) )   &    |- ( ph -> F : Z --> X )   &    |- ( ph -> A. k e. ZZ A. u e. ( S ` k ) A. v e. ( S ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) )   &    |- ( ph -> A. k e. Z A. n e. ( M ... k ) ( F ` k ) e. ( S ` n ) )   =>    |- ( ph -> F e. ( Cau ` D ) )
Theorem	iscmet3lem2 23090*	Lemma for iscmet3 23091. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- Z = ( ZZ>= ` M )   &    |- J = ( MetOpen ` D )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> D e. ( Met ` X ) )   &    |- ( ph -> F : Z --> X )   &    |- ( ph -> A. k e. ZZ A. u e. ( S ` k ) A. v e. ( S ` k ) ( u D v ) < ( ( 1 / 2 ) ^ k ) )   &    |- ( ph -> A. k e. Z A. n e. ( M ... k ) ( F ` k ) e. ( S ` n ) )   &    |- ( ph -> G e. ( Fil ` X ) )   &    |- ( ph -> S : ZZ --> G )   &    |- ( ph -> F e. dom ( ~~> t ` J ) )   =>    |- ( ph -> ( J fLim G ) =/= (/) )
Theorem	iscmet3 23091*	The property " D is a complete metric" expressed in terms of functions on NN (or any other upper integer set). Thus, we only have to look at functions on NN, and not all possible Cauchy filters, to determine completeness. (The proof uses countable choice.) (Contributed by NM, 18-Dec-2006.) (Revised by Mario Carneiro, 5-May-2014.)
|- Z = ( ZZ>= ` M )   &    |- J = ( MetOpen ` D )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> D e. ( Met ` X ) )   =>    |- ( ph -> ( D e. ( CMet ` X ) <-> A. f e. ( Cau ` D ) ( f : Z --> X -> f e. dom ( ~~> t ` J ) ) ) )
Theorem	iscmet2 23092	A metric D is complete iff all Cauchy sequences converge to a point in the space. The proof uses countable choice. Part of Definition 1.4-3 of [Kreyszig] p. 28. (Contributed by NM, 7-Sep-2006.) (Revised by Mario Carneiro, 15-Oct-2015.)
|- J = ( MetOpen ` D )   =>    |- ( D e. ( CMet ` X ) <-> ( D e. ( Met ` X ) /\ ( Cau ` D ) C_ dom ( ~~> t ` J ) ) )
Theorem	cfilresi 23093	A Cauchy filter on a metric subspace extends to a Cauchy filter in the larger space. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- ( ( D e. ( *Met ` X ) /\ F e. (CauFil ` ( D |` ( Y X. Y ) ) ) ) -> ( X filGen F ) e. (CauFil ` D ) )
Theorem	cfilres 23094	Cauchy filter on a metric subspace. (Contributed by Mario Carneiro, 15-Oct-2015.)
|- ( ( D e. ( *Met ` X ) /\ F e. ( Fil ` X ) /\ Y e. F ) -> ( F e. (CauFil ` D ) <-> ( F ↾t Y ) e. (CauFil ` ( D |` ( Y X. Y ) ) ) ) )
Theorem	caussi 23095	Cauchy sequence on a metric subspace. (Contributed by NM, 30-Jan-2008.) (Revised by Mario Carneiro, 30-Dec-2013.)
|- ( D e. ( *Met ` X ) -> ( Cau ` ( D |` ( Y X. Y ) ) ) C_ ( Cau ` D ) )
Theorem	causs 23096	Cauchy sequence on a metric subspace. (Contributed by NM, 29-Jan-2008.) (Revised by Mario Carneiro, 30-Dec-2013.)
|- ( ( D e. ( *Met ` X ) /\ F : NN --> Y ) -> ( F e. ( Cau ` D ) <-> F e. ( Cau ` ( D |` ( Y X. Y ) ) ) ) )
Theorem	equivcfil 23097*	If the metric D is "strongly finer" than C (meaning that there is a positive real constant R such that C ( x , y ) <_ R x. D ( x , y )), all the D-Cauchy filters are also C-Cauchy. (Using this theorem twice in each direction states that if two metrics are strongly equivalent, then they have the same Cauchy sequences.) (Contributed by Mario Carneiro, 14-Sep-2015.)
|- ( ph -> C e. ( Met ` X ) )   &    |- ( ph -> D e. ( Met ` X ) )   &    |- ( ph -> R e. RR+ )   &    |- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x C y ) <_ ( R x. ( x D y ) ) )   =>    |- ( ph -> (CauFil ` D ) C_ (CauFil ` C ) )
Theorem	equivcau 23098*	If the metric D is "strongly finer" than C (meaning that there is a positive real constant R such that C ( x , y ) <_ R x. D ( x , y )), all the D-Cauchy sequences are also C-Cauchy. (Using this theorem twice in each direction states that if two metrics are strongly equivalent, then they have the same Cauchy sequences.) (Contributed by Mario Carneiro, 14-Sep-2015.)
|- ( ph -> C e. ( Met ` X ) )   &    |- ( ph -> D e. ( Met ` X ) )   &    |- ( ph -> R e. RR+ )   &    |- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x C y ) <_ ( R x. ( x D y ) ) )   =>    |- ( ph -> ( Cau ` D ) C_ ( Cau ` C ) )
Theorem	lmle 23099*	If the distance from each member of a converging sequence to a given point is less than or equal to a given amount, so is the convergence value. (Contributed by NM, 23-Dec-2007.) (Proof shortened by Mario Carneiro, 1-May-2014.)
|- Z = ( ZZ>= ` M )   &    |- J = ( MetOpen ` D )   &    |- ( ph -> D e. ( *Met ` X ) )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F ( ~~> t ` J ) P )   &    |- ( ph -> Q e. X )   &    |- ( ph -> R e. RR* )   &    |- ( ( ph /\ k e. Z ) -> ( Q D ( F ` k ) ) <_ R )   =>    |- ( ph -> ( Q D P ) <_ R )
Theorem	nglmle 23100*	If the norm of each member of a converging sequence is less than or equal to a given amount, so is the norm of the convergence value. (Contributed by NM, 25-Dec-2007.) (Revised by AV, 16-Oct-2021.)
|- X = ( Base ` G )   &    |- D = ( ( dist ` G ) |` ( X X. X ) )   &    |- J = ( MetOpen ` D )   &    |- N = ( norm ` G )   &    |- ( ph -> G e. NrmGrp )   &    |- ( ph -> F : NN --> X )   &    |- ( ph -> F ( ~~> t ` J ) P )   &    |- ( ph -> R e. RR* )   &    |- ( ( ph /\ k e. NN ) -> ( N ` ( F ` k ) ) <_ R )   =>    |- ( ph -> ( N ` P ) <_ R )