![]() |
Metamath
Proof Explorer Theorem List (p. 294 of 454) | < 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-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | chabs1i 29301 | Hilbert lattice absorption law. From definition of lattice in [Kalmbach] p. 14. (Contributed by NM, 10-Jun-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ∨ℋ (𝐴 ∩ 𝐵)) = 𝐴 | ||
Theorem | chabs2i 29302 | Hilbert lattice absorption law. From definition of lattice in [Kalmbach] p. 14. (Contributed by NM, 16-Jun-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ∩ (𝐴 ∨ℋ 𝐵)) = 𝐴 | ||
Theorem | chjidm 29303 | Idempotent law for Hilbert lattice join. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.) |
⊢ (𝐴 ∈ Cℋ → (𝐴 ∨ℋ 𝐴) = 𝐴) | ||
Theorem | chjidmi 29304 | Idempotent law for Hilbert lattice join. (Contributed by NM, 15-Jun-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ ⇒ ⊢ (𝐴 ∨ℋ 𝐴) = 𝐴 | ||
Theorem | chj12i 29305 | A rearrangement of Hilbert lattice join. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ ⇒ ⊢ (𝐴 ∨ℋ (𝐵 ∨ℋ 𝐶)) = (𝐵 ∨ℋ (𝐴 ∨ℋ 𝐶)) | ||
Theorem | chj4i 29306 | Rearrangement of the join of 4 Hilbert lattice elements. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝐷 ∈ Cℋ ⇒ ⊢ ((𝐴 ∨ℋ 𝐵) ∨ℋ (𝐶 ∨ℋ 𝐷)) = ((𝐴 ∨ℋ 𝐶) ∨ℋ (𝐵 ∨ℋ 𝐷)) | ||
Theorem | chjjdiri 29307 | Hilbert lattice join distributes over itself. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ ⇒ ⊢ ((𝐴 ∨ℋ 𝐵) ∨ℋ 𝐶) = ((𝐴 ∨ℋ 𝐶) ∨ℋ (𝐵 ∨ℋ 𝐶)) | ||
Theorem | chdmm1 29308 | De Morgan's law for meet in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (⊥‘(𝐴 ∩ 𝐵)) = ((⊥‘𝐴) ∨ℋ (⊥‘𝐵))) | ||
Theorem | chdmm2 29309 | De Morgan's law for meet in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (⊥‘((⊥‘𝐴) ∩ 𝐵)) = (𝐴 ∨ℋ (⊥‘𝐵))) | ||
Theorem | chdmm3 29310 | De Morgan's law for meet in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (⊥‘(𝐴 ∩ (⊥‘𝐵))) = ((⊥‘𝐴) ∨ℋ 𝐵)) | ||
Theorem | chdmm4 29311 | De Morgan's law for meet in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (⊥‘((⊥‘𝐴) ∩ (⊥‘𝐵))) = (𝐴 ∨ℋ 𝐵)) | ||
Theorem | chdmj1 29312 | De Morgan's law for join in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (⊥‘(𝐴 ∨ℋ 𝐵)) = ((⊥‘𝐴) ∩ (⊥‘𝐵))) | ||
Theorem | chdmj2 29313 | De Morgan's law for join in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (⊥‘((⊥‘𝐴) ∨ℋ 𝐵)) = (𝐴 ∩ (⊥‘𝐵))) | ||
Theorem | chdmj3 29314 | De Morgan's law for join in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (⊥‘(𝐴 ∨ℋ (⊥‘𝐵))) = ((⊥‘𝐴) ∩ 𝐵)) | ||
Theorem | chdmj4 29315 | De Morgan's law for join in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (⊥‘((⊥‘𝐴) ∨ℋ (⊥‘𝐵))) = (𝐴 ∩ 𝐵)) | ||
Theorem | chjass 29316 | Associative law for Hilbert lattice join. From definition of lattice in [Kalmbach] p. 14. (Contributed by NM, 10-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ((𝐴 ∨ℋ 𝐵) ∨ℋ 𝐶) = (𝐴 ∨ℋ (𝐵 ∨ℋ 𝐶))) | ||
Theorem | chj12 29317 | A rearrangement of Hilbert lattice join. (Contributed by NM, 15-Jun-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → (𝐴 ∨ℋ (𝐵 ∨ℋ 𝐶)) = (𝐵 ∨ℋ (𝐴 ∨ℋ 𝐶))) | ||
Theorem | chj4 29318 | Rearrangement of the join of 4 Hilbert lattice elements. (Contributed by NM, 15-Jun-2006.) (New usage is discouraged.) |
⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ (𝐶 ∈ Cℋ ∧ 𝐷 ∈ Cℋ )) → ((𝐴 ∨ℋ 𝐵) ∨ℋ (𝐶 ∨ℋ 𝐷)) = ((𝐴 ∨ℋ 𝐶) ∨ℋ (𝐵 ∨ℋ 𝐷))) | ||
Theorem | ledii 29319 | An ortholattice is distributive in one ordering direction. (Contributed by NM, 6-Aug-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ ⇒ ⊢ ((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)) ⊆ (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) | ||
Theorem | lediri 29320 | An ortholattice is distributive in one ordering direction. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ ⇒ ⊢ ((𝐴 ∩ 𝐶) ∨ℋ (𝐵 ∩ 𝐶)) ⊆ ((𝐴 ∨ℋ 𝐵) ∩ 𝐶) | ||
Theorem | lejdii 29321 | An ortholattice is distributive in one ordering direction (join version). (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ ⇒ ⊢ (𝐴 ∨ℋ (𝐵 ∩ 𝐶)) ⊆ ((𝐴 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐶)) | ||
Theorem | lejdiri 29322 | An ortholattice is distributive in one ordering direction (join version). (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ ⇒ ⊢ ((𝐴 ∩ 𝐵) ∨ℋ 𝐶) ⊆ ((𝐴 ∨ℋ 𝐶) ∩ (𝐵 ∨ℋ 𝐶)) | ||
Theorem | ledi 29323 | An ortholattice is distributive in one ordering direction. (Contributed by NM, 14-Jun-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)) ⊆ (𝐴 ∩ (𝐵 ∨ℋ 𝐶))) | ||
Theorem | spansn0 29324 | The span of the singleton of the zero vector is the zero subspace. (Contributed by NM, 14-Jan-2005.) (New usage is discouraged.) |
⊢ (span‘{0ℎ}) = 0ℋ | ||
Theorem | span0 29325 | The span of the empty set is the zero subspace. Remark 11.6.e of [Schechter] p. 276. (Contributed by NM, 3-Jun-2004.) (New usage is discouraged.) |
⊢ (span‘∅) = 0ℋ | ||
Theorem | elspani 29326* | Membership in the span of a subset of Hilbert space. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ⊆ ℋ → (𝐵 ∈ (span‘𝐴) ↔ ∀𝑥 ∈ Sℋ (𝐴 ⊆ 𝑥 → 𝐵 ∈ 𝑥))) | ||
Theorem | spanuni 29327 | The span of a union is the subspace sum of spans. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.) |
⊢ 𝐴 ⊆ ℋ & ⊢ 𝐵 ⊆ ℋ ⇒ ⊢ (span‘(𝐴 ∪ 𝐵)) = ((span‘𝐴) +ℋ (span‘𝐵)) | ||
Theorem | spanun 29328 | The span of a union is the subspace sum of spans. (Contributed by NM, 9-Jun-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ) → (span‘(𝐴 ∪ 𝐵)) = ((span‘𝐴) +ℋ (span‘𝐵))) | ||
Theorem | sshhococi 29329 | The join of two Hilbert space subsets (not necessarily closed subspaces) equals the join of their closures (double orthocomplements). (Contributed by NM, 1-Jun-2004.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
⊢ 𝐴 ⊆ ℋ & ⊢ 𝐵 ⊆ ℋ ⇒ ⊢ (𝐴 ∨ℋ 𝐵) = ((⊥‘(⊥‘𝐴)) ∨ℋ (⊥‘(⊥‘𝐵))) | ||
Theorem | hne0 29330 | Hilbert space has a nonzero vector iff it is not trivial. (Contributed by NM, 24-Feb-2006.) (New usage is discouraged.) |
⊢ ( ℋ ≠ 0ℋ ↔ ∃𝑥 ∈ ℋ 𝑥 ≠ 0ℎ) | ||
Theorem | chsup0 29331 | The supremum of the empty set. (Contributed by NM, 13-Aug-2002.) (New usage is discouraged.) |
⊢ ( ∨ℋ ‘∅) = 0ℋ | ||
Theorem | h1deoi 29332 | Membership in orthocomplement of 1-dimensional subspace. (Contributed by NM, 7-Jul-2001.) (New usage is discouraged.) |
⊢ 𝐵 ∈ ℋ ⇒ ⊢ (𝐴 ∈ (⊥‘{𝐵}) ↔ (𝐴 ∈ ℋ ∧ (𝐴 ·ih 𝐵) = 0)) | ||
Theorem | h1dei 29333* | Membership in 1-dimensional subspace. (Contributed by NM, 7-Jul-2001.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
⊢ 𝐵 ∈ ℋ ⇒ ⊢ (𝐴 ∈ (⊥‘(⊥‘{𝐵})) ↔ (𝐴 ∈ ℋ ∧ ∀𝑥 ∈ ℋ ((𝐵 ·ih 𝑥) = 0 → (𝐴 ·ih 𝑥) = 0))) | ||
Theorem | h1did 29334 | A generating vector belongs to the 1-dimensional subspace it generates. (Contributed by NM, 22-Jul-2001.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → 𝐴 ∈ (⊥‘(⊥‘{𝐴}))) | ||
Theorem | h1dn0 29335 | A nonzero vector generates a (nonzero) 1-dimensional subspace. (Contributed by NM, 22-Jul-2001.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ) → (⊥‘(⊥‘{𝐴})) ≠ 0ℋ) | ||
Theorem | h1de2i 29336 | Membership in 1-dimensional subspace. All members are collinear with the generating vector. (Contributed by NM, 17-Jul-2001.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (𝐴 ∈ (⊥‘(⊥‘{𝐵})) → ((𝐵 ·ih 𝐵) ·ℎ 𝐴) = ((𝐴 ·ih 𝐵) ·ℎ 𝐵)) | ||
Theorem | h1de2bi 29337 | Membership in 1-dimensional subspace. All members are collinear with the generating vector. (Contributed by NM, 19-Jul-2001.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (𝐵 ≠ 0ℎ → (𝐴 ∈ (⊥‘(⊥‘{𝐵})) ↔ 𝐴 = (((𝐴 ·ih 𝐵) / (𝐵 ·ih 𝐵)) ·ℎ 𝐵))) | ||
Theorem | h1de2ctlem 29338* | Lemma for h1de2ci 29339. (Contributed by NM, 19-Jul-2001.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (𝐴 ∈ (⊥‘(⊥‘{𝐵})) ↔ ∃𝑥 ∈ ℂ 𝐴 = (𝑥 ·ℎ 𝐵)) | ||
Theorem | h1de2ci 29339* | Membership in 1-dimensional subspace. All members are collinear with the generating vector. (Contributed by NM, 21-Jul-2001.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
⊢ 𝐵 ∈ ℋ ⇒ ⊢ (𝐴 ∈ (⊥‘(⊥‘{𝐵})) ↔ ∃𝑥 ∈ ℂ 𝐴 = (𝑥 ·ℎ 𝐵)) | ||
Theorem | spansni 29340 | The span of a singleton in Hilbert space equals its closure. (Contributed by NM, 3-Jun-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ ⇒ ⊢ (span‘{𝐴}) = (⊥‘(⊥‘{𝐴})) | ||
Theorem | elspansni 29341* | Membership in the span of a singleton. (Contributed by NM, 3-Jun-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ ⇒ ⊢ (𝐵 ∈ (span‘{𝐴}) ↔ ∃𝑥 ∈ ℂ 𝐵 = (𝑥 ·ℎ 𝐴)) | ||
Theorem | spansn 29342 | The span of a singleton in Hilbert space equals its closure. (Contributed by NM, 4-Jun-2004.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (span‘{𝐴}) = (⊥‘(⊥‘{𝐴}))) | ||
Theorem | spansnch 29343 | The span of a Hilbert space singleton belongs to the Hilbert lattice. (Contributed by NM, 9-Jun-2004.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (span‘{𝐴}) ∈ Cℋ ) | ||
Theorem | spansnsh 29344 | The span of a Hilbert space singleton is a subspace. (Contributed by NM, 17-Dec-2004.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (span‘{𝐴}) ∈ Sℋ ) | ||
Theorem | spansnchi 29345 | The span of a singleton in Hilbert space is a closed subspace. (Contributed by NM, 3-Jun-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℋ ⇒ ⊢ (span‘{𝐴}) ∈ Cℋ | ||
Theorem | spansnid 29346 | A vector belongs to the span of its singleton. (Contributed by NM, 3-Jun-2004.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → 𝐴 ∈ (span‘{𝐴})) | ||
Theorem | spansnmul 29347 | A scalar product with a vector belongs to the span of its singleton. (Contributed by NM, 3-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℂ) → (𝐵 ·ℎ 𝐴) ∈ (span‘{𝐴})) | ||
Theorem | elspansncl 29348 | A member of a span of a singleton is a vector. (Contributed by NM, 17-Dec-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ (span‘{𝐴})) → 𝐵 ∈ ℋ) | ||
Theorem | elspansn 29349* | Membership in the span of a singleton. (Contributed by NM, 5-Jun-2004.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → (𝐵 ∈ (span‘{𝐴}) ↔ ∃𝑥 ∈ ℂ 𝐵 = (𝑥 ·ℎ 𝐴))) | ||
Theorem | elspansn2 29350 | Membership in the span of a singleton. All members are collinear with the generating vector. (Contributed by NM, 5-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐵 ≠ 0ℎ) → (𝐴 ∈ (span‘{𝐵}) ↔ 𝐴 = (((𝐴 ·ih 𝐵) / (𝐵 ·ih 𝐵)) ·ℎ 𝐵))) | ||
Theorem | spansncol 29351 | The singletons of collinear vectors have the same span. (Contributed by NM, 6-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (span‘{(𝐵 ·ℎ 𝐴)}) = (span‘{𝐴})) | ||
Theorem | spansneleqi 29352 | Membership relation implied by equality of spans. (Contributed by NM, 6-Jun-2004.) (New usage is discouraged.) |
⊢ (𝐴 ∈ ℋ → ((span‘{𝐴}) = (span‘{𝐵}) → 𝐴 ∈ (span‘{𝐵}))) | ||
Theorem | spansneleq 29353 | Membership relation that implies equality of spans. (Contributed by NM, 6-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ) → (𝐴 ∈ (span‘{𝐵}) → (span‘{𝐴}) = (span‘{𝐵}))) | ||
Theorem | spansnss 29354 | The span of the singleton of an element of a subspace is included in the subspace. (Contributed by NM, 5-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ 𝐴) → (span‘{𝐵}) ⊆ 𝐴) | ||
Theorem | elspansn3 29355 | A member of the span of the singleton of a vector is a member of a subspace containing the vector. (Contributed by NM, 16-Dec-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ (span‘{𝐵})) → 𝐶 ∈ 𝐴) | ||
Theorem | elspansn4 29356 | A span membership condition implying two vectors belong to the same subspace. (Contributed by NM, 17-Dec-2004.) (New usage is discouraged.) |
⊢ (((𝐴 ∈ Sℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ (span‘{𝐵}) ∧ 𝐶 ≠ 0ℎ)) → (𝐵 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴)) | ||
Theorem | elspansn5 29357 | A vector belonging to both a subspace and the span of the singleton of a vector not in it must be zero. (Contributed by NM, 17-Dec-2004.) (New usage is discouraged.) |
⊢ (𝐴 ∈ Sℋ → (((𝐵 ∈ ℋ ∧ ¬ 𝐵 ∈ 𝐴) ∧ (𝐶 ∈ (span‘{𝐵}) ∧ 𝐶 ∈ 𝐴)) → 𝐶 = 0ℎ)) | ||
Theorem | spansnss2 29358 | The span of the singleton of an element of a subspace is included in the subspace. (Contributed by NM, 16-Dec-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ ℋ) → (𝐵 ∈ 𝐴 ↔ (span‘{𝐵}) ⊆ 𝐴)) | ||
Theorem | normcan 29359 | Cancellation-type law that "extracts" a vector 𝐴 from its inner product with a proportional vector 𝐵. (Contributed by NM, 18-Mar-2006.) (New usage is discouraged.) |
⊢ ((𝐵 ∈ ℋ ∧ 𝐵 ≠ 0ℎ ∧ 𝐴 ∈ (span‘{𝐵})) → (((𝐴 ·ih 𝐵) / ((normℎ‘𝐵)↑2)) ·ℎ 𝐵) = 𝐴) | ||
Theorem | pjspansn 29360 | A projection on the span of a singleton. (The proof ws shortened by Mario Carneiro, 15-Dec-2013.) (Contributed by NM, 28-May-2006.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ) → ((projℎ‘(span‘{𝐴}))‘𝐵) = (((𝐵 ·ih 𝐴) / ((normℎ‘𝐴)↑2)) ·ℎ 𝐴)) | ||
Theorem | spansnpji 29361 | A subset of Hilbert space is orthogonal to the span of the singleton of a projection onto its orthocomplement. (Contributed by NM, 4-Jun-2004.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
⊢ 𝐴 ⊆ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ 𝐴 ⊆ (⊥‘(span‘{((projℎ‘(⊥‘𝐴))‘𝐵)})) | ||
Theorem | spanunsni 29362 | The span of the union of a closed subspace with a singleton equals the span of its union with an orthogonal singleton. (Contributed by NM, 3-Jun-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (span‘(𝐴 ∪ {𝐵})) = (span‘(𝐴 ∪ {((projℎ‘(⊥‘𝐴))‘𝐵)})) | ||
Theorem | spanpr 29363 | The span of a pair of vectors. (Contributed by NM, 9-Jun-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (span‘{(𝐴 +ℎ 𝐵)}) ⊆ (span‘{𝐴, 𝐵})) | ||
Theorem | h1datomi 29364 | A 1-dimensional subspace is an atom. (Contributed by NM, 20-Jul-2001.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (𝐴 ⊆ (⊥‘(⊥‘{𝐵})) → (𝐴 = (⊥‘(⊥‘{𝐵})) ∨ 𝐴 = 0ℋ)) | ||
Theorem | h1datom 29365 | A 1-dimensional subspace is an atom. (Contributed by NM, 22-Jul-2001.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ ℋ) → (𝐴 ⊆ (⊥‘(⊥‘{𝐵})) → (𝐴 = (⊥‘(⊥‘{𝐵})) ∨ 𝐴 = 0ℋ))) | ||
Definition | df-cm 29366* | Define the commutes relation (on the Hilbert lattice). Definition of commutes in [Kalmbach] p. 20, who uses the notation xCy for "x commutes with y." See cmbri 29373 for membership relation. (Contributed by NM, 14-Jun-2004.) (New usage is discouraged.) |
⊢ 𝐶ℋ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ 𝑥 = ((𝑥 ∩ 𝑦) ∨ℋ (𝑥 ∩ (⊥‘𝑦))))} | ||
Theorem | cmbr 29367 | 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 29368 | Variation of orthomodular law. Definition in [Kalmbach] p. 22. (Contributed by NM, 31-Oct-2000.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∨ℋ ((⊥‘𝐴) ∩ 𝐵)) = 𝐵) | ||
Theorem | pjoml3i 29369 | Variation of orthomodular law. (Contributed by NM, 24-Jun-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐵 ⊆ 𝐴 → (𝐴 ∩ ((⊥‘𝐴) ∨ℋ 𝐵)) = 𝐵) | ||
Theorem | pjoml4i 29370 | Variation of orthomodular law. (Contributed by NM, 6-Dec-2000.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ∨ℋ (𝐵 ∩ ((⊥‘𝐴) ∨ℋ (⊥‘𝐵)))) = (𝐴 ∨ℋ 𝐵) | ||
Theorem | pjoml5i 29371 | The orthomodular law. Remark in [Kalmbach] p. 22. (Contributed by NM, 12-Jun-2006.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ∨ℋ ((⊥‘𝐴) ∩ (𝐴 ∨ℋ 𝐵))) = (𝐴 ∨ℋ 𝐵) | ||
Theorem | pjoml6i 29372* | 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 29373 | 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 29374 | Commutation is symmetric. Theorem 3.4 of [Beran] p. 45. (Contributed by NM, 3-Nov-2000.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 𝐶ℋ 𝐵 → 𝐵 𝐶ℋ 𝐴) | ||
Theorem | cmcmi 29375 | Commutation is symmetric. Theorem 2(v) of [Kalmbach] p. 22. (Contributed by NM, 4-Nov-2000.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 𝐶ℋ 𝐵 ↔ 𝐵 𝐶ℋ 𝐴) | ||
Theorem | cmcm2i 29376 | 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 29377 | Commutation with orthocomplement. Remark in [Kalmbach] p. 23. (Contributed by NM, 4-Nov-2000.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 𝐶ℋ 𝐵 ↔ (⊥‘𝐴) 𝐶ℋ 𝐵) | ||
Theorem | cmcm4i 29378 | Commutation with orthocomplement. Remark in [Kalmbach] p. 23. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 𝐶ℋ 𝐵 ↔ (⊥‘𝐴) 𝐶ℋ (⊥‘𝐵)) | ||
Theorem | cmbr2i 29379 | 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 29380 | Commutation is symmetric. Theorem 2(v) of [Kalmbach] p. 22. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐴 𝐶ℋ 𝐵 ⇒ ⊢ 𝐵 𝐶ℋ 𝐴 | ||
Theorem | cmcm2ii 29381 | 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 29382 | Commutation with orthocomplement. Remark in [Kalmbach] p. 23. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐴 𝐶ℋ 𝐵 ⇒ ⊢ (⊥‘𝐴) 𝐶ℋ 𝐵 | ||
Theorem | cmbr3i 29383 | 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 29384 | Alternate definition for the commutes relation. (Contributed by NM, 6-Dec-2000.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 𝐶ℋ 𝐵 ↔ (𝐴 ∩ ((⊥‘𝐴) ∨ℋ 𝐵)) ⊆ 𝐵) | ||
Theorem | lecmi 29385 | 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 29386 | 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 29387 | A Hilbert lattice element commutes with its join. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ 𝐴 𝐶ℋ (𝐴 ∨ℋ 𝐵) | ||
Theorem | cmj2i 29388 | A Hilbert lattice element commutes with its join. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ 𝐵 𝐶ℋ (𝐴 ∨ℋ 𝐵) | ||
Theorem | cmm1i 29389 | A Hilbert lattice element commutes with its meet. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ 𝐴 𝐶ℋ (𝐴 ∩ 𝐵) | ||
Theorem | cmm2i 29390 | A Hilbert lattice element commutes with its meet. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ 𝐵 𝐶ℋ (𝐴 ∩ 𝐵) | ||
Theorem | cmbr3 29391 | 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 29392 | The zero Hilbert lattice element commutes with every element. (Contributed by NM, 16-Jun-2006.) (New usage is discouraged.) |
⊢ (𝐴 ∈ Cℋ → 0ℋ 𝐶ℋ 𝐴) | ||
Theorem | cmidi 29393 | The commutes relation is reflexive. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ ⇒ ⊢ 𝐴 𝐶ℋ 𝐴 | ||
Theorem | pjoml2 29394 | Variation of orthomodular law. Definition in [Kalmbach] p. 22. (Contributed by NM, 13-Jun-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐴 ⊆ 𝐵) → (𝐴 ∨ℋ ((⊥‘𝐴) ∩ 𝐵)) = 𝐵) | ||
Theorem | pjoml3 29395 | Variation of orthomodular law. (Contributed by NM, 24-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐵 ⊆ 𝐴 → (𝐴 ∩ ((⊥‘𝐴) ∨ℋ 𝐵)) = 𝐵)) | ||
Theorem | pjoml5 29396 | The orthomodular law. Remark in [Kalmbach] p. 22. (Contributed by NM, 12-Jun-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ∨ℋ ((⊥‘𝐴) ∩ (𝐴 ∨ℋ 𝐵))) = (𝐴 ∨ℋ 𝐵)) | ||
Theorem | cmcm 29397 | Commutation is symmetric. Theorem 2(v) of [Kalmbach] p. 22. (Contributed by NM, 13-Jun-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝐶ℋ 𝐵 ↔ 𝐵 𝐶ℋ 𝐴)) | ||
Theorem | cmcm3 29398 | Commutation with orthocomplement. Remark in [Kalmbach] p. 23. (Contributed by NM, 13-Jun-2006.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝐶ℋ 𝐵 ↔ (⊥‘𝐴) 𝐶ℋ 𝐵)) | ||
Theorem | cmcm2 29399 | 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 29400 | 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ℋ ∧ 𝐴 ⊆ 𝐵) → 𝐴 𝐶ℋ 𝐵) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |