Home Metamath Proof ExplorerTheorem List (p. 250 of 324) < Previous  Next > Browser slow? Try the Unicode version.

 Color key: Metamath Proof Explorer (1-22341) Hilbert Space Explorer (22342-23864) Users' Mathboxes (23865-32387)

Theorem List for Metamath Proof Explorer - 24901-25000   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremcvmliftlem8 24901* Lemma for cvmlift 24908. The functions are continuous functions because they are defined as where is continuous and is a homeomorphism. (Contributed by Mario Carneiro, 16-Feb-2015.)
t t                      CovMap                                                                       t

Theoremcvmliftlem9 24902* Lemma for cvmlift 24908. The functions are defined on almost disjoint intervals, but they overlap at the edges. Here we show that at these points the functions agree on their common domain. (Contributed by Mario Carneiro, 14-Feb-2015.)
t t                      CovMap

Theoremcvmliftlem10 24903* Lemma for cvmlift 24908. The function is going to be our complete lifted path, formed by unioning together all the functions (each of which is defined on one segment of the interval). Here we prove by induction that is a continuous function and a lift of by applying cvmliftlem6 24899, cvmliftlem7 24900 (to show it is a function and a lift), cvmliftlem8 24901 (to show it is continuous), and cvmliftlem9 24902 (to show that different functions agree on the intersection of their domains, so that the pasting lemma paste 17298 gives that is well-defined and continuous). (Contributed by Mario Carneiro, 14-Feb-2015.)
t t                      CovMap                                                                       t        t

Theoremcvmliftlem11 24904* Lemma for cvmlift 24908. (Contributed by Mario Carneiro, 14-Feb-2015.)
t t                      CovMap

Theoremcvmliftlem13 24905* Lemma for cvmlift 24908. The initial value of is because is a subset of which takes value at . (Contributed by Mario Carneiro, 16-Feb-2015.)
t t                      CovMap

Theoremcvmliftlem14 24906* Lemma for cvmlift 24908. Putting the results of cvmliftlem11 24904, cvmliftlem13 24905 and cvmliftmo 24893 together, we have that is a continuous function, satisfies and , and is equal to any other function which also has these properties, so it follows that is the unique lift of . (Contributed by Mario Carneiro, 16-Feb-2015.)
t t                      CovMap

Theoremcvmliftlem15 24907* Lemma for cvmlift 24908. Discharge the assumptions of cvmliftlem14 24906. The set of all open subsets of the unit interval such that is contained in an even covering of some open set in is a cover of by the definition of a covering map, so by the Lebesgue number lemma lebnumii 18930, there is a subdivision of the unit interval into equal parts such that each part is entirely contained within one such open set of . Then using finite choice ac6sfi 7301 to uniformly select one such subset and one even covering of each subset, we are ready to finish the proof with cvmliftlem14 24906. (Contributed by Mario Carneiro, 14-Feb-2015.)
t t                      CovMap

Theoremcvmlift 24908* One of the important properties of covering maps is that any path in the base space "lifts" to a path in the covering space such that , and given a starting point in the covering space this lift is unique. The proof is contained in cvmliftlem1 24894 thru cvmliftlem15 24907. (Contributed by Mario Carneiro, 16-Feb-2015.)
CovMap

Theoremcvmfo 24909 A covering map is an onto function. (Contributed by Mario Carneiro, 13-Feb-2015.)
CovMap

Theoremcvmliftiota 24910* Write out a function that is the unique lift of . (Contributed by Mario Carneiro, 16-Feb-2015.)
CovMap

Theoremcvmlift2lem1 24911* Lemma for cvmlift2 24925. (Contributed by Mario Carneiro, 1-Jun-2015.)

Theoremcvmlift2lem9a 24912* Lemma for cvmlift2 24925 and cvmlift3 24937. (Contributed by Mario Carneiro, 9-Jul-2015.)
t t        CovMap                                                                t

Theoremcvmlift2lem2 24913* Lemma for cvmlift2 24925. (Contributed by Mario Carneiro, 7-May-2015.)
CovMap

Theoremcvmlift2lem3 24914* Lemma for cvmlift2 24925. (Contributed by Mario Carneiro, 7-May-2015.)
CovMap

Theoremcvmlift2lem4 24915* Lemma for cvmlift2 24925. (Contributed by Mario Carneiro, 1-Jun-2015.)
CovMap

Theoremcvmlift2lem5 24916* Lemma for cvmlift2 24925. (Contributed by Mario Carneiro, 7-May-2015.)
CovMap

Theoremcvmlift2lem6 24917* Lemma for cvmlift2 24925. (Contributed by Mario Carneiro, 7-May-2015.)
CovMap                                           t

Theoremcvmlift2lem7 24918* Lemma for cvmlift2 24925. (Contributed by Mario Carneiro, 7-May-2015.)
CovMap

Theoremcvmlift2lem8 24919* Lemma for cvmlift2 24925. (Contributed by Mario Carneiro, 9-Mar-2015.)
CovMap

Theoremcvmlift2lem9 24920* Lemma for cvmlift2 24925. (Contributed by Mario Carneiro, 1-Jun-2015.)
CovMap                                           t t                                    t        t                                    t               t

Theoremcvmlift2lem10 24921* Lemma for cvmlift2 24925. (Contributed by Mario Carneiro, 1-Jun-2015.)
CovMap                                           t t                      t t

Theoremcvmlift2lem11 24922* Lemma for cvmlift2 24925. (Contributed by Mario Carneiro, 1-Jun-2015.)
CovMap                                                                              t t

Theoremcvmlift2lem12 24923* Lemma for cvmlift2 24925. (Contributed by Mario Carneiro, 1-Jun-2015.)
CovMap

Theoremcvmlift2lem13 24924* Lemma for cvmlift2 24925. (Contributed by Mario Carneiro, 7-May-2015.)
CovMap

Theoremcvmlift2 24925* A two-dimensional version of cvmlift 24908. There is a unique lift of functions on the unit square which commutes with the covering map. (Contributed by Mario Carneiro, 1-Jun-2015.)
CovMap

Theoremcvmliftphtlem 24926* Lemma for cvmliftpht 24927. (Contributed by Mario Carneiro, 6-Jul-2015.)
CovMap

Theoremcvmliftpht 24927* If and are path-homotopic, then their lifts and are also path-homotopic. (Contributed by Mario Carneiro, 6-Jul-2015.)
CovMap

Theoremcvmlift3lem1 24928* Lemma for cvmlift3 24937. (Contributed by Mario Carneiro, 6-Jul-2015.)
CovMap        SCon       𝑛Locally PCon

Theoremcvmlift3lem2 24929* Lemma for cvmlift2 24925. (Contributed by Mario Carneiro, 6-Jul-2015.)
CovMap        SCon       𝑛Locally PCon

Theoremcvmlift3lem3 24930* Lemma for cvmlift2 24925. (Contributed by Mario Carneiro, 6-Jul-2015.)
CovMap        SCon       𝑛Locally PCon

Theoremcvmlift3lem4 24931* Lemma for cvmlift2 24925. (Contributed by Mario Carneiro, 6-Jul-2015.)
CovMap        SCon       𝑛Locally PCon

Theoremcvmlift3lem5 24932* Lemma for cvmlift2 24925. (Contributed by Mario Carneiro, 6-Jul-2015.)
CovMap        SCon       𝑛Locally PCon

Theoremcvmlift3lem6 24933* Lemma for cvmlift3 24937. (Contributed by Mario Carneiro, 9-Jul-2015.)
CovMap        SCon       𝑛Locally PCon                                          t t                                                                       t

Theoremcvmlift3lem7 24934* Lemma for cvmlift3 24937. (Contributed by Mario Carneiro, 9-Jul-2015.)
CovMap        SCon       𝑛Locally PCon                                          t t                                    t PCon

Theoremcvmlift3lem8 24935* Lemma for cvmlift2 24925. (Contributed by Mario Carneiro, 6-Jul-2015.)
CovMap        SCon       𝑛Locally PCon                                          t t

Theoremcvmlift3lem9 24936* Lemma for cvmlift2 24925. (Contributed by Mario Carneiro, 7-May-2015.)
CovMap        SCon       𝑛Locally PCon                                          t t

Theoremcvmlift3 24937* A general version of cvmlift 24908. If is simply connected and weakly locally path-connected, then there is a unique lift of functions on which commutes with the covering map. (Contributed by Mario Carneiro, 9-Jul-2015.)
CovMap        SCon       𝑛Locally PCon

19.4.10  Normal numbers

Theoremsnmlff 24938* The function from snmlval 24940 is a mapping from positive integers to real numbers in the range . (Contributed by Mario Carneiro, 6-Apr-2015.)

Theoremsnmlfval 24939* The function from snmlval 24940 maps to the relative density of in the first digits of the digit string of in base . (Contributed by Mario Carneiro, 6-Apr-2015.)

Theoremsnmlval 24940* The property " is simply normal in base ". A number is simply normal if each digit occurs in the base- digit string of with frequency (which is consistent with the expectation in an infinite random string of numbers selected from ). (Contributed by Mario Carneiro, 6-Apr-2015.)

Theoremsnmlflim 24941* If is simply normal, then the function of relative density of in the digit string converges to , i.e. the set of occurences of in the digit string has natural density . (Contributed by Mario Carneiro, 6-Apr-2015.)

19.4.11  Godel-sets of formulas

Syntaxcgoe 24942 The Godel-set of membership.

Syntaxcgna 24943 The Godel-set for the Sheffer stroke.

Syntaxcgol 24944 The Godel-set of universal quantification. (Note that this is not a wff.)

Syntaxcsat 24945 The satisfaction function.

Syntaxcfmla 24946 The formula set predicate.

Syntaxcsate 24947 The -satisfaction function.

Syntaxcprv 24948 The "proves" relation.

Definitiondf-goel 24949 Define the Godel-set of membership. Here the arguments correspond to vN and vP , so actually means v0 v1 , not . (Contributed by Mario Carneiro, 14-Jul-2013.)

Definitiondf-gona 24950 Define the Godel-set for the Sheffer stroke NAND. Here the arguments are also Godel-sets corresponding to smaller formulae. (Contributed by Mario Carneiro, 14-Jul-2013.)

Definitiondf-goal 24951 Define the Godel-set of universal quantification. Here corresponds to vN , and represents another formula, and this expression is where is the -th variable, is the code for . Note that this is a class expression, not a wff. (Contributed by Mario Carneiro, 14-Jul-2013.)

Definitiondf-sat 24952* Define the satisfaction predicate. This recursive construction builds up a function over wff codes and simultaneously defines the set of assignments to all variables from that makes the coded wff true in the model , where is interpreted as the binary relation on . The interpretation of the statement is that for the model , is a valuation of the variables (v0 , v1 , etc.) and is a code for a wff using that is true under the assignment . The function is defined by finite recursion; only operates on wffs of depth at most , and operates on all wffs. The coding scheme for the wffs is defined so that
• vi vj is coded as ,
• is coded as , and
• vi is coded as .

(Contributed by Mario Carneiro, 14-Jul-2013.)

Definitiondf-sate 24953* A simplified version of the satisfaction predicate, using the standard membership relation and eliminating the extra variable . (Contributed by Mario Carneiro, 14-Jul-2013.)

Definitiondf-fmla 24954 Define the predicate which defines the set of valid Godel formulas. The parameter defines the maximum height of the formulas: the set is all formulas of the form or (which in our coding scheme is the set ; see df-sat 24952 for the full coding scheme), and each extra level adds to the complexity of the formulas in . is the set of all valid formulas. (Contributed by Mario Carneiro, 14-Jul-2013.)

Syntaxcgon 24955 The Godel-set of negation. (Note that this is not a wff.)

Syntaxcgoa 24956 The Godel-set of conjunction.

Syntaxcgoi 24957 The Godel-set of implication.

Syntaxcgoo 24958 The Godel-set of disjunction.

Syntaxcgob 24959 The Godel-set of equivalence.

Syntaxcgoq 24960 The Godel-set of equality.

Syntaxcgox 24961 The Godel-set of existential quantification. (Note that this is not a wff.)

Definitiondf-gonot 24962 Define the Godel-set of negation. Here the argument is also a Godel-set corresponding to smaller formulae. Note that this is a class expression, not a wff. (Contributed by Mario Carneiro, 14-Jul-2013.)

Definitiondf-goan 24963* Define the Godel-set of conjunction. Here the arguments and are also Godel-sets corresponding to smaller formulae. (Contributed by Mario Carneiro, 14-Jul-2013.)

Definitiondf-goim 24964* Define the Godel-set of implication. Here the arguments and are also Godel-sets corresponding to smaller formulae. Note that this is a class expression, not a wff. (Contributed by Mario Carneiro, 14-Jul-2013.)

Definitiondf-goor 24965* Define the Godel-set of disjunction. Here the arguments and are also Godel-sets corresponding to smaller formulae. Note that this is a class expression, not a wff. (Contributed by Mario Carneiro, 14-Jul-2013.)

Definitiondf-gobi 24966* Define the Godel-set of equivalence. Here the arguments and are also Godel-sets corresponding to smaller formulae. Note that this is a class expression, not a wff. (Contributed by Mario Carneiro, 14-Jul-2013.)

Definitiondf-goeq 24967* Define the Godel-set of equality. Here the arguments correspond to vN and vP , so actually means v0 v1 , not . Here we use the trick mentioned in ax-ext 2382 to introduce equality as a defined notion in terms of . The expression max here is a convenient way of getting a dummy variable distinct from and . (Contributed by Mario Carneiro, 14-Jul-2013.)

Definitiondf-goex 24968 Define the Godel-set of existential quantification. Here corresponds to vN , and represents another formula, and this expression is where is the -th variable, is the code for . Note that this is a class expression, not a wff. (Contributed by Mario Carneiro, 14-Jul-2013.)

Definitiondf-prv 24969* Define the "proves" relation on a set. A wff is true in a model if for every valuation , the interpretation of the wff using the membership relation on is true. (Contributed by Mario Carneiro, 14-Jul-2013.)

19.4.12  Models of ZF

Syntaxcgze 24970 The Axiom of Extensionality.

Syntaxcgzr 24971 The Axiom Scheme of Replacement.

Syntaxcgzp 24972 The Axiom of Power Sets.

Syntaxcgzu 24973 The Axiom of Unions.

Syntaxcgzg 24974 The Axiom of Regularity.

Syntaxcgzi 24975 The Axiom of Infinity.

Syntaxcgzf 24976 The set of models of ZF.

Definitiondf-gzext 24977 The Godel-set version of the Axiom of Extensionality. (Contributed by Mario Carneiro, 14-Jul-2013.)

Definitiondf-gzrep 24978 The Godel-set version of the Axiom Scheme of Replacement. Since this is a scheme and not a single axiom, it manifests as a function on wffs, each giving rise to a different axiom. (Contributed by Mario Carneiro, 14-Jul-2013.)

Definitiondf-gzpow 24979 The Godel-set version of the Axiom of Power Sets. (Contributed by Mario Carneiro, 14-Jul-2013.)

Definitiondf-gzun 24980 The Godel-set version of the Axiom of Unions. (Contributed by Mario Carneiro, 14-Jul-2013.)

Definitiondf-gzreg 24981 The Godel-set version of the Axiom of Regularity. (Contributed by Mario Carneiro, 14-Jul-2013.)

Definitiondf-gzinf 24982 The Godel-set version of the Axiom of Infinity. (Contributed by Mario Carneiro, 14-Jul-2013.)

Definitiondf-gzf 24983* Define the class of all (transitive) models of ZF. (Contributed by Mario Carneiro, 14-Jul-2013.)

19.4.13  Splitting fields

Syntaxcitr 24984 Integral subring of a ring.
IntgRing

Syntaxccpms 24985 Completion of a metric space.
cplMetSp

Syntaxchlb 24986 Embeddings for a direct limit.
HomLimB

Syntaxchlim 24987 Direct limit structure.
HomLim

Syntaxcpfl 24988 Polynomial extension field.
polyFld

Syntaxcsf1 24989 Splitting field for a single polynomial (auxiliary).
splitFld1

Syntaxcsf 24990 Splitting field for a finite set of polynomials.
splitFld

Syntaxcpsl 24991 Splitting field for a sequence of polynomials.
polySplitLim

Definitiondf-irng 24992* Define the subring of elements of integral over in a ring. (Contributed by Mario Carneiro, 2-Dec-2014.)
IntgRing Monic1ps

Definitiondf-cplmet 24993* A function which completes the given metric space. (Contributed by Mario Carneiro, 2-Dec-2014.)
cplMetSp s s s sSet

Definitiondf-homlimb 24994* The input to this function is a sequence (on ) of homomorphisms . The resulting structure is the direct limit of the direct system so defined. This function returns the pair where is the terminal object and is a sequence of functions such that and . (Contributed by Mario Carneiro, 2-Dec-2014.)
HomLimB

Definitiondf-homlim 24995* The input to this function is a sequence (on ) of structures and homomorphisms . The resulting structure is the direct limit of the direct system so defined, and maintains any structures that were present in the original objects. TODO: generalize to directed sets? (Contributed by Mario Carneiro, 2-Dec-2014.)
HomLim HomLimB

Definitiondf-plfl 24996* Define the field extension that augments a field with the root of the given irreducible polynomial, and extends the norm if one exists and the extension is unique. (Contributed by Mario Carneiro, 2-Dec-2014.)
polyFld Poly1 RSpan ~QG s ~QG toNrmGrp AbsVal sSet deg1 deg1

Definitiondf-sfl1 24997* Temporary construction for the splitting field of a polynomial. The inputs are a field and a polynomial that we want to split, along with a tuple in the same format as the output. The output is a tuple where is the splitting field and is an injective homomorphism from the original field .

The function works by repeatedly finding the smallest monic irreducible factor, and extending the field by that factor using the polyFld construction. We keep track of a total order in each of the splitting fields so that we can pick an element definably without needing global choice. (Contributed by Mario Carneiro, 2-Dec-2014.)

splitFld1 Poly1 mPoly Monic1p Irred r deg1 polyFld deg1

Definitiondf-sfl 24998* Define the splitting field of a finite collection of polynomials, given a total ordered base field. The output is a tuple where is the totally ordered splitting field and is an injective homomorphism from the original field . (Contributed by Mario Carneiro, 2-Dec-2014.)
splitFld splitFld1

Definitiondf-psl 24999* Define the direct limit of an increasing sequence of fields produced by pasting together the splitting fields for each sequence of polynomials. That is, given a ring , a strict order on , and a sequence of finite sets of polynomials to split, we construct the direct limit system of field extensions by splitting one set at a time and passing the resulting construction to HomLim. (Contributed by Mario Carneiro, 2-Dec-2014.)
polySplitLim splitFld HomLim