HomeTheorem List (p. 324 of 494)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 324 of 494) | < 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: | Metamath Proof Explorer
(1-30937) |
Hilbert Space Explorer
(30938-32460) |
Users' Mathboxes
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | cvbr 32301* | 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 32302* | 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 32303 | Contraposition law for the covers relation. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ⋖ℋ 𝐵 ↔ (⊥‘𝐵) ⋖ℋ (⊥‘𝐴))) | ||
| Theorem | cvpss 32304 | The covers relation implies proper subset. (Contributed by NM, 10-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ⋖ℋ 𝐵 → 𝐴 ⊊ 𝐵)) | ||
| Theorem | cvnbtwn 32305 | The covers relation implies no in-betweenness. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → (𝐴 ⋖ℋ 𝐵 → ¬ (𝐴 ⊊ 𝐶 ∧ 𝐶 ⊊ 𝐵))) | ||
| Theorem | cvnbtwn2 32306 | The covers relation implies no in-betweenness. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → (𝐴 ⋖ℋ 𝐵 → ((𝐴 ⊊ 𝐶 ∧ 𝐶 ⊆ 𝐵) → 𝐶 = 𝐵))) | ||
| Theorem | cvnbtwn3 32307 | The covers relation implies no in-betweenness. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → (𝐴 ⋖ℋ 𝐵 → ((𝐴 ⊆ 𝐶 ∧ 𝐶 ⊊ 𝐵) → 𝐶 = 𝐴))) | ||
| Theorem | cvnbtwn4 32308 | 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 32309 | The covers relation is not symmetric. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ⋖ℋ 𝐵 → ¬ 𝐵 ⋖ℋ 𝐴)) | ||
| Theorem | cvnref 32310 | The covers relation is not reflexive. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ Cℋ → ¬ 𝐴 ⋖ℋ 𝐴) | ||
| Theorem | cvntr 32311 | The covers relation is not transitive. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ((𝐴 ⋖ℋ 𝐵 ∧ 𝐵 ⋖ℋ 𝐶) → ¬ 𝐴 ⋖ℋ 𝐶)) | ||
| Theorem | spansncv2 32312 | 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 32313* | 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 32314 | Consequence of the modular pair property. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.) |
| ⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ (𝐴 𝑀ℋ 𝐵 ∧ 𝐶 ⊆ 𝐵)) → ((𝐶 ∨ℋ 𝐴) ∩ 𝐵) = (𝐶 ∨ℋ (𝐴 ∩ 𝐵))) | ||
| Theorem | mdbr2 32315* | Binary relation expressing the modular pair property. This version has a weaker constraint than mdbr 32313. (Contributed by NM, 15-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝑀ℋ 𝐵 ↔ ∀𝑥 ∈ Cℋ (𝑥 ⊆ 𝐵 → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) ⊆ (𝑥 ∨ℋ (𝐴 ∩ 𝐵))))) | ||
| Theorem | mdbr3 32316* | 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 32317* | 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 32318* | Binary relation expressing the dual modular pair property. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝑀ℋ* 𝐵 ↔ ∀𝑥 ∈ Cℋ (𝐵 ⊆ 𝑥 → ((𝑥 ∩ 𝐴) ∨ℋ 𝐵) = (𝑥 ∩ (𝐴 ∨ℋ 𝐵))))) | ||
| Theorem | dmdmd 32319 | 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 32320 | 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 32321 | Consequence of the dual modular pair property. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.) |
| ⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ (𝐴 𝑀ℋ* 𝐵 ∧ 𝐵 ⊆ 𝐶)) → ((𝐶 ∩ 𝐴) ∨ℋ 𝐵) = (𝐶 ∩ (𝐴 ∨ℋ 𝐵))) | ||
| Theorem | dmdbr2 32322* | Binary relation expressing the dual modular pair property. This version has a weaker constraint than dmdbr 32318. (Contributed by NM, 30-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝑀ℋ* 𝐵 ↔ ∀𝑥 ∈ Cℋ (𝐵 ⊆ 𝑥 → (𝑥 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ ((𝑥 ∩ 𝐴) ∨ℋ 𝐵)))) | ||
| Theorem | dmdi2 32323 | Consequence of the dual modular pair property. (Contributed by NM, 14-Jan-2005.) (New usage is discouraged.) |
| ⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ (𝐴 𝑀ℋ* 𝐵 ∧ 𝐵 ⊆ 𝐶)) → (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ ((𝐶 ∩ 𝐴) ∨ℋ 𝐵)) | ||
| Theorem | dmdbr3 32324* | 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 32325* | 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 32326 | Consequence of the dual modular pair property. (Contributed by NM, 14-Jan-2005.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → (𝐴 𝑀ℋ* 𝐵 → ((𝐶 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝐶 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))) | ||
| Theorem | dmdbr5 32327* | Binary relation expressing the dual modular pair property. (Contributed by NM, 15-Jan-2005.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝑀ℋ* 𝐵 ↔ ∀𝑥 ∈ Cℋ (𝑥 ⊆ (𝐴 ∨ℋ 𝐵) → 𝑥 ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)))) | ||
| Theorem | mddmd2 32328* | 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 32329 | 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 32330 | 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 32331 | 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 32332 | 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 32333 | 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 32334 | 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 32335 | 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 32336 | 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 32337 | 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 32338 | 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 32339 | 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 32340* | 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 32341* | 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 32342* | 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 32343 | 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 32344 | Lemma for mdslmd1i 32348. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝐷 ∈ Cℋ & ⊢ 𝑅 ∈ Cℋ ⇒ ⊢ (((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) → (((𝑅 ∨ℋ 𝐴) ⊆ 𝐷 → (((𝑅 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷) ⊆ ((𝑅 ∨ℋ 𝐴) ∨ℋ (𝐶 ∩ 𝐷))) → ((((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑅 ∧ 𝑅 ⊆ (𝐷 ∩ 𝐵)) → ((𝑅 ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ (𝑅 ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)))))) | ||
| Theorem | mdslmd1lem2 32345 | Lemma for mdslmd1i 32348. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝐷 ∈ Cℋ & ⊢ 𝑅 ∈ Cℋ ⇒ ⊢ (((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) → (((𝑅 ∩ 𝐵) ⊆ (𝐷 ∩ 𝐵) → (((𝑅 ∩ 𝐵) ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ ((𝑅 ∩ 𝐵) ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)))) → (((𝐶 ∩ 𝐷) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷) → ((𝑅 ∨ℋ 𝐶) ∩ 𝐷) ⊆ (𝑅 ∨ℋ (𝐶 ∩ 𝐷))))) | ||
| Theorem | mdslmd1lem3 32346* | Lemma for mdslmd1i 32348. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝐷 ∈ Cℋ ⇒ ⊢ ((𝑥 ∈ Cℋ ∧ ((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))))) → (((𝑥 ∨ℋ 𝐴) ⊆ 𝐷 → (((𝑥 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷) ⊆ ((𝑥 ∨ℋ 𝐴) ∨ℋ (𝐶 ∩ 𝐷))) → ((((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑥 ∧ 𝑥 ⊆ (𝐷 ∩ 𝐵)) → ((𝑥 ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ (𝑥 ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)))))) | ||
| Theorem | mdslmd1lem4 32347* | Lemma for mdslmd1i 32348. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝐷 ∈ Cℋ ⇒ ⊢ ((𝑥 ∈ Cℋ ∧ ((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))))) → (((𝑥 ∩ 𝐵) ⊆ (𝐷 ∩ 𝐵) → (((𝑥 ∩ 𝐵) ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ ((𝑥 ∩ 𝐵) ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)))) → (((𝐶 ∩ 𝐷) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐷) → ((𝑥 ∨ℋ 𝐶) ∩ 𝐷) ⊆ (𝑥 ∨ℋ (𝐶 ∩ 𝐷))))) | ||
| Theorem | mdslmd1i 32348 | 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 32349 | 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 32350 | 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 32351 | 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 32352 | 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 32353* | 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 32354 | 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 32355 | 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 32356 | 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 32357 | 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 32358 and elat2 32359 for membership relations. (Contributed by NM, 14-Aug-2002.) (New usage is discouraged.) |
| ⊢ HAtoms = {𝑥 ∈ Cℋ ∣ 0ℋ ⋖ℋ 𝑥} | ||
| Theorem | ela 32358 | 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 32359* | 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 32360 | 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 32361 | An atom covers the zero subspace. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ HAtoms → 0ℋ ⋖ℋ 𝐴) | ||
| Theorem | atssch 32362 | Atoms are a subset of the Hilbert lattice. (Contributed by NM, 14-Aug-2002.) (New usage is discouraged.) |
| ⊢ HAtoms ⊆ Cℋ | ||
| Theorem | atelch 32363 | An atom is a Hilbert lattice element. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ HAtoms → 𝐴 ∈ Cℋ ) | ||
| Theorem | atne0 32364 | An atom is not the Hilbert lattice zero. (Contributed by NM, 13-Aug-2002.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ HAtoms → 𝐴 ≠ 0ℋ) | ||
| Theorem | atss 32365 | 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 32366 | Two atoms in a subset relationship are equal. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ HAtoms ∧ 𝐵 ∈ HAtoms) → (𝐴 ⊆ 𝐵 ↔ 𝐴 = 𝐵)) | ||
| Theorem | atcveq0 32367 | 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 32368 | A 1-dimensional subspace is an atom. (Contributed by NM, 22-Jul-2001.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ) → (⊥‘(⊥‘{𝐴})) ∈ HAtoms) | ||
| Theorem | spansna 32369 | 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 32370 | 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 32371 | 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 32372* | 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 32373* | 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 32374 | 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 32375 | The Hilbert lattice has the covering property. (Contributed by NM, 11-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms) → (𝐴 ⊊ (𝐴 ∨ℋ 𝐵) ↔ 𝐴 ⋖ℋ (𝐴 ∨ℋ 𝐵))) | ||
| Theorem | chjatom 32376 | 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 32377* | 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 32378* | 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 32379* | 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 32380* | 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 32381* | 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 32382* | 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 32383* | 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 32384* | A consequence of relative atomicity. (Contributed by NM, 30-Jun-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (¬ 𝐴 ⊆ 𝐵 ↔ ∃𝑥 ∈ HAtoms (𝑥 ⊆ 𝐴 ∧ ¬ 𝑥 ⊆ 𝐵)) | ||
| Theorem | cvati 32385* | 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 32386* | An alternate way to express the covering property. (Contributed by NM, 30-Nov-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ⋖ℋ 𝐵 ↔ (𝐴 ⊊ 𝐵 ∧ ∃𝑥 ∈ HAtoms (𝐴 ∨ℋ 𝑥) = 𝐵)) | ||
| Theorem | cvexchlem 32387 | Lemma for cvexchi 32388. (Contributed by NM, 10-Jun-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ ((𝐴 ∩ 𝐵) ⋖ℋ 𝐵 → 𝐴 ⋖ℋ (𝐴 ∨ℋ 𝐵)) | ||
| Theorem | cvexchi 32388 | 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 32389* | A consequence of relative atomicity. (Contributed by NM, 1-Jul-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (¬ 𝐴 ⊆ 𝐵 ↔ ∃𝑥 ∈ HAtoms (𝑥 ⊆ 𝐴 ∧ ¬ 𝑥 ⊆ 𝐵))) | ||
| Theorem | chrelat3 32390* | A consequence of relative atomicity. (Contributed by NM, 2-Jul-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ HAtoms (𝑥 ⊆ 𝐴 → 𝑥 ⊆ 𝐵))) | ||
| Theorem | chrelat3i 32391* | 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 (𝑥 ⊆ 𝐴 → 𝑥 ⊆ 𝐵)) | ||
| Theorem | chrelat4i 32392* | A consequence of relative atomicity. Extensionality principle: two lattice elements are equal iff they majorize the same atoms. (Contributed by NM, 30-Jun-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 = 𝐵 ↔ ∀𝑥 ∈ HAtoms (𝑥 ⊆ 𝐴 ↔ 𝑥 ⊆ 𝐵)) | ||
| Theorem | cvexch 32393 | 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, 21-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ((𝐴 ∩ 𝐵) ⋖ℋ 𝐵 ↔ 𝐴 ⋖ℋ (𝐴 ∨ℋ 𝐵))) | ||
| Theorem | cvp 32394 | The Hilbert lattice satisfies the covering property of Definition 7.4 of [MaedaMaeda] p. 31 and its converse. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms) → ((𝐴 ∩ 𝐵) = 0ℋ ↔ 𝐴 ⋖ℋ (𝐴 ∨ℋ 𝐵))) | ||
| Theorem | atnssm0 32395 | The meet of a Hilbert lattice element and an incomparable atom is the zero subspace. (Contributed by NM, 30-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms) → (¬ 𝐵 ⊆ 𝐴 ↔ (𝐴 ∩ 𝐵) = 0ℋ)) | ||
| Theorem | atnemeq0 32396 | The meet of distinct atoms is the zero subspace. (Contributed by NM, 25-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ HAtoms ∧ 𝐵 ∈ HAtoms) → (𝐴 ≠ 𝐵 ↔ (𝐴 ∩ 𝐵) = 0ℋ)) | ||
| Theorem | atssma 32397 | The meet with an atom's superset is the atom. (Contributed by NM, 12-Jun-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ HAtoms ∧ 𝐵 ∈ Cℋ ) → (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) ∈ HAtoms)) | ||
| Theorem | atcv0eq 32398 | Two atoms covering the zero subspace are equal. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ HAtoms ∧ 𝐵 ∈ HAtoms) → (0ℋ ⋖ℋ (𝐴 ∨ℋ 𝐵) ↔ 𝐴 = 𝐵)) | ||
| Theorem | atcv1 32399 | Two atoms covering the zero subspace are equal. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.) |
| ⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ 𝐴 ⋖ℋ (𝐵 ∨ℋ 𝐶)) → (𝐴 = 0ℋ ↔ 𝐵 = 𝐶)) | ||
| Theorem | atexch 32400 | The Hilbert lattice satisfies the atom exchange property. Proposition 1(i) of [Kalmbach] p. 140. A version of this theorem related to vector analysis was originally proved by Hermann Grassmann in 1862. Also Definition 3.4-3(b) in [MegPav2000] p. 2345 (PDF p. 8) (use atnemeq0 32396 to obtain atom inequality). (Contributed by NM, 27-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) → ((𝐵 ⊆ (𝐴 ∨ℋ 𝐶) ∧ (𝐴 ∩ 𝐵) = 0ℋ) → 𝐶 ⊆ (𝐴 ∨ℋ 𝐵))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |