Home | Metamath
Proof Explorer Theorem List (p. 162 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | cgsu 16101 | Extend class notation to include finitely supported group sums. |
g | ||
Definition | df-0g 16102* | Define group identity element. Remark: this definition is required here because the symbol is already used in df-gsum 16103. The related theorems are provided later, see grpidval 17260. (Contributed by NM, 20-Aug-2011.) |
Definition | df-gsum 16103* |
Define the group sum for the structure of a finite sequence of
elements whose values are defined by the expression and whose set
of indices is .
It may be viewed as a product (if is a
multiplication), a sum (if is an addition) or whatever. The
variable is
normally a free variable in ( i.e. can
be
thought of as ). The definition is meaningful in different
contexts, depending on the size of the index set and each
demanding different properties of .
1. If and has an identity element, then the sum equals this identity. 2. If and is any magma, then the sum is the sum of the elements, evaluated left-to-right, i.e. etc. 3. If is a finite set (or is nonzero for finitely many indices) and is a commutative monoid, then the sum adds up these elements in some order, which is then uniquely defined. 4. If is an infinite set and is a Hausdorff topological group, then there is a meaningful sum, but g cannot handle this case. See df-tsms 21930. Remark: this definition is required here because the symbol g is already used in df-prds 16108 and df-imas 16168. The related theorems are provided later, see gsumvalx 17270. (Contributed by FL, 5-Sep-2010.) (Revised by FL, 17-Oct-2011.) (Revised by Mario Carneiro, 7-Dec-2014.) |
g | ||
Definition | df-topgen 16104* | Define a function that converts a basis to its corresponding topology. Equivalent to the definition of a topology generated by a basis in [Munkres] p. 78 (see tgval2 20760). The first use of this definition is tgval 20759 but the token is used in df-pt 16105. See tgval3 20767 for an alternate expression for the value. (Contributed by NM, 16-Jul-2006.) |
Definition | df-pt 16105* | Define the product topology on a collection of topologies. For convenience, it is defined on arbitrary collections of sets, expressed as a function from some index set to the subbases of each factor space. (Contributed by Mario Carneiro, 3-Feb-2015.) |
Syntax | cprds 16106 | The function constructing structure products. |
s | ||
Syntax | cpws 16107 | The function constructing structure powers. |
s | ||
Definition | df-prds 16108* | Define a structure product. This can be a product of groups, rings, modules, or ordered topological fields; any unused components will have garbage in them but this is usually not relevant for the purpose of inheriting the structures present in the factors. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Thierry Arnoux, 15-Jun-2019.) |
s Scalar g TopSet comp comp | ||
Theorem | reldmprds 16109 | The structure product is a well-behaved binary operator. (Contributed by Stefan O'Rear, 7-Jan-2015.) (Revised by Thierry Arnoux, 15-Jun-2019.) |
s | ||
Definition | df-pws 16110* | Define a structure power, which is just a structure product where all the factors are the same. (Contributed by Mario Carneiro, 11-Jan-2015.) |
s Scalars | ||
Theorem | prdsbasex 16111* | Lemma for structure products. (Contributed by Mario Carneiro, 3-Jan-2015.) |
Theorem | imasvalstr 16112 | Structure product value is a structure. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 30-Apr-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
Scalar TopSet Struct ; | ||
Theorem | prdsvalstr 16113 | Structure product value is a structure. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 30-Apr-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
Scalar TopSet comp Struct ; | ||
Theorem | prdsvallem 16114 | Lemma for prdsbas 16117 and similar theorems. (Contributed by Mario Carneiro, 7-Jan-2017.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
Scalar TopSet comp Slot Scalar TopSet comp | ||
Theorem | prdsval 16115* | Value of the structure product. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 7-Jan-2017.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
s g comp Scalar TopSet comp | ||
Theorem | prdssca 16116 | Scalar ring of a structure product. (Contributed by Stefan O'Rear, 5-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
s Scalar | ||
Theorem | prdsbas 16117* | Base set of a structure product. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
s | ||
Theorem | prdsplusg 16118* | Addition in a structure product. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
s | ||
Theorem | prdsmulr 16119* | Multiplication in a structure product. (Contributed by Mario Carneiro, 11-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
s | ||
Theorem | prdsvsca 16120* | Scalar multiplication in a structure product. (Contributed by Stefan O'Rear, 5-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
s | ||
Theorem | prdsip 16121* | Inner product in a structure product. (Contributed by Thierry Arnoux, 16-Jun-2019.) |
s g | ||
Theorem | prdsle 16122* | Structure product weak ordering. (Contributed by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
s | ||
Theorem | prdsless 16123 | Closure of the order relation on a structure product. (Contributed by Mario Carneiro, 16-Aug-2015.) |
s | ||
Theorem | prdsds 16124* | Structure product distance function. (Contributed by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
s | ||
Theorem | prdsdsfn 16125 | Structure product distance function. (Contributed by Mario Carneiro, 15-Sep-2015.) |
s | ||
Theorem | prdstset 16126 | Structure product topology. (Contributed by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
s TopSet | ||
Theorem | prdshom 16127* | Structure product hom-sets. (Contributed by Mario Carneiro, 7-Jan-2017.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
s | ||
Theorem | prdsco 16128* | Structure product composition operation. (Contributed by Mario Carneiro, 7-Jan-2017.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
s comp comp | ||
Theorem | prdsbas2 16129* | The base set of a structure product is an indexed set product. (Contributed by Stefan O'Rear, 10-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.) |
s | ||
Theorem | prdsbasmpt 16130* | A constructed tuple is a point in a structure product iff each coordinate is in the proper base set. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
s | ||
Theorem | prdsbasfn 16131 | Points in the structure product are functions; use this with dffn5 6241 to establish equalities. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
s | ||
Theorem | prdsbasprj 16132 | Each point in a structure product restricts on each coordinate to the relevant base set. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
s | ||
Theorem | prdsplusgval 16133* | Value of a componentwise sum in a structure product. (Contributed by Stefan O'Rear, 10-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.) |
s | ||
Theorem | prdsplusgfval 16134 | Value of a structure product sum at a single coordinate. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
s | ||
Theorem | prdsmulrval 16135* | Value of a componentwise ring product in a structure product. (Contributed by Mario Carneiro, 11-Jan-2015.) |
s | ||
Theorem | prdsmulrfval 16136 | Value of a structure product's ring product at a single coordinate. (Contributed by Mario Carneiro, 11-Jan-2015.) |
s | ||
Theorem | prdsleval 16137* | Value of the product ordering in a structure product. (Contributed by Mario Carneiro, 15-Aug-2015.) |
s | ||
Theorem | prdsdsval 16138* | Value of the metric in a structure product. (Contributed by Mario Carneiro, 20-Aug-2015.) |
s | ||
Theorem | prdsvscaval 16139* | Scalar multiplication in a structure product is pointwise. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
s | ||
Theorem | prdsvscafval 16140 | Scalar multiplication of a single coordinate in a structure product. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
s | ||
Theorem | prdsbas3 16141* | The base set of an indexed structure product. (Contributed by Mario Carneiro, 13-Sep-2015.) |
s | ||
Theorem | prdsbasmpt2 16142* | A constructed tuple is a point in a structure product iff each coordinate is in the proper base set. (Contributed by Mario Carneiro, 3-Jul-2015.) (Revised by Mario Carneiro, 13-Sep-2015.) |
s | ||
Theorem | prdsbascl 16143* | An element of the base has projections closed in the factors. (Contributed by Mario Carneiro, 27-Aug-2015.) |
s | ||
Theorem | prdsdsval2 16144* | Value of the metric in a structure product. (Contributed by Mario Carneiro, 20-Aug-2015.) |
s | ||
Theorem | prdsdsval3 16145* | Value of the metric in a structure product. (Contributed by Mario Carneiro, 27-Aug-2015.) |
s | ||
Theorem | pwsval 16146 | Value of a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.) |
s Scalar s | ||
Theorem | pwsbas 16147 | Base set of a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.) |
s | ||
Theorem | pwselbasb 16148 | Membership in the base set of a structure product. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
s | ||
Theorem | pwselbas 16149 | An element of a structure power is a function from the index set to the base set of the structure. (Contributed by Mario Carneiro, 11-Jan-2015.) (Revised by Mario Carneiro, 5-Jun-2015.) |
s | ||
Theorem | pwsplusgval 16150 | Value of addition in a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.) |
s | ||
Theorem | pwsmulrval 16151 | Value of multiplication in a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.) |
s | ||
Theorem | pwsle 16152 | Ordering in a structure power. (Contributed by Mario Carneiro, 16-Aug-2015.) |
s | ||
Theorem | pwsleval 16153* | Ordering in a structure power. (Contributed by Mario Carneiro, 16-Aug-2015.) |
s | ||
Theorem | pwsvscafval 16154 | Scalar multiplication in a structure power is pointwise. (Contributed by Mario Carneiro, 11-Jan-2015.) |
s Scalar | ||
Theorem | pwsvscaval 16155 | Scalar multiplication of a single coordinate in a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.) |
s Scalar | ||
Theorem | pwssca 16156 | The ring of scalars of a structure product. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
s Scalar Scalar | ||
Theorem | pwsdiagel 16157 | Membership of diagonal elements in the structure power base set. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
s | ||
Theorem | pwssnf1o 16158* | Triviality of singleton powers: set equipollence. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
s | ||
Syntax | cordt 16159 | Extend class notation with the order topology. |
ordTop | ||
Syntax | cxrs 16160 | Extend class notation with the extended real number structure. |
Definition | df-ordt 16161* | Define the order topology, given an order , written as below. A closed subbasis for the order topology is given by the closed rays and , along with itself. (Contributed by Mario Carneiro, 3-Sep-2015.) |
ordTop | ||
Definition | df-xrs 16162* | The extended real number structure. Unlike df-cnfld 19747, the extended real numbers do not have good algebraic properties, so this is not actually a group or anything higher, even though it has just as many operations as df-cnfld 19747. The main interest in this structure is in its ordering, which is complete and compact. The metric described here is an extension of the absolute value metric, but it is not itself a metric because is infinitely far from all other points. The topology is based on the order and not the extended metric (which would make an isolated point since there is nothing else in the -ball around it). All components of this structure agree with ℂfld when restricted to . (Contributed by Mario Carneiro, 20-Aug-2015.) |
TopSet ordTop | ||
Syntax | cqtop 16163 | Extend class notation with the quotient topology function. |
qTop | ||
Syntax | cimas 16164 | Image structure function. |
s | ||
Syntax | cqus 16165 | Quotient structure function. |
s | ||
Syntax | cxps 16166 | Binary product structure function. |
s | ||
Definition | df-qtop 16167* | Define the quotient topology given a function and topology on the domain of . (Contributed by Mario Carneiro, 23-Mar-2015.) |
qTop | ||
Definition | df-imas 16168* |
Define an image structure, which takes a structure and a function on the
base set, and maps all the operations via the function. For this to
work properly
must either be injective or satisfy the
well-definedness condition
for each relevant operation.
Note that although we call this an "image" by association to df-ima 5127, in order to keep the definition simple we consider only the case when the domain of is equal to the base set of . Other cases can be achieved by restricting (with df-res 5126) and/or ( with df-ress 15865) to their common domain. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by AV, 6-Oct-2020.) |
s Scalar Scalar Scalar TopSet qTop inf g | ||
Definition | df-qus 16169* | Define a quotient ring (or quotient group), which is a special case of an image structure df-imas 16168 where the image function is . (Contributed by Mario Carneiro, 23-Feb-2015.) |
s s | ||
Definition | df-xps 16170* | Define a binary product on structures. (Contributed by Mario Carneiro, 14-Aug-2015.) |
s s Scalars | ||
Theorem | imasval 16171* | Value of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Mario Carneiro, 11-Jul-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 6-Oct-2020.) |
s Scalar qTop inf g Scalar TopSet | ||
Theorem | imasbas 16172 | The base set of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Mario Carneiro, 11-Jul-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 6-Oct-2020.) |
s | ||
Theorem | imasds 16173* | The distance function of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Mario Carneiro, 11-Jul-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 6-Oct-2020.) |
s inf g | ||
Theorem | imasdsfn 16174 | The distance function is a function on the base set. (Contributed by Mario Carneiro, 20-Aug-2015.) (Proof shortened by AV, 6-Oct-2020.) |
s | ||
Theorem | imasdsval 16175* | The distance function of an image structure. (Contributed by Mario Carneiro, 20-Aug-2015.) (Revised by AV, 6-Oct-2020.) |
s inf g | ||
Theorem | imasdsval2 16176* | The distance function of an image structure. (Contributed by Mario Carneiro, 20-Aug-2015.) (Revised by AV, 6-Oct-2020.) |
s inf g | ||
Theorem | imasplusg 16177* | The group operation in an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Mario Carneiro, 11-Jul-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
s | ||
Theorem | imasmulr 16178* | The ring multiplication in an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Mario Carneiro, 11-Jul-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
s | ||
Theorem | imassca 16179 | The scalar field of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
s Scalar Scalar | ||
Theorem | imasvsca 16180* | The scalar multiplication operation of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) |
s Scalar | ||
Theorem | imasip 16181* | The inner product of an image structure. (Contributed by Thierry Arnoux, 16-Jun-2019.) |
s | ||
Theorem | imastset 16182 | The topology of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) |
s TopSet qTop | ||
Theorem | imasle 16183 | The ordering of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015.) |
s | ||
Theorem | f1ocpbllem 16184 | Lemma for f1ocpbl 16185. (Contributed by Mario Carneiro, 24-Feb-2015.) |
Theorem | f1ocpbl 16185 | An injection is compatible with any operations on the base set. (Contributed by Mario Carneiro, 24-Feb-2015.) |
Theorem | f1ovscpbl 16186 | An injection is compatible with any operations on the base set. (Contributed by Mario Carneiro, 15-Aug-2015.) |
Theorem | f1olecpbl 16187 | An injection is compatible with any relations on the base set. (Contributed by Mario Carneiro, 24-Feb-2015.) |
Theorem | imasaddfnlem 16188* | The image structure operation is a function if the original operation is compatible with the function. (Contributed by Mario Carneiro, 23-Feb-2015.) |
Theorem | imasaddvallem 16189* | The operation of an image structure is defined to distribute over the mapping function. (Contributed by Mario Carneiro, 23-Feb-2015.) |
Theorem | imasaddflem 16190* | The image set operations are closed if the original operation is. (Contributed by Mario Carneiro, 23-Feb-2015.) |
Theorem | imasaddfn 16191* | The image structure's group operation is a function. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Mario Carneiro, 10-Jul-2015.) |
s | ||
Theorem | imasaddval 16192* | The value of an image structure's group operation. (Contributed by Mario Carneiro, 23-Feb-2015.) |
s | ||
Theorem | imasaddf 16193* | The image structure's group operation is closed in the base set. (Contributed by Mario Carneiro, 23-Feb-2015.) |
s | ||
Theorem | imasmulfn 16194* | The image structure's ring multiplication is a function. (Contributed by Mario Carneiro, 23-Feb-2015.) |
s | ||
Theorem | imasmulval 16195* | The value of an image structure's ring multiplication. (Contributed by Mario Carneiro, 23-Feb-2015.) |
s | ||
Theorem | imasmulf 16196* | The image structure's ring multiplication is closed in the base set. (Contributed by Mario Carneiro, 23-Feb-2015.) |
s | ||
Theorem | imasvscafn 16197* | The image structure's scalar multiplication is a function. (Contributed by Mario Carneiro, 24-Feb-2015.) |
s Scalar | ||
Theorem | imasvscaval 16198* | The value of an image structure's scalar multiplication. (Contributed by Mario Carneiro, 24-Feb-2015.) |
s Scalar | ||
Theorem | imasvscaf 16199* | The image structure's scalar multiplication is closed in the base set. (Contributed by Mario Carneiro, 24-Feb-2015.) |
s Scalar | ||
Theorem | imasless 16200 | The order relation defined on an image set is a subset of the base set. (Contributed by Mario Carneiro, 24-Feb-2015.) |
s |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |