Home | Metamath
Proof Explorer Theorem List (p. 293 of 426) | < 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-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | atcv0 29201 | An atom covers the zero subspace. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.) |
⊢ (𝐴 ∈ HAtoms → 0ℋ ⋖ℋ 𝐴) | ||
Theorem | atssch 29202 | Atoms are a subset of the Hilbert lattice. (Contributed by NM, 14-Aug-2002.) (New usage is discouraged.) |
⊢ HAtoms ⊆ Cℋ | ||
Theorem | atelch 29203 | An atom is a Hilbert lattice element. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.) |
⊢ (𝐴 ∈ HAtoms → 𝐴 ∈ Cℋ ) | ||
Theorem | atne0 29204 | An atom is not the Hilbert lattice zero. (Contributed by NM, 13-Aug-2002.) (New usage is discouraged.) |
⊢ (𝐴 ∈ HAtoms → 𝐴 ≠ 0ℋ) | ||
Theorem | atss 29205 | 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 29206 | Two atoms in a subset relationship are equal. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ HAtoms ∧ 𝐵 ∈ HAtoms) → (𝐴 ⊆ 𝐵 ↔ 𝐴 = 𝐵)) | ||
Theorem | atcveq0 29207 | 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 29208 | A 1-dimensional subspace is an atom. (Contributed by NM, 22-Jul-2001.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ) → (⊥‘(⊥‘{𝐴})) ∈ HAtoms) | ||
Theorem | spansna 29209 | 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 29210 | 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 29211 | 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 29212* | 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 29213* | 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 29214 | 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 29215 | The Hilbert lattice has the covering property. (Contributed by NM, 11-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms) → (𝐴 ⊊ (𝐴 ∨ℋ 𝐵) ↔ 𝐴 ⋖ℋ (𝐴 ∨ℋ 𝐵))) | ||
Theorem | chjatom 29216 | 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 29217* | 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 29218* | 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 29219* | 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 29220* | 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 29221* | 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 29222* | 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 29223* | 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 29224* | A consequence of relative atomicity. (Contributed by NM, 30-Jun-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (¬ 𝐴 ⊆ 𝐵 ↔ ∃𝑥 ∈ HAtoms (𝑥 ⊆ 𝐴 ∧ ¬ 𝑥 ⊆ 𝐵)) | ||
Theorem | cvati 29225* | 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 29226* | An alternate way to express the covering property. (Contributed by NM, 30-Nov-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ⋖ℋ 𝐵 ↔ (𝐴 ⊊ 𝐵 ∧ ∃𝑥 ∈ HAtoms (𝐴 ∨ℋ 𝑥) = 𝐵)) | ||
Theorem | cvexchlem 29227 | Lemma for cvexchi 29228. (Contributed by NM, 10-Jun-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ ((𝐴 ∩ 𝐵) ⋖ℋ 𝐵 → 𝐴 ⋖ℋ (𝐴 ∨ℋ 𝐵)) | ||
Theorem | cvexchi 29228 | 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 29229* | A consequence of relative atomicity. (Contributed by NM, 1-Jul-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (¬ 𝐴 ⊆ 𝐵 ↔ ∃𝑥 ∈ HAtoms (𝑥 ⊆ 𝐴 ∧ ¬ 𝑥 ⊆ 𝐵))) | ||
Theorem | chrelat3 29230* | A consequence of relative atomicity. (Contributed by NM, 2-Jul-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ HAtoms (𝑥 ⊆ 𝐴 → 𝑥 ⊆ 𝐵))) | ||
Theorem | chrelat3i 29231* | 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 29232* | 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 29233 | 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 29234 | 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 29235 | 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 29236 | The meet of distinct atoms is the zero subspace. (Contributed by NM, 25-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ HAtoms ∧ 𝐵 ∈ HAtoms) → (𝐴 ≠ 𝐵 ↔ (𝐴 ∩ 𝐵) = 0ℋ)) | ||
Theorem | atssma 29237 | 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 29238 | Two atoms covering the zero subspace are equal. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ HAtoms ∧ 𝐵 ∈ HAtoms) → (0ℋ ⋖ℋ (𝐴 ∨ℋ 𝐵) ↔ 𝐴 = 𝐵)) | ||
Theorem | atcv1 29239 | Two atoms covering the zero subspace are equal. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.) |
⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ 𝐴 ⋖ℋ (𝐵 ∨ℋ 𝐶)) → (𝐴 = 0ℋ ↔ 𝐵 = 𝐶)) | ||
Theorem | atexch 29240 | 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 29236 to obtain atom inequality). (Contributed by NM, 27-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) → ((𝐵 ⊆ (𝐴 ∨ℋ 𝐶) ∧ (𝐴 ∩ 𝐵) = 0ℋ) → 𝐶 ⊆ (𝐴 ∨ℋ 𝐵))) | ||
Theorem | atomli 29241 | An assertion holding in atomic orthomodular lattices that is equivalent to the exchange axiom. Proposition 3.2.17 of [PtakPulmannova] p. 66. (Contributed by NM, 24-Jun-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ ⇒ ⊢ (𝐵 ∈ HAtoms → ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ∈ (HAtoms ∪ {0ℋ})) | ||
Theorem | atoml2i 29242 | An assertion holding in atomic orthomodular lattices that is equivalent to the exchange axiom. Proposition P8(ii) of [BeltramettiCassinelli1] p. 400. (Contributed by NM, 12-Jun-2006.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ ⇒ ⊢ ((𝐵 ∈ HAtoms ∧ ¬ 𝐵 ⊆ 𝐴) → ((𝐴 ∨ℋ 𝐵) ∩ (⊥‘𝐴)) ∈ HAtoms) | ||
Theorem | atordi 29243 | An ordering law for a Hilbert lattice atom and a commuting subspace. (Contributed by NM, 12-Jun-2006.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ ⇒ ⊢ ((𝐵 ∈ HAtoms ∧ 𝐴 𝐶ℋ 𝐵) → (𝐵 ⊆ 𝐴 ∨ 𝐵 ⊆ (⊥‘𝐴))) | ||
Theorem | atcvatlem 29244 | Lemma for atcvati 29245. (Contributed by NM, 27-Jun-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ ⇒ ⊢ (((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) ∧ (𝐴 ≠ 0ℋ ∧ 𝐴 ⊊ (𝐵 ∨ℋ 𝐶))) → (¬ 𝐵 ⊆ 𝐴 → 𝐴 ∈ HAtoms)) | ||
Theorem | atcvati 29245 | A nonzero Hilbert lattice element less than the join of two atoms is an atom. (Contributed by NM, 28-Jun-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ ⇒ ⊢ ((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) → ((𝐴 ≠ 0ℋ ∧ 𝐴 ⊊ (𝐵 ∨ℋ 𝐶)) → 𝐴 ∈ HAtoms)) | ||
Theorem | atcvat2i 29246 | A Hilbert lattice element covered by the join of two distinct atoms is an atom. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ ⇒ ⊢ ((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) → ((¬ 𝐵 = 𝐶 ∧ 𝐴 ⋖ℋ (𝐵 ∨ℋ 𝐶)) → 𝐴 ∈ HAtoms)) | ||
Theorem | atord 29247 | An ordering law for a Hilbert lattice atom and a commuting subspace. (Contributed by NM, 12-Jun-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ∧ 𝐴 𝐶ℋ 𝐵) → (𝐵 ⊆ 𝐴 ∨ 𝐵 ⊆ (⊥‘𝐴))) | ||
Theorem | atcvat2 29248 | A Hilbert lattice element covered by the join of two distinct atoms is an atom. (Contributed by NM, 29-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) → ((¬ 𝐵 = 𝐶 ∧ 𝐴 ⋖ℋ (𝐵 ∨ℋ 𝐶)) → 𝐴 ∈ HAtoms)) | ||
Theorem | chirredlem1 29249* | Lemma for chirredi 29253. (Contributed by NM, 14-Jun-2006.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ ⇒ ⊢ (((𝑝 ∈ HAtoms ∧ (𝑞 ∈ Cℋ ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ ((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝑝 ∩ (⊥‘𝑟)) = 0ℋ) | ||
Theorem | chirredlem2 29250* | Lemma for chirredi 29253. (Contributed by NM, 15-Jun-2006.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ ⇒ ⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ ((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → ((⊥‘𝑟) ∩ (𝑝 ∨ℋ 𝑞)) = 𝑞) | ||
Theorem | chirredlem3 29251* | Lemma for chirredi 29253. (Contributed by NM, 15-Jun-2006.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ (𝑥 ∈ Cℋ → 𝐴 𝐶ℋ 𝑥) ⇒ ⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ (𝑟 ∈ HAtoms ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝑟 ⊆ 𝐴 → 𝑟 = 𝑝)) | ||
Theorem | chirredlem4 29252* | Lemma for chirredi 29253. (Contributed by NM, 15-Jun-2006.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ (𝑥 ∈ Cℋ → 𝐴 𝐶ℋ 𝑥) ⇒ ⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ (𝑟 ∈ HAtoms ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝑟 = 𝑝 ∨ 𝑟 = 𝑞)) | ||
Theorem | chirredi 29253* | The Hilbert lattice is irreducible: any element that commutes with all elements must be zero or one. Theorem 14.8.4 of [BeltramettiCassinelli] p. 166. (Contributed by NM, 15-Jun-2006.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ (𝑥 ∈ Cℋ → 𝐴 𝐶ℋ 𝑥) ⇒ ⊢ (𝐴 = 0ℋ ∨ 𝐴 = ℋ) | ||
Theorem | chirred 29254* | The Hilbert lattice is irreducible: any element that commutes with all elements must be zero or one. Theorem 14.8.4 of [BeltramettiCassinelli] p. 166. (Contributed by NM, 16-Jun-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ ∀𝑥 ∈ Cℋ 𝐴 𝐶ℋ 𝑥) → (𝐴 = 0ℋ ∨ 𝐴 = ℋ)) | ||
Theorem | atcvat3i 29255 | A condition implying that a certain lattice element is an atom. Part of Lemma 3.2.20 of [PtakPulmannova] p. 68. (Contributed by NM, 2-Jul-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ ⇒ ⊢ ((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) → (((¬ 𝐵 = 𝐶 ∧ ¬ 𝐶 ⊆ 𝐴) ∧ 𝐵 ⊆ (𝐴 ∨ℋ 𝐶)) → (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) ∈ HAtoms)) | ||
Theorem | atcvat4i 29256* | A condition implying existence of an atom with the properties shown. Lemma 3.2.20 of [PtakPulmannova] p. 68. (Contributed by NM, 2-Jul-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ ⇒ ⊢ ((𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms) → ((𝐴 ≠ 0ℋ ∧ 𝐵 ⊆ (𝐴 ∨ℋ 𝐶)) → ∃𝑥 ∈ HAtoms (𝑥 ⊆ 𝐴 ∧ 𝐵 ⊆ (𝐶 ∨ℋ 𝑥)))) | ||
Theorem | atdmd 29257 | Two Hilbert lattice elements have the dual modular pair property if the first is an atom. Theorem 7.6(c) of [MaedaMaeda] p. 31. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ HAtoms ∧ 𝐵 ∈ Cℋ ) → 𝐴 𝑀ℋ* 𝐵) | ||
Theorem | atmd 29258 | Two Hilbert lattice elements have the modular pair property if the first is an atom. Theorem 7.6(b) of [MaedaMaeda] p. 31. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ HAtoms ∧ 𝐵 ∈ Cℋ ) → 𝐴 𝑀ℋ 𝐵) | ||
Theorem | atmd2 29259 | Two Hilbert lattice elements have the dual modular pair property if the second is an atom. Part of Exercise 6 of [Kalmbach] p. 103. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms) → 𝐴 𝑀ℋ 𝐵) | ||
Theorem | atabsi 29260 | Absorption of an incomparable atom. Similar to Exercise 7.1 of [MaedaMaeda] p. 34. (Contributed by NM, 15-Jul-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐶 ∈ HAtoms → (¬ 𝐶 ⊆ (𝐴 ∨ℋ 𝐵) → ((𝐴 ∨ℋ 𝐶) ∩ 𝐵) = (𝐴 ∩ 𝐵))) | ||
Theorem | atabs2i 29261 | Absorption of an incomparable atom. (Contributed by NM, 18-Jul-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐶 ∈ HAtoms → (¬ 𝐶 ⊆ (𝐴 ∨ℋ 𝐵) → ((𝐴 ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) = 𝐴)) | ||
Theorem | mdsymlem1 29262* | Lemma for mdsymi 29270. (Contributed by NM, 1-Jul-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 = (𝐴 ∨ℋ 𝑝) ⇒ ⊢ (((𝑝 ∈ Cℋ ∧ (𝐵 ∩ 𝐶) ⊆ 𝐴) ∧ (𝐵 𝑀ℋ* 𝐴 ∧ 𝑝 ⊆ (𝐴 ∨ℋ 𝐵))) → 𝑝 ⊆ 𝐴) | ||
Theorem | mdsymlem2 29263* | Lemma for mdsymi 29270. (Contributed by NM, 1-Jul-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 = (𝐴 ∨ℋ 𝑝) ⇒ ⊢ (((𝑝 ∈ HAtoms ∧ (𝐵 ∩ 𝐶) ⊆ 𝐴) ∧ (𝐵 𝑀ℋ* 𝐴 ∧ 𝑝 ⊆ (𝐴 ∨ℋ 𝐵))) → (𝐵 ≠ 0ℋ → ∃𝑟 ∈ HAtoms ∃𝑞 ∈ HAtoms (𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵)))) | ||
Theorem | mdsymlem3 29264* | Lemma for mdsymi 29270. (Contributed by NM, 2-Jul-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 = (𝐴 ∨ℋ 𝑝) ⇒ ⊢ ((((𝑝 ∈ HAtoms ∧ ¬ (𝐵 ∩ 𝐶) ⊆ 𝐴) ∧ 𝑝 ⊆ (𝐴 ∨ℋ 𝐵)) ∧ 𝐴 ≠ 0ℋ) → ∃𝑟 ∈ HAtoms ∃𝑞 ∈ HAtoms (𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵))) | ||
Theorem | mdsymlem4 29265* | Lemma for mdsymi 29270. This is the forward direction of Lemma 4(i) of [Maeda] p. 168. (Contributed by NM, 2-Jul-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 = (𝐴 ∨ℋ 𝑝) ⇒ ⊢ (𝑝 ∈ HAtoms → ((𝐵 𝑀ℋ* 𝐴 ∧ ((𝐴 ≠ 0ℋ ∧ 𝐵 ≠ 0ℋ) ∧ 𝑝 ⊆ (𝐴 ∨ℋ 𝐵))) → ∃𝑞 ∈ HAtoms ∃𝑟 ∈ HAtoms (𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵)))) | ||
Theorem | mdsymlem5 29266* | Lemma for mdsymi 29270. (Contributed by NM, 2-Jul-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 = (𝐴 ∨ℋ 𝑝) ⇒ ⊢ ((𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms) → (¬ 𝑞 = 𝑝 → ((𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵)) → (((𝑐 ∈ Cℋ ∧ 𝐴 ⊆ 𝑐) ∧ 𝑝 ∈ HAtoms) → (𝑝 ⊆ 𝑐 → 𝑝 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴)))))) | ||
Theorem | mdsymlem6 29267* | Lemma for mdsymi 29270. This is the converse direction of Lemma 4(i) of [Maeda] p. 168, and is based on the proof of Theorem 1(d) to (e) of [Maeda] p. 167. (Contributed by NM, 2-Jul-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 = (𝐴 ∨ℋ 𝑝) ⇒ ⊢ (∀𝑝 ∈ HAtoms (𝑝 ⊆ (𝐴 ∨ℋ 𝐵) → ∃𝑞 ∈ HAtoms ∃𝑟 ∈ HAtoms (𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵))) → 𝐵 𝑀ℋ* 𝐴) | ||
Theorem | mdsymlem7 29268* | Lemma for mdsymi 29270. Lemma 4(i) of [Maeda] p. 168. Note that Maeda's 1965 definition of dual modular pair has reversed arguments compared to the later (1970) definition given in Remark 29.6 of [MaedaMaeda] p. 130, which is the one that we use. (Contributed by NM, 3-Jul-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 = (𝐴 ∨ℋ 𝑝) ⇒ ⊢ ((𝐴 ≠ 0ℋ ∧ 𝐵 ≠ 0ℋ) → (𝐵 𝑀ℋ* 𝐴 ↔ ∀𝑝 ∈ HAtoms (𝑝 ⊆ (𝐴 ∨ℋ 𝐵) → ∃𝑞 ∈ HAtoms ∃𝑟 ∈ HAtoms (𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵))))) | ||
Theorem | mdsymlem8 29269* | Lemma for mdsymi 29270. Lemma 4(ii) of [Maeda] p. 168. (Contributed by NM, 3-Jul-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 = (𝐴 ∨ℋ 𝑝) ⇒ ⊢ ((𝐴 ≠ 0ℋ ∧ 𝐵 ≠ 0ℋ) → (𝐵 𝑀ℋ* 𝐴 ↔ 𝐴 𝑀ℋ* 𝐵)) | ||
Theorem | mdsymi 29270 | M-symmetry of the Hilbert lattice. Lemma 5 of [Maeda] p. 168. (Contributed by NM, 3-Jul-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 𝑀ℋ 𝐵 ↔ 𝐵 𝑀ℋ 𝐴) | ||
Theorem | mdsym 29271 | M-symmetry of the Hilbert lattice. Lemma 5 of [Maeda] p. 168. (Contributed by NM, 6-Jul-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝑀ℋ 𝐵 ↔ 𝐵 𝑀ℋ 𝐴)) | ||
Theorem | dmdsym 29272 | Dual M-symmetry of the Hilbert lattice. (Contributed by NM, 25-Jul-2007.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝑀ℋ* 𝐵 ↔ 𝐵 𝑀ℋ* 𝐴)) | ||
Theorem | atdmd2 29273 | Two Hilbert lattice elements have the dual modular pair property if the second is an atom. (Contributed by NM, 6-Jul-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms) → 𝐴 𝑀ℋ* 𝐵) | ||
Theorem | sumdmdii 29274 | If the subspace sum of two Hilbert lattice elements is closed, then the elements are a dual modular pair. Remark in [MaedaMaeda] p. 139. (Contributed by NM, 12-Jul-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ ((𝐴 +ℋ 𝐵) = (𝐴 ∨ℋ 𝐵) → 𝐴 𝑀ℋ* 𝐵) | ||
Theorem | cmmdi 29275 | Commuting subspaces form a modular pair. (Contributed by NM, 16-Jan-2005.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 𝐶ℋ 𝐵 → 𝐴 𝑀ℋ 𝐵) | ||
Theorem | cmdmdi 29276 | Commuting subspaces form a dual modular pair. (Contributed by NM, 25-Apr-2006.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 𝐶ℋ 𝐵 → 𝐴 𝑀ℋ* 𝐵) | ||
Theorem | sumdmdlem 29277 | Lemma for sumdmdi 29279. The span of vector 𝐶 not in the subspace sum is "trimmed off." (Contributed by NM, 18-Dec-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ ((𝐶 ∈ ℋ ∧ ¬ 𝐶 ∈ (𝐴 +ℋ 𝐵)) → ((𝐵 +ℋ (span‘{𝐶})) ∩ 𝐴) = (𝐵 ∩ 𝐴)) | ||
Theorem | sumdmdlem2 29278* | Lemma for sumdmdi 29279. (Contributed by NM, 23-Dec-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (∀𝑥 ∈ HAtoms ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵) → (𝐴 +ℋ 𝐵) = (𝐴 ∨ℋ 𝐵)) | ||
Theorem | sumdmdi 29279 | The subspace sum of two Hilbert lattice elements is closed iff the elements are a dual modular pair. Theorem 2 of [Holland] p. 1519. (Contributed by NM, 14-Dec-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ ((𝐴 +ℋ 𝐵) = (𝐴 ∨ℋ 𝐵) ↔ 𝐴 𝑀ℋ* 𝐵) | ||
Theorem | dmdbr4ati 29280* | Dual modular pair property in terms of atoms. (Contributed by NM, 15-Jan-2005.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 𝑀ℋ* 𝐵 ↔ ∀𝑥 ∈ HAtoms ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)) | ||
Theorem | dmdbr5ati 29281* | Dual modular pair property in terms of atoms. (Contributed by NM, 14-Jan-2005.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 𝑀ℋ* 𝐵 ↔ ∀𝑥 ∈ HAtoms (𝑥 ⊆ (𝐴 ∨ℋ 𝐵) → 𝑥 ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))) | ||
Theorem | dmdbr6ati 29282* | Dual modular pair property in terms of atoms. The modular law takes the form of the shearing identity. (Contributed by NM, 18-Jan-2005.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 𝑀ℋ* 𝐵 ↔ ∀𝑥 ∈ HAtoms ((𝐴 ∨ℋ 𝐵) ∩ 𝑥) = ((((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵) ∩ 𝑥)) | ||
Theorem | dmdbr7ati 29283* | Dual modular pair property in terms of atoms. (Contributed by NM, 18-Jan-2005.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 𝑀ℋ* 𝐵 ↔ ∀𝑥 ∈ HAtoms ((𝐴 ∨ℋ 𝐵) ∩ 𝑥) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)) | ||
Theorem | mdoc1i 29284 | Orthocomplements form a modular pair. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ ⇒ ⊢ 𝐴 𝑀ℋ (⊥‘𝐴) | ||
Theorem | mdoc2i 29285 | Orthocomplements form a modular pair. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ ⇒ ⊢ (⊥‘𝐴) 𝑀ℋ 𝐴 | ||
Theorem | dmdoc1i 29286 | Orthocomplements form a dual modular pair. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ ⇒ ⊢ 𝐴 𝑀ℋ* (⊥‘𝐴) | ||
Theorem | dmdoc2i 29287 | Orthocomplements form a dual modular pair. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ ⇒ ⊢ (⊥‘𝐴) 𝑀ℋ* 𝐴 | ||
Theorem | mdcompli 29288 | A condition equivalent to the modular pair property. Part of proof of Theorem 1.14 of [MaedaMaeda] p. 4. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 𝑀ℋ 𝐵 ↔ (𝐴 ∩ (⊥‘(𝐴 ∩ 𝐵))) 𝑀ℋ (𝐵 ∩ (⊥‘(𝐴 ∩ 𝐵)))) | ||
Theorem | dmdcompli 29289 | A condition equivalent to the dual modular pair property. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 𝑀ℋ* 𝐵 ↔ (𝐴 ∩ (⊥‘(𝐴 ∩ 𝐵))) 𝑀ℋ* (𝐵 ∩ (⊥‘(𝐴 ∩ 𝐵)))) | ||
Theorem | mddmdin0i 29290* | If dual modular implies modular whenever meet is zero, then dual modular implies modular for arbitrary lattice elements. This theorem is needed for the remark after Lemma 7 of [Holland] p. 1524 to hold. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ ∀𝑥 ∈ Cℋ ∀𝑦 ∈ Cℋ ((𝑥 𝑀ℋ* 𝑦 ∧ (𝑥 ∩ 𝑦) = 0ℋ) → 𝑥 𝑀ℋ 𝑦) ⇒ ⊢ (𝐴 𝑀ℋ* 𝐵 → 𝐴 𝑀ℋ 𝐵) | ||
Theorem | cdjreui 29291* | A member of the sum of disjoint subspaces has a unique decomposition. Part of Lemma 5 of [Holland] p. 1520. (Contributed by NM, 20-May-2005.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ ⇒ ⊢ ((𝐶 ∈ (𝐴 +ℋ 𝐵) ∧ (𝐴 ∩ 𝐵) = 0ℋ) → ∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦)) | ||
Theorem | cdj1i 29292* | Two ways to express "𝐴 and 𝐵 are completely disjoint subspaces." (1) => (2) in Lemma 5 of [Holland] p. 1520. (Contributed by NM, 21-May-2005.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ ⇒ ⊢ (∃𝑤 ∈ ℝ (0 < 𝑤 ∧ ∀𝑦 ∈ 𝐴 ∀𝑣 ∈ 𝐵 ((normℎ‘𝑦) + (normℎ‘𝑣)) ≤ (𝑤 · (normℎ‘(𝑦 +ℎ 𝑣)))) → ∃𝑥 ∈ ℝ (0 < 𝑥 ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((normℎ‘𝑦) = 1 → 𝑥 ≤ (normℎ‘(𝑦 −ℎ 𝑧))))) | ||
Theorem | cdj3lem1 29293* | A property of "𝐴 and 𝐵 are completely disjoint subspaces." Part of Lemma 5 of [Holland] p. 1520. (Contributed by NM, 23-May-2005.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ ⇒ ⊢ (∃𝑥 ∈ ℝ (0 < 𝑥 ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ((normℎ‘𝑦) + (normℎ‘𝑧)) ≤ (𝑥 · (normℎ‘(𝑦 +ℎ 𝑧)))) → (𝐴 ∩ 𝐵) = 0ℋ) | ||
Theorem | cdj3lem2 29294* | Lemma for cdj3i 29300. Value of the first-component function 𝑆. (Contributed by NM, 23-May-2005.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ & ⊢ 𝑆 = (𝑥 ∈ (𝐴 +ℋ 𝐵) ↦ (℩𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑥 = (𝑧 +ℎ 𝑤))) ⇒ ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ∧ (𝐴 ∩ 𝐵) = 0ℋ) → (𝑆‘(𝐶 +ℎ 𝐷)) = 𝐶) | ||
Theorem | cdj3lem2a 29295* | Lemma for cdj3i 29300. Closure of the first-component function 𝑆. (Contributed by NM, 25-May-2005.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ & ⊢ 𝑆 = (𝑥 ∈ (𝐴 +ℋ 𝐵) ↦ (℩𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑥 = (𝑧 +ℎ 𝑤))) ⇒ ⊢ ((𝐶 ∈ (𝐴 +ℋ 𝐵) ∧ (𝐴 ∩ 𝐵) = 0ℋ) → (𝑆‘𝐶) ∈ 𝐴) | ||
Theorem | cdj3lem2b 29296* | Lemma for cdj3i 29300. The first-component function 𝑆 is bounded if the subspaces are completely disjoint. (Contributed by NM, 26-May-2005.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ & ⊢ 𝑆 = (𝑥 ∈ (𝐴 +ℋ 𝐵) ↦ (℩𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑥 = (𝑧 +ℎ 𝑤))) ⇒ ⊢ (∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((normℎ‘𝑥) + (normℎ‘𝑦)) ≤ (𝑣 · (normℎ‘(𝑥 +ℎ 𝑦)))) → ∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑢 ∈ (𝐴 +ℋ 𝐵)(normℎ‘(𝑆‘𝑢)) ≤ (𝑣 · (normℎ‘𝑢)))) | ||
Theorem | cdj3lem3 29297* | Lemma for cdj3i 29300. Value of the second-component function 𝑇. (Contributed by NM, 23-May-2005.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ & ⊢ 𝑇 = (𝑥 ∈ (𝐴 +ℋ 𝐵) ↦ (℩𝑤 ∈ 𝐵 ∃𝑧 ∈ 𝐴 𝑥 = (𝑧 +ℎ 𝑤))) ⇒ ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ∧ (𝐴 ∩ 𝐵) = 0ℋ) → (𝑇‘(𝐶 +ℎ 𝐷)) = 𝐷) | ||
Theorem | cdj3lem3a 29298* | Lemma for cdj3i 29300. Closure of the second-component function 𝑇. (Contributed by NM, 26-May-2005.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ & ⊢ 𝑇 = (𝑥 ∈ (𝐴 +ℋ 𝐵) ↦ (℩𝑤 ∈ 𝐵 ∃𝑧 ∈ 𝐴 𝑥 = (𝑧 +ℎ 𝑤))) ⇒ ⊢ ((𝐶 ∈ (𝐴 +ℋ 𝐵) ∧ (𝐴 ∩ 𝐵) = 0ℋ) → (𝑇‘𝐶) ∈ 𝐵) | ||
Theorem | cdj3lem3b 29299* | Lemma for cdj3i 29300. The second-component function 𝑇 is bounded if the subspaces are completely disjoint. (Contributed by NM, 31-May-2005.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ & ⊢ 𝑇 = (𝑥 ∈ (𝐴 +ℋ 𝐵) ↦ (℩𝑤 ∈ 𝐵 ∃𝑧 ∈ 𝐴 𝑥 = (𝑧 +ℎ 𝑤))) ⇒ ⊢ (∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((normℎ‘𝑥) + (normℎ‘𝑦)) ≤ (𝑣 · (normℎ‘(𝑥 +ℎ 𝑦)))) → ∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑢 ∈ (𝐴 +ℋ 𝐵)(normℎ‘(𝑇‘𝑢)) ≤ (𝑣 · (normℎ‘𝑢)))) | ||
Theorem | cdj3i 29300* | Two ways to express "𝐴 and 𝐵 are completely disjoint subspaces." (1) <=> (3) in Lemma 5 of [Holland] p. 1520. (Contributed by NM, 1-Jun-2005.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ & ⊢ 𝑆 = (𝑥 ∈ (𝐴 +ℋ 𝐵) ↦ (℩𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑥 = (𝑧 +ℎ 𝑤))) & ⊢ 𝑇 = (𝑥 ∈ (𝐴 +ℋ 𝐵) ↦ (℩𝑤 ∈ 𝐵 ∃𝑧 ∈ 𝐴 𝑥 = (𝑧 +ℎ 𝑤))) & ⊢ (𝜑 ↔ ∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑢 ∈ (𝐴 +ℋ 𝐵)(normℎ‘(𝑆‘𝑢)) ≤ (𝑣 · (normℎ‘𝑢)))) & ⊢ (𝜓 ↔ ∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑢 ∈ (𝐴 +ℋ 𝐵)(normℎ‘(𝑇‘𝑢)) ≤ (𝑣 · (normℎ‘𝑢)))) ⇒ ⊢ (∃𝑣 ∈ ℝ (0 < 𝑣 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ((normℎ‘𝑥) + (normℎ‘𝑦)) ≤ (𝑣 · (normℎ‘(𝑥 +ℎ 𝑦)))) ↔ ((𝐴 ∩ 𝐵) = 0ℋ ∧ 𝜑 ∧ 𝜓)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |