HomeTheorem List (p. 292 of 426)
Unicode version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 292 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 | ||
| Theorem | stji1i 29101 | Join of components of Sasaki arrow ->1. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
        
         | ||
| Theorem | stm1i 29102 | State of component of unit meet. (Contributed by NM, 11-Nov-1999.) (New usage is discouraged.) |
 | ||
| Theorem | stm1ri 29103 | State of component of unit meet. (Contributed by NM, 11-Nov-1999.) (New usage is discouraged.) |
|
| ||
| Theorem | stm1addi 29104 | Sum of states whose meet is 1. (Contributed by NM, 11-Nov-1999.) (New usage is discouraged.) |
 | ||
| Theorem | staddi 29105 | 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 29106 | Sum of states whose meet is 1. (Contributed by NM, 11-Nov-1999.) (New usage is discouraged.) |
  | ||
| Theorem | stadd3i 29107 | 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 29108 | The state of the zero subspace. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
  | ||
| Theorem | strlem1 29109* |
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 29110* | Lemma for strong state theorem. (Contributed by NM, 28-Oct-1999.) (New usage is discouraged.) |
  
 
| ||
| Theorem | strlem3a 29111* |
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 29112* |
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 29113* | Lemma for strong state theorem. (Contributed by NM, 2-Nov-1999.) (New usage is discouraged.) |
|
| ||
| Theorem | strlem5 29114* | Lemma for strong state theorem. (Contributed by NM, 2-Nov-1999.) (New usage is discouraged.) |
 | ||
| Theorem | strlem6 29115* | Lemma for strong state theorem. (Contributed by NM, 2-Nov-1999.) (New usage is discouraged.) |
|
| ||
| Theorem | stri 29116* | 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 29117* | Strong state theorem (bidirectional version). (Contributed by NM, 7-Apr-2001.) (New usage is discouraged.) |
|
| ||
| Theorem | hstrlem2 29118* | Lemma for strong set of CH states theorem. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.) |
|
| ||
| Theorem | hstrlem3a 29119* |
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 29120* |
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 29121* | Lemma for strong set of CH states theorem. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.) |
|
| ||
| Theorem | hstrlem5 29122* | Lemma for strong set of CH states theorem. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.) |
|
| ||
| Theorem | hstrlem6 29123* | Lemma for strong set of CH states theorem. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.) |
|
| ||
| Theorem | hstri 29124* | 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 29125* | 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 29126* | 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 29127 | Lemma for Jauch-Piron theorem. (Contributed by NM, 8-Apr-2001.) (New usage is discouraged.) |
|
| ||
| Theorem | jplem2 29128* | Lemma for Jauch-Piron theorem. (Contributed by NM, 8-Apr-2001.) (New usage is discouraged.) |
|
| ||
| Theorem | jpi 29129* |
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 29111 for the proof that is
a state.) (Contributed by NM, 8-Apr-2001.)
(New usage is discouraged.)
|
|
| ||
| Theorem | golem1 29130 | Lemma for Godowski's equation. (Contributed by NM, 10-Nov-2002.) (New usage is discouraged.) |
    
| ||
| Theorem | golem2 29131 | Lemma for Godowski's equation. (Contributed by NM, 13-Nov-1999.) (New usage is discouraged.) |
|
| ||
| Theorem | goeqi 29132 | 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 29133* | Property of a strong classical state. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
| ||
| Theorem | stcltr2i 29134* | Property of a strong classical state. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
|
| ||
| Theorem | stcltrlem1 29135* | Lemma for strong classical state theorem. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
|
| ||
| Theorem | stcltrlem2 29136* | Lemma for strong classical state theorem. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
|
| ||
| Theorem | stcltrthi 29137* |
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 29138* |
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 29141
and cvbr2 29142 for membership
relations. (Contributed by NM, 4-Jun-2004.)
(New usage is discouraged.)
|
    
   | ||
| Definition | df-md 29139* | 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 29153 for membership relation. (Contributed by NM, 14-Jun-2004.) (New usage is discouraged.) |
| ||
| Definition | df-dmd 29140* | 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 29158 for membership relation. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.) |
| ||
| Theorem | cvbr 29141* |
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 29142* |
Binary relation expressing covers .
Definition of covers in
[Kalmbach] p. 15. (Contributed by NM,
9-Jun-2004.)
(New usage is discouraged.)
|
|
| ||
| Theorem | cvcon3 29143 | Contraposition law for the covers relation. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.) |
| | ||
| Theorem | cvpss 29144 | The covers relation implies proper subset. (Contributed by NM, 10-Jun-2004.) (New usage is discouraged.) |
| | ||
| Theorem | cvnbtwn 29145 | The covers relation implies no in-betweenness. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.) |
|
| ||
| Theorem | cvnbtwn2 29146 | The covers relation implies no in-betweenness. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.) |
|
| ||
| Theorem | cvnbtwn3 29147 | The covers relation implies no in-betweenness. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.) |
|
| ||
| Theorem | cvnbtwn4 29148 | 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 29149 | The covers relation is not symmetric. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.) |
| | ||
| Theorem | cvnref 29150 | The covers relation is not reflexive. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.) |
|
| ||
| Theorem | cvntr 29151 | The covers relation is not transitive. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.) |
|
| ||
| Theorem | spansncv2 29152 | 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 29153* |
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 29154 | Consequence of the modular pair property. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.) |
|
| ||
| Theorem | mdbr2 29155* | Binary relation expressing the modular pair property. This version has a weaker constraint than mdbr 29153. (Contributed by NM, 15-Jun-2004.) (New usage is discouraged.) |
|
| ||
| Theorem | mdbr3 29156* | 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 29157* | 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 29158* | Binary relation expressing the dual modular pair property. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.) |
| | ||
| Theorem | dmdmd 29159 | 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 29160 | 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 29161 | Consequence of the dual modular pair property. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.) |
|
| ||
| Theorem | dmdbr2 29162* | Binary relation expressing the dual modular pair property. This version has a weaker constraint than dmdbr 29158. (Contributed by NM, 30-Jun-2004.) (New usage is discouraged.) |
| | ||
| Theorem | dmdi2 29163 | Consequence of the dual modular pair property. (Contributed by NM, 14-Jan-2005.) (New usage is discouraged.) |
|
| ||
| Theorem | dmdbr3 29164* | 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 29165* | 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 29166 | Consequence of the dual modular pair property. (Contributed by NM, 14-Jan-2005.) (New usage is discouraged.) |
|
| ||
| Theorem | dmdbr5 29167* | Binary relation expressing the dual modular pair property. (Contributed by NM, 15-Jan-2005.) (New usage is discouraged.) |
|
| ||
| Theorem | mddmd2 29168* | 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 29169 | 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 29170 | Ordering implies the modular pair property. Remark in [MaedaMaeda] p. 1. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| | ||
| Theorem | ssmd2 29171 | Ordering implies the modular pair property. Remark in [MaedaMaeda] p. 1. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| | ||
| Theorem | ssdmd1 29172 | Ordering implies the dual modular pair property. Remark in [MaedaMaeda] p. 1. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.) |
| | ||
| Theorem | ssdmd2 29173 | Ordering implies the dual modular pair property. Remark in [MaedaMaeda] p. 1. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.) |
| | ||
| Theorem | dmdsl3 29174 | 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 29175 | 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 29176 | 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 29177 | 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 29178 | 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 29179 | 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 29180* | 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 29181* | 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 29182* | 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 29183 | 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 29184 | Lemma for mdslmd1i 29188. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
|
| ||
| Theorem | mdslmd1lem2 29185 | Lemma for mdslmd1i 29188. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
|
| ||
| Theorem | mdslmd1lem3 29186* | Lemma for mdslmd1i 29188. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
|
| ||
| Theorem | mdslmd1lem4 29187* | Lemma for mdslmd1i 29188. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
|
| ||
| Theorem | mdslmd1i 29188 | 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 29189 | 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 29190 | 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 29191 | 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 29192 | 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 29193* | 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 29194 | 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 29195 | 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 29196 | 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 29197 | 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 29198 and elat2 29199 for membership relations. (Contributed by NM, 14-Aug-2002.) (New usage is discouraged.) |
| HAtoms
| ||
| Theorem | ela 29198 | 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 29199* | 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 29200 | A Hilbert lattice element is an atom iff it covers the zero subspace. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.) |
|
HAtoms
| ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |