Home(or GIF version for IE).
| Home |
Metamath Proof Explorer | < Previous Next > |
| Bad symbols?
Use Mozilla (or GIF version for IE). |
| Color key: | Metamath Proof
Explorer
(1-4957)
|
Hilbert Space Explorer
(4958-5787)
|
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | cmcm 5501 | Commutation is symmetric. Theorem 2(v) of [Kalmbach] p. 22. |
| ⊢ A ∈ Cℋ & ⊢ B ∈ Cℋ ⇒ ⊢ (A Com B ↔ B Com A) | ||
| Theorem | cmcm2 5502 | Commutation with orthocomplement. Theorem 2.3(i) of [Beran] p. 39. |
| ⊢ A ∈ Cℋ & ⊢ B ∈ Cℋ ⇒ ⊢ (A Com B ↔ A Com (⊥ ‘B)) | ||
| Theorem | cmcm3 5503 | Commutation with orthocomplement. Remark in [Kalmbach] p. 23. |
| ⊢ A ∈ Cℋ & ⊢ B ∈ Cℋ ⇒ ⊢ (A Com B ↔ (⊥ ‘A) Com B) | ||
| Theorem | cmcm4 5504 | Commutation with orthocomplement. Remark in [Kalmbach] p. 23. |
| ⊢ A ∈ Cℋ & ⊢ B ∈ Cℋ ⇒ ⊢ (A Com B ↔ (⊥ ‘A) Com (⊥ ‘B)) | ||
| Theorem | cmbr2 5505 | Alternate definition of the commutes relation. Remark in [Kalmbach] p. 23. |
| ⊢ A ∈ Cℋ & ⊢ B ∈ Cℋ ⇒ ⊢ (A Com B ↔ A = ((A ∨ℋ B) ∩ (A ∨ℋ (⊥ ‘B)))) | ||
| Theorem | cmcmi 5506 | Commutation is symmetric. Theorem 2(v) of [Kalmbach] p. 22. |
| ⊢ A ∈ Cℋ & ⊢ B ∈ Cℋ & ⊢ A Com B ⇒ ⊢ B Com A | ||
| Theorem | cmcm2i 5507 | Commutation with orthocomplement. Theorem 2.3(i) of [Beran] p. 39. |
| ⊢ A ∈ Cℋ & ⊢ B ∈ Cℋ & ⊢ A Com B ⇒ ⊢ A Com (⊥ ‘B) | ||
| Theorem | cmcm3i 5508 | Commutation with orthocomplement. Remark of [Kalmbach] p. 23. |
| ⊢ A ∈ Cℋ & ⊢ B ∈ Cℋ & ⊢ A Com B ⇒ ⊢ (⊥ ‘A) Com B | ||
| Theorem | cmbr3 5509 | Alternate definition for the commutes relation. Lemma 3 of [Kalmbach] p. 23. |
| ⊢ A ∈ Cℋ & ⊢ B ∈ Cℋ ⇒ ⊢ (A Com B ↔ (A ∩ ((⊥ ‘A) ∨ℋ B)) = (A ∩ B)) | ||
| Theorem | cmbr4 5510 | Alternate definition for the commutes relation. |
| ⊢ A ∈ Cℋ & ⊢ B ∈ Cℋ ⇒ ⊢ (A Com B ↔ (A ∩ ((⊥ ‘A) ∨ℋ B)) ⊆ B) | ||
| Theorem | cmle 5511 | Comparable Hilbert lattice elements commute. Theorem 2.3(iii) of [Beran] p. 40. |
| ⊢ A ∈ Cℋ & ⊢ B ∈ Cℋ & ⊢ A ⊆ B ⇒ ⊢ A Com B | ||
| Theorem | cmj1 5512 | A Hilbert lattice element commutes with its join. |
| ⊢ A ∈ Cℋ & ⊢ B ∈ Cℋ ⇒ ⊢ A Com (A ∨ℋ B) | ||
| Theorem | cmj2 5513 | A Hilbert lattice element commutes with its join. |
| ⊢ A ∈ Cℋ & ⊢ B ∈ Cℋ ⇒ ⊢ B Com (A ∨ℋ B) | ||
| Theorem | cmm1 5514 | A Hilbert lattice element commutes with its meet. |
| ⊢ A ∈ Cℋ & ⊢ B ∈ Cℋ ⇒ ⊢ A Com (A ∩ B) | ||
| Theorem | cmm2 5515 | A Hilbert lattice element commutes with its meet. |
| ⊢ A ∈ Cℋ & ⊢ B ∈ Cℋ ⇒ ⊢ B Com (A ∩ B) | ||
| Theorem | cmid 5516 | The commutes relation is reflexive. |
| ⊢ A ∈ Cℋ ⇒ ⊢ A Com A | ||
| Theorem | pjoml3t 5517 | Variation of orthomodular law. |
| ⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ) → (B ⊆ A → (A ∩ ((⊥ ‘A) ∨ℋ B)) = B)) | ||
| Theorem | fh1 5518 | Foulis-Holland Theorem. If any 2 pairs in a triple of orthomodular lattice elements commute, the triple is distributive. First of two parts. Theorem 5 of [Kalmbach] p. 25. |
| ⊢ A ∈ Cℋ & ⊢ B ∈ Cℋ & ⊢ C ∈ Cℋ & ⊢ A Com B & ⊢ A Com C ⇒ ⊢ (A ∩ (B ∨ℋ C)) = ((A ∩ B) ∨ℋ (A ∩ C)) | ||
| Theorem | fh2 5519 | Foulis-Holland Theorem. If any 2 pairs in a triple of orthomodular lattice elements commute, the triple is distributive. Second of two parts. Theorem 5 of [Kalmbach] p. 25. |
| ⊢ A ∈ Cℋ & ⊢ B ∈ Cℋ & ⊢ C ∈ Cℋ & ⊢ A Com B & ⊢ A Com C ⇒ ⊢ (B ∩ (A ∨ℋ C)) = ((B ∩ A) ∨ℋ (B ∩ C)) | ||
| Theorem | qlax1 5520 | One of the equations showing Cℋ is an ortholattice. (This corresponds to axiom "ax-1" in the Quantum Logic Explorer.) |
| ⊢ A ∈ Cℋ ⇒ ⊢ A = (⊥ ‘(⊥ ‘A)) | ||
| Theorem | qlax2 5521 | One of the equations showing Cℋ is an ortholattice. (This corresponds to axiom "ax-2" in the Quantum Logic Explorer.) |
| ⊢ A ∈ Cℋ & ⊢ B ∈ Cℋ ⇒ ⊢ (A ∨ℋ B) = (B ∨ℋ A) | ||
| Theorem | qlax3 5522 | One of the equations showing Cℋ is an ortholattice. (This corresponds to axiom "ax-3" in the Quantum Logic Explorer.) |
| ⊢ A ∈ Cℋ & ⊢ B ∈ Cℋ & ⊢ C ∈ Cℋ ⇒ ⊢ ((A ∨ℋ B) ∨ℋ C) = (A ∨ℋ (B ∨ℋ C)) | ||
| Theorem | qlax4 5523 | One of the equations showing Cℋ is an ortholattice. (This corresponds to axiom "ax-4" in the Quantum Logic Explorer.) |
| ⊢ A ∈ Cℋ & ⊢ B ∈ Cℋ ⇒ ⊢ (A ∨ℋ (B ∨ℋ (⊥ ‘B))) = (B ∨ℋ (⊥ ‘B)) | ||
| Theorem | qlax5 5524 | One of the equations showing Cℋ is an ortholattice. (This corresponds to axiom "ax-5" in the Quantum Logic Explorer.) |
| ⊢ A ∈ Cℋ & ⊢ B ∈ Cℋ ⇒ ⊢ (A ∨ℋ (⊥ ‘((⊥ ‘A) ∨ℋ B))) = A | ||
| Theorem | qlaxr1 5525 | One of the conditions showing Cℋ is an ortholattice. (This corresponds to axiom "ax-r1" in the Quantum Logic Explorer.) |
| ⊢ A ∈ Cℋ & ⊢ B ∈ Cℋ & ⊢ A = B ⇒ ⊢ B = A | ||
| Theorem | qlaxr2 5526 | One of the conditions showing Cℋ is an ortholattice. (This corresponds to axiom "ax-r2" in the Quantum Logic Explorer.) |
| ⊢ A ∈ Cℋ & ⊢ B ∈ Cℋ & ⊢ C ∈ Cℋ & ⊢ A = B & ⊢ B = C ⇒ ⊢ A = C | ||
| Theorem | qlaxr4 5527 | One of the conditions showing Cℋ is an ortholattice. (This corresponds to axiom "ax-r4" in the Quantum Logic Explorer.) |
| ⊢ A ∈ Cℋ & ⊢ B ∈ Cℋ & ⊢ A = B ⇒ ⊢ (⊥ ‘A) = (⊥ ‘B) | ||
| Theorem | qlaxr5 5528 | One of the conditions showing Cℋ is an ortholattice. (This corresponds to axiom "ax-r5" in the Quantum Logic Explorer.) |
| ⊢ A ∈ Cℋ & ⊢ B ∈ Cℋ & ⊢ C ∈ Cℋ & ⊢ A = B ⇒ ⊢ (A ∨ℋ C) = (B ∨ℋ C) | ||
| Theorem | qlaxr3 5529 | A variation of the orthomodular law, showing Cℋ is an orthomodular lattice. (This corresponds to axiom "ax-r3" in the Quantum Logic Explorer.) |
| ⊢ A ∈ Cℋ & ⊢ B ∈ Cℋ & ⊢ C ∈ Cℋ & ⊢ (C ∨ℋ (⊥ ‘C)) = ((⊥ ‘((⊥ ‘A) ∨ℋ (⊥ ‘B))) ∨ℋ (⊥ ‘(A ∨ℋ B))) ⇒ ⊢ A = B | ||
| Theorem | osumlem1 5530 | Lemma for osum 5538. |
| ⊢ A ∈ Cℋ & ⊢ B ∈ Cℋ & ⊢ B ⊆ (⊥ ‘A) & ⊢ (φ ↔ (((C ∈ A ∧ D ∈ B) ∧ R = (C +v D)) ∧ ((x ∈ A ∧ y ∈ (⊥ ‘A)) ∧ z = (x +v y)))) ⇒ ⊢ (φ → (((C ∈ ℋ ∧ D ∈ ℋ ) ∧ R ∈ ℋ ) ∧ ((x ∈ ℋ ∧ y ∈ ℋ ) ∧ z ∈ ℋ ))) | ||
| Theorem | osumlem2 5531 | Lemma for osum 5538. |
| ⊢ A ∈ Cℋ & ⊢ B ∈ Cℋ & ⊢ B ⊆ (⊥ ‘A) & ⊢ (φ ↔ (((C ∈ A ∧ D ∈ B) ∧ R = (C +v D)) ∧ ((x ∈ A ∧ y ∈ (⊥ ‘A)) ∧ z = (x +v y)))) ⇒ ⊢ (φ → (((norm ‘(C −v x))↑2) + ((norm ‘(D −v y))↑2)) = ((norm ‘(R −v z))↑2)) | ||
| Theorem | osumlem3 5532 | Lemma for osum 5538. |
| ⊢ A ∈ Cℋ & ⊢ B ∈ Cℋ & ⊢ B ⊆ (⊥ ‘A) & ⊢ (φ ↔ (((C ∈ A ∧ D ∈ B) ∧ R = (C +v D)) ∧ ((x ∈ A ∧ y ∈ (⊥ ‘A)) ∧ z = (x +v y)))) ⇒ ⊢ (φ → (norm ‘(D −v y)) ≤ (norm ‘(R −v z))) | ||
| Theorem | osumlem4 5533 | Lemma for osum 5538. |
| ⊢ A ∈ Cℋ & ⊢ B ∈ Cℋ & ⊢ B ⊆ (⊥ ‘A) & ⊢ G ∈ V & ⊢ H ∈ V ⇒ ⊢ ((((F:ℕ–→A ∧ G:ℕ–→B) ∧ ∀w ∈ ℕ (H ‘w) = ((F ‘w) +v (G ‘w))) ∧ ((x ∈ A ∧ y ∈ (⊥ ‘A)) ∧ z = (x +v y))) → (H ⇝v z → G ⇝v y)) | ||
| Theorem | osumlem5 5534 | Lemma for osum 5538. |
| ⊢ A ∈ Cℋ & ⊢ B ∈ Cℋ ⇒ ⊢ (H:ℕ–→(A +ℋ B) → ∃f∃g((f:ℕ–→A ∧ g:ℕ–→B) ∧ ∀w ∈ ℕ (H ‘w) = ((f ‘w) +v (g ‘w)))) | ||
| Theorem | osumlem6 5535 | Lemma for osum 5538. |
| ⊢ A ∈ Cℋ & ⊢ B ∈ Cℋ & ⊢ B ⊆ (⊥ ‘A) & ⊢ H ∈ V ⇒ ⊢ (((H:ℕ–→(A +ℋ B) ∧ H ⇝v z) ∧ ((x ∈ A ∧ y ∈ (⊥ ‘A)) ∧ z = (x +v y))) → y ∈ B) | ||
| Theorem | osumlem7 5536 | Lemma for osum 5538. |
| ⊢ A ∈ Cℋ & ⊢ B ∈ Cℋ & ⊢ B ⊆ (⊥ ‘A) ⇒ ⊢ (A +ℋ B) ∈ Cℋ | ||
| Theorem | osumlem8 5537 | Lemma for osum 5538. |
| ⊢ A ∈ Cℋ & ⊢ B ∈ Cℋ ⇒ ⊢ (B ⊆ (⊥ ‘A) → (A +ℋ B) ∈ Cℋ ) | ||
| Theorem | osum 5538 | If two closed subspaces of a Hilbert space are orthogonal, their subspace sum equals their subspace join. Lemma 3 of [Kalmbach] p. 67. Note that the Axiom of Choice is used for this proof (in osumlem5 5534 and via pjpjtht 5262 in osumlem7 5536). |
| ⊢ A ∈ Cℋ & ⊢ B ∈ Cℋ ⇒ ⊢ (A ⊆ (⊥ ‘B) → (A +ℋ B) = (A ∨ℋ B)) | ||
| Theorem | spansnj 5539 | The subspace sum of a closed subspace and a one-dimensional subspace equals their join. (Proof suggested by Eric Schechter 1-Jun-04.) |
| ⊢ A ∈ Cℋ & ⊢ B ∈ ℋ ⇒ ⊢ (A +ℋ (span ‘{B})) = (A ∨ℋ (span ‘{B})) | ||
| Theorem | spansnjt 5540 | The subspace sum of a closed subspace and a one-dimensional subspace equals their join. |
| ⊢ ((A ∈ Cℋ ∧ B ∈ ℋ ) → (A +ℋ (span ‘{B})) = (A ∨ℋ (span ‘{B}))) | ||
| Theorem | spansnsclt 5541 | The subspace sum of a closed subspace and a one-dimensional subspace is closed. |
| ⊢ ((A ∈ Cℋ ∧ B ∈ ℋ ) → (A +ℋ (span ‘{B})) ∈ Cℋ ) | ||
| Theorem | spansncv 5542 | Hilbert space has the covering property (using spans of singletons to represent atoms). Exercise 5 of [Kalmbach] p. 153. |
| ⊢ A ∈ Cℋ & ⊢ B ∈ Cℋ & ⊢ C ∈ ℋ ⇒ ⊢ ((A ⊂ B ∧ B ⊆ (A ∨ℋ (span ‘{C}))) → B = (A ∨ℋ (span ‘{C}))) | ||
| Theorem | spansncvt 5543 | Hilbert space has the covering property (using spans of singletons to represent atoms). Exercise 5 of [Kalmbach] p. 153. |
| ⊢ ((A ∈ Cℋ ∧ B ∈ Cℋ ∧ C ∈ ℋ ) → ((A ⊂ B ∧ B ⊆ (A ∨ℋ (span ‘{C}))) → B = (A ∨ℋ (span ‘{C})))) | ||
| Theorem | 5oalem1 5544 | Lemma for orthoarguesian law 5OA. |
| ⊢ A ∈ Sℋ & ⊢ B ∈ Sℋ & ⊢ C ∈ Sℋ & ⊢ R ∈ Sℋ ⇒ ⊢ ((((x ∈ A ∧ y ∈ B) ∧ v = (x +v y)) ∧ (z ∈ C ∧ (x −v z) ∈ R)) → v ∈ (B +ℋ (A ∩ (C +ℋ R)))) | ||
| Theorem | 5oalem2 5545 | Lemma for orthoarguesian law 5OA. |
| ⊢ A ∈ Sℋ & ⊢ B ∈ Sℋ & ⊢ C ∈ Sℋ & ⊢ D ∈ Sℋ ⇒ ⊢ ((((x ∈ A ∧ y ∈ B) ∧ (z ∈ C ∧ w ∈ D)) ∧ (x +v y) = (z +v w)) → (x −v z) ∈ ((A +ℋ C) ∩ (B +ℋ D))) | ||
| Theorem | 5oalem3 5546 | Lemma for orthoarguesian law 5OA. |
| ⊢ A ∈ Sℋ & ⊢ B ∈ Sℋ & ⊢ C ∈ Sℋ & ⊢ D ∈ Sℋ & ⊢ F ∈ Sℋ & ⊢ G ∈ Sℋ ⇒ ⊢ (((((x ∈ A ∧ y ∈ B) ∧ (z ∈ C ∧ w ∈ D)) ∧ (f ∈ F ∧ g ∈ G)) ∧ ((x +v y) = (f +v g) ∧ (z +v w) = (f +v g))) → (x −v z) ∈ (((A +ℋ F) ∩ (B +ℋ G)) +ℋ ((C +ℋ F) ∩ (D +ℋ G)))) | ||
| Theorem | 5oalem4 5547 | Lemma for orthoarguesian law 5OA. |
| ⊢ A ∈ Sℋ & ⊢ B ∈ Sℋ & ⊢ C ∈ Sℋ & ⊢ D ∈ Sℋ & ⊢ F ∈ Sℋ & ⊢ G ∈ Sℋ ⇒ ⊢ (((((x ∈ A ∧ y ∈ B) ∧ (z ∈ C ∧ w ∈ D)) ∧ (f ∈ F ∧ g ∈ G)) ∧ ((x +v y) = (f +v g) ∧ (z +v w) = (f +v g))) → (x −v z) ∈ (((A +ℋ C) ∩ (B +ℋ D)) ∩ (((A +ℋ F) ∩ (B +ℋ G)) +ℋ ((C +ℋ F) ∩ (D +ℋ G))))) | ||
| Theorem | 5oalem5 5548 | Lemma for orthoarguesian law 5OA. |
| ⊢ A ∈ Sℋ & ⊢ B ∈ Sℋ & ⊢ C ∈ Sℋ & ⊢ D ∈ Sℋ & ⊢ F ∈ Sℋ & ⊢ G ∈ Sℋ & ⊢ R ∈ Sℋ & ⊢ S ∈ Sℋ ⇒ ⊢ (((((x ∈ A ∧ y ∈ B) ∧ (z ∈ C ∧ w ∈ D)) ∧ ((f ∈ F ∧ g ∈ G) ∧ (v ∈ R ∧ u ∈ S))) ∧ (((x +v y) = (v +v u) ∧ (z +v w) = (v +v u)) ∧ (f +v g) = (v +v u))) → (x −v z) ∈ ((((A +ℋ C) ∩ (B +ℋ D)) ∩ (((A +ℋ R) ∩ (B +ℋ S)) +ℋ ((C +ℋ R) ∩ (D +ℋ S)))) ∩ ((((A +ℋ F) ∩ (B +ℋ G)) ∩ (((A +ℋ R) ∩ (B +ℋ S)) +ℋ ((F +ℋ R) ∩ (G +ℋ S)))) +ℋ (((C +ℋ F) ∩ (D +ℋ G)) ∩ (((C +ℋ R) ∩ (D +ℋ S)) +ℋ ((F +ℋ R) ∩ (G +ℋ S))))))) | ||
| Theorem | 5oalem6 5549 | Lemma for orthoarguesian law 5OA. |
| ⊢ A ∈ Sℋ & ⊢ B ∈ Sℋ & ⊢ C ∈ Sℋ & ⊢ D ∈ Sℋ & ⊢ F ∈ Sℋ & ⊢ G ∈ Sℋ & ⊢ R ∈ Sℋ & ⊢ S ∈ Sℋ ⇒ ⊢ (((((x ∈ A ∧ y ∈ B) ∧ h = (x +v y)) ∧ ((z ∈ C ∧ w ∈ D) ∧ h = (z +v w))) ∧ (((f ∈ F ∧ g ∈ G) ∧ h = (f +v g)) ∧ ((v ∈ R ∧ u ∈ S) ∧ h = (v +v u)))) → h ∈ (B +ℋ (A ∩ (C +ℋ ((((A +ℋ C) ∩ (B +ℋ D)) ∩ (((A +ℋ R) ∩ (B +ℋ S)) +ℋ ((C +ℋ R) ∩ (D +ℋ S)))) ∩ ((((A +ℋ F) ∩ (B +ℋ G)) ∩ (((A +ℋ R) ∩ (B +ℋ S)) +ℋ ((F +ℋ R) ∩ (G +ℋ S)))) +ℋ (((C +ℋ F) ∩ (D +ℋ G)) ∩ (((C +ℋ R) ∩ (D +ℋ S)) +ℋ ((F +ℋ R) ∩ (G +ℋ S)))))))))) | ||
| Theorem | 5oalem7 5550 | Lemma for orthoarguesian law 5OA. |
| ⊢ A ∈ Sℋ & ⊢ B ∈ Sℋ & ⊢ C ∈ Sℋ & ⊢ D ∈ Sℋ & ⊢ F ∈ Sℋ & ⊢ G ∈ Sℋ & ⊢ R ∈ Sℋ & ⊢ S ∈ Sℋ ⇒ ⊢ (((A +ℋ B) ∩ (C +ℋ D)) ∩ ((F +ℋ G) ∩ (R +ℋ S))) ⊆ (B +ℋ (A ∩ (C +ℋ ((((A +ℋ C) ∩ (B +ℋ D)) ∩ (((A +ℋ R) ∩ (B +ℋ S)) +ℋ ((C +ℋ R) ∩ (D +ℋ S)))) ∩ ((((A +ℋ F) ∩ (B +ℋ G)) ∩ (((A +ℋ R) ∩ (B +ℋ S)) +ℋ ((F +ℋ R) ∩ (G +ℋ S)))) +ℋ (((C +ℋ F) ∩ (D +ℋ G)) ∩ (((C +ℋ R) ∩ (D +ℋ S)) +ℋ ((F +ℋ R) ∩ (G +ℋ S))))))))) | ||
| Theorem | 5oa 5551 | Orthoarguesian law 5OA. This 8-variable inference is called 5OA because it can be converted to a 5-variable equation (see Quantum Logic Explorer). |
| ⊢ A ∈ Cℋ & ⊢ B ∈ Cℋ & ⊢ C ∈ Cℋ & ⊢ D ∈ Cℋ & ⊢ F ∈ Cℋ & ⊢ G ∈ Cℋ & ⊢ R ∈ Cℋ & ⊢ S ∈ Cℋ & ⊢ A ⊆ (⊥ ‘B) & ⊢ C ⊆ (⊥ ‘D) & ⊢ F ⊆ (⊥ ‘G) & ⊢ R ⊆ (⊥ ‘S) ⇒ ⊢ (((A ∨ℋ B) ∩ (C ∨ℋ D)) ∩ ((F ∨ℋ G) ∩ (R ∨ℋ S))) ⊆ (B ∨ℋ (A ∩ (C ∨ℋ ((((A ∨ℋ C) ∩ (B ∨ℋ D)) ∩ (((A ∨ℋ R) ∩ (B ∨ℋ S)) ∨ℋ ((C ∨ℋ R) ∩ (D ∨ℋ S)))) ∩ ((((A ∨ℋ F) ∩ (B ∨ℋ G)) ∩ (((A ∨ℋ R) ∩ (B ∨ℋ S)) ∨ℋ ((F ∨ℋ R) ∩ (G ∨ℋ S)))) ∨ℋ (((C ∨ℋ F) ∩ (D ∨ℋ G)) ∩ (((C ∨ℋ R) ∩ (D ∨ℋ S)) ∨ℋ ((F ∨ℋ R) ∩ (G ∨ℋ S))))))))) | ||
| Theorem | 3oalem1 5552 | Lemma for 3OA (weak) orthoarguesian law. |
| ⊢ B ∈ Cℋ & ⊢ C ∈ Cℋ & ⊢ R ∈ Cℋ & ⊢ S ∈ Cℋ ⇒ ⊢ ((((x ∈ B ∧ y ∈ R) ∧ v = (x +v y)) ∧ ((z ∈ C ∧ w ∈ S) ∧ v = (z +v w))) → (((x ∈ ℋ ∧ y ∈ ℋ ) ∧ v ∈ ℋ ) ∧ (z ∈ ℋ ∧ w ∈ ℋ ))) | ||
| Theorem | 3oalem2 5553 | Lemma for 3OA (weak) orthoarguesian law. |
| ⊢ B ∈ Cℋ & ⊢ C ∈ Cℋ & ⊢ R ∈ Cℋ & ⊢ S ∈ Cℋ ⇒ ⊢ ((((x ∈ B ∧ y ∈ R) ∧ v = (x +v y)) ∧ ((z ∈ C ∧ w ∈ S) ∧ v = (z +v w))) → v ∈ (B +ℋ (R ∩ (S +ℋ ((B +ℋ C) ∩ (R +ℋ S)))))) | ||
| Theorem | 3oalem3 5554 | Lemma for 3OA (weak) orthoarguesian law. |
| ⊢ B ∈ Cℋ & ⊢ C ∈ Cℋ & ⊢ R ∈ Cℋ & ⊢ S ∈ Cℋ ⇒ ⊢ ((B +ℋ R) ∩ (C +ℋ S)) ⊆ (B +ℋ (R ∩ (S +ℋ ((B +ℋ C) ∩ (R +ℋ S))))) | ||
| Theorem | 3oalem4 5555 | Lemma for 3OA (weak) orthoarguesian law. |
| ⊢ R = ((⊥ ‘B) ∩ (B ∨ℋ A)) ⇒ ⊢ R ⊆ (⊥ ‘B) | ||
| Theorem | 3oalem5 5556 | Lemma for 3OA (weak) orthoarguesian law. |
| ⊢ A ∈ Cℋ & ⊢ B ∈ Cℋ & ⊢ C ∈ Cℋ & ⊢ R = ((⊥ ‘B) ∩ (B ∨ℋ A)) & ⊢ S = ((⊥ ‘C) ∩ (C ∨ℋ A)) ⇒ ⊢ ((B +ℋ R) ∩ (C +ℋ S)) = ((B ∨ℋ R) ∩ (C ∨ℋ S)) | ||
| Theorem | 3oalem6 5557 | Lemma for 3OA (weak) orthoarguesian law. |
| ⊢ A ∈ Cℋ & ⊢ B ∈ Cℋ & ⊢ C ∈ Cℋ & ⊢ R = ((⊥ ‘B) ∩ (B ∨ℋ A)) & ⊢ S = ((⊥ ‘C) ∩ (C ∨ℋ A)) ⇒ ⊢ (B +ℋ (R ∩ (S +ℋ ((B +ℋ C) ∩ (R +ℋ S))))) ⊆ (B ∨ℋ (R ∩ (S ∨ℋ ((B ∨ℋ C) ∩ (R ∨ℋ S))))) | ||
| Theorem | 3oa 5558 | 3OA (weak) orthoarguesian law. Equation (IV) of [GodowskiGreechie] p. 249. |
| ⊢ A ∈ Cℋ & ⊢ B ∈ Cℋ & ⊢ C ∈ Cℋ & ⊢ R = ((⊥ ‘B) ∩ (B ∨ℋ A)) & ⊢ S = ((⊥ ‘C) ∩ (C ∨ℋ A)) ⇒ ⊢ ((B ∨ℋ R) ∩ (C ∨ℋ S)) ⊆ (B ∨ℋ (R ∩ (S ∨ℋ ((B ∨ℋ C) ∩ (R ∨ℋ S))))) | ||
| Theorem | pjorth 5559 | Projection components on orthocomplemented subspaces are orthogonal. |
| ⊢ A ∈ ℋ & ⊢ B ∈ ℋ ⇒ ⊢ (H ∈ Cℋ → (((Proj ‘H) ‘A) ·i ((Proj ‘(⊥ ‘H)) ‘B)) = 0) | ||
| Theorem | pjch1t 5560 | Property of identity projection. Remark of [Beran] p. 111. |
| ⊢ (A ∈ ℋ → ((Proj ‘ ℋ ) ‘A) = A) | ||
| Theorem | pjot 5561 | The orthogonal projection. Lemma 4.4(i) of [Beran] p. 111. |
| ⊢ ((H ∈ Cℋ ∧ A ∈ ℋ ) → ((Proj ‘(⊥ ‘H)) ‘A) = (((Proj ‘ ℋ ) ‘A) −v ((Proj ‘H) ‘A))) | ||
| Theorem | pjch0t 5562 | Property of the null projection. Remark of [Beran] p. 111. |
| ⊢ (A ∈ ℋ → ((Proj ‘0ℋ) ‘A) = 0v) | ||
| Theorem | pjidm 5563 | A projection is idempotent. Property (ii) of [Beran] p. 109. |
| ⊢ H ∈ Cℋ & ⊢ A ∈ ℋ ⇒ ⊢ ((Proj ‘H) ‘((Proj ‘H) ‘A)) = ((Proj ‘H) ‘A) | ||
| Theorem | pjadj 5564 | A projection is self-adjoint. Property (i) of [Beran] p. 109. |
| ⊢ H ∈ Cℋ & ⊢ A ∈ ℋ & ⊢ B ∈ ℋ ⇒ ⊢ (((Proj ‘H) ‘A) ·i B) = (A ·i ((Proj ‘H) ‘B)) | ||
| Theorem | pjcomp 5565 | Component of a projection. |
| ⊢ H ∈ Cℋ & ⊢ A ∈ ℋ & ⊢ B ∈ ℋ ⇒ ⊢ ((A ∈ H ∧ B ∈ (⊥ ‘H)) → ((Proj ‘H) ‘(A +v B)) = A) | ||
| Theorem | pjadd 5566 | Projection of vector sum is sum of projections. |
| ⊢ H ∈ Cℋ & ⊢ A ∈ ℋ & ⊢ B ∈ ℋ ⇒ ⊢ ((Proj ‘H) ‘(A +v B)) = (((Proj ‘H) ‘A) +v ((Proj ‘H) ‘B)) | ||
| Theorem | pjinorm 5567 | The inner product of a projection and its argument is the square of the norm of the projection. |
| ⊢ H ∈ Cℋ & ⊢ A ∈ ℋ ⇒ ⊢ (((Proj ‘H) ‘A) ·i A) = ((norm ‘((Proj ‘H) ‘A))↑2) | ||
| Theorem | pjmul 5568 | Projection of (scalar) product is product of projection. |
| ⊢ H ∈ Cℋ & ⊢ A ∈ ℋ & ⊢ C ∈ ℂ ⇒ ⊢ ((Proj ‘H) ‘(C ·s A)) = (C ·s ((Proj ‘H) ‘A)) | ||
| Theorem | pjsub 5569 | Projection of vector difference is difference of projections. |
| ⊢ H ∈ Cℋ & ⊢ A ∈ ℋ & ⊢ B ∈ ℋ ⇒ ⊢ ((Proj ‘H) ‘(A −v B)) = (((Proj ‘H) ‘A) −v ((Proj ‘H) ‘B)) | ||
| Theorem | pjsslem 5570 | Lemma for subset relationships of projections. |
| ⊢ H ∈ Cℋ & ⊢ A ∈ ℋ & ⊢ G ∈ Cℋ ⇒ ⊢ (((Proj ‘(⊥ ‘H)) ‘A) −v ((Proj ‘(⊥ ‘G)) ‘A)) = (((Proj ‘G) ‘A) −v ((Proj ‘H) ‘A)) | ||
| Theorem | pjss2 5571 | Subset relationship for projections. Theorem 4.5(i)->(ii) of [Beran] p. 112. |
| ⊢ H ∈ Cℋ & ⊢ A ∈ ℋ & ⊢ G ∈ Cℋ ⇒ ⊢ (H ⊆ G → ((Proj ‘H) ‘((Proj ‘G) ‘A)) = ((Proj ‘H) ‘A)) | ||
| Theorem | pjssm 5572 | Projection meet property. Remark of [Kalmbach] p. 66. Also Theorem 4.5(i)->(iv) of [Beran] p. 112. |
| ⊢ H ∈ Cℋ & ⊢ A ∈ ℋ & ⊢ G ∈ Cℋ ⇒ ⊢ (H ⊆ G → (((Proj ‘G) ‘A) −v ((Proj ‘H) ‘A)) = ((Proj ‘(G ∩ (⊥ ‘H))) ‘A)) | ||
| Theorem | pjssge0 5573 | Theorem 4.5(iv)->(v) of [Beran] p. 112. |
| ⊢ H ∈ Cℋ & ⊢ A ∈ ℋ & ⊢ G ∈ Cℋ ⇒ ⊢ ((((Proj ‘G) ‘A) −v ((Proj ‘H) ‘A)) = ((Proj ‘(G ∩ (⊥ ‘H))) ‘A) → 0 ≤ ((((Proj ‘G) ‘A) −v ((Proj ‘H) ‘A)) ·i A)) | ||
| Theorem | pjdifnorm 5574 | Theorem 4.5(v)<->(vi) of [Beran] p. 112. |
| ⊢ H ∈ Cℋ & ⊢ A ∈ ℋ & ⊢ G ∈ Cℋ ⇒ ⊢ (0 ≤ ((((Proj ‘G) ‘A) −v ((Proj ‘H) ‘A)) ·i A) ↔ (norm ‘((Proj ‘H) ‘A)) ≤ (norm ‘((Proj ‘G) ‘A))) | ||
| Theorem | pjcj 5575 | The projection on a subspace join is the sum of the projections. |
| ⊢ H ∈ Cℋ & ⊢ A ∈ ℋ & ⊢ G ∈ Cℋ ⇒ ⊢ (H ⊆ (⊥ ‘G) → ((Proj ‘(H ∨ℋ G)) ‘A) = (((Proj ‘H) ‘A) +v ((Proj ‘G) ‘A))) | ||
| Theorem | pjadjt 5576 | A projection is self-adjoint. Property (i) of [Beran] p. 109. |
| ⊢ H ∈ Cℋ ⇒ ⊢ ((A ∈ ℋ ∧ B ∈ ℋ ) → (((Proj ‘H) ‘A) ·i B) = (A ·i ((Proj ‘H) ‘B))) | ||
| Theorem | pjaddt 5577 | Projection of vector sum is sum of projections. |
| ⊢ H ∈ Cℋ ⇒ ⊢ ((A ∈ ℋ ∧ B ∈ ℋ ) → ((Proj ‘H) ‘(A +v B)) = (((Proj ‘H) ‘A) +v ((Proj ‘H) ‘B))) | ||
| Theorem | pjsubt 5578 | Projection of vector difference is difference of projections. |
| ⊢ H ∈ Cℋ ⇒ ⊢ ((A ∈ ℋ ∧ B ∈ ℋ ) → ((Proj ‘H) ‘(A −v B)) = (((Proj ‘H) ‘A) −v ((Proj ‘H) ‘B))) | ||
| Theorem | pjmult 5579 | Projection of scalar product is scalar product of projection. |
| ⊢ H ∈ Cℋ ⇒ ⊢ ((A ∈ ℂ ∧ B ∈ ℋ ) → ((Proj ‘H) ‘(A ·s B)) = (A ·s ((Proj ‘H) ‘B))) | ||
| Theorem | pjcjt2 5580 | The projection on a subspace join is the sum of the projections. |
| ⊢ ((H ∈ Cℋ ∧ G ∈ Cℋ ∧ A ∈ ℋ ) → (H ⊆ (⊥ ‘G) → ((Proj ‘(H ∨ℋ G)) ‘A) = (((Proj ‘H) ‘A) +v ((Proj ‘G) ‘A)))) | ||
| Theorem | pj0 5581 | The projection of the zero vector. |
| ⊢ H ∈ C< | ||