![]() |
Metamath
Proof Explorer Theorem List (p. 312 of 480) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cmbr 31101 | Binary relation expressing 𝐴 commutes with 𝐵. Definition of commutes in [Kalmbach] p. 20. (Contributed by NM, 14-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝐶ℋ 𝐵 ↔ 𝐴 = ((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ (⊥‘𝐵))))) | ||
Theorem | pjoml2i 31102 | Variation of orthomodular law. Definition in [Kalmbach] p. 22. (Contributed by NM, 31-Oct-2000.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∨ℋ ((⊥‘𝐴) ∩ 𝐵)) = 𝐵) | ||
Theorem | pjoml3i 31103 | Variation of orthomodular law. (Contributed by NM, 24-Jun-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐵 ⊆ 𝐴 → (𝐴 ∩ ((⊥‘𝐴) ∨ℋ 𝐵)) = 𝐵) | ||
Theorem | pjoml4i 31104 | Variation of orthomodular law. (Contributed by NM, 6-Dec-2000.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ∨ℋ (𝐵 ∩ ((⊥‘𝐴) ∨ℋ (⊥‘𝐵)))) = (𝐴 ∨ℋ 𝐵) | ||
Theorem | pjoml5i 31105 | The orthomodular law. Remark in [Kalmbach] p. 22. (Contributed by NM, 12-Jun-2006.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ∨ℋ ((⊥‘𝐴) ∩ (𝐴 ∨ℋ 𝐵))) = (𝐴 ∨ℋ 𝐵) | ||
Theorem | pjoml6i 31106* | An equivalent of the orthomodular law. Theorem 29.13(e) of [MaedaMaeda] p. 132. (Contributed by NM, 30-May-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ⊆ 𝐵 → ∃𝑥 ∈ Cℋ (𝐴 ⊆ (⊥‘𝑥) ∧ (𝐴 ∨ℋ 𝑥) = 𝐵)) | ||
Theorem | cmbri 31107 | Binary relation expressing the commutes relation. Definition of commutes in [Kalmbach] p. 20. (Contributed by NM, 6-Aug-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 𝐶ℋ 𝐵 ↔ 𝐴 = ((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ (⊥‘𝐵)))) | ||
Theorem | cmcmlem 31108 | Commutation is symmetric. Theorem 3.4 of [Beran] p. 45. (Contributed by NM, 3-Nov-2000.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 𝐶ℋ 𝐵 → 𝐵 𝐶ℋ 𝐴) | ||
Theorem | cmcmi 31109 | Commutation is symmetric. Theorem 2(v) of [Kalmbach] p. 22. (Contributed by NM, 4-Nov-2000.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 𝐶ℋ 𝐵 ↔ 𝐵 𝐶ℋ 𝐴) | ||
Theorem | cmcm2i 31110 | Commutation with orthocomplement. Theorem 2.3(i) of [Beran] p. 39. (Contributed by NM, 4-Nov-2000.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 𝐶ℋ 𝐵 ↔ 𝐴 𝐶ℋ (⊥‘𝐵)) | ||
Theorem | cmcm3i 31111 | Commutation with orthocomplement. Remark in [Kalmbach] p. 23. (Contributed by NM, 4-Nov-2000.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 𝐶ℋ 𝐵 ↔ (⊥‘𝐴) 𝐶ℋ 𝐵) | ||
Theorem | cmcm4i 31112 | Commutation with orthocomplement. Remark in [Kalmbach] p. 23. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 𝐶ℋ 𝐵 ↔ (⊥‘𝐴) 𝐶ℋ (⊥‘𝐵)) | ||
Theorem | cmbr2i 31113 | Alternate definition of the commutes relation. Remark in [Kalmbach] p. 23. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 𝐶ℋ 𝐵 ↔ 𝐴 = ((𝐴 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ (⊥‘𝐵)))) | ||
Theorem | cmcmii 31114 | Commutation is symmetric. Theorem 2(v) of [Kalmbach] p. 22. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐴 𝐶ℋ 𝐵 ⇒ ⊢ 𝐵 𝐶ℋ 𝐴 | ||
Theorem | cmcm2ii 31115 | Commutation with orthocomplement. Theorem 2.3(i) of [Beran] p. 39. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐴 𝐶ℋ 𝐵 ⇒ ⊢ 𝐴 𝐶ℋ (⊥‘𝐵) | ||
Theorem | cmcm3ii 31116 | Commutation with orthocomplement. Remark in [Kalmbach] p. 23. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐴 𝐶ℋ 𝐵 ⇒ ⊢ (⊥‘𝐴) 𝐶ℋ 𝐵 | ||
Theorem | cmbr3i 31117 | Alternate definition for the commutes relation. Lemma 3 of [Kalmbach] p. 23. (Contributed by NM, 6-Dec-2000.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 𝐶ℋ 𝐵 ↔ (𝐴 ∩ ((⊥‘𝐴) ∨ℋ 𝐵)) = (𝐴 ∩ 𝐵)) | ||
Theorem | cmbr4i 31118 | Alternate definition for the commutes relation. (Contributed by NM, 6-Dec-2000.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 𝐶ℋ 𝐵 ↔ (𝐴 ∩ ((⊥‘𝐴) ∨ℋ 𝐵)) ⊆ 𝐵) | ||
Theorem | lecmi 31119 | Comparable Hilbert lattice elements commute. Theorem 2.3(iii) of [Beran] p. 40. (Contributed by NM, 16-Jan-2005.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ⊆ 𝐵 → 𝐴 𝐶ℋ 𝐵) | ||
Theorem | lecmii 31120 | Comparable Hilbert lattice elements commute. Theorem 2.3(iii) of [Beran] p. 40. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐴 ⊆ 𝐵 ⇒ ⊢ 𝐴 𝐶ℋ 𝐵 | ||
Theorem | cmj1i 31121 | A Hilbert lattice element commutes with its join. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ 𝐴 𝐶ℋ (𝐴 ∨ℋ 𝐵) | ||
Theorem | cmj2i 31122 | A Hilbert lattice element commutes with its join. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ 𝐵 𝐶ℋ (𝐴 ∨ℋ 𝐵) | ||
Theorem | cmm1i 31123 | A Hilbert lattice element commutes with its meet. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ 𝐴 𝐶ℋ (𝐴 ∩ 𝐵) | ||
Theorem | cmm2i 31124 | A Hilbert lattice element commutes with its meet. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ 𝐵 𝐶ℋ (𝐴 ∩ 𝐵) | ||
Theorem | cmbr3 31125 | Alternate definition for the commutes relation. Lemma 3 of [Kalmbach] p. 23. (Contributed by NM, 14-Jun-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝐶ℋ 𝐵 ↔ (𝐴 ∩ ((⊥‘𝐴) ∨ℋ 𝐵)) = (𝐴 ∩ 𝐵))) | ||
Theorem | cm0 31126 | The zero Hilbert lattice element commutes with every element. (Contributed by NM, 16-Jun-2006.) (New usage is discouraged.) |
⊢ (𝐴 ∈ Cℋ → 0ℋ 𝐶ℋ 𝐴) | ||
Theorem | cmidi 31127 | The commutes relation is reflexive. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ ⇒ ⊢ 𝐴 𝐶ℋ 𝐴 | ||
Theorem | pjoml2 31128 | Variation of orthomodular law. Definition in [Kalmbach] p. 22. (Contributed by NM, 13-Jun-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐴 ⊆ 𝐵) → (𝐴 ∨ℋ ((⊥‘𝐴) ∩ 𝐵)) = 𝐵) | ||
Theorem | pjoml3 31129 | Variation of orthomodular law. (Contributed by NM, 24-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐵 ⊆ 𝐴 → (𝐴 ∩ ((⊥‘𝐴) ∨ℋ 𝐵)) = 𝐵)) | ||
Theorem | pjoml5 31130 | The orthomodular law. Remark in [Kalmbach] p. 22. (Contributed by NM, 12-Jun-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ∨ℋ ((⊥‘𝐴) ∩ (𝐴 ∨ℋ 𝐵))) = (𝐴 ∨ℋ 𝐵)) | ||
Theorem | cmcm 31131 | Commutation is symmetric. Theorem 2(v) of [Kalmbach] p. 22. (Contributed by NM, 13-Jun-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝐶ℋ 𝐵 ↔ 𝐵 𝐶ℋ 𝐴)) | ||
Theorem | cmcm3 31132 | Commutation with orthocomplement. Remark in [Kalmbach] p. 23. (Contributed by NM, 13-Jun-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝐶ℋ 𝐵 ↔ (⊥‘𝐴) 𝐶ℋ 𝐵)) | ||
Theorem | cmcm2 31133 | Commutation with orthocomplement. Theorem 2.3(i) of [Beran] p. 39. (Contributed by NM, 14-Jun-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝐶ℋ 𝐵 ↔ 𝐴 𝐶ℋ (⊥‘𝐵))) | ||
Theorem | lecm 31134 | Comparable Hilbert lattice elements commute. Theorem 2.3(iii) of [Beran] p. 40. (Contributed by NM, 13-Jun-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐴 ⊆ 𝐵) → 𝐴 𝐶ℋ 𝐵) | ||
Theorem | fh1 31135 | 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.) |
⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ (𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶)) → (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) = ((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶))) | ||
Theorem | fh2 31136 | 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.) |
⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ (𝐵 𝐶ℋ 𝐴 ∧ 𝐵 𝐶ℋ 𝐶)) → (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) = ((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶))) | ||
Theorem | cm2j 31137 | 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.) |
⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ (𝐴 𝐶ℋ 𝐵 ∧ 𝐴 𝐶ℋ 𝐶)) → 𝐴 𝐶ℋ (𝐵 ∨ℋ 𝐶)) | ||
Theorem | fh1i 31138 | 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.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝐴 𝐶ℋ 𝐵 & ⊢ 𝐴 𝐶ℋ 𝐶 ⇒ ⊢ (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) = ((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)) | ||
Theorem | fh2i 31139 | 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.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝐴 𝐶ℋ 𝐵 & ⊢ 𝐴 𝐶ℋ 𝐶 ⇒ ⊢ (𝐵 ∩ (𝐴 ∨ℋ 𝐶)) = ((𝐵 ∩ 𝐴) ∨ℋ (𝐵 ∩ 𝐶)) | ||
Theorem | fh3i 31140 | Variation of the Foulis-Holland Theorem. (Contributed by NM, 16-Jan-2005.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝐴 𝐶ℋ 𝐵 & ⊢ 𝐴 𝐶ℋ 𝐶 ⇒ ⊢ (𝐴 ∨ℋ (𝐵 ∩ 𝐶)) = ((𝐴 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐶)) | ||
Theorem | fh4i 31141 | Variation of the Foulis-Holland Theorem. (Contributed by NM, 16-Jan-2005.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝐴 𝐶ℋ 𝐵 & ⊢ 𝐴 𝐶ℋ 𝐶 ⇒ ⊢ (𝐵 ∨ℋ (𝐴 ∩ 𝐶)) = ((𝐵 ∨ℋ 𝐴) ∩ (𝐵 ∨ℋ 𝐶)) | ||
Theorem | cm2ji 31142 | 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.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝐴 𝐶ℋ 𝐵 & ⊢ 𝐴 𝐶ℋ 𝐶 ⇒ ⊢ 𝐴 𝐶ℋ (𝐵 ∨ℋ 𝐶) | ||
Theorem | cm2mi 31143 | 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.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝐴 𝐶ℋ 𝐵 & ⊢ 𝐴 𝐶ℋ 𝐶 ⇒ ⊢ 𝐴 𝐶ℋ (𝐵 ∩ 𝐶) | ||
Theorem | qlax1i 31144 | One of the equations showing Cℋ is an ortholattice. (This corresponds to axiom "ax-1" in the Quantum Logic Explorer.) (Contributed by NM, 4-Aug-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ ⇒ ⊢ 𝐴 = (⊥‘(⊥‘𝐴)) | ||
Theorem | qlax2i 31145 | One of the equations showing Cℋ is an ortholattice. (This corresponds to axiom "ax-2" in the Quantum Logic Explorer.) (Contributed by NM, 4-Aug-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ∨ℋ 𝐵) = (𝐵 ∨ℋ 𝐴) | ||
Theorem | qlax3i 31146 | One of the equations showing Cℋ is an ortholattice. (This corresponds to axiom "ax-3" in the Quantum Logic Explorer.) (Contributed by NM, 4-Aug-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ ⇒ ⊢ ((𝐴 ∨ℋ 𝐵) ∨ℋ 𝐶) = (𝐴 ∨ℋ (𝐵 ∨ℋ 𝐶)) | ||
Theorem | qlax4i 31147 | One of the equations showing Cℋ is an ortholattice. (This corresponds to axiom "ax-4" in the Quantum Logic Explorer.) (Contributed by NM, 4-Aug-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ∨ℋ (𝐵 ∨ℋ (⊥‘𝐵))) = (𝐵 ∨ℋ (⊥‘𝐵)) | ||
Theorem | qlax5i 31148 | One of the equations showing Cℋ is an ortholattice. (This corresponds to axiom "ax-5" in the Quantum Logic Explorer.) (Contributed by NM, 4-Aug-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ∨ℋ (⊥‘((⊥‘𝐴) ∨ℋ 𝐵))) = 𝐴 | ||
Theorem | qlaxr1i 31149 | One of the conditions showing Cℋ is an ortholattice. (This corresponds to axiom "ax-r1" in the Quantum Logic Explorer.) (Contributed by NM, 4-Aug-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐴 = 𝐵 ⇒ ⊢ 𝐵 = 𝐴 | ||
Theorem | qlaxr2i 31150 | One of the conditions showing Cℋ is an ortholattice. (This corresponds to axiom "ax-r2" in the Quantum Logic Explorer.) (Contributed by NM, 4-Aug-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝐴 = 𝐵 & ⊢ 𝐵 = 𝐶 ⇒ ⊢ 𝐴 = 𝐶 | ||
Theorem | qlaxr4i 31151 | One of the conditions showing Cℋ is an ortholattice. (This corresponds to axiom "ax-r4" in the Quantum Logic Explorer.) (Contributed by NM, 4-Aug-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐴 = 𝐵 ⇒ ⊢ (⊥‘𝐴) = (⊥‘𝐵) | ||
Theorem | qlaxr5i 31152 | One of the conditions showing Cℋ is an ortholattice. (This corresponds to axiom "ax-r5" in the Quantum Logic Explorer.) (Contributed by NM, 4-Aug-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 ∨ℋ 𝐶) = (𝐵 ∨ℋ 𝐶) | ||
Theorem | qlaxr3i 31153 | A variation of the orthomodular law, showing Cℋ 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.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ (𝐶 ∨ℋ (⊥‘𝐶)) = ((⊥‘((⊥‘𝐴) ∨ℋ (⊥‘𝐵))) ∨ℋ (⊥‘(𝐴 ∨ℋ 𝐵))) ⇒ ⊢ 𝐴 = 𝐵 | ||
Theorem | chscllem1 31154* | Lemma for chscl 31158. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐴 ∈ Cℋ ) & ⊢ (𝜑 → 𝐵 ∈ Cℋ ) & ⊢ (𝜑 → 𝐵 ⊆ (⊥‘𝐴)) & ⊢ (𝜑 → 𝐻:ℕ⟶(𝐴 +ℋ 𝐵)) & ⊢ (𝜑 → 𝐻 ⇝𝑣 𝑢) & ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((projℎ‘𝐴)‘(𝐻‘𝑛))) ⇒ ⊢ (𝜑 → 𝐹:ℕ⟶𝐴) | ||
Theorem | chscllem2 31155* | Lemma for chscl 31158. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐴 ∈ Cℋ ) & ⊢ (𝜑 → 𝐵 ∈ Cℋ ) & ⊢ (𝜑 → 𝐵 ⊆ (⊥‘𝐴)) & ⊢ (𝜑 → 𝐻:ℕ⟶(𝐴 +ℋ 𝐵)) & ⊢ (𝜑 → 𝐻 ⇝𝑣 𝑢) & ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((projℎ‘𝐴)‘(𝐻‘𝑛))) ⇒ ⊢ (𝜑 → 𝐹 ∈ dom ⇝𝑣 ) | ||
Theorem | chscllem3 31156* | Lemma for chscl 31158. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐴 ∈ Cℋ ) & ⊢ (𝜑 → 𝐵 ∈ Cℋ ) & ⊢ (𝜑 → 𝐵 ⊆ (⊥‘𝐴)) & ⊢ (𝜑 → 𝐻:ℕ⟶(𝐴 +ℋ 𝐵)) & ⊢ (𝜑 → 𝐻 ⇝𝑣 𝑢) & ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((projℎ‘𝐴)‘(𝐻‘𝑛))) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ 𝐴) & ⊢ (𝜑 → 𝐷 ∈ 𝐵) & ⊢ (𝜑 → (𝐻‘𝑁) = (𝐶 +ℎ 𝐷)) ⇒ ⊢ (𝜑 → 𝐶 = (𝐹‘𝑁)) | ||
Theorem | chscllem4 31157* | Lemma for chscl 31158. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐴 ∈ Cℋ ) & ⊢ (𝜑 → 𝐵 ∈ Cℋ ) & ⊢ (𝜑 → 𝐵 ⊆ (⊥‘𝐴)) & ⊢ (𝜑 → 𝐻:ℕ⟶(𝐴 +ℋ 𝐵)) & ⊢ (𝜑 → 𝐻 ⇝𝑣 𝑢) & ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((projℎ‘𝐴)‘(𝐻‘𝑛))) & ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ((projℎ‘𝐵)‘(𝐻‘𝑛))) ⇒ ⊢ (𝜑 → 𝑢 ∈ (𝐴 +ℋ 𝐵)) | ||
Theorem | chscl 31158 | 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.) |
⊢ (𝜑 → 𝐴 ∈ Cℋ ) & ⊢ (𝜑 → 𝐵 ∈ Cℋ ) & ⊢ (𝜑 → 𝐵 ⊆ (⊥‘𝐴)) ⇒ ⊢ (𝜑 → (𝐴 +ℋ 𝐵) ∈ Cℋ ) | ||
Theorem | osumi 31159 | If two closed subspaces of a Hilbert space are orthogonal, their subspace sum equals their subspace join. Lemma 3 of [Kalmbach] p. 67. Note that the (countable) Axiom of Choice is used for this proof via pjhth 30910, although "the hard part" of this proof, chscl 31158, requires no choice. (Contributed by NM, 28-Oct-1999.) (Revised by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ⊆ (⊥‘𝐵) → (𝐴 +ℋ 𝐵) = (𝐴 ∨ℋ 𝐵)) | ||
Theorem | osumcori 31160 | Corollary of osumi 31159. (Contributed by NM, 5-Nov-2000.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ ((𝐴 ∩ 𝐵) +ℋ (𝐴 ∩ (⊥‘𝐵))) = ((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ (⊥‘𝐵))) | ||
Theorem | osumcor2i 31161 | Corollary of osumi 31159, showing it holds under the weaker hypothesis that 𝐴 and 𝐵 commute. (Contributed by NM, 6-Dec-2000.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 𝐶ℋ 𝐵 → (𝐴 +ℋ 𝐵) = (𝐴 ∨ℋ 𝐵)) | ||
Theorem | osum 31162 | If two closed subspaces of a Hilbert space are orthogonal, their subspace sum equals their subspace join. Lemma 3 of [Kalmbach] p. 67. (Contributed by NM, 31-Oct-2005.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐴 ⊆ (⊥‘𝐵)) → (𝐴 +ℋ 𝐵) = (𝐴 ∨ℋ 𝐵)) | ||
Theorem | spansnji 31163 | The subspace sum of a closed subspace and a one-dimensional subspace equals their join. (Proof suggested by Eric Schechter 1-Jun-2004.) (Contributed by NM, 1-Jun-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (𝐴 +ℋ (span‘{𝐵})) = (𝐴 ∨ℋ (span‘{𝐵})) | ||
Theorem | spansnj 31164 | The subspace sum of a closed subspace and a one-dimensional subspace equals their join. (Contributed by NM, 4-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℋ (span‘{𝐵})) = (𝐴 ∨ℋ (span‘{𝐵}))) | ||
Theorem | spansnscl 31165 | The subspace sum of a closed subspace and a one-dimensional subspace is closed. (Contributed by NM, 17-Dec-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ ℋ) → (𝐴 +ℋ (span‘{𝐵})) ∈ Cℋ ) | ||
Theorem | sumspansn 31166 | The sum of two vectors belong to the span of one of them iff the other vector also belongs. (Contributed by NM, 1-Nov-2005.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝐴 +ℎ 𝐵) ∈ (span‘{𝐴}) ↔ 𝐵 ∈ (span‘{𝐴}))) | ||
Theorem | spansnm0i 31167 | The meet of different one-dimensional subspaces is the zero subspace. (Contributed by NM, 1-Nov-2005.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (¬ 𝐴 ∈ (span‘{𝐵}) → ((span‘{𝐴}) ∩ (span‘{𝐵})) = 0ℋ) | ||
Theorem | nonbooli 31168 | A Hilbert lattice with two or more dimensions fails the distributive law and therefore cannot be a Boolean algebra. This counterexample demonstrates a condition where ((𝐻 ∩ 𝐹) ∨ℋ (𝐻 ∩ 𝐺)) = 0ℋ but (𝐻 ∩ (𝐹 ∨ℋ 𝐺)) ≠ 0ℋ. The antecedent specifies that the vectors 𝐴 and 𝐵 are nonzero and non-colinear. The last three hypotheses assign one-dimensional subspaces to 𝐹, 𝐺, and 𝐻. (Contributed by NM, 1-Nov-2005.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ & ⊢ 𝐹 = (span‘{𝐴}) & ⊢ 𝐺 = (span‘{𝐵}) & ⊢ 𝐻 = (span‘{(𝐴 +ℎ 𝐵)}) ⇒ ⊢ (¬ (𝐴 ∈ 𝐺 ∨ 𝐵 ∈ 𝐹) → (𝐻 ∩ (𝐹 ∨ℋ 𝐺)) ≠ ((𝐻 ∩ 𝐹) ∨ℋ (𝐻 ∩ 𝐺))) | ||
Theorem | spansncvi 31169 | Hilbert space has the covering property (using spans of singletons to represent atoms). Exercise 5 of [Kalmbach] p. 153. (Contributed by NM, 7-Jun-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ ℋ ⇒ ⊢ ((𝐴 ⊊ 𝐵 ∧ 𝐵 ⊆ (𝐴 ∨ℋ (span‘{𝐶}))) → 𝐵 = (𝐴 ∨ℋ (span‘{𝐶}))) | ||
Theorem | spansncv 31170 | Hilbert space has the covering property (using spans of singletons to represent atoms). Exercise 5 of [Kalmbach] p. 153. (Contributed by NM, 9-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 ⊊ 𝐵 ∧ 𝐵 ⊆ (𝐴 ∨ℋ (span‘{𝐶}))) → 𝐵 = (𝐴 ∨ℋ (span‘{𝐶})))) | ||
Theorem | 5oalem1 31171 | Lemma for orthoarguesian law 5OA. (Contributed by NM, 1-Apr-2000.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ & ⊢ 𝐶 ∈ Sℋ & ⊢ 𝑅 ∈ Sℋ ⇒ ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ (𝑧 ∈ 𝐶 ∧ (𝑥 −ℎ 𝑧) ∈ 𝑅)) → 𝑣 ∈ (𝐵 +ℋ (𝐴 ∩ (𝐶 +ℋ 𝑅)))) | ||
Theorem | 5oalem2 31172 | Lemma for orthoarguesian law 5OA. (Contributed by NM, 2-Apr-2000.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ & ⊢ 𝐶 ∈ Sℋ & ⊢ 𝐷 ∈ Sℋ ⇒ ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷)) ∧ (𝑥 +ℎ 𝑦) = (𝑧 +ℎ 𝑤)) → (𝑥 −ℎ 𝑧) ∈ ((𝐴 +ℋ 𝐶) ∩ (𝐵 +ℋ 𝐷))) | ||
Theorem | 5oalem3 31173 | Lemma for orthoarguesian law 5OA. (Contributed by NM, 2-Apr-2000.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ & ⊢ 𝐶 ∈ Sℋ & ⊢ 𝐷 ∈ Sℋ & ⊢ 𝐹 ∈ Sℋ & ⊢ 𝐺 ∈ Sℋ ⇒ ⊢ (((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷)) ∧ (𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺)) ∧ ((𝑥 +ℎ 𝑦) = (𝑓 +ℎ 𝑔) ∧ (𝑧 +ℎ 𝑤) = (𝑓 +ℎ 𝑔))) → (𝑥 −ℎ 𝑧) ∈ (((𝐴 +ℋ 𝐹) ∩ (𝐵 +ℋ 𝐺)) +ℋ ((𝐶 +ℋ 𝐹) ∩ (𝐷 +ℋ 𝐺)))) | ||
Theorem | 5oalem4 31174 | Lemma for orthoarguesian law 5OA. (Contributed by NM, 2-Apr-2000.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ & ⊢ 𝐶 ∈ Sℋ & ⊢ 𝐷 ∈ Sℋ & ⊢ 𝐹 ∈ Sℋ & ⊢ 𝐺 ∈ Sℋ ⇒ ⊢ (((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷)) ∧ (𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺)) ∧ ((𝑥 +ℎ 𝑦) = (𝑓 +ℎ 𝑔) ∧ (𝑧 +ℎ 𝑤) = (𝑓 +ℎ 𝑔))) → (𝑥 −ℎ 𝑧) ∈ (((𝐴 +ℋ 𝐶) ∩ (𝐵 +ℋ 𝐷)) ∩ (((𝐴 +ℋ 𝐹) ∩ (𝐵 +ℋ 𝐺)) +ℋ ((𝐶 +ℋ 𝐹) ∩ (𝐷 +ℋ 𝐺))))) | ||
Theorem | 5oalem5 31175 | Lemma for orthoarguesian law 5OA. (Contributed by NM, 2-May-2000.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ & ⊢ 𝐶 ∈ Sℋ & ⊢ 𝐷 ∈ Sℋ & ⊢ 𝐹 ∈ Sℋ & ⊢ 𝐺 ∈ Sℋ & ⊢ 𝑅 ∈ Sℋ & ⊢ 𝑆 ∈ Sℋ ⇒ ⊢ (((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷)) ∧ ((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺) ∧ (𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆))) ∧ (((𝑥 +ℎ 𝑦) = (𝑣 +ℎ 𝑢) ∧ (𝑧 +ℎ 𝑤) = (𝑣 +ℎ 𝑢)) ∧ (𝑓 +ℎ 𝑔) = (𝑣 +ℎ 𝑢))) → (𝑥 −ℎ 𝑧) ∈ ((((𝐴 +ℋ 𝐶) ∩ (𝐵 +ℋ 𝐷)) ∩ (((𝐴 +ℋ 𝑅) ∩ (𝐵 +ℋ 𝑆)) +ℋ ((𝐶 +ℋ 𝑅) ∩ (𝐷 +ℋ 𝑆)))) ∩ ((((𝐴 +ℋ 𝐹) ∩ (𝐵 +ℋ 𝐺)) ∩ (((𝐴 +ℋ 𝑅) ∩ (𝐵 +ℋ 𝑆)) +ℋ ((𝐹 +ℋ 𝑅) ∩ (𝐺 +ℋ 𝑆)))) +ℋ (((𝐶 +ℋ 𝐹) ∩ (𝐷 +ℋ 𝐺)) ∩ (((𝐶 +ℋ 𝑅) ∩ (𝐷 +ℋ 𝑆)) +ℋ ((𝐹 +ℋ 𝑅) ∩ (𝐺 +ℋ 𝑆))))))) | ||
Theorem | 5oalem6 31176 | Lemma for orthoarguesian law 5OA. (Contributed by NM, 4-May-2000.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ & ⊢ 𝐶 ∈ Sℋ & ⊢ 𝐷 ∈ Sℋ & ⊢ 𝐹 ∈ Sℋ & ⊢ 𝐺 ∈ Sℋ & ⊢ 𝑅 ∈ Sℋ & ⊢ 𝑆 ∈ Sℋ ⇒ ⊢ (((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ ℎ = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐷) ∧ ℎ = (𝑧 +ℎ 𝑤))) ∧ (((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐺) ∧ ℎ = (𝑓 +ℎ 𝑔)) ∧ ((𝑣 ∈ 𝑅 ∧ 𝑢 ∈ 𝑆) ∧ ℎ = (𝑣 +ℎ 𝑢)))) → ℎ ∈ (𝐵 +ℋ (𝐴 ∩ (𝐶 +ℋ ((((𝐴 +ℋ 𝐶) ∩ (𝐵 +ℋ 𝐷)) ∩ (((𝐴 +ℋ 𝑅) ∩ (𝐵 +ℋ 𝑆)) +ℋ ((𝐶 +ℋ 𝑅) ∩ (𝐷 +ℋ 𝑆)))) ∩ ((((𝐴 +ℋ 𝐹) ∩ (𝐵 +ℋ 𝐺)) ∩ (((𝐴 +ℋ 𝑅) ∩ (𝐵 +ℋ 𝑆)) +ℋ ((𝐹 +ℋ 𝑅) ∩ (𝐺 +ℋ 𝑆)))) +ℋ (((𝐶 +ℋ 𝐹) ∩ (𝐷 +ℋ 𝐺)) ∩ (((𝐶 +ℋ 𝑅) ∩ (𝐷 +ℋ 𝑆)) +ℋ ((𝐹 +ℋ 𝑅) ∩ (𝐺 +ℋ 𝑆)))))))))) | ||
Theorem | 5oalem7 31177 | Lemma for orthoarguesian law 5OA. (Contributed by NM, 4-May-2000.) TODO: replace uses of ee4anv 2346 with 4exdistrv 1959 as in 3oalem3 31181. (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ & ⊢ 𝐶 ∈ Sℋ & ⊢ 𝐷 ∈ Sℋ & ⊢ 𝐹 ∈ Sℋ & ⊢ 𝐺 ∈ Sℋ & ⊢ 𝑅 ∈ Sℋ & ⊢ 𝑆 ∈ Sℋ ⇒ ⊢ (((𝐴 +ℋ 𝐵) ∩ (𝐶 +ℋ 𝐷)) ∩ ((𝐹 +ℋ 𝐺) ∩ (𝑅 +ℋ 𝑆))) ⊆ (𝐵 +ℋ (𝐴 ∩ (𝐶 +ℋ ((((𝐴 +ℋ 𝐶) ∩ (𝐵 +ℋ 𝐷)) ∩ (((𝐴 +ℋ 𝑅) ∩ (𝐵 +ℋ 𝑆)) +ℋ ((𝐶 +ℋ 𝑅) ∩ (𝐷 +ℋ 𝑆)))) ∩ ((((𝐴 +ℋ 𝐹) ∩ (𝐵 +ℋ 𝐺)) ∩ (((𝐴 +ℋ 𝑅) ∩ (𝐵 +ℋ 𝑆)) +ℋ ((𝐹 +ℋ 𝑅) ∩ (𝐺 +ℋ 𝑆)))) +ℋ (((𝐶 +ℋ 𝐹) ∩ (𝐷 +ℋ 𝐺)) ∩ (((𝐶 +ℋ 𝑅) ∩ (𝐷 +ℋ 𝑆)) +ℋ ((𝐹 +ℋ 𝑅) ∩ (𝐺 +ℋ 𝑆))))))))) | ||
Theorem | 5oai 31178 | Orthoarguesian law 5OA. This 8-variable inference is called 5OA because it can be converted to a 5-variable equation (see Quantum Logic Explorer). (Contributed by NM, 5-May-2000.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝐷 ∈ Cℋ & ⊢ 𝐹 ∈ Cℋ & ⊢ 𝐺 ∈ Cℋ & ⊢ 𝑅 ∈ Cℋ & ⊢ 𝑆 ∈ Cℋ & ⊢ 𝐴 ⊆ (⊥‘𝐵) & ⊢ 𝐶 ⊆ (⊥‘𝐷) & ⊢ 𝐹 ⊆ (⊥‘𝐺) & ⊢ 𝑅 ⊆ (⊥‘𝑆) ⇒ ⊢ (((𝐴 ∨ℋ 𝐵) ∩ (𝐶 ∨ℋ 𝐷)) ∩ ((𝐹 ∨ℋ 𝐺) ∩ (𝑅 ∨ℋ 𝑆))) ⊆ (𝐵 ∨ℋ (𝐴 ∩ (𝐶 ∨ℋ ((((𝐴 ∨ℋ 𝐶) ∩ (𝐵 ∨ℋ 𝐷)) ∩ (((𝐴 ∨ℋ 𝑅) ∩ (𝐵 ∨ℋ 𝑆)) ∨ℋ ((𝐶 ∨ℋ 𝑅) ∩ (𝐷 ∨ℋ 𝑆)))) ∩ ((((𝐴 ∨ℋ 𝐹) ∩ (𝐵 ∨ℋ 𝐺)) ∩ (((𝐴 ∨ℋ 𝑅) ∩ (𝐵 ∨ℋ 𝑆)) ∨ℋ ((𝐹 ∨ℋ 𝑅) ∩ (𝐺 ∨ℋ 𝑆)))) ∨ℋ (((𝐶 ∨ℋ 𝐹) ∩ (𝐷 ∨ℋ 𝐺)) ∩ (((𝐶 ∨ℋ 𝑅) ∩ (𝐷 ∨ℋ 𝑆)) ∨ℋ ((𝐹 ∨ℋ 𝑅) ∩ (𝐺 ∨ℋ 𝑆))))))))) | ||
Theorem | 3oalem1 31179* | Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝑅 ∈ Cℋ & ⊢ 𝑆 ∈ Cℋ ⇒ ⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → (((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) ∧ 𝑣 ∈ ℋ) ∧ (𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ))) | ||
Theorem | 3oalem2 31180* | Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝑅 ∈ Cℋ & ⊢ 𝑆 ∈ Cℋ ⇒ ⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝑅) ∧ 𝑣 = (𝑥 +ℎ 𝑦)) ∧ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝑆) ∧ 𝑣 = (𝑧 +ℎ 𝑤))) → 𝑣 ∈ (𝐵 +ℋ (𝑅 ∩ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆)))))) | ||
Theorem | 3oalem3 31181 | Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝑅 ∈ Cℋ & ⊢ 𝑆 ∈ Cℋ ⇒ ⊢ ((𝐵 +ℋ 𝑅) ∩ (𝐶 +ℋ 𝑆)) ⊆ (𝐵 +ℋ (𝑅 ∩ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆))))) | ||
Theorem | 3oalem4 31182 | Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
⊢ 𝑅 = ((⊥‘𝐵) ∩ (𝐵 ∨ℋ 𝐴)) ⇒ ⊢ 𝑅 ⊆ (⊥‘𝐵) | ||
Theorem | 3oalem5 31183 | Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝑅 = ((⊥‘𝐵) ∩ (𝐵 ∨ℋ 𝐴)) & ⊢ 𝑆 = ((⊥‘𝐶) ∩ (𝐶 ∨ℋ 𝐴)) ⇒ ⊢ ((𝐵 +ℋ 𝑅) ∩ (𝐶 +ℋ 𝑆)) = ((𝐵 ∨ℋ 𝑅) ∩ (𝐶 ∨ℋ 𝑆)) | ||
Theorem | 3oalem6 31184 | Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝑅 = ((⊥‘𝐵) ∩ (𝐵 ∨ℋ 𝐴)) & ⊢ 𝑆 = ((⊥‘𝐶) ∩ (𝐶 ∨ℋ 𝐴)) ⇒ ⊢ (𝐵 +ℋ (𝑅 ∩ (𝑆 +ℋ ((𝐵 +ℋ 𝐶) ∩ (𝑅 +ℋ 𝑆))))) ⊆ (𝐵 ∨ℋ (𝑅 ∩ (𝑆 ∨ℋ ((𝐵 ∨ℋ 𝐶) ∩ (𝑅 ∨ℋ 𝑆))))) | ||
Theorem | 3oai 31185 | 3OA (weak) orthoarguesian law. Equation IV of [GodowskiGreechie] p. 249. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝑅 = ((⊥‘𝐵) ∩ (𝐵 ∨ℋ 𝐴)) & ⊢ 𝑆 = ((⊥‘𝐶) ∩ (𝐶 ∨ℋ 𝐴)) ⇒ ⊢ ((𝐵 ∨ℋ 𝑅) ∩ (𝐶 ∨ℋ 𝑆)) ⊆ (𝐵 ∨ℋ (𝑅 ∩ (𝑆 ∨ℋ ((𝐵 ∨ℋ 𝐶) ∩ (𝑅 ∨ℋ 𝑆))))) | ||
Theorem | pjorthi 31186 | Projection components on orthocomplemented subspaces are orthogonal. (Contributed by NM, 26-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (𝐻 ∈ Cℋ → (((projℎ‘𝐻)‘𝐴) ·ih ((projℎ‘(⊥‘𝐻))‘𝐵)) = 0) | ||
Theorem | pjch1 31187 | Property of identity projection. Remark in [Beran] p. 111. (Contributed by NM, 28-Oct-1999.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → ((projℎ‘ ℋ)‘𝐴) = 𝐴) | ||
Theorem | pjo 31188 | The orthogonal projection. Lemma 4.4(i) of [Beran] p. 111. (Contributed by NM, 30-Oct-1999.) (New usage is discouraged.) |
⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → ((projℎ‘(⊥‘𝐻))‘𝐴) = (((projℎ‘ ℋ)‘𝐴) −ℎ ((projℎ‘𝐻)‘𝐴))) | ||
Theorem | pjcompi 31189 | Component of a projection. (Contributed by NM, 31-Oct-1999.) (Revised by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Cℋ ⇒ ⊢ ((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ (⊥‘𝐻)) → ((projℎ‘𝐻)‘(𝐴 +ℎ 𝐵)) = 𝐴) | ||
Theorem | pjidmi 31190 | A projection is idempotent. Property (ii) of [Beran] p. 109. (Contributed by NM, 28-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ ⇒ ⊢ ((projℎ‘𝐻)‘((projℎ‘𝐻)‘𝐴)) = ((projℎ‘𝐻)‘𝐴) | ||
Theorem | pjadjii 31191 | A projection is self-adjoint. Property (i) of [Beran] p. 109. (Contributed by NM, 30-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (((projℎ‘𝐻)‘𝐴) ·ih 𝐵) = (𝐴 ·ih ((projℎ‘𝐻)‘𝐵)) | ||
Theorem | pjaddii 31192 | Projection of vector sum is sum of projections. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ ((projℎ‘𝐻)‘(𝐴 +ℎ 𝐵)) = (((projℎ‘𝐻)‘𝐴) +ℎ ((projℎ‘𝐻)‘𝐵)) | ||
Theorem | pjinormii 31193 | The inner product of a projection and its argument is the square of the norm of the projection. Remark in [Halmos] p. 44. (Contributed by NM, 13-Aug-2000.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ ⇒ ⊢ (((projℎ‘𝐻)‘𝐴) ·ih 𝐴) = ((normℎ‘((projℎ‘𝐻)‘𝐴))↑2) | ||
Theorem | pjmulii 31194 | Projection of (scalar) product is product of projection. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ & ⊢ 𝐶 ∈ ℂ ⇒ ⊢ ((projℎ‘𝐻)‘(𝐶 ·ℎ 𝐴)) = (𝐶 ·ℎ ((projℎ‘𝐻)‘𝐴)) | ||
Theorem | pjsubii 31195 | Projection of vector difference is difference of projections. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ ((projℎ‘𝐻)‘(𝐴 −ℎ 𝐵)) = (((projℎ‘𝐻)‘𝐴) −ℎ ((projℎ‘𝐻)‘𝐵)) | ||
Theorem | pjsslem 31196 | Lemma for subset relationships of projections. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ & ⊢ 𝐺 ∈ Cℋ ⇒ ⊢ (((projℎ‘(⊥‘𝐻))‘𝐴) −ℎ ((projℎ‘(⊥‘𝐺))‘𝐴)) = (((projℎ‘𝐺)‘𝐴) −ℎ ((projℎ‘𝐻)‘𝐴)) | ||
Theorem | pjss2i 31197 | Subset relationship for projections. Theorem 4.5(i)->(ii) of [Beran] p. 112. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ & ⊢ 𝐺 ∈ Cℋ ⇒ ⊢ (𝐻 ⊆ 𝐺 → ((projℎ‘𝐻)‘((projℎ‘𝐺)‘𝐴)) = ((projℎ‘𝐻)‘𝐴)) | ||
Theorem | pjssmii 31198 | Projection meet property. Remark in [Kalmbach] p. 66. Also Theorem 4.5(i)->(iv) of [Beran] p. 112. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ & ⊢ 𝐺 ∈ Cℋ ⇒ ⊢ (𝐻 ⊆ 𝐺 → (((projℎ‘𝐺)‘𝐴) −ℎ ((projℎ‘𝐻)‘𝐴)) = ((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘𝐴)) | ||
Theorem | pjssge0ii 31199 | Theorem 4.5(iv)->(v) of [Beran] p. 112. (Contributed by NM, 13-Aug-2000.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ & ⊢ 𝐺 ∈ Cℋ ⇒ ⊢ ((((projℎ‘𝐺)‘𝐴) −ℎ ((projℎ‘𝐻)‘𝐴)) = ((projℎ‘(𝐺 ∩ (⊥‘𝐻)))‘𝐴) → 0 ≤ ((((projℎ‘𝐺)‘𝐴) −ℎ ((projℎ‘𝐻)‘𝐴)) ·ih 𝐴)) | ||
Theorem | pjdifnormii 31200 | Theorem 4.5(v)<->(vi) of [Beran] p. 112. (Contributed by NM, 13-Aug-2000.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ & ⊢ 𝐺 ∈ Cℋ ⇒ ⊢ (0 ≤ ((((projℎ‘𝐺)‘𝐴) −ℎ ((projℎ‘𝐻)‘𝐴)) ·ih 𝐴) ↔ (normℎ‘((projℎ‘𝐻)‘𝐴)) ≤ (normℎ‘((projℎ‘𝐺)‘𝐴))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |