mmtheorems83 - Metamath Proof Explorer

Jump to page: Contents + 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12229

Statement List for Metamath Proof Explorer - 8201-8300 - Page 83 of 123

Type	Label	Description
Statement
Theorem	fsumcn 8201	A finite sum of functions to complex numbers from a common metric space is continuous. The class expression for F normally contains free variable k to index it.
|- C e. Met   &   |- X = dom dom C   &   |- D = (abs o. - )   &   |- J = (Open` C)   &   |- K = (Open` D)   &   |- (k e. NN -> F e. (J Cn K))   &   |- G = {<.w, v>. | (w e. X /\ v = sum_k e. (1...N)(F` w))}   =>   |- (N e. NN -> G e. (J Cn K))
Theorem	iscms2lem3 8202	Lemma for iscms2 8205. If the arbitrary sequence F is Cauchy, so is the constructed function G.
Theorem	iscms2lem4 8203	Lemma for iscms2 8205. Whenever the constructed function G converges, so does the arbitrary Cauchy sequence F.
Theorem	iscms2lem5 8204	Lemma for iscms2 8205. If all Cauchy sequences g that are functions on NN converge, then any arbitrary Cauchy sequence F also converges.
Theorem	iscms2 8205	The property "D is a complete metric" expressed in terms of functions on NN. Thus we only have to look at functions on NN, and not all possible Cauchy sequences, to determine completeness.
|- X = dom dom D   =>   |- (D e. CMet <-> (D e. Met /\ A.f e. (Cau` D)(f:NN-->X -> E.x e. X f(~~>m` D)x)))
Theorem	iscms2i 8206	Properties that determine a complete metric space.
|- X = dom dom D   &   |- D e. Met   &   |- ((f e. (Cau` D) /\ f:NN-->X) -> E.x e. X f(~~>m` D)x)   =>   |- D e. CMet
Theorem	lmcau 8207	Every convergent sequence in a metric space is a Cauchy sequence. Theorem 1.4-5 of [Kreyszig] p. 28. Warning: The HTML proof page is 0.5MB in size.
|- P e. V   =>   |- ((D e. Met /\ F(~~>m` D)P) -> F e. (Cau` D))
Theorem	cmsss 8208	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.
|- X = dom dom D   &   |- J = (Open` D)   =>   |- ((D e. CMet /\ Y (_ X) -> ((D |` (Y X. Y)) e. CMet <-> Y e. (Clsd` J)))
Examples of complete metric spaces
Theorem	cncms 8209	The set of complex numbers is a complete metric space under the absolute value metric.
|- D = (abs o. - )   =>   |- D e. CMet
Baire's Category Theorem
Theorem	bcthlem1 8210	Lemma for bcth 8243. Property of exponentially decreasing terms.
Theorem	bcthlem2 8211	Lemma for bcth 8243. For any m, we can always find a greater n meeting the convergence criterion.
Theorem	bcthlem3 8212	Lemma for bcth 8243. Two ways to express the first component of a ball (expressed as an ordered pair) in the sequence of balls g.
Theorem	bcthlem4 8213	Lemma for bcth 8243. Closure of the ball components in a sequence g of ordered pairs (that represents a sequence of balls).
Theorem	bcthlem5 8214	Lemma for bcth 8243. Helper lemma expressing the base set for use with topology theorems.
Theorem	bcthlem6 8215	Lemma for bcth 8243. Helper lemma showing the open sets of the metric D form a topology.
Theorem	bcthlem7 8216	Lemma for bcth 8243. If M is rare in X, i.e. the interior of its closure is empty, then its closure does not include any ball.
Theorem	bcthlem8 8217	Lemma for bcth 8243. Any open nonempty set includes a ball of radius less than 1 / (2^k).
Theorem	bcthlem9 8218	Lemma for bcth 8243. If M is rare in X, the intersection of the complement of its closure with any ball is nonempty and open. (Use bcthlem8 8217 for existence of an included ball.)
Theorem	bcthlem10 8219	Lemma for bcth 8243. If M is rare in X, the complement of its closure is not empty and is open.
Theorem	bcthlem11 8220	Lemma for bcth 8243. Triangle inequality.
Theorem	bcthlem12 8221	Lemma for bcth 8243. Helper lemma for satisfying the antecendent of acdc5 7705.
Theorem	bcthlem13 8222	Lemma for bcth 8243. In the sequence g of balls (expressed as ordered pairs), for any m, there is a larger n whose ball's center distance from limit p is less than half of the ball radius at m.
Theorem	bcthlem14 8223	Lemma for bcth 8243. Helper lemma for satisfying the antecendent of acdc5 7705.
Theorem	bcthlem15 8224	Lemma for bcth 8243. Relationship between a ball Q and the next ball P in sequence g, according to the generating function F 's value (KFQ).
Theorem	bcthlem16 8225	Lemma for bcth 8243. A ball in sequence g is included in the complement of the closure of reference sequence M.
Theorem	bcthlem17 8226	Lemma for bcth 8243. The radius of the balls in sequence g decreases exponentially.
Theorem	bcthlem18 8227	Lemma for bcth 8243. Sequence g represents a series of nested balls.
Theorem	bcthlem19 8228	Lemma for bcth 8243. The distance between the center of a ball at m and any later ball in sequence g is less than half the radius of the ball at m.
Theorem	bcthlem20 8229	Lemma for bcth 8243. A weaker version of bcthlem19 8228.
Theorem	bcthlem21 8230	Lemma for bcth 8243. A defining property for (1st o. g) to be a Cauchy sequence.
Theorem	bcthlem22 8231	Lemma for bcth 8243. The sequence of ball centers (1st o. g) is a Cauchy sequence.
Theorem	bcthlem23 8232	Lemma for bcth 8243. Since sequence of ball centers (1st o. g) is a Cauchy sequence and the metric space is complete, the sequence converges to a point p in the metric space.
Theorem	bcthlem24 8233	Lemma for bcth 8243. An upper limit for the distance between a ball center at m and the convergence point q, in terms of any later ball center at n.
Theorem	bcthlem25 8234	Lemma for bcth 8243. Helper lemma to remove the dependence on n of the upper limit in bcthlem24 8233.
Theorem	bcthlem26 8235	Lemma for bcth 8243. The convergence point q belongs to every ball in sequence g.
Theorem	bcthlem27 8236	Lemma for bcth 8243. The convergence point q belongs to the complement of the interior of any member of reference sequence M.
Theorem	bcthlem28 8237	Lemma for bcth 8243. The convergence point q does not belong to any member of reference sequence M.
Theorem	bcthlem29 8238	Lemma for bcth 8243. Therefore the union of all members of reference sequence M does not occupy the entire metric space X. Also, use metric space completeness (via bcthlem23 8232) to eliminate the limit point q from the antecedents.
Theorem	bcthlem30 8239	Lemma for bcth 8243. Apply the Axiom of Dependent Choice acdc5 7705 to show the existence of the recursive sequence of balls g.
Theorem	bcthlem31 8240	Lemma for bcth 8243. Eliminate the antecedents involving sequence g.
Theorem	bcthlem32 8241	Lemma for bcth 8243. Eliminate hypotheses no longer needed.
Theorem	bcthlem33 8242	Lemma for bcth 8243. All members of reference sequence M cannot have an empty interior.
Theorem	bcth 8243	Baire's Category Theorem. If a nonempty metric space is complete, it is nonmeager in itself. In other words, the metric space cannot be the countable union of rare closed subsets (where rare means having an 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.)
|- X = dom dom D   &   |- J = (Open` D)   =>   |- (((D e. CMet /\ X =/= (/) /\ M:NN-->P~X) /\ (U.ran M = X /\ ran M (_ (Clsd` J))) -> E.k e. NN ((int` J)` (M` k)) =/= (/))
Group theory
Definitions and basic properties for groups
Syntax	cgr 8244	Extend class notation with the class of all group operations.
class Grp
Syntax	cgi 8245	Extend class notation with a function mapping a group operation to the group's identity element.
class Id
Syntax	cgn 8246	Extend class notation with a function mapping a group operation to the inverse function for the group.
class inv
Syntax	cgs 8247	Extend class notation with a function mapping a group operation to the division (or subtraction) operation for the group.
class /g
Syntax	cgx 8248	Extend class notation with a function mapping a group operation to the power operation for the group.
class ^g
Definition	df-grp 8249	Define the class of all group operations. The base set for a group can be determined from its group operation. Based on the definition in Exercise 28 of [Herstein] p. 54.
|- Grp = {g | E.t(g:(t X. t)-->t /\ A.x e. t A.y e. t A.z e. t ((xgy)gz) = (xg(ygz)) /\ E.u e. t A.x e. t ((ugx) = x /\ E.y e. t (ygx) = u))}
Definition	df-gid 8250	Define a function that maps a group operation to the group's identity element.
|- Id = {<.g, y>. | y = U.{u e. ran g | A.x e. ran g((ugx) = x /\ (xgu) = x)}}
Definition	df-ginv 8251	Define a function that maps a group operation to the group's inverse function.
|- inv = {<.g, f>. | (g e. Grp /\ f = {<.x, y>. | (x e. ran g /\ y = U.{z e. ran g | (zgx) = (Id` g)})})}
Definition	df-gdiv 8252	Define a function that maps a group operation to the group's division (or subtraction) operation.
|- /g = {<.g, f>. | (g e. Grp /\ f = {<.<.x, y>., z>. | ((x e. ran g /\ y e. ran g) /\ z = (xg((inv` g)` y)))})}
Definition	df-gx 8253	Define a function that maps a group operation to the group's power operation.
|- ^g = {<.g, f>. | (g e. Grp /\ f = {<.<.x, y>., z>. | ((x e. ran g /\ y e. ZZ) /\ z = if(y = 0, (Id` g), if(0 < y, ((g seq1 (NN X. {x}))` y), ((inv` g)` ((g seq1 (NN X. {x}))` -uy)))))})}
Theorem	isgrp 8254	The predicate "is a group operation." Note that X is the base set of the group.
|- X = ran G   =>   |- (G e. A -> (G e. Grp <-> (G:(X X. X)-->X /\ A.x e. X A.y e. X A.z e. X ((xGy)Gz) = (xG(yGz)) /\ E.u e. X A.x e. X ((uGx) = x /\ E.y e. X (yGx) = u))))
Theorem	isgrpi 8255	Properties that determine a group operation. Read N as N(x).
|- X e. V   &   |- G:(X X. X)-->X   &   |- ((x e. X /\ y e. X /\ z e. X) -> ((xGy)Gz) = (xG(yGz)))   &   |- U e. X   &   |- (x e. X -> (UGx) = x)   &   |- (x e. X -> N e. X)   &   |- (x e. X -> (NGx) = U)   =>   |- G e. Grp
Theorem	grpfo 8256	A group operation maps onto the group's underlying set.
|- X = ran G   =>   |- (G e. Grp -> G:(X X. X)-onto->X)
Theorem	grpcl 8257	Closure law for a group operation.
|- X = ran G   =>   |- ((G e. Grp /\ A e. X /\ B e. X) -> (AGB) e. X)
Theorem	grplidinv 8258	A group has a left identity element, and every member has a left inverse.
|- X = ran G   =>   |- (G e. Grp -> E.u e. X A.x e. X ((uGx) = x /\ E.y e. X (yGx) = u))
Theorem	grpn0 8259	The base set of a group is not empty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.)
|- X = ran G   =>   |- (G e. Grp -> X =/= (/))
Theorem	grpass 8260	A group operation is associative.
|- X = ran G   =>   |- ((G e. Grp /\ (A e. X /\ B e. X /\ C e. X)) -> ((AGB)GC) = (AG(BGC)))
Theorem	grpidinvlem1 8261	Lemma for grpidinv 8265.
Theorem	grpidinvlem2 8262	Lemma for grpidinv 8265.
Theorem	grpidinvlem3 8263	Lemma for grpidinv 8265.
Theorem	grpidinvlem4 8264	Lemma for grpidinv 8265.
Theorem	grpidinv 8265	A group has a left and right identity element, and every member has a left and right inverse.
|- X = ran G   =>   |- (G e. Grp -> E.u e. X A.x e. X (((uGx) = x /\ (xGu) = x) /\ E.y e. X ((yGx) = u /\ (xGy) = u)))
Theorem	grpideu 8266	The left identity element of a group is unique. Lemma 2.2.1(a) of [Herstein] p. 55.
|- X = ran G   =>   |- (G e. Grp -> E!u e. X A.x e. X (uGx) = x)
Theorem	grprndm 8267	A group's range in terms of its domain.
|- (G e. Grp -> ran G = dom dom G)
Theorem	0ngrp 8268	The empty set is not a group.
|- -. (/) e. Grp
Theorem	grprn 8269	The range of a group operation. Useful for satisfying group base set hypotheses of the form X = ran G.
|- G e. Grp   &   |- dom G = (X X. X)   =>   |- X = ran G
Theorem	grprlidrid 8270	In a group a left and right identity element is a left identity element. (Contributed by FL, 5-Feb-2010.)
|- X = ran G   =>   |- (G e. Grp -> U.{u e. X | A.x e. X ((uGx) = x /\ (xGu) = x)} = U.{u e. X | A.x e. X (uGx) = x})
Theorem	gid0 8271	The identity of the empty set is the empty set. (Contributed by FL, 5-Feb-2010.)
|- (Id` (/)) = (/)
Theorem	fungid 8272	Id is a function. (Contributed by FL, 5-Feb-2010.)
|- Fun Id
Theorem	grpsn 8273	The group operation for the singleton group.
|- A e. V   =>   |- {<.<.A, A>., A>.} e. Grp
Theorem	grpidvallem 8274	The value of the identity element of a group.
|- X = ran G   &   |- U = (Id` G)   &   |- G e. Grp   =>   |- U = U.{u e. X | A.x e. X (uGx) = x}
Theorem	grpidval 8275	The value of the identity element of a group.
|- X = ran G   &   |- U = (Id` G)   =>   |- (G e. Grp -> U = U.{u e. X | A.x e. X (uGx) = x})
Theorem	grpidcl 8276	The identity element of a group belongs to the group.
|- X = ran G   &   |- U = (Id` G)   =>   |- (G e. Grp -> U e. X)
Theorem	grpidinv2 8277	A group's properties using the explicit identity element.
|- X = ran G   &   |- U = (Id` G)   =>   |- ((G e. Grp /\ A e. X) -> (((UGA) = A /\ (AGU) = A) /\ E.y e. X ((yGA) = U /\ (AGy) = U)))
Theorem	grplid 8278	The identity element of a group is a left identity.
|- X = ran G   &   |- U = (Id` G)   =>   |- ((G e. Grp /\ A e. X) -> (UGA) = A)
Theorem	grprid 8279	The identity element of a group is a right identity.
|- X = ran G   &   |- U = (Id` G)   =>   |- ((G e. Grp /\ A e. X) -> (AGU) = A)
Theorem	grprcan 8280	Right cancellation law for groups.
|- X = ran G   =>   |- ((G e. Grp /\ (A e. X /\ B e. X /\ C e. X)) -> ((AGC) = (BGC) <-> A = B))
Theorem	grpinveu 8281	The left inverse element of a group is unique. Lemma 2.2.1(b) of [Herstein] p. 55.
|- X = ran G   &   |- U = (Id` G)   =>   |- ((G e. Grp /\ A e. X) -> E!y e. X (yGA) = U)
Theorem	grpid 8282	Two ways of saying that an element of a group is the identity element. (Contributed by Paul Chapman, 25-Feb-2008.)
|- X = ran G   &   |- U = (Id` G)   =>   |- ((G e. Grp /\ A e. X) -> (A = U <-> (AGA) = A))
Theorem	grpinvfval 8283	The inverse function of a group.
|- X = ran G   &   |- U = (Id` G)   &   |- N = (inv` G)   =>   |- (G e. Grp -> N = {<.x, n>. | (x e. X /\ n = U.{y e. X | (yGx) = U})})
Theorem	grpinvval 8284	The inverse of a group element.
|- X = ran G   &   |- U = (Id` G)   &   |- N = (inv` G)   =>   |- ((G e. Grp /\ A e. X) -> (N` A) = U.{y e. X | (yGA) = U})
Theorem	grpinvcl 8285	A group element's inverse is a group element.
|- X = ran G   &   |- N = (inv` G)   =>   |- ((G e. Grp /\ A e. X) -> (N` A) e. X)
Theorem	grpinv 8286	The properties of a group element's inverse.
|- X = ran G   &   |- U = (Id` G)   &   |- N = (inv` G)   =>   |- ((G e. Grp /\ A e. X) -> (((N` A)GA) = U /\ (AG(N` A)) = U))
Theorem	grplinv 8287	The left inverse of a group element.
|- X = ran G   &   |- U = (Id` G)   &   |- N = (inv` G)   =>   |- ((G e. Grp /\ A e. X) -> ((N` A)GA) = U)
Theorem	grprinv 8288	The right inverse of a group element.
|- X = ran G   &   |- U = (Id` G)   &   |- N = (inv` G)   =>   |- ((G e. Grp /\ A e. X) -> (AG(N` A)) = U)
Theorem	grpinvid1 8289	The inverse of a group element expressed in terms of the identity element.
|- X = ran G   &   |- U = (Id` G)   &   |- N = (inv` G)   =>   |- ((G e. Grp /\ A e. X /\ B e. X) -> ((N` A) = B <-> (AGB) = U))
Theorem	grpinvid2 8290	The inverse of a group element expressed in terms of the identity element.
|- X = ran G   &   |- U = (Id` G)   &   |- N = (inv` G)   =>   |- ((G e. Grp /\ A e. X /\ B e. X) -> ((N` A) = B <-> (BGA) = U))
Theorem	grpinvid 8291	The inverse of the identity element of a group.
|- U = (Id` G)   &   |- N = (inv` G)   =>   |- (G e. Grp -> (N` U) = U)
Theorem	grplcan 8292	Left cancellation law for groups.
|- X = ran G   =>   |- ((G e. Grp /\ (A e. X /\ B e. X /\ C e. X)) -> ((CGA) = (CGB) <-> A = B))
Theorem	isgrp2i 8293	An alternate way to show a group operation. Exercise 1 of [Herstein] p. 57.
|- X e. V   &   |- X =/= (/)   &   |- G:(X X. X)-->X   &   |- ((x e. X /\ y e. X /\ z e. X) -> ((xGy)Gz) = (xG(yGz)))   &   |- ((x e. X /\ y e. X) -> E.z e. X (zGx) = y)   &   |- ((x e. X /\ y e. X) -> E.z e. X (xGz) = y)   =>   |- G e. Grp
Theorem	grpasscan1 8294	An associative cancellation law for groups. (Contributed by Paul Chapman, 25-Feb-2008.)
|- X = ran G   &   |- N = (inv` G)   =>   |- ((G e. Grp /\ A e. X /\ B e. X) -> (AG((N` A)GB)) = B)
Theorem	grpasscan2 8295	An associative cancellation law for groups. (Contributed by Paul Chapman, 17-Apr-2009.)
|- X = ran G   &   |- N = (inv` G)   =>   |- ((G e. Grp /\ A e. X /\ B e. X) -> ((AG(N` B))GB) = A)
Theorem	grp2inv 8296	Double inverse law for groups. Lemma 2.2.1(c) of [Herstein] p. 55.
|- X = ran G   &   |- N = (inv` G)   =>   |- ((G e. Grp /\ A e. X) -> (N` (N` A)) = A)
Theorem	grpinvf 8297	Mapping of the inverse function of a group.
|- X = ran G   &   |- N = (inv` G)   =>   |- (G e. Grp -> N:X-1-1-onto->X)
Theorem	grpinvop 8298	The inverse of the group operation reverses the arguments. Lemma 2.2.1(d) of [Herstein] p. 55.
|- X = ran G   &   |- N = (inv` G)   =>   |- ((G e. Grp /\ A e. X /\ B e. X) -> (N` (AGB)) = ((N` B)G(N` A)))
Theorem	grpdivfval 8299	Group division (or subtraction) operation.
|- X = ran G   &   |- N = (inv` G)   &   |- D = ( /g ` G)   =>   |- (G e. Grp -> D = {<.<.x, y>., z>. | ((x e. X /\ y e. X) /\ z = (xG(N` y)))})
Theorem	grpdivval 8300	Group division (or subtraction) operation value.
|- X = ran G   &   |- N = (inv` G)   &   |- D = ( /g ` G)   =>   |- ((G e. Grp /\ A e. X /\ B e. X) -> (ADB) = (AG(N` B)))