Home | Metamath
Proof ExplorerTheorem List
(p. 229 of 311)
| < 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-21328) |
Hilbert Space Explorer
(21329-22851) |
Users' Mathboxes
(22852-31058) |

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

Statement | ||

Theorem | chirredlem2 22801* | Lemma for chirredi 22804. (Contributed by NM, 15-Jun-2006.) (New usage is discouraged.) |

HAtoms HAtoms | ||

Theorem | chirredlem3 22802* | Lemma for chirredi 22804. (Contributed by NM, 15-Jun-2006.) (New usage is discouraged.) |

HAtoms HAtoms HAtoms | ||

Theorem | chirredlem4 22803* | Lemma for chirredi 22804. (Contributed by NM, 15-Jun-2006.) (New usage is discouraged.) |

HAtoms HAtoms HAtoms | ||

Theorem | chirredi 22804* | The Hilbert lattice is irreducible: any element that commutes with all elements must be zero or one. Theorem 14.8.4 of [BeltramettiCassinelli] p. 166. (Contributed by NM, 15-Jun-2006.) (New usage is discouraged.) |

Theorem | chirred 22805* | The Hilbert lattice is irreducible: any element that commutes with all elements must be zero or one. Theorem 14.8.4 of [BeltramettiCassinelli] p. 166. (Contributed by NM, 16-Jun-2006.) (New usage is discouraged.) |

15.9.55 Atoms (cont.) | ||

Theorem | atcvat3i 22806 | A condition implying that a certain lattice element is an atom. Part of Lemma 3.2.20 of [PtakPulmannova] p. 68. (Contributed by NM, 2-Jul-2004.) (New usage is discouraged.) |

HAtoms HAtoms HAtoms | ||

Theorem | atcvat4i 22807* | A condition implying existence of an atom with the properties shown. Lemma 3.2.20 of [PtakPulmannova] p. 68. (Contributed by NM, 2-Jul-2004.) (New usage is discouraged.) |

HAtoms HAtoms HAtoms | ||

Theorem | atdmd 22808 | Two Hilbert lattice elements have the dual modular pair property if the first is an atom. Theorem 7.6(c) of [MaedaMaeda] p. 31. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.) |

HAtoms | ||

Theorem | atmd 22809 | Two Hilbert lattice elements have the modular pair property if the first is an atom. Theorem 7.6(b) of [MaedaMaeda] p. 31. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.) |

HAtoms | ||

Theorem | atmd2 22810 | Two Hilbert lattice elements have the dual modular pair property if the second is an atom. Part of Exercise 6 of [Kalmbach] p. 103. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.) |

HAtoms | ||

Theorem | atabsi 22811 | Absorption of an incomparable atom. Similar to Exercise 7.1 of [MaedaMaeda] p. 34. (Contributed by NM, 15-Jul-2004.) (New usage is discouraged.) |

HAtoms | ||

Theorem | atabs2i 22812 | Absorption of an incomparable atom. (Contributed by NM, 18-Jul-2004.) (New usage is discouraged.) |

HAtoms | ||

15.9.56 Modular symmetry | ||

Theorem | mdsymlem1 22813* | Lemma for mdsymi 22821. (Contributed by NM, 1-Jul-2004.) (New usage is discouraged.) |

Theorem | mdsymlem2 22814* | Lemma for mdsymi 22821. (Contributed by NM, 1-Jul-2004.) (New usage is discouraged.) |

HAtoms HAtoms HAtoms | ||

Theorem | mdsymlem3 22815* | Lemma for mdsymi 22821. (Contributed by NM, 2-Jul-2004.) (New usage is discouraged.) |

HAtoms HAtoms HAtoms | ||

Theorem | mdsymlem4 22816* | Lemma for mdsymi 22821. This is the forward direction of Lemma 4(i) of [Maeda] p. 168. (Contributed by NM, 2-Jul-2004.) (New usage is discouraged.) |

HAtoms HAtoms HAtoms | ||

Theorem | mdsymlem5 22817* | Lemma for mdsymi 22821. (Contributed by NM, 2-Jul-2004.) (New usage is discouraged.) |

HAtoms HAtoms HAtoms | ||

Theorem | mdsymlem6 22818* | Lemma for mdsymi 22821. This is the converse direction of Lemma 4(i) of [Maeda] p. 168, and is based on the proof of Theorem 1(d) to (e) of [Maeda] p. 167. (Contributed by NM, 2-Jul-2004.) (New usage is discouraged.) |

HAtoms HAtoms HAtoms | ||

Theorem | mdsymlem7 22819* | Lemma for mdsymi 22821. Lemma 4(i) of [Maeda] p. 168. Note that Maeda's 1965 definition of dual modular pair has reversed arguments compared to the later (1970) definition given in Remark 29.6 of [MaedaMaeda] p. 130, which is the one that we use. (Contributed by NM, 3-Jul-2004.) (New usage is discouraged.) |

HAtoms HAtoms HAtoms | ||

Theorem | mdsymlem8 22820* | Lemma for mdsymi 22821. Lemma 4(ii) of [Maeda] p. 168. (Contributed by NM, 3-Jul-2004.) (New usage is discouraged.) |

Theorem | mdsymi 22821 | M-symmetry of the Hilbert lattice. Lemma 5 of [Maeda] p. 168. (Contributed by NM, 3-Jul-2004.) (New usage is discouraged.) |

Theorem | mdsym 22822 | M-symmetry of the Hilbert lattice. Lemma 5 of [Maeda] p. 168. (Contributed by NM, 6-Jul-2004.) (New usage is discouraged.) |

Theorem | dmdsym 22823 | Dual M-symmetry of the Hilbert lattice. (Contributed by NM, 25-Jul-2007.) (New usage is discouraged.) |

Theorem | atdmd2 22824 | Two Hilbert lattice elements have the dual modular pair property if the second is an atom. (Contributed by NM, 6-Jul-2004.) (New usage is discouraged.) |

HAtoms | ||

Theorem | sumdmdii 22825 | If the subspace sum of two Hilbert lattice elements is closed, then the elements are a dual modular pair. Remark in [MaedaMaeda] p. 139. (Contributed by NM, 12-Jul-2004.) (New usage is discouraged.) |

Theorem | cmmdi 22826 | Commuting subspaces form a modular pair. (Contributed by NM, 16-Jan-2005.) (New usage is discouraged.) |

Theorem | cmdmdi 22827 | Commuting subspaces form a dual modular pair. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.) |

Theorem | sumdmdlem 22828 | Lemma for sumdmdi 22830. The span of vector not in the subspace sum is "trimmed off." (Contributed by NM, 18-Dec-2004.) (New usage is discouraged.) |

Theorem | sumdmdlem2 22829* | Lemma for sumdmdi 22830. (Contributed by NM, 23-Dec-2004.) (New usage is discouraged.) |

HAtoms | ||

Theorem | sumdmdi 22830 | The subspace sum of two Hilbert lattice elements is closed iff the elements are a dual modular pair. Theorem 2 of [Holland] p. 1519. (Contributed by NM, 14-Dec-2004.) (New usage is discouraged.) |

Theorem | dmdbr4ati 22831* | Dual modular pair property in terms of atoms. (Contributed by NM, 15-Jan-2005.) (New usage is discouraged.) |

HAtoms | ||

Theorem | dmdbr5ati 22832* | Dual modular pair property in terms of atoms. (Contributed by NM, 14-Jan-2005.) (New usage is discouraged.) |

HAtoms | ||

Theorem | dmdbr6ati 22833* | Dual modular pair property in terms of atoms. The modular law takes the form of the shearing identity. (Contributed by NM, 18-Jan-2005.) (New usage is discouraged.) |

HAtoms | ||

Theorem | dmdbr7ati 22834* | Dual modular pair property in terms of atoms. (Contributed by NM, 18-Jan-2005.) (New usage is discouraged.) |

HAtoms | ||

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

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

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

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

Theorem | mdcompli 22839 | 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 22840 | A condition equivalent to the dual modular pair property. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |

Theorem | mddmdin0i 22841* | 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 22842* | 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 22843* | 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 22844* | 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 22845* | Lemma for cdj3i 22851. Value of the first-component function . (Contributed by NM, 23-May-2005.) (New usage is discouraged.) |

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

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

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

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

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

Theorem | cdj3i 22851* | 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 16 SUPPLEMENTARY MATERIAL (USER'S
MATHBOXES) | ||

16.1 Mathboxes for user
contributions | ||

16.1.1 Mathbox guidelines | ||

Theorem | mathbox 22852 |
(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 9304. 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.) |

16.2 Mathbox for Stefan
Allan | ||

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

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

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

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

16.3 Mathbox for Mario
Carneiro | ||

16.3.1 Miscellaneous stuff | ||

Theorem | quartfull 22857 | 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.) |

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

16.3.2 Zeta function | ||

Syntax | czeta 22858 | The Riemann zeta function. |

Definition | df-zeta 22859* | Define the Riemann zeta function. This definition uses a series expansion of the alternating zeta function ~? zetaalt that is convergent everywhere except , but going from the alternating zeta function to the regular zeta function requires dividing by , which has zeroes other than . To extract the correct value of the zeta function at these points, we extend the divided alternating zeta function by continuity. (Contributed by Mario Carneiro, 18-Jul-2014.) |

Theorem | zetacvg 22860* | The zeta series is convergent. (Contributed by Mario Carneiro, 18-Jul-2014.) |

16.3.3 Gamma function | ||

Syntax | clgam 22861 | Logarithm of the Gamma function. |

Syntax | cgam 22862 | The Gamma function. |

Definition | df-lgam 22863* | Define the log-Gamma function. We can work with this form of the gamma function a bit easier than the equivalent expression for the gamma function itself, and moreover this function is not actually equal to because the branch cuts are placed differently (we do have , though). This definition is attributed to Euler, and unlike the usual integral definition is defined on the entire complex plane except the nonpositive integers , where the function has simple poles. (Contributed by Mario Carneiro, 12-Jul-2014.) |

Definition | df-gam 22864 | Define the Gamma function. See df-lgam 22863 for more information about the reason for this definition in terms of the log-gamma function. (Contributed by Mario Carneiro, 12-Jul-2014.) |

Theorem | eldmgm 22865 | Elementhood in the set of non-nonpositive integers. (Contributed by Mario Carneiro, 12-Jul-2014.) |

Theorem | dmgmaddn0 22866 | If is not a nonpositive integer, then is nonzero for any nonnegative integer . (Contributed by Mario Carneiro, 12-Jul-2014.) |

Theorem | dmgmseqn0 22867* | If is not a nonpositive integer, then is nonzero for any . (Contributed by Mario Carneiro, 12-Jul-2014.) |

16.3.4 Derangements and the
Subfactorial | ||

Theorem | deranglem 22868* | Lemma for derangements. (Contributed by Mario Carneiro, 19-Jan-2015.) |

Theorem | derangval 22869* | Define the derangement function, which counts the number of bijections from a set to itself such that no element is mapped to itself. (Contributed by Mario Carneiro, 19-Jan-2015.) |

Theorem | derangf 22870* | The derangement number is a function from finite sets to nonnegative integers. (Contributed by Mario Carneiro, 19-Jan-2015.) |

Theorem | derang0 22871* | The derangement number of the empty set. (Contributed by Mario Carneiro, 19-Jan-2015.) |

Theorem | derangsn 22872* | The derangement number of a singleton. (Contributed by Mario Carneiro, 19-Jan-2015.) |

Theorem | derangenlem 22873* | One half of derangen 22874. (Contributed by Mario Carneiro, 22-Jan-2015.) |

Theorem | derangen 22874* | The derangement number is a cardinal invariant, i.e. it only depends on the size of a set and not on its contents. (Contributed by Mario Carneiro, 22-Jan-2015.) |

Theorem | subfacval 22875* | The subfactorial is defined as the number of derangements (see derangval 22869) of the set . (Contributed by Mario Carneiro, 21-Jan-2015.) |

Theorem | derangen2 22876* | Write the derangement number in terms of the subfactorial. (Contributed by Mario Carneiro, 22-Jan-2015.) |

Theorem | subfacf 22877* | The subfactorial is a function from nonnegative integers to nonnegative integers. (Contributed by Mario Carneiro, 19-Jan-2015.) |

Theorem | subfaclefac 22878* | The subfactorial is less than the factorial. (Contributed by Mario Carneiro, 19-Jan-2015.) |

Theorem | subfac0 22879* | The subfactorial at zero. (Contributed by Mario Carneiro, 19-Jan-2015.) |

Theorem | subfac1 22880* | The subfactorial at one. (Contributed by Mario Carneiro, 19-Jan-2015.) |

Theorem | subfacp1lem1 22881* | Lemma for subfacp1 22888. The set together with partitions the set . (Contributed by Mario Carneiro, 23-Jan-2015.) |

Theorem | subfacp1lem2a 22882* | Lemma for subfacp1 22888. Properties of a bijection on augmented with the two-element flip to get a bijection on . (Contributed by Mario Carneiro, 23-Jan-2015.) |