Home | Metamath
Proof Explorer Theorem List (p. 285 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 | span0 28401 | The span of the empty set is the zero subspace. Remark 11.6.e of [Schechter] p. 276. (Contributed by NM, 3-Jun-2004.) (New usage is discouraged.) |
Theorem | elspani 28402* | Membership in the span of a subset of Hilbert space. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.) |
Theorem | spanuni 28403 | The span of a union is the subspace sum of spans. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.) |
Theorem | spanun 28404 | The span of a union is the subspace sum of spans. (Contributed by NM, 9-Jun-2006.) (New usage is discouraged.) |
Theorem | sshhococi 28405 | The join of two Hilbert space subsets (not necessarily closed subspaces) equals the join of their closures (double orthocomplements). (Contributed by NM, 1-Jun-2004.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
Theorem | hne0 28406 | Hilbert space has a nonzero vector iff it is not trivial. (Contributed by NM, 24-Feb-2006.) (New usage is discouraged.) |
Theorem | chsup0 28407 | The supremum of the empty set. (Contributed by NM, 13-Aug-2002.) (New usage is discouraged.) |
Theorem | h1deoi 28408 | Membership in orthocomplement of 1-dimensional subspace. (Contributed by NM, 7-Jul-2001.) (New usage is discouraged.) |
Theorem | h1dei 28409* | Membership in 1-dimensional subspace. (Contributed by NM, 7-Jul-2001.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
Theorem | h1did 28410 | A generating vector belongs to the 1-dimensional subspace it generates. (Contributed by NM, 22-Jul-2001.) (New usage is discouraged.) |
Theorem | h1dn0 28411 | A nonzero vector generates a (nonzero) 1-dimensional subspace. (Contributed by NM, 22-Jul-2001.) (New usage is discouraged.) |
Theorem | h1de2i 28412 | Membership in 1-dimensional subspace. All members are collinear with the generating vector. (Contributed by NM, 17-Jul-2001.) (New usage is discouraged.) |
Theorem | h1de2bi 28413 | Membership in 1-dimensional subspace. All members are collinear with the generating vector. (Contributed by NM, 19-Jul-2001.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
Theorem | h1de2ctlem 28414* | Lemma for h1de2ci 28415. (Contributed by NM, 19-Jul-2001.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
Theorem | h1de2ci 28415* | Membership in 1-dimensional subspace. All members are collinear with the generating vector. (Contributed by NM, 21-Jul-2001.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
Theorem | spansni 28416 | The span of a singleton in Hilbert space equals its closure. (Contributed by NM, 3-Jun-2004.) (New usage is discouraged.) |
Theorem | elspansni 28417* | Membership in the span of a singleton. (Contributed by NM, 3-Jun-2004.) (New usage is discouraged.) |
Theorem | spansn 28418 | The span of a singleton in Hilbert space equals its closure. (Contributed by NM, 4-Jun-2004.) (New usage is discouraged.) |
Theorem | spansnch 28419 | The span of a Hilbert space singleton belongs to the Hilbert lattice. (Contributed by NM, 9-Jun-2004.) (New usage is discouraged.) |
Theorem | spansnsh 28420 | The span of a Hilbert space singleton is a subspace. (Contributed by NM, 17-Dec-2004.) (New usage is discouraged.) |
Theorem | spansnchi 28421 | The span of a singleton in Hilbert space is a closed subspace. (Contributed by NM, 3-Jun-2004.) (New usage is discouraged.) |
Theorem | spansnid 28422 | A vector belongs to the span of its singleton. (Contributed by NM, 3-Jun-2004.) (New usage is discouraged.) |
Theorem | spansnmul 28423 | A scalar product with a vector belongs to the span of its singleton. (Contributed by NM, 3-Jun-2004.) (New usage is discouraged.) |
Theorem | elspansncl 28424 | A member of a span of a singleton is a vector. (Contributed by NM, 17-Dec-2004.) (New usage is discouraged.) |
Theorem | elspansn 28425* | Membership in the span of a singleton. (Contributed by NM, 5-Jun-2004.) (New usage is discouraged.) |
Theorem | elspansn2 28426 | Membership in the span of a singleton. All members are collinear with the generating vector. (Contributed by NM, 5-Jun-2004.) (New usage is discouraged.) |
Theorem | spansncol 28427 | The singletons of collinear vectors have the same span. (Contributed by NM, 6-Jun-2004.) (New usage is discouraged.) |
Theorem | spansneleqi 28428 | Membership relation implied by equality of spans. (Contributed by NM, 6-Jun-2004.) (New usage is discouraged.) |
Theorem | spansneleq 28429 | Membership relation that implies equality of spans. (Contributed by NM, 6-Jun-2004.) (New usage is discouraged.) |
Theorem | spansnss 28430 | The span of the singleton of an element of a subspace is included in the subspace. (Contributed by NM, 5-Jun-2004.) (New usage is discouraged.) |
Theorem | elspansn3 28431 | A member of the span of the singleton of a vector is a member of a subspace containing the vector. (Contributed by NM, 16-Dec-2004.) (New usage is discouraged.) |
Theorem | elspansn4 28432 | A span membership condition implying two vectors belong to the same subspace. (Contributed by NM, 17-Dec-2004.) (New usage is discouraged.) |
Theorem | elspansn5 28433 | A vector belonging to both a subspace and the span of the singleton of a vector not in it must be zero. (Contributed by NM, 17-Dec-2004.) (New usage is discouraged.) |
Theorem | spansnss2 28434 | The span of the singleton of an element of a subspace is included in the subspace. (Contributed by NM, 16-Dec-2004.) (New usage is discouraged.) |
Theorem | normcan 28435 | Cancellation-type law that "extracts" a vector from its inner product with a proportional vector . (Contributed by NM, 18-Mar-2006.) (New usage is discouraged.) |
Theorem | pjspansn 28436 | A projection on the span of a singleton. (The proof ws shortened by Mario Carneiro, 15-Dec-2013.) (Contributed by NM, 28-May-2006.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
Theorem | spansnpji 28437 | A subset of Hilbert space is orthogonal to the span of the singleton of a projection onto its orthocomplement. (Contributed by NM, 4-Jun-2004.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
Theorem | spanunsni 28438 | The span of the union of a closed subspace with a singleton equals the span of its union with an orthogonal singleton. (Contributed by NM, 3-Jun-2004.) (New usage is discouraged.) |
Theorem | spanpr 28439 | The span of a pair of vectors. (Contributed by NM, 9-Jun-2006.) (New usage is discouraged.) |
Theorem | h1datomi 28440 | A 1-dimensional subspace is an atom. (Contributed by NM, 20-Jul-2001.) (New usage is discouraged.) |
Theorem | h1datom 28441 | A 1-dimensional subspace is an atom. (Contributed by NM, 22-Jul-2001.) (New usage is discouraged.) |
Definition | df-cm 28442* | Define the commutes relation (on the Hilbert lattice). Definition of commutes in [Kalmbach] p. 20, who uses the notation xCy for "x commutes with y." See cmbri 28449 for membership relation. (Contributed by NM, 14-Jun-2004.) (New usage is discouraged.) |
Theorem | cmbr 28443 | Binary relation expressing commutes with . Definition of commutes in [Kalmbach] p. 20. (Contributed by NM, 14-Jun-2004.) (New usage is discouraged.) |
Theorem | pjoml2i 28444 | Variation of orthomodular law. Definition in [Kalmbach] p. 22. (Contributed by NM, 31-Oct-2000.) (New usage is discouraged.) |
Theorem | pjoml3i 28445 | Variation of orthomodular law. (Contributed by NM, 24-Jun-2004.) (New usage is discouraged.) |
Theorem | pjoml4i 28446 | Variation of orthomodular law. (Contributed by NM, 6-Dec-2000.) (New usage is discouraged.) |
Theorem | pjoml5i 28447 | The orthomodular law. Remark in [Kalmbach] p. 22. (Contributed by NM, 12-Jun-2006.) (New usage is discouraged.) |
Theorem | pjoml6i 28448* | An equivalent of the orthomodular law. Theorem 29.13(e) of [MaedaMaeda] p. 132. (Contributed by NM, 30-May-2004.) (New usage is discouraged.) |
Theorem | cmbri 28449 | Binary relation expressing the commutes relation. Definition of commutes in [Kalmbach] p. 20. (Contributed by NM, 6-Aug-2004.) (New usage is discouraged.) |
Theorem | cmcmlem 28450 | Commutation is symmetric. Theorem 3.4 of [Beran] p. 45. (Contributed by NM, 3-Nov-2000.) (New usage is discouraged.) |
Theorem | cmcmi 28451 | Commutation is symmetric. Theorem 2(v) of [Kalmbach] p. 22. (Contributed by NM, 4-Nov-2000.) (New usage is discouraged.) |
Theorem | cmcm2i 28452 | Commutation with orthocomplement. Theorem 2.3(i) of [Beran] p. 39. (Contributed by NM, 4-Nov-2000.) (New usage is discouraged.) |
Theorem | cmcm3i 28453 | Commutation with orthocomplement. Remark in [Kalmbach] p. 23. (Contributed by NM, 4-Nov-2000.) (New usage is discouraged.) |
Theorem | cmcm4i 28454 | Commutation with orthocomplement. Remark in [Kalmbach] p. 23. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.) |
Theorem | cmbr2i 28455 | Alternate definition of the commutes relation. Remark in [Kalmbach] p. 23. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.) |
Theorem | cmcmii 28456 | Commutation is symmetric. Theorem 2(v) of [Kalmbach] p. 22. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.) |
Theorem | cmcm2ii 28457 | Commutation with orthocomplement. Theorem 2.3(i) of [Beran] p. 39. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.) |
Theorem | cmcm3ii 28458 | Commutation with orthocomplement. Remark in [Kalmbach] p. 23. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.) |
Theorem | cmbr3i 28459 | Alternate definition for the commutes relation. Lemma 3 of [Kalmbach] p. 23. (Contributed by NM, 6-Dec-2000.) (New usage is discouraged.) |
Theorem | cmbr4i 28460 | Alternate definition for the commutes relation. (Contributed by NM, 6-Dec-2000.) (New usage is discouraged.) |
Theorem | lecmi 28461 | Comparable Hilbert lattice elements commute. Theorem 2.3(iii) of [Beran] p. 40. (Contributed by NM, 16-Jan-2005.) (New usage is discouraged.) |
Theorem | lecmii 28462 | Comparable Hilbert lattice elements commute. Theorem 2.3(iii) of [Beran] p. 40. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.) |
Theorem | cmj1i 28463 | A Hilbert lattice element commutes with its join. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.) |
Theorem | cmj2i 28464 | A Hilbert lattice element commutes with its join. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.) |
Theorem | cmm1i 28465 | A Hilbert lattice element commutes with its meet. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.) |
Theorem | cmm2i 28466 | A Hilbert lattice element commutes with its meet. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.) |
Theorem | cmbr3 28467 | Alternate definition for the commutes relation. Lemma 3 of [Kalmbach] p. 23. (Contributed by NM, 14-Jun-2006.) (New usage is discouraged.) |
Theorem | cm0 28468 | The zero Hilbert lattice element commutes with every element. (Contributed by NM, 16-Jun-2006.) (New usage is discouraged.) |
Theorem | cmidi 28469 | The commutes relation is reflexive. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.) |
Theorem | pjoml2 28470 | Variation of orthomodular law. Definition in [Kalmbach] p. 22. (Contributed by NM, 13-Jun-2006.) (New usage is discouraged.) |
Theorem | pjoml3 28471 | Variation of orthomodular law. (Contributed by NM, 24-Jun-2004.) (New usage is discouraged.) |
Theorem | pjoml5 28472 | The orthomodular law. Remark in [Kalmbach] p. 22. (Contributed by NM, 12-Jun-2006.) (New usage is discouraged.) |
Theorem | cmcm 28473 | Commutation is symmetric. Theorem 2(v) of [Kalmbach] p. 22. (Contributed by NM, 13-Jun-2006.) (New usage is discouraged.) |
Theorem | cmcm3 28474 | Commutation with orthocomplement. Remark in [Kalmbach] p. 23. (Contributed by NM, 13-Jun-2006.) (New usage is discouraged.) |
Theorem | cmcm2 28475 | Commutation with orthocomplement. Theorem 2.3(i) of [Beran] p. 39. (Contributed by NM, 14-Jun-2006.) (New usage is discouraged.) |
Theorem | lecm 28476 | Comparable Hilbert lattice elements commute. Theorem 2.3(iii) of [Beran] p. 40. (Contributed by NM, 13-Jun-2006.) (New usage is discouraged.) |
Theorem | fh1 28477 | Foulis-Holland Theorem. If any 2 pairs in a triple of orthomodular lattice elements commute, the triple is distributive. First of two parts. Theorem 5 of [Kalmbach] p. 25. (Contributed by NM, 14-Jun-2006.) (New usage is discouraged.) |
Theorem | fh2 28478 | Foulis-Holland Theorem. If any 2 pairs in a triple of orthomodular lattice elements commute, the triple is distributive. Second of two parts. Theorem 5 of [Kalmbach] p. 25. (Contributed by NM, 14-Jun-2006.) (New usage is discouraged.) |
Theorem | cm2j 28479 | A lattice element that commutes with two others also commutes with their join. Theorem 4.2 of [Beran] p. 49. (Contributed by NM, 15-Jun-2006.) (New usage is discouraged.) |
Theorem | fh1i 28480 | Foulis-Holland Theorem. If any 2 pairs in a triple of orthomodular lattice elements commute, the triple is distributive. First of two parts. Theorem 5 of [Kalmbach] p. 25. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.) |
Theorem | fh2i 28481 | Foulis-Holland Theorem. If any 2 pairs in a triple of orthomodular lattice elements commute, the triple is distributive. Second of two parts. Theorem 5 of [Kalmbach] p. 25. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.) |
Theorem | fh3i 28482 | Variation of the Foulis-Holland Theorem. (Contributed by NM, 16-Jan-2005.) (New usage is discouraged.) |
Theorem | fh4i 28483 | Variation of the Foulis-Holland Theorem. (Contributed by NM, 16-Jan-2005.) (New usage is discouraged.) |
Theorem | cm2ji 28484 | A lattice element that commutes with two others also commutes with their join. Theorem 4.2 of [Beran] p. 49. (Contributed by NM, 11-May-2009.) (New usage is discouraged.) |
Theorem | cm2mi 28485 | A lattice element that commutes with two others also commutes with their meet. Theorem 4.2 of [Beran] p. 49. (Contributed by NM, 11-May-2009.) (New usage is discouraged.) |
Theorem | qlax1i 28486 | One of the equations showing is an ortholattice. (This corresponds to axiom "ax-1" in the Quantum Logic Explorer.) (Contributed by NM, 4-Aug-2004.) (New usage is discouraged.) |
Theorem | qlax2i 28487 | One of the equations showing is an ortholattice. (This corresponds to axiom "ax-2" in the Quantum Logic Explorer.) (Contributed by NM, 4-Aug-2004.) (New usage is discouraged.) |
Theorem | qlax3i 28488 | One of the equations showing is an ortholattice. (This corresponds to axiom "ax-3" in the Quantum Logic Explorer.) (Contributed by NM, 4-Aug-2004.) (New usage is discouraged.) |
Theorem | qlax4i 28489 | One of the equations showing is an ortholattice. (This corresponds to axiom "ax-4" in the Quantum Logic Explorer.) (Contributed by NM, 4-Aug-2004.) (New usage is discouraged.) |
Theorem | qlax5i 28490 | One of the equations showing is an ortholattice. (This corresponds to axiom "ax-5" in the Quantum Logic Explorer.) (Contributed by NM, 4-Aug-2004.) (New usage is discouraged.) |
Theorem | qlaxr1i 28491 | One of the conditions showing is an ortholattice. (This corresponds to axiom "ax-r1" in the Quantum Logic Explorer.) (Contributed by NM, 4-Aug-2004.) (New usage is discouraged.) |
Theorem | qlaxr2i 28492 | One of the conditions showing is an ortholattice. (This corresponds to axiom "ax-r2" in the Quantum Logic Explorer.) (Contributed by NM, 4-Aug-2004.) (New usage is discouraged.) |
Theorem | qlaxr4i 28493 | One of the conditions showing is an ortholattice. (This corresponds to axiom "ax-r4" in the Quantum Logic Explorer.) (Contributed by NM, 4-Aug-2004.) (New usage is discouraged.) |
Theorem | qlaxr5i 28494 | One of the conditions showing is an ortholattice. (This corresponds to axiom "ax-r5" in the Quantum Logic Explorer.) (Contributed by NM, 4-Aug-2004.) (New usage is discouraged.) |
Theorem | qlaxr3i 28495 | A variation of the orthomodular law, showing is an orthomodular lattice. (This corresponds to axiom "ax-r3" in the Quantum Logic Explorer.) (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.) |
Theorem | chscllem1 28496* | Lemma for chscl 28500. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
Theorem | chscllem2 28497* | Lemma for chscl 28500. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
Theorem | chscllem3 28498* | Lemma for chscl 28500. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
Theorem | chscllem4 28499* | Lemma for chscl 28500. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
Theorem | chscl 28500 | The subspace sum of two closed orthogonal spaces is closed. (Contributed by NM, 19-Oct-1999.) (Proof shortened by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |