HomeTheorem List (p. 238 of 325)
Unicode version.
| Home |
Metamath
Proof Explorer Theorem List (p. 238 of 325) | < Previous Next > |
| Browser slow? Try the
Unicode version. |
| Color key: | Metamath Proof Explorer
(1-22374) |
Hilbert Space Explorer
(22375-23897) |
Users' Mathboxes
(23898-32447) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | stm1addi 23701 | Sum of states whose meet is 1. (Contributed by NM, 11-Nov-1999.) (New usage is discouraged.) |
        
       
 | ||
| Theorem | staddi 23702 | If the sum of 2 states is 2, then each state is 1. (Contributed by NM, 12-Nov-1999.) (New usage is discouraged.) |
|
| ||
| Theorem | stm1add3i 23703 | Sum of states whose meet is 1. (Contributed by NM, 11-Nov-1999.) (New usage is discouraged.) |
  | ||
| Theorem | stadd3i 23704 | If the sum of 3 states is 3, then each state is 1. (Contributed by NM, 13-Nov-1999.) (New usage is discouraged.) |
| | ||
| Theorem | st0 23705 | The state of the zero subspace. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
  | ||
| Theorem | strlem1 23706* |
Lemma for strong state theorem: if closed subspace is not
contained in ,
there is a unit vector 
in their difference.
(Contributed by NM, 25-Oct-1999.) (New usage is discouraged.)
|
 
 ![\](setminus.gif "\"){kind=small}  | ||
| Theorem | strlem2 23707* | Lemma for strong state theorem. (Contributed by NM, 28-Oct-1999.) (New usage is discouraged.) |
  
 
| ||
| Theorem | strlem3a 23708* |
Lemma for strong state theorem: the function , that maps a closed
subspace to the square of the norm of its projection onto a unit vector,
is a state. (Contributed by NM, 28-Oct-1999.)
(New usage is discouraged.)
|
 ![/\](wedge.gif "/\"){kind=small}
| ||
| Theorem | strlem3 23709* |
Lemma for strong state theorem: the function , that maps a closed
subspace to the square of the norm of its projection onto a unit vector,
is a state. This lemma restates the hypotheses in a more convenient
form to work with. (Contributed by NM, 28-Oct-1999.)
(New usage is discouraged.)
|
 
| ||
| Theorem | strlem4 23710* | Lemma for strong state theorem. (Contributed by NM, 2-Nov-1999.) (New usage is discouraged.) |
|
| ||
| Theorem | strlem5 23711* | Lemma for strong state theorem. (Contributed by NM, 2-Nov-1999.) (New usage is discouraged.) |
 | ||
| Theorem | strlem6 23712* | Lemma for strong state theorem. (Contributed by NM, 2-Nov-1999.) (New usage is discouraged.) |
|
| ||
| Theorem | stri 23713* | Strong state theorem. The states on a Hilbert lattice define an ordering. Remark in [Mayet] p. 370. (Contributed by NM, 2-Nov-1999.) (New usage is discouraged.) |
 
| ||
| Theorem | strb 23714* | Strong state theorem (bidirectional version). (Contributed by NM, 7-Apr-2001.) (New usage is discouraged.) |
|
| ||
| Theorem | hstrlem2 23715* | Lemma for strong set of CH states theorem. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.) |
|
| ||
| Theorem | hstrlem3a 23716* |
Lemma for strong set of CH states theorem: the function , that
maps a closed subspace to the square of the norm of its projection onto
a unit vector, is a state. (Contributed by NM, 30-Jun-2006.)
(New usage is discouraged.)
|
 | ||
| Theorem | hstrlem3 23717* |
Lemma for strong set of CH states theorem: the function , that
maps a closed subspace to the square of the norm of its projection onto
a unit vector, is a state. This lemma restates the hypotheses in a more
convenient form to work with. (Contributed by NM, 30-Jun-2006.)
(New usage is discouraged.)
|
|
| ||
| Theorem | hstrlem4 23718* | Lemma for strong set of CH states theorem. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.) |
|
| ||
| Theorem | hstrlem5 23719* | Lemma for strong set of CH states theorem. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.) |
|
| ||
| Theorem | hstrlem6 23720* | Lemma for strong set of CH states theorem. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.) |
|
| ||
| Theorem | hstri 23721* | Hilbert space admits a strong set of Hilbert-space-valued states (CH-states). Theorem in [Mayet3] p. 10. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.) |
|
| ||
| Theorem | hstrbi 23722* | Strong CH-state theorem (bidirectional version). Theorem in [Mayet3] p. 10 and its converse. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.) |
|
| ||
| Theorem | largei 23723* | A Hilbert lattice admits a largei set of states. Remark in [Mayet] p. 370. (Contributed by NM, 7-Apr-2001.) (New usage is discouraged.) |
| | ||
| Theorem | jplem1 23724 | Lemma for Jauch-Piron theorem. (Contributed by NM, 8-Apr-2001.) (New usage is discouraged.) |
|
| ||
| Theorem | jplem2 23725* | Lemma for Jauch-Piron theorem. (Contributed by NM, 8-Apr-2001.) (New usage is discouraged.) |
|
| ||
| Theorem | jpi 23726* |
The function , that
maps a closed subspace to the square of the
norm of its projection onto a unit vector, is a Jauch-Piron state.
Remark in [Mayet] p. 370. (See strlem3a 23708 for the proof that is
a state.) (Contributed by NM, 8-Apr-2001.)
(New usage is discouraged.)
|
|
| ||
| Theorem | golem1 23727 | Lemma for Godowski's equation. (Contributed by NM, 10-Nov-2002.) (New usage is discouraged.) |
      
| ||
| Theorem | golem2 23728 | Lemma for Godowski's equation. (Contributed by NM, 13-Nov-1999.) (New usage is discouraged.) |
|
| ||
| Theorem | goeqi 23729 | Godowski's equation, shown here as a variant equivalent to Equation SF of [Godowski] p. 730. (Contributed by NM, 10-Nov-2002.) (New usage is discouraged.) |
| | ||
| Theorem | stcltr1i 23730* | Property of a strong classical state. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
| ||
| Theorem | stcltr2i 23731* | Property of a strong classical state. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
|
| ||
| Theorem | stcltrlem1 23732* | Lemma for strong classical state theorem. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
|
| ||
| Theorem | stcltrlem2 23733* | Lemma for strong classical state theorem. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
|
| ||
| Theorem | stcltrthi 23734* |
Theorem for classically strong set of states. If there exists a
"classically strong set of states" on lattice (or actually any
ortholattice, which would have an identical proof), then any two
elements of the lattice commute, i.e., the lattice is distributive.
(Proof due to Mladen Pavicic.) Theorem 3.3 of [MegPav2000] p. 2344.
(Contributed by NM, 24-Oct-1999.) (New usage is discouraged.)
|
| ||
| Definition | df-cv 23735* |
Define the covers relation (on the Hilbert lattice). Definition 3.2.18
of [PtakPulmannova] p. 68, whose
notation we use. Ptak/Pulmannova's
notation  is read " covers " or " is
covered by
" , and it means that is larger than and
there is nothing in between. See cvbr 23738
and cvbr2 23739 for membership
relations. (Contributed by NM, 4-Jun-2004.)
(New usage is discouraged.)
|
    
   | ||
| Definition | df-md 23736* | Define the modular pair relation (on the Hilbert lattice). Definition 1.1 of [MaedaMaeda] p. 1, who use the notation (x,y)M for "the ordered pair <x,y> is a modular pair." See mdbr 23750 for membership relation. (Contributed by NM, 14-Jun-2004.) (New usage is discouraged.) |
| ||
| Definition | df-dmd 23737* | Define the dual modular pair relation (on the Hilbert lattice). Definition 1.1 of [MaedaMaeda] p. 1, who use the notation (x,y)M* for "the ordered pair <x,y> is a dual modular pair." See dmdbr 23755 for membership relation. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.) |
| ||
| Theorem | cvbr 23738* |
Binary relation expressing covers ,
which means that
is larger than
and there is nothing in between. Definition 3.2.18
of [PtakPulmannova] p. 68.
(Contributed by NM, 4-Jun-2004.)
(New usage is discouraged.)
|
| | ||
| Theorem | cvbr2 23739* |
Binary relation expressing covers .
Definition of covers in
[Kalmbach] p. 15. (Contributed by NM,
9-Jun-2004.)
(New usage is discouraged.)
|
| | ||
| Theorem | cvcon3 23740 | Contraposition law for the covers relation. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.) |
| | ||
| Theorem | cvpss 23741 | The covers relation implies proper subset. (Contributed by NM, 10-Jun-2004.) (New usage is discouraged.) |
| | ||
| Theorem | cvnbtwn 23742 | The covers relation implies no in-betweenness. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.) |
|
| ||
| Theorem | cvnbtwn2 23743 | The covers relation implies no in-betweenness. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.) |
|
| ||
| Theorem | cvnbtwn3 23744 | The covers relation implies no in-betweenness. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.) |
|
| ||
| Theorem | cvnbtwn4 23745 | The covers relation implies no in-betweenness. Part of proof of Lemma 7.5.1 of [MaedaMaeda] p. 31. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.) |
 | ||
| Theorem | cvnsym 23746 | The covers relation is not symmetric. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.) |
| | ||
| Theorem | cvnref 23747 | The covers relation is not reflexive. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.) |
|
| ||
| Theorem | cvntr 23748 | The covers relation is not transitive. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.) |
|
| ||
| Theorem | spansncv2 23749 | Hilbert space has the covering property (using spans of singletons to represent atoms). Proposition 1(ii) of [Kalmbach] p. 153. (Contributed by NM, 9-Jun-2004.) (New usage is discouraged.) |
| ||
| Theorem | mdbr 23750* |
Binary relation expressing is a modular pair.
Definition 1.1 of [MaedaMaeda] p. 1.
(Contributed by NM, 14-Jun-2004.)
(New usage is discouraged.)
|
| | ||
| Theorem | mdi 23751 | Consequence of the modular pair property. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.) |
|
| ||
| Theorem | mdbr2 23752* | Binary relation expressing the modular pair property. This version has a weaker constraint than mdbr 23750. (Contributed by NM, 15-Jun-2004.) (New usage is discouraged.) |
|
| ||
| Theorem | mdbr3 23753* | Binary relation expressing the modular pair property. This version quantifies an equality instead of an inference. (Contributed by NM, 6-Jul-2004.) (New usage is discouraged.) |
| | ||
| Theorem | mdbr4 23754* | Binary relation expressing the modular pair property. This version quantifies an ordering instead of an inference. (Contributed by NM, 6-Jul-2004.) (New usage is discouraged.) |
| | ||
| Theorem | dmdbr 23755* | Binary relation expressing the dual modular pair property. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.) |
| | ||
| Theorem | dmdmd 23756 | The dual modular pair property expressed in terms of the modular pair property, that hold in Hilbert lattices. Remark 29.6 of [MaedaMaeda] p. 130. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.) |
| | ||
| Theorem | mddmd 23757 | The modular pair property expressed in terms of the dual modular pair property. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.) |
| | ||
| Theorem | dmdi 23758 | Consequence of the dual modular pair property. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.) |
|
| ||
| Theorem | dmdbr2 23759* | Binary relation expressing the dual modular pair property. This version has a weaker constraint than dmdbr 23755. (Contributed by NM, 30-Jun-2004.) (New usage is discouraged.) |
| | ||
| Theorem | dmdi2 23760 | Consequence of the dual modular pair property. (Contributed by NM, 14-Jan-2005.) (New usage is discouraged.) |
|
| ||
| Theorem | dmdbr3 23761* | Binary relation expressing the dual modular pair property. This version quantifies an equality instead of an inference. (Contributed by NM, 6-Jul-2004.) (New usage is discouraged.) |
|
| ||
| Theorem | dmdbr4 23762* | Binary relation expressing the dual modular pair property. This version quantifies an ordering instead of an inference. (Contributed by NM, 6-Jul-2004.) (New usage is discouraged.) |
| | ||
| Theorem | dmdi4 23763 | Consequence of the dual modular pair property. (Contributed by NM, 14-Jan-2005.) (New usage is discouraged.) |
|
| ||
| Theorem | dmdbr5 23764* | Binary relation expressing the dual modular pair property. (Contributed by NM, 15-Jan-2005.) (New usage is discouraged.) |
|
| ||
| Theorem | mddmd2 23765* | Relationship between modular pairs and dual-modular pairs. Lemma 1.2 of [MaedaMaeda] p. 1. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
|
| ||
| Theorem | mdsl0 23766 | A sublattice condition that transfers the modular pair property. Exercise 12 of [Kalmbach] p. 103. Also Lemma 1.5.3 of [MaedaMaeda] p. 2. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.) |
|
| ||
| Theorem | ssmd1 23767 | Ordering implies the modular pair property. Remark in [MaedaMaeda] p. 1. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| | ||
| Theorem | ssmd2 23768 | Ordering implies the modular pair property. Remark in [MaedaMaeda] p. 1. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| | ||
| Theorem | ssdmd1 23769 | Ordering implies the dual modular pair property. Remark in [MaedaMaeda] p. 1. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.) |
| | ||
| Theorem | ssdmd2 23770 | Ordering implies the dual modular pair property. Remark in [MaedaMaeda] p. 1. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.) |
| | ||
| Theorem | dmdsl3 23771 | Sublattice mapping for a dual-modular pair. Part of Theorem 1.3 of [MaedaMaeda] p. 2. (Contributed by NM, 26-Apr-2006.) (New usage is discouraged.) |
|
| ||
| Theorem | mdsl3 23772 | Sublattice mapping for a modular pair. Part of Theorem 1.3 of [MaedaMaeda] p. 2. (Contributed by NM, 26-Apr-2006.) (New usage is discouraged.) |
|
| ||
| Theorem | mdslle1i 23773 | Order preservation of the one-to-one onto mapping between the two sublattices in Lemma 1.3 of [MaedaMaeda] p. 2. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.) |
|
| ||
| Theorem | mdslle2i 23774 | Order preservation of the one-to-one onto mapping between the two sublattices in Lemma 1.3 of [MaedaMaeda] p. 2. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.) |
|
| ||
| Theorem | mdslj1i 23775 | Join preservation of the one-to-one onto mapping between the two sublattices in Lemma 1.3 of [MaedaMaeda] p. 2. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.) |
|
| ||
| Theorem | mdslj2i 23776 | Meet preservation of the reverse mapping between the two sublattices in Lemma 1.3 of [MaedaMaeda] p. 2. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.) |
|
| ||
| Theorem | mdsl1i 23777* | If the modular pair property holds in a sublattice, it holds in the whole lattice. Lemma 1.4 of [MaedaMaeda] p. 2. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.) |
|
| ||
| Theorem | mdsl2i 23778* | If the modular pair property holds in a sublattice, it holds in the whole lattice. Lemma 1.4 of [MaedaMaeda] p. 2. (Contributed by NM, 28-Apr-2006.) (New usage is discouraged.) |
| | ||
| Theorem | mdsl2bi 23779* | If the modular pair property holds in a sublattice, it holds in the whole lattice. Lemma 1.4 of [MaedaMaeda] p. 2. (Contributed by NM, 24-Dec-2006.) (New usage is discouraged.) |
| | ||
| Theorem | cvmdi 23780 | The covering property implies the modular pair property. Lemma 7.5.1 of [MaedaMaeda] p. 31. (Contributed by NM, 16-Jun-2004.) (New usage is discouraged.) |
| | ||
| Theorem | mdslmd1lem1 23781 | Lemma for mdslmd1i 23785. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
|
| ||
| Theorem | mdslmd1lem2 23782 | Lemma for mdslmd1i 23785. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
|
| ||
| Theorem | mdslmd1lem3 23783* | Lemma for mdslmd1i 23785. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
|
| ||
| Theorem | mdslmd1lem4 23784* | Lemma for mdslmd1i 23785. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
|
| ||
| Theorem | mdslmd1i 23785 | Preservation of the modular pair property in the one-to-one onto mapping between the two sublattices in Lemma 1.3 of [MaedaMaeda] p. 2 (meet version). (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.) |
|
| ||
| Theorem | mdslmd2i 23786 | Preservation of the modular pair property in the one-to-one onto mapping between the two sublattices in Lemma 1.3 of [MaedaMaeda] p. 2 (join version). (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
|
| ||
| Theorem | mdsldmd1i 23787 | Preservation of the dual modular pair property in the one-to-one onto mapping between the two sublattices in Lemma 1.3 of [MaedaMaeda] p. 2. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
|
| ||
| Theorem | mdslmd3i 23788 | Modular pair conditions that imply the modular pair property in a sublattice. Lemma 1.5.1 of [MaedaMaeda] p. 2. (Contributed by NM, 23-Dec-2006.) (New usage is discouraged.) |
|
| ||
| Theorem | mdslmd4i 23789 | Modular pair condition that implies the modular pair property in a sublattice. Lemma 1.5.2 of [MaedaMaeda] p. 2. (Contributed by NM, 24-Dec-2006.) (New usage is discouraged.) |
|
| ||
| Theorem | csmdsymi 23790* | Cross-symmetry implies M-symmetry. Theorem 1.9.1 of [MaedaMaeda] p. 3. (Contributed by NM, 24-Dec-2006.) (New usage is discouraged.) |
| ||
| Theorem | mdexchi 23791 | An exchange lemma for modular pairs. Lemma 1.6 of [MaedaMaeda] p. 2. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.) |
|
| ||
| Theorem | cvmd 23792 | The covering property implies the modular pair property. Lemma 7.5.1 of [MaedaMaeda] p. 31. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
|
| ||
| Theorem | cvdmd 23793 | The covering property implies the dual modular pair property. Lemma 7.5.2 of [MaedaMaeda] p. 31. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| | ||
| Definition | df-at 23794 | Define the set of atoms in a Hilbert lattice. An atom is a nonzero element of a lattice such that anything less than it is zero, i.e. it is the smallest nonzero element of the lattice. Definition of atom in [Kalmbach] p. 15. See ela 23795 and elat2 23796 for membership relations. (Contributed by NM, 14-Aug-2002.) (New usage is discouraged.) |
| HAtoms
| ||
| Theorem | ela 23795 | Atoms in a Hilbert lattice are the elements that cover the zero subspace. Definition of atom in [Kalmbach] p. 15. (Contributed by NM, 9-Jun-2004.) (New usage is discouraged.) |
|
HAtoms
| ||
| Theorem | elat2 23796* | Expanded membership relation for the set of atoms, i.e. the predicate "is an atom (of the Hilbert lattice)." An atom is a nonzero element of a lattice such that anything less than it is zero, i.e. it is the smallest nonzero element of the lattice. (Contributed by NM, 9-Jun-2004.) (New usage is discouraged.) |
HAtoms 
| ||
| Theorem | elatcv0 23797 | A Hilbert lattice element is an atom iff it covers the zero subspace. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.) |
|
HAtoms
| ||
| Theorem | atcv0 23798 | An atom covers the zero subspace. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.) |
|
HAtoms | ||
| Theorem | atssch 23799 | Atoms are a subset of the Hilbert lattice. (Contributed by NM, 14-Aug-2002.) (New usage is discouraged.) |
| HAtoms | ||
| Theorem | atelch 23800 | An atom is a Hilbert lattice element. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.) |
|
HAtoms | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |