![]() |
Metamath
Proof Explorer Theorem List (p. 324 of 491) | < 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-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | goeqi 32301 | 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.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝐹 = ((⊥‘𝐴) ∨ℋ (𝐴 ∩ 𝐵)) & ⊢ 𝐺 = ((⊥‘𝐵) ∨ℋ (𝐵 ∩ 𝐶)) & ⊢ 𝐻 = ((⊥‘𝐶) ∨ℋ (𝐶 ∩ 𝐴)) & ⊢ 𝐷 = ((⊥‘𝐵) ∨ℋ (𝐵 ∩ 𝐴)) ⇒ ⊢ ((𝐹 ∩ 𝐺) ∩ 𝐻) ⊆ 𝐷 | ||
Theorem | stcltr1i 32302* | Property of a strong classical state. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
⊢ (𝜑 ↔ (𝑆 ∈ States ∧ ∀𝑥 ∈ Cℋ ∀𝑦 ∈ Cℋ (((𝑆‘𝑥) = 1 → (𝑆‘𝑦) = 1) → 𝑥 ⊆ 𝑦))) & ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝜑 → (((𝑆‘𝐴) = 1 → (𝑆‘𝐵) = 1) → 𝐴 ⊆ 𝐵)) | ||
Theorem | stcltr2i 32303* | Property of a strong classical state. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
⊢ (𝜑 ↔ (𝑆 ∈ States ∧ ∀𝑥 ∈ Cℋ ∀𝑦 ∈ Cℋ (((𝑆‘𝑥) = 1 → (𝑆‘𝑦) = 1) → 𝑥 ⊆ 𝑦))) & ⊢ 𝐴 ∈ Cℋ ⇒ ⊢ (𝜑 → ((𝑆‘𝐴) = 1 → 𝐴 = ℋ)) | ||
Theorem | stcltrlem1 32304* | Lemma for strong classical state theorem. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
⊢ (𝜑 ↔ (𝑆 ∈ States ∧ ∀𝑥 ∈ Cℋ ∀𝑦 ∈ Cℋ (((𝑆‘𝑥) = 1 → (𝑆‘𝑦) = 1) → 𝑥 ⊆ 𝑦))) & ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝜑 → ((𝑆‘𝐵) = 1 → (𝑆‘((⊥‘𝐴) ∨ℋ (𝐴 ∩ 𝐵))) = 1)) | ||
Theorem | stcltrlem2 32305* | Lemma for strong classical state theorem. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
⊢ (𝜑 ↔ (𝑆 ∈ States ∧ ∀𝑥 ∈ Cℋ ∀𝑦 ∈ Cℋ (((𝑆‘𝑥) = 1 → (𝑆‘𝑦) = 1) → 𝑥 ⊆ 𝑦))) & ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝜑 → 𝐵 ⊆ ((⊥‘𝐴) ∨ℋ (𝐴 ∩ 𝐵))) | ||
Theorem | stcltrthi 32306* | Theorem for classically strong set of states. If there exists a "classically strong set of states" on lattice Cℋ (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.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ ∃𝑠 ∈ States ∀𝑥 ∈ Cℋ ∀𝑦 ∈ Cℋ (((𝑠‘𝑥) = 1 → (𝑠‘𝑦) = 1) → 𝑥 ⊆ 𝑦) ⇒ ⊢ 𝐵 ⊆ ((⊥‘𝐴) ∨ℋ (𝐴 ∩ 𝐵)) | ||
Definition | df-cv 32307* | 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 32310 and cvbr2 32311 for membership relations. (Contributed by NM, 4-Jun-2004.) (New usage is discouraged.) |
⊢ ⋖ℋ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ (𝑥 ⊊ 𝑦 ∧ ¬ ∃𝑧 ∈ Cℋ (𝑥 ⊊ 𝑧 ∧ 𝑧 ⊊ 𝑦)))} | ||
Definition | df-md 32308* | 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 32322 for membership relation. (Contributed by NM, 14-Jun-2004.) (New usage is discouraged.) |
⊢ 𝑀ℋ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ ∀𝑧 ∈ Cℋ (𝑧 ⊆ 𝑦 → ((𝑧 ∨ℋ 𝑥) ∩ 𝑦) = (𝑧 ∨ℋ (𝑥 ∩ 𝑦))))} | ||
Definition | df-dmd 32309* | 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 32327 for membership relation. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.) |
⊢ 𝑀ℋ* = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ ∀𝑧 ∈ Cℋ (𝑦 ⊆ 𝑧 → ((𝑧 ∩ 𝑥) ∨ℋ 𝑦) = (𝑧 ∩ (𝑥 ∨ℋ 𝑦))))} | ||
Theorem | cvbr 32310* | 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.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ⋖ℋ 𝐵 ↔ (𝐴 ⊊ 𝐵 ∧ ¬ ∃𝑥 ∈ Cℋ (𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝐵)))) | ||
Theorem | cvbr2 32311* | Binary relation expressing 𝐵 covers 𝐴. Definition of covers in [Kalmbach] p. 15. (Contributed by NM, 9-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ⋖ℋ 𝐵 ↔ (𝐴 ⊊ 𝐵 ∧ ∀𝑥 ∈ Cℋ ((𝐴 ⊊ 𝑥 ∧ 𝑥 ⊆ 𝐵) → 𝑥 = 𝐵)))) | ||
Theorem | cvcon3 32312 | Contraposition law for the covers relation. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ⋖ℋ 𝐵 ↔ (⊥‘𝐵) ⋖ℋ (⊥‘𝐴))) | ||
Theorem | cvpss 32313 | The covers relation implies proper subset. (Contributed by NM, 10-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ⋖ℋ 𝐵 → 𝐴 ⊊ 𝐵)) | ||
Theorem | cvnbtwn 32314 | The covers relation implies no in-betweenness. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → (𝐴 ⋖ℋ 𝐵 → ¬ (𝐴 ⊊ 𝐶 ∧ 𝐶 ⊊ 𝐵))) | ||
Theorem | cvnbtwn2 32315 | The covers relation implies no in-betweenness. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → (𝐴 ⋖ℋ 𝐵 → ((𝐴 ⊊ 𝐶 ∧ 𝐶 ⊆ 𝐵) → 𝐶 = 𝐵))) | ||
Theorem | cvnbtwn3 32316 | The covers relation implies no in-betweenness. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → (𝐴 ⋖ℋ 𝐵 → ((𝐴 ⊆ 𝐶 ∧ 𝐶 ⊊ 𝐵) → 𝐶 = 𝐴))) | ||
Theorem | cvnbtwn4 32317 | 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.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → (𝐴 ⋖ℋ 𝐵 → ((𝐴 ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵) → (𝐶 = 𝐴 ∨ 𝐶 = 𝐵)))) | ||
Theorem | cvnsym 32318 | The covers relation is not symmetric. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ⋖ℋ 𝐵 → ¬ 𝐵 ⋖ℋ 𝐴)) | ||
Theorem | cvnref 32319 | The covers relation is not reflexive. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.) |
⊢ (𝐴 ∈ Cℋ → ¬ 𝐴 ⋖ℋ 𝐴) | ||
Theorem | cvntr 32320 | The covers relation is not transitive. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ((𝐴 ⋖ℋ 𝐵 ∧ 𝐵 ⋖ℋ 𝐶) → ¬ 𝐴 ⋖ℋ 𝐶)) | ||
Theorem | spansncv2 32321 | 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.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ ℋ) → (¬ (span‘{𝐵}) ⊆ 𝐴 → 𝐴 ⋖ℋ (𝐴 ∨ℋ (span‘{𝐵})))) | ||
Theorem | mdbr 32322* | Binary relation expressing 〈𝐴, 𝐵〉 is a modular pair. Definition 1.1 of [MaedaMaeda] p. 1. (Contributed by NM, 14-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝑀ℋ 𝐵 ↔ ∀𝑥 ∈ Cℋ (𝑥 ⊆ 𝐵 → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) = (𝑥 ∨ℋ (𝐴 ∩ 𝐵))))) | ||
Theorem | mdi 32323 | Consequence of the modular pair property. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.) |
⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ (𝐴 𝑀ℋ 𝐵 ∧ 𝐶 ⊆ 𝐵)) → ((𝐶 ∨ℋ 𝐴) ∩ 𝐵) = (𝐶 ∨ℋ (𝐴 ∩ 𝐵))) | ||
Theorem | mdbr2 32324* | Binary relation expressing the modular pair property. This version has a weaker constraint than mdbr 32322. (Contributed by NM, 15-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝑀ℋ 𝐵 ↔ ∀𝑥 ∈ Cℋ (𝑥 ⊆ 𝐵 → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) ⊆ (𝑥 ∨ℋ (𝐴 ∩ 𝐵))))) | ||
Theorem | mdbr3 32325* | 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.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝑀ℋ 𝐵 ↔ ∀𝑥 ∈ Cℋ (((𝑥 ∩ 𝐵) ∨ℋ 𝐴) ∩ 𝐵) = ((𝑥 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐵)))) | ||
Theorem | mdbr4 32326* | 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.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝑀ℋ 𝐵 ↔ ∀𝑥 ∈ Cℋ (((𝑥 ∩ 𝐵) ∨ℋ 𝐴) ∩ 𝐵) ⊆ ((𝑥 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐵)))) | ||
Theorem | dmdbr 32327* | Binary relation expressing the dual modular pair property. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝑀ℋ* 𝐵 ↔ ∀𝑥 ∈ Cℋ (𝐵 ⊆ 𝑥 → ((𝑥 ∩ 𝐴) ∨ℋ 𝐵) = (𝑥 ∩ (𝐴 ∨ℋ 𝐵))))) | ||
Theorem | dmdmd 32328 | 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.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝑀ℋ* 𝐵 ↔ (⊥‘𝐴) 𝑀ℋ (⊥‘𝐵))) | ||
Theorem | mddmd 32329 | The modular pair property expressed in terms of the dual modular pair property. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝑀ℋ 𝐵 ↔ (⊥‘𝐴) 𝑀ℋ* (⊥‘𝐵))) | ||
Theorem | dmdi 32330 | Consequence of the dual modular pair property. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.) |
⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ (𝐴 𝑀ℋ* 𝐵 ∧ 𝐵 ⊆ 𝐶)) → ((𝐶 ∩ 𝐴) ∨ℋ 𝐵) = (𝐶 ∩ (𝐴 ∨ℋ 𝐵))) | ||
Theorem | dmdbr2 32331* | Binary relation expressing the dual modular pair property. This version has a weaker constraint than dmdbr 32327. (Contributed by NM, 30-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝑀ℋ* 𝐵 ↔ ∀𝑥 ∈ Cℋ (𝐵 ⊆ 𝑥 → (𝑥 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ ((𝑥 ∩ 𝐴) ∨ℋ 𝐵)))) | ||
Theorem | dmdi2 32332 | Consequence of the dual modular pair property. (Contributed by NM, 14-Jan-2005.) (New usage is discouraged.) |
⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ (𝐴 𝑀ℋ* 𝐵 ∧ 𝐵 ⊆ 𝐶)) → (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ ((𝐶 ∩ 𝐴) ∨ℋ 𝐵)) | ||
Theorem | dmdbr3 32333* | 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.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝑀ℋ* 𝐵 ↔ ∀𝑥 ∈ Cℋ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵) = ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)))) | ||
Theorem | dmdbr4 32334* | 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.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝑀ℋ* 𝐵 ↔ ∀𝑥 ∈ Cℋ ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))) | ||
Theorem | dmdi4 32335 | Consequence of the dual modular pair property. (Contributed by NM, 14-Jan-2005.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → (𝐴 𝑀ℋ* 𝐵 → ((𝐶 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝐶 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))) | ||
Theorem | dmdbr5 32336* | Binary relation expressing the dual modular pair property. (Contributed by NM, 15-Jan-2005.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝑀ℋ* 𝐵 ↔ ∀𝑥 ∈ Cℋ (𝑥 ⊆ (𝐴 ∨ℋ 𝐵) → 𝑥 ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)))) | ||
Theorem | mddmd2 32337* | 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.) |
⊢ (𝐴 ∈ Cℋ → (∀𝑥 ∈ Cℋ 𝐴 𝑀ℋ 𝑥 ↔ ∀𝑥 ∈ Cℋ 𝐴 𝑀ℋ* 𝑥)) | ||
Theorem | mdsl0 32338 | 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.) |
⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ (𝐶 ∈ Cℋ ∧ 𝐷 ∈ Cℋ )) → ((((𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐵) ∧ (𝐴 ∩ 𝐵) = 0ℋ) ∧ 𝐴 𝑀ℋ 𝐵) → 𝐶 𝑀ℋ 𝐷)) | ||
Theorem | ssmd1 32339 | Ordering implies the modular pair property. Remark in [MaedaMaeda] p. 1. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐴 ⊆ 𝐵) → 𝐴 𝑀ℋ 𝐵) | ||
Theorem | ssmd2 32340 | Ordering implies the modular pair property. Remark in [MaedaMaeda] p. 1. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐴 ⊆ 𝐵) → 𝐵 𝑀ℋ 𝐴) | ||
Theorem | ssdmd1 32341 | Ordering implies the dual modular pair property. Remark in [MaedaMaeda] p. 1. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐴 ⊆ 𝐵) → 𝐴 𝑀ℋ* 𝐵) | ||
Theorem | ssdmd2 32342 | Ordering implies the dual modular pair property. Remark in [MaedaMaeda] p. 1. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐴 ⊆ 𝐵) → (⊥‘𝐵) 𝑀ℋ (⊥‘𝐴)) | ||
Theorem | dmdsl3 32343 | 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.) |
⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ (𝐵 𝑀ℋ* 𝐴 ∧ 𝐴 ⊆ 𝐶 ∧ 𝐶 ⊆ (𝐴 ∨ℋ 𝐵))) → ((𝐶 ∩ 𝐵) ∨ℋ 𝐴) = 𝐶) | ||
Theorem | mdsl3 32344 | 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.) |
⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ (𝐴 𝑀ℋ 𝐵 ∧ (𝐴 ∩ 𝐵) ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐵)) → ((𝐶 ∨ℋ 𝐴) ∩ 𝐵) = 𝐶) | ||
Theorem | mdslle1i 32345 | 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.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝐷 ∈ Cℋ ⇒ ⊢ ((𝐵 𝑀ℋ* 𝐴 ∧ 𝐴 ⊆ (𝐶 ∩ 𝐷) ∧ (𝐶 ∨ℋ 𝐷) ⊆ (𝐴 ∨ℋ 𝐵)) → (𝐶 ⊆ 𝐷 ↔ (𝐶 ∩ 𝐵) ⊆ (𝐷 ∩ 𝐵))) | ||
Theorem | mdslle2i 32346 | 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.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝐷 ∈ Cℋ ⇒ ⊢ ((𝐴 𝑀ℋ 𝐵 ∧ (𝐴 ∩ 𝐵) ⊆ (𝐶 ∩ 𝐷) ∧ (𝐶 ∨ℋ 𝐷) ⊆ 𝐵) → (𝐶 ⊆ 𝐷 ↔ (𝐶 ∨ℋ 𝐴) ⊆ (𝐷 ∨ℋ 𝐴))) | ||
Theorem | mdslj1i 32347 | 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.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝐷 ∈ Cℋ ⇒ ⊢ (((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ (𝐴 ⊆ (𝐶 ∩ 𝐷) ∧ (𝐶 ∨ℋ 𝐷) ⊆ (𝐴 ∨ℋ 𝐵))) → ((𝐶 ∨ℋ 𝐷) ∩ 𝐵) = ((𝐶 ∩ 𝐵) ∨ℋ (𝐷 ∩ 𝐵))) | ||
Theorem | mdslj2i 32348 | 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.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝐷 ∈ Cℋ ⇒ ⊢ (((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ∩ 𝐵) ⊆ (𝐶 ∩ 𝐷) ∧ (𝐶 ∨ℋ 𝐷) ⊆ 𝐵)) → ((𝐶 ∩ 𝐷) ∨ℋ 𝐴) = ((𝐶 ∨ℋ 𝐴) ∩ (𝐷 ∨ℋ 𝐴))) | ||
Theorem | mdsl1i 32349* | 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.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (∀𝑥 ∈ Cℋ (((𝐴 ∩ 𝐵) ⊆ 𝑥 ∧ 𝑥 ⊆ (𝐴 ∨ℋ 𝐵)) → (𝑥 ⊆ 𝐵 → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) = (𝑥 ∨ℋ (𝐴 ∩ 𝐵)))) ↔ 𝐴 𝑀ℋ 𝐵) | ||
Theorem | mdsl2i 32350* | 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.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 𝑀ℋ 𝐵 ↔ ∀𝑥 ∈ Cℋ (((𝐴 ∩ 𝐵) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐵) → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) ⊆ (𝑥 ∨ℋ (𝐴 ∩ 𝐵)))) | ||
Theorem | mdsl2bi 32351* | 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.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 𝑀ℋ 𝐵 ↔ ∀𝑥 ∈ Cℋ (((𝐴 ∩ 𝐵) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐵) → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) = (𝑥 ∨ℋ (𝐴 ∩ 𝐵)))) | ||
Theorem | cvmdi 32352 | 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.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ ((𝐴 ∩ 𝐵) ⋖ℋ 𝐵 → 𝐴 𝑀ℋ 𝐵) | ||
Theorem | mdslmd1lem1 32353 | Lemma for mdslmd1i 32357. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝐷 ∈ Cℋ & ⊢ 𝑅 ∈ Cℋ ⇒ ⊢ (((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) → (((𝑅 ∨ℋ 𝐴) ⊆ 𝐷 → (((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷) ⊆ ((𝑅 ∨ℋ 𝐴) ∨ℋ (𝐶 ∩ 𝐷))) → ((((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵)) → ((𝑅 ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ (𝑅 ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)))))) | ||
Theorem | mdslmd1lem2 32354 | Lemma for mdslmd1i 32357. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝐷 ∈ Cℋ & ⊢ 𝑅 ∈ Cℋ ⇒ ⊢ (((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) → (((𝑅 ∩ 𝐵) ⊆ (𝐷 ∩ 𝐵) → (((𝑅 ∩ 𝐵) ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ ((𝑅 ∩ 𝐵) ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)))) → (((𝐶 ∩ 𝐷) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷) → ((𝑅 ∨ℋ 𝐶) ∩ 𝐷) ⊆ (𝑅 ∨ℋ (𝐶 ∩ 𝐷))))) | ||
Theorem | mdslmd1lem3 32355* | Lemma for mdslmd1i 32357. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝐷 ∈ Cℋ ⇒ ⊢ ((𝑥 ∈ Cℋ ∧ ((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))))) → (((𝑥 ∨ℋ 𝐴) ⊆ 𝐷 → (((𝑥 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷) ⊆ ((𝑥 ∨ℋ 𝐴) ∨ℋ (𝐶 ∩ 𝐷))) → ((((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑥 ∧ 𝑥 ⊆ (𝐷 ∩ 𝐵)) → ((𝑥 ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ (𝑥 ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)))))) | ||
Theorem | mdslmd1lem4 32356* | Lemma for mdslmd1i 32357. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝐷 ∈ Cℋ ⇒ ⊢ ((𝑥 ∈ Cℋ ∧ ((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))))) → (((𝑥 ∩ 𝐵) ⊆ (𝐷 ∩ 𝐵) → (((𝑥 ∩ 𝐵) ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ ((𝑥 ∩ 𝐵) ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)))) → (((𝐶 ∩ 𝐷) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐷) → ((𝑥 ∨ℋ 𝐶) ∩ 𝐷) ⊆ (𝑥 ∨ℋ (𝐶 ∩ 𝐷))))) | ||
Theorem | mdslmd1i 32357 | 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.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝐷 ∈ Cℋ ⇒ ⊢ (((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ (𝐴 ⊆ (𝐶 ∩ 𝐷) ∧ (𝐶 ∨ℋ 𝐷) ⊆ (𝐴 ∨ℋ 𝐵))) → (𝐶 𝑀ℋ 𝐷 ↔ (𝐶 ∩ 𝐵) 𝑀ℋ (𝐷 ∩ 𝐵))) | ||
Theorem | mdslmd2i 32358 | 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.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝐷 ∈ Cℋ ⇒ ⊢ (((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ∩ 𝐵) ⊆ (𝐶 ∩ 𝐷) ∧ (𝐶 ∨ℋ 𝐷) ⊆ 𝐵)) → (𝐶 𝑀ℋ 𝐷 ↔ (𝐶 ∨ℋ 𝐴) 𝑀ℋ (𝐷 ∨ℋ 𝐴))) | ||
Theorem | mdsldmd1i 32359 | 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.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝐷 ∈ Cℋ ⇒ ⊢ (((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ (𝐴 ⊆ (𝐶 ∩ 𝐷) ∧ (𝐶 ∨ℋ 𝐷) ⊆ (𝐴 ∨ℋ 𝐵))) → (𝐶 𝑀ℋ* 𝐷 ↔ (𝐶 ∩ 𝐵) 𝑀ℋ* (𝐷 ∩ 𝐵))) | ||
Theorem | mdslmd3i 32360 | 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.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝐷 ∈ Cℋ ⇒ ⊢ (((𝐴 𝑀ℋ 𝐵 ∧ (𝐴 ∩ 𝐵) 𝑀ℋ 𝐶) ∧ ((𝐴 ∩ 𝐶) ⊆ 𝐷 ∧ 𝐷 ⊆ 𝐴)) → 𝐷 𝑀ℋ (𝐵 ∩ 𝐶)) | ||
Theorem | mdslmd4i 32361 | 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.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝐷 ∈ Cℋ ⇒ ⊢ ((𝐴 𝑀ℋ 𝐵 ∧ ((𝐴 ∩ 𝐵) ⊆ 𝐶 ∧ 𝐶 ⊆ 𝐴) ∧ ((𝐴 ∩ 𝐵) ⊆ 𝐷 ∧ 𝐷 ⊆ 𝐵)) → 𝐶 𝑀ℋ 𝐷) | ||
Theorem | csmdsymi 32362* | Cross-symmetry implies M-symmetry. Theorem 1.9.1 of [MaedaMaeda] p. 3. (Contributed by NM, 24-Dec-2006.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ ((∀𝑐 ∈ Cℋ (𝑐 𝑀ℋ 𝐵 → 𝐵 𝑀ℋ* 𝑐) ∧ 𝐴 𝑀ℋ 𝐵) → 𝐵 𝑀ℋ 𝐴) | ||
Theorem | mdexchi 32363 | An exchange lemma for modular pairs. Lemma 1.6 of [MaedaMaeda] p. 2. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ ⇒ ⊢ ((𝐴 𝑀ℋ 𝐵 ∧ 𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴) → ((𝐶 ∨ℋ 𝐴) 𝑀ℋ 𝐵 ∧ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵) = (𝐴 ∩ 𝐵))) | ||
Theorem | cvmd 32364 | 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.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ (𝐴 ∩ 𝐵) ⋖ℋ 𝐵) → 𝐴 𝑀ℋ 𝐵) | ||
Theorem | cvdmd 32365 | 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.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐵 ⋖ℋ (𝐴 ∨ℋ 𝐵)) → 𝐴 𝑀ℋ* 𝐵) | ||
Definition | df-at 32366 | 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 32367 and elat2 32368 for membership relations. (Contributed by NM, 14-Aug-2002.) (New usage is discouraged.) |
⊢ HAtoms = {𝑥 ∈ Cℋ ∣ 0ℋ ⋖ℋ 𝑥} | ||
Theorem | ela 32367 | 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 ↔ (𝐴 ∈ Cℋ ∧ 0ℋ ⋖ℋ 𝐴)) | ||
Theorem | elat2 32368* | 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 ↔ (𝐴 ∈ Cℋ ∧ (𝐴 ≠ 0ℋ ∧ ∀𝑥 ∈ Cℋ (𝑥 ⊆ 𝐴 → (𝑥 = 𝐴 ∨ 𝑥 = 0ℋ))))) | ||
Theorem | elatcv0 32369 | A Hilbert lattice element is an atom iff it covers the zero subspace. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.) |
⊢ (𝐴 ∈ Cℋ → (𝐴 ∈ HAtoms ↔ 0ℋ ⋖ℋ 𝐴)) | ||
Theorem | atcv0 32370 | An atom covers the zero subspace. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.) |
⊢ (𝐴 ∈ HAtoms → 0ℋ ⋖ℋ 𝐴) | ||
Theorem | atssch 32371 | Atoms are a subset of the Hilbert lattice. (Contributed by NM, 14-Aug-2002.) (New usage is discouraged.) |
⊢ HAtoms ⊆ Cℋ | ||
Theorem | atelch 32372 | An atom is a Hilbert lattice element. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.) |
⊢ (𝐴 ∈ HAtoms → 𝐴 ∈ Cℋ ) | ||
Theorem | atne0 32373 | An atom is not the Hilbert lattice zero. (Contributed by NM, 13-Aug-2002.) (New usage is discouraged.) |
⊢ (𝐴 ∈ HAtoms → 𝐴 ≠ 0ℋ) | ||
Theorem | atss 32374 | A lattice element smaller than an atom is either the atom or zero. (Contributed by NM, 25-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms) → (𝐴 ⊆ 𝐵 → (𝐴 = 𝐵 ∨ 𝐴 = 0ℋ))) | ||
Theorem | atsseq 32375 | Two atoms in a subset relationship are equal. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ HAtoms ∧ 𝐵 ∈ HAtoms) → (𝐴 ⊆ 𝐵 ↔ 𝐴 = 𝐵)) | ||
Theorem | atcveq0 32376 | A Hilbert lattice element covered by an atom must be the zero subspace. (Contributed by NM, 11-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms) → (𝐴 ⋖ℋ 𝐵 ↔ 𝐴 = 0ℋ)) | ||
Theorem | h1da 32377 | A 1-dimensional subspace is an atom. (Contributed by NM, 22-Jul-2001.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ) → (⊥‘(⊥‘{𝐴})) ∈ HAtoms) | ||
Theorem | spansna 32378 | The span of the singleton of a vector is an atom. (Contributed by NM, 18-Dec-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ) → (span‘{𝐴}) ∈ HAtoms) | ||
Theorem | sh1dle 32379 | A 1-dimensional subspace is less than or equal to any subspace containing its generating vector. (Contributed by NM, 24-Nov-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ 𝐴) → (⊥‘(⊥‘{𝐵})) ⊆ 𝐴) | ||
Theorem | ch1dle 32380 | A 1-dimensional subspace is less than or equal to any member of Cℋ containing its generating vector. (Contributed by NM, 30-May-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ 𝐴) → (⊥‘(⊥‘{𝐵})) ⊆ 𝐴) | ||
Theorem | atom1d 32381* | The 1-dimensional subspaces of Hilbert space are its atoms. Part of Remark 10.3.5 of [BeltramettiCassinelli] p. 107. (Contributed by NM, 4-Jun-2004.) (New usage is discouraged.) |
⊢ (𝐴 ∈ HAtoms ↔ ∃𝑥 ∈ ℋ (𝑥 ≠ 0ℎ ∧ 𝐴 = (span‘{𝑥}))) | ||
Theorem | superpos 32382* | Superposition Principle. If 𝐴 and 𝐵 are distinct atoms, there exists a third atom, distinct from 𝐴 and 𝐵, that is the superposition of 𝐴 and 𝐵. Definition 3.4-3(a) in [MegPav2000] p. 2345 (PDF p. 8). (Contributed by NM, 9-Jun-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ HAtoms ∧ 𝐵 ∈ HAtoms ∧ 𝐴 ≠ 𝐵) → ∃𝑥 ∈ HAtoms (𝑥 ≠ 𝐴 ∧ 𝑥 ≠ 𝐵 ∧ 𝑥 ⊆ (𝐴 ∨ℋ 𝐵))) | ||
Theorem | chcv1 32383 | The Hilbert lattice has the covering property. Proposition 1(ii) of [Kalmbach] p. 140 (and its converse). (Contributed by NM, 11-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms) → (¬ 𝐵 ⊆ 𝐴 ↔ 𝐴 ⋖ℋ (𝐴 ∨ℋ 𝐵))) | ||
Theorem | chcv2 32384 | The Hilbert lattice has the covering property. (Contributed by NM, 11-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms) → (𝐴 ⊊ (𝐴 ∨ℋ 𝐵) ↔ 𝐴 ⋖ℋ (𝐴 ∨ℋ 𝐵))) | ||
Theorem | chjatom 32385 | The join of a closed subspace and an atom equals their subspace sum. Special case of remark in [Kalmbach] p. 65, stating that if 𝐴 or 𝐵 is finite-dimensional, then this equality holds. (Contributed by NM, 4-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms) → (𝐴 +ℋ 𝐵) = (𝐴 ∨ℋ 𝐵)) | ||
Theorem | shatomici 32386* | The lattice of Hilbert subspaces is atomic, i.e. any nonzero element is greater than or equal to some atom. Part of proof of Theorem 16.9 of [MaedaMaeda] p. 70. (Contributed by NM, 24-Nov-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ ⇒ ⊢ (𝐴 ≠ 0ℋ → ∃𝑥 ∈ HAtoms 𝑥 ⊆ 𝐴) | ||
Theorem | hatomici 32387* | The Hilbert lattice is atomic, i.e. any nonzero element is greater than or equal to some atom. Remark in [Kalmbach] p. 140. (Contributed by NM, 22-Jul-2001.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ ⇒ ⊢ (𝐴 ≠ 0ℋ → ∃𝑥 ∈ HAtoms 𝑥 ⊆ 𝐴) | ||
Theorem | hatomic 32388* | A Hilbert lattice is atomic, i.e. any nonzero element is greater than or equal to some atom. Remark in [Kalmbach] p. 140. Also Definition 3.4-2 in [MegPav2000] p. 2345 (PDF p. 8). (Contributed by NM, 24-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐴 ≠ 0ℋ) → ∃𝑥 ∈ HAtoms 𝑥 ⊆ 𝐴) | ||
Theorem | shatomistici 32389* | The lattice of Hilbert subspaces is atomistic, i.e. any element is the supremum of its atoms. Part of proof of Theorem 16.9 of [MaedaMaeda] p. 70. (Contributed by NM, 26-Nov-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ ⇒ ⊢ 𝐴 = (span‘∪ {𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴}) | ||
Theorem | hatomistici 32390* | Cℋ is atomistic, i.e. any element is the supremum of its atoms. Remark in [Kalmbach] p. 140. (Contributed by NM, 14-Aug-2002.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ ⇒ ⊢ 𝐴 = ( ∨ℋ ‘{𝑥 ∈ HAtoms ∣ 𝑥 ⊆ 𝐴}) | ||
Theorem | chpssati 32391* | Two Hilbert lattice elements in a proper subset relationship imply the existence of an atom less than or equal to one but not the other. (Contributed by NM, 10-Jun-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ⊊ 𝐵 → ∃𝑥 ∈ HAtoms (𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ 𝐴)) | ||
Theorem | chrelati 32392* | The Hilbert lattice is relatively atomic. Remark 2 of [Kalmbach] p. 149. (Contributed by NM, 11-Jun-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ⊊ 𝐵 → ∃𝑥 ∈ HAtoms (𝐴 ⊊ (𝐴 ∨ℋ 𝑥) ∧ (𝐴 ∨ℋ 𝑥) ⊆ 𝐵)) | ||
Theorem | chrelat2i 32393* | A consequence of relative atomicity. (Contributed by NM, 30-Jun-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (¬ 𝐴 ⊆ 𝐵 ↔ ∃𝑥 ∈ HAtoms (𝑥 ⊆ 𝐴 ∧ ¬ 𝑥 ⊆ 𝐵)) | ||
Theorem | cvati 32394* | If a Hilbert lattice element covers another, it equals the other joined with some atom. This is a consequence of the relative atomicity of Hilbert space. (Contributed by NM, 30-Nov-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ⋖ℋ 𝐵 → ∃𝑥 ∈ HAtoms (𝐴 ∨ℋ 𝑥) = 𝐵) | ||
Theorem | cvbr4i 32395* | An alternate way to express the covering property. (Contributed by NM, 30-Nov-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ⋖ℋ 𝐵 ↔ (𝐴 ⊊ 𝐵 ∧ ∃𝑥 ∈ HAtoms (𝐴 ∨ℋ 𝑥) = 𝐵)) | ||
Theorem | cvexchlem 32396 | Lemma for cvexchi 32397. (Contributed by NM, 10-Jun-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ ((𝐴 ∩ 𝐵) ⋖ℋ 𝐵 → 𝐴 ⋖ℋ (𝐴 ∨ℋ 𝐵)) | ||
Theorem | cvexchi 32397 | The Hilbert lattice satisfies the exchange axiom. Proposition 1(iii) of [Kalmbach] p. 140 and its converse. Originally proved by Garrett Birkhoff in 1933. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ ((𝐴 ∩ 𝐵) ⋖ℋ 𝐵 ↔ 𝐴 ⋖ℋ (𝐴 ∨ℋ 𝐵)) | ||
Theorem | chrelat2 32398* | A consequence of relative atomicity. (Contributed by NM, 1-Jul-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (¬ 𝐴 ⊆ 𝐵 ↔ ∃𝑥 ∈ HAtoms (𝑥 ⊆ 𝐴 ∧ ¬ 𝑥 ⊆ 𝐵))) | ||
Theorem | chrelat3 32399* | A consequence of relative atomicity. (Contributed by NM, 2-Jul-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ HAtoms (𝑥 ⊆ 𝐴 → 𝑥 ⊆ 𝐵))) | ||
Theorem | chrelat3i 32400* | A consequence of the relative atomicity of Hilbert space: the ordering of Hilbert lattice elements is completely determined by the atoms they majorize. (Contributed by NM, 30-Jun-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ HAtoms (𝑥 ⊆ 𝐴 → 𝑥 ⊆ 𝐵)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |