Home | Metamath
Proof ExplorerTheorem List
(p. 231 of 315)
| < Previous Next > |

Browser slow? Try the
Unicode version. |

Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs

Color key: | Metamath Proof Explorer
(1-21494) |
Hilbert Space Explorer
(21495-23017) |
Users' Mathboxes
(23018-31433) |

Type | Label | Description |
---|---|---|

Statement | ||

Theorem | mdoc1i 23001 | Orthocomplements form a modular pair. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |

Theorem | mdoc2i 23002 | Orthocomplements form a modular pair. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |

Theorem | dmdoc1i 23003 | Orthocomplements form a dual modular pair. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |

Theorem | dmdoc2i 23004 | Orthocomplements form a dual modular pair. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |

Theorem | mdcompli 23005 | A condition equivalent to the modular pair property. Part of proof of Theorem 1.14 of [MaedaMaeda] p. 4. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |

Theorem | dmdcompli 23006 | A condition equivalent to the dual modular pair property. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |

Theorem | mddmdin0i 23007* | If dual modular implies modular whenever meet is zero, then dual modular implies modular for arbitrary lattice elements. This theorem is needed for the remark after Lemma 7 of [Holland] p. 1524 to hold. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |

Theorem | cdjreui 23008* | A member of the sum of disjoint subspaces has a unique decomposition. Part of Lemma 5 of [Holland] p. 1520. (Contributed by NM, 20-May-2005.) (New usage is discouraged.) |

Theorem | cdj1i 23009* | Two ways to express " and are completely disjoint subspaces." (1) => (2) in Lemma 5 of [Holland] p. 1520. (Contributed by NM, 21-May-2005.) (New usage is discouraged.) |

Theorem | cdj3lem1 23010* | A property of " and are completely disjoint subspaces." Part of Lemma 5 of [Holland] p. 1520. (Contributed by NM, 23-May-2005.) (New usage is discouraged.) |

Theorem | cdj3lem2 23011* | Lemma for cdj3i 23017. Value of the first-component function . (Contributed by NM, 23-May-2005.) (New usage is discouraged.) |

Theorem | cdj3lem2a 23012* | Lemma for cdj3i 23017. Closure of the first-component function . (Contributed by NM, 25-May-2005.) (New usage is discouraged.) |

Theorem | cdj3lem2b 23013* | Lemma for cdj3i 23017. The first-component function is bounded if the subspaces are completely disjoint. (Contributed by NM, 26-May-2005.) (New usage is discouraged.) |

Theorem | cdj3lem3 23014* | Lemma for cdj3i 23017. Value of the second-component function . (Contributed by NM, 23-May-2005.) (New usage is discouraged.) |

Theorem | cdj3lem3a 23015* | Lemma for cdj3i 23017. Closure of the second-component function . (Contributed by NM, 26-May-2005.) (New usage is discouraged.) |

Theorem | cdj3lem3b 23016* | Lemma for cdj3i 23017. The second-component function is bounded if the subspaces are completely disjoint. (Contributed by NM, 31-May-2005.) (New usage is discouraged.) |

Theorem | cdj3i 23017* | Two ways to express " and are completely disjoint subspaces." (1) <=> (3) in Lemma 5 of [Holland] p. 1520. (Contributed by NM, 1-Jun-2005.) (New usage is discouraged.) |

PART 18 SUPPLEMENTARY MATERIAL (USER'S
MATHBOXES) | ||

18.1 Mathboxes for user
contributions | ||

18.1.1 Mathbox guidelines | ||

Theorem | mathbox 23018 |
(This theorem is a dummy placeholder for these guidelines. The name of
this theorem, "mathbox", is hard-coded into the Metamath program
to
identify the start of the mathbox section for web page generation.)
A "mathbox" is a user-contributed section that is maintained by its contributor independently from the main part of set.mm.
By making a contribution, you agree to release it into the public domain, according to the statement at the beginning of set.mm. Mathboxes are provided to help keep your work synchronized with changes in set.mm, but they shouldn't be depended on as a permanent archive. If you want to preserve your original contribution, it is your responsibility to keep your own copy of it along with the version of set.mm that works with it.
1. If at all possible, please use only 0-ary class constants for new definitions, for example as in df-div 9420. 2. Try to follow the style of the rest of set.mm. Each $p and $a statement must be immediately preceded with the comment that will be shown on its web page description. The metamath program command "write source set.mm /rewrap" will take care of wrapping comment lines and indentation conventions. All mathbox content will be on public display and should hopefully reflect the overall quality of the web site. 3. Before submitting a revised mathbox, please make sure it verifies against the current set.mm. 4. Mathboxes should be independent i.e. the proofs should verify with all other mathboxes removed. If you need a theorem from another mathbox, that is fine (and encouraged), but let me know so I can move the theorem to the main section. One way avoid undesired accidental use of other mathbox theorems is to develop your mathbox using a modified set.mm that has mathboxes removed.
1. I may decide to move some theorems to the main part of set.mm for general use. In that case, an author acknowledgment will be added to the description of the theorem. 2. I may make changes to mathboxes to maintain the overall quality of set.mm. Normally I will let you know if a change might impact what you are working on. 3. If you use theorems from another user's mathbox, I don't provide assurance that they are based on correct or consistent $a statements. (If you find such a problem, please let me know so it can be corrected.) (Contributed by NM, 20-Feb-2007.) (New usage is discouraged.) |

18.2 Mathbox for Stefan
Allan | ||

Theorem | foo3 23019 | A theorem about the universal class. (Contributed by Stefan Allan, 9-Dec-2008.) |

Theorem | xfree 23020 | A partial converse to 19.9t 1784. (Contributed by Stefan Allan, 21-Dec-2008.) (Revised by Mario Carneiro, 11-Dec-2016.) |

Theorem | xfree2 23021 | A partial converse to 19.9t 1784. (Contributed by Stefan Allan, 21-Dec-2008.) |

Theorem | addltmulALT 23022 | A proof readability experiment for addltmul 9943. (Contributed by Stefan Allan, 30-Oct-2010.) (Proof modification is discouraged.) |

18.3 Mathbox for Thierry
Arnoux | ||

Theorem | mptcnv 23023* | The converse of a mapping function. (Contributed by Thierry Arnoux, 16-Jan-2017.) |

Theorem | reximddv 23024* | Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Thierry Arnoux, 7-Dec-2016.) |

Theorem | infi 23025 | If is finite, is finite. (Contributed by Thierry Arnoux, 17-Apr-2017.) |

Theorem | fzspl 23026 | Split the last element of a finite set of sequential integers. (more generic than fzsuc 10831) (Contributed by Thierry Arnoux, 7-Nov-2016.) |

Theorem | fzsplit3 23027 | Split a finite interval of integers into two parts. (Contributed by Thierry Arnoux, 2-May-2017.) |

Theorem | bcm1n 23028 | The proportion of one binomial coefficient to another with decreased by 1. (Contributed by Thierry Arnoux, 9-Nov-2016.) |

Theorem | ltesubnnd 23029 | Subtracting an integer number from another number decreases it. See ltsubrpd 10414 (Contributed by Thierry Arnoux, 18-Apr-2017.) |

Theorem | ifeqeqx 23030* | An equality theorem tailored for ballotlemsf1o 23068 (Contributed by Thierry Arnoux, 14-Apr-2017.) |

Theorem | fdmrn 23031 | A different way to write is a function. (Contributed by Thierry Arnoux, 7-Dec-2016.) |

Theorem | nvof1o 23032 | An involution is a bijection. (Contributed by Thierry Arnoux, 7-Dec-2016.) |

Theorem | f1o3d 23033* | Describe an implicit one-to-one onto function. (Contributed by Thierry Arnoux, 23-Apr-2017.) |

Theorem | rinvf1o 23034 | Sufficient conditions for the restriction of an involution to be a bijection (Contributed by Thierry Arnoux, 7-Dec-2016.) |

Theorem | elabreximd 23035* | Class substitution in an image set. (Contributed by Thierry Arnoux, 30-Dec-2016.) |

Theorem | abrexss 23036* | A necessary condition for an image set to be a subset. (Contributed by Thierry Arnoux, 6-Feb-2017.) |

Theorem | dfimafnf 23037* | Alternate definition of the image of a function. (Contributed by Raph Levien, 20-Nov-2006.) (Revised by Thierry Arnoux, 24-Apr-2017.) |

Theorem | funimass4f 23038 | Membership relation for the values of a function whose image is a subclass. (Contributed by Thierry Arnoux, 24-Apr-2017.) |

Theorem | addeq0 23039 | Two complex which add up to zero are each other's negatives. (Contributed by Thierry Arnoux, 2-May-2017.) |

18.3.1 Bertrand's Ballot Problem | ||

Theorem | ballotlemoex 23040* | is a set. (Contributed by Thierry Arnoux, 7-Dec-2016.) |

Theorem | ballotlem1 23041* | The size of the universe is a binomial coefficient. (Contributed by Thierry Arnoux, 23-Nov-2016.) |

Theorem | ballotlemelo 23042* | Elementhood in . (Contributed by Thierry Arnoux, 17-Apr-2017.) |

Theorem | ballotlem2 23043* | The probability that the first vote picked in a count is a B (Contributed by Thierry Arnoux, 23-Nov-2016.) |

Theorem | ballotlemfval 23044* | The value of F. (Contributed by Thierry Arnoux, 23-Nov-2016.) |

Theorem | ballotlemfelz 23045* | has values in . (Contributed by Thierry Arnoux, 23-Nov-2016.) |

Theorem | ballotlemfp1 23046* | If the th ballot is for A, goes up 1. If the th ballot is for B, goes down 1. (Contributed by Thierry Arnoux, 24-Nov-2016.) |

Theorem | ballotlemfc0 23047* | takes value 0 between negative and positive values. (Contributed by Thierry Arnoux, 24-Nov-2016.) |

Theorem | ballotlemfcc 23048* | takes value 0 between positive and negative values. (Contributed by Thierry Arnoux, 2-Apr-2017.) |

Theorem | ballotlemfmpn 23049* | finishes counting at . (Contributed by Thierry Arnoux, 25-Nov-2016.) |

Theorem | ballotlemfval0 23050* | always starts counting at 0 . (Contributed by Thierry Arnoux, 25-Nov-2016.) |

Theorem | ballotleme 23051* | Elements of . (Contributed by Thierry Arnoux, 14-Dec-2016.) |

Theorem | ballotlemodife 23052* | Elements of . (Contributed by Thierry Arnoux, 7-Dec-2016.) |

Theorem | ballotlem4 23053* | If the first pick is a vote for B, A is not ahead throughout the count (Contributed by Thierry Arnoux, 25-Nov-2016.) |

Theorem | ballotlem5 23054* | If A is not ahead throughout, there is a where votes are tied. (Contributed by Thierry Arnoux, 1-Dec-2016.) |

Theorem | ballotlemi 23055* | Value of for a given counting . (Contributed by Thierry Arnoux, 1-Dec-2016.) |

Theorem | ballotlemiex 23056* | Properties of . (Contributed by Thierry Arnoux, 12-Dec-2016.) |

Theorem | ballotlemi1 23057* | The first tie cannot be reached at the first pick. (Contributed by Thierry Arnoux, 12-Mar-2017.) |

Theorem | ballotlemii 23058* | The first tie cannot be reached at the first pick. (Contributed by Thierry Arnoux, 4-Apr-2017.) |

Theorem | ballotlemsup 23059* | The set of zeroes of satisfies the conditions to have a supremum (Contributed by Thierry Arnoux, 1-Dec-2016.) |

Theorem | ballotlemimin 23060* | is the first tie. (Contributed by Thierry Arnoux, 1-Dec-2016.) |

Theorem | ballotlemic 23061* | If the first vote is for B, the vote on the first tie is for A. (Contributed by Thierry Arnoux, 1-Dec-2016.) |

Theorem | ballotlem1c 23062* | If the first vote is for A, the vote on the first tie is for B. (Contributed by Thierry Arnoux, 4-Apr-2017.) |

Theorem | ballotlemsval 23063* | Value of (Contributed by Thierry Arnoux, 12-Apr-2017.) |

Theorem | ballotlemsv 23064* | Value of evaluated at for a given counting . (Contributed by Thierry Arnoux, 12-Apr-2017.) |

Theorem | ballotlemsgt1 23065* | maps values less than to values greater than 1. (Contributed by Thierry Arnoux, 28-Apr-2017.) |

Theorem | ballotlemsdom 23066* | Domain of for a given counting . (Contributed by Thierry Arnoux, 12-Apr-2017.) |

Theorem | ballotlemsel1i 23067* | The range is invariant under . (Contributed by Thierry Arnoux, 28-Apr-2017.) |

Theorem | ballotlemsf1o 23068* | The defined is a bijection, and an involution. (Contributed by Thierry Arnoux, 14-Apr-2017.) |

Theorem | ballotlemsi 23069* | The image by of the first tie pick is the first pick. (Contributed by Thierry Arnoux, 14-Apr-2017.) |

Theorem | ballotlemsima 23070* | The image by of an interval before the first pick. (Contributed by Thierry Arnoux, 5-May-2017.) |

Theorem | ballotlemieq 23071* | If two countings share the same first tie, they also have the same swap function. (Contributed by Thierry Arnoux, 18-Apr-2017.) |

Theorem | ballotlemrval 23072* | Value of . (Contributed by Thierry Arnoux, 14-Apr-2017.) |

Theorem | ballotlemscr 23073* | The image of by (Contributed by Thierry Arnoux, 21-Apr-2017.) |

Theorem | ballotlemrv 23074* | Value of evaluated at . (Contributed by Thierry Arnoux, 17-Apr-2017.) |

Theorem | ballotlemrv1 23075* | Value of before the tie. (Contributed by Thierry Arnoux, 11-Apr-2017.) |

Theorem | ballotlemrv2 23076* | Value of after the tie. (Contributed by Thierry Arnoux, 11-Apr-2017.) |

Theorem | ballotlemro 23077* | Range of is included in . (Contributed by Thierry Arnoux, 17-Apr-2017.) |

Theorem | ballotlemgval 23078* | Expand the value of . (Contributed by Thierry Arnoux, 21-Apr-2017.) |

Theorem | ballotlemgun 23079* | A property of the defined operator (Contributed by Thierry Arnoux, 26-Apr-2017.) |

Theorem | ballotlemfg 23080* | Express the value of in terms of . (Contributed by Thierry Arnoux, 21-Apr-2017.) |

Theorem | ballotlemfrc 23081* | Express the value of in terms of the newly defined . (Contributed by Thierry Arnoux, 21-Apr-2017.) |

Theorem | ballotlemfrci 23082* | Reverse counting preserves a tie at the first tie. (Contributed by Thierry Arnoux, 21-Apr-2017.) |

Theorem | ballotlemfrceq 23083* | Value of for a reverse counting . (Contributed by Thierry Arnoux, 27-Apr-2017.) |

Theorem | ballotlemfrcn0 23084* | Value of for a reversed counting , before the first tie, cannot be zero . (Contributed by Thierry Arnoux, 25-Apr-2017.) |

Theorem | ballotlemrc 23085* | Range of . (Contributed by Thierry Arnoux, 19-Apr-2017.) |

Theorem | ballotlemirc 23086* | Applying does not change first ties. (Contributed by Thierry Arnoux, 19-Apr-2017.) |

Theorem | ballotlemrinv0 23087* | Lemma for ballotlemrinv 23088. (Contributed by Thierry Arnoux, 18-Apr-2017.) |

Theorem | ballotlemrinv 23088* | is its own inverse : it is an involution. (Contributed by Thierry Arnoux, 10-Apr-2017.) |

Theorem | ballotlem1ri 23089* | When the vote on the first tie is for A, the first vote is also for A on the reverse counting. (Contributed by Thierry Arnoux, 18-Apr-2017.) |

Theorem | ballotlem7 23090* | is a bijection between two subsets of : one where a vote for A is picked first, and one where a vote for B is picked first (Contributed by Thierry Arnoux, 12-Dec-2016.) |

Theorem | ballotlem8 23091* | There are as many countings with ties starting with a ballot for A as there are starting with a ballot for B. (Contributed by Thierry Arnoux, 7-Dec-2016.) |

Theorem | ballotth 23092* | Bertrand's ballot problem : the probability that A is ahead throughout the counting. (Contributed by Thierry Arnoux, 7-Dec-2016.) |

18.4 Mathbox for Mario
Carneiro | ||

18.4.1 Miscellaneous stuff | ||

Theorem | quartfull 23093 | The quartic equation, written out in full. This actually makes a fairly good Metamath stress test. Note that the length of this formula could be shortened significantly if the intermediate expressions were expanded and simplified, but it's not like this theorem will be used anyway. (Contributed by Mario Carneiro, 6-May-2015.) |

; ; ; ;; ; ; ; ;; ; ; ;; ; ; ; ;; ; ; ; ;; ; ; ;; ; ; ;; ; ; ; ;; |