![]() |
Metamath
Proof Explorer Theorem List (p. 410 of 485) | < 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-30805) |
![]() (30806-32328) |
![]() (32329-48426) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dihglblem3aN 40901* | Isomorphism H of a lattice glb. (Contributed by NM, 7-Apr-2014.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = {𝑢 ∈ 𝐵 ∣ ∃𝑣 ∈ 𝑆 𝑢 = (𝑣 ∧ 𝑊)} & ⊢ 𝐽 = ((DIsoB‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ (𝐺‘𝑆) ≤ 𝑊) → (𝐼‘(𝐺‘𝑆)) = ∩ 𝑥 ∈ 𝑇 (𝐼‘𝑥)) | ||
Theorem | dihglblem4 40902* | Isomorphism H of a lattice glb. (Contributed by NM, 21-Mar-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = {𝑢 ∈ 𝐵 ∣ ∃𝑣 ∈ 𝑆 𝑢 = (𝑣 ∧ 𝑊)} & ⊢ 𝐽 = ((DIsoB‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) → (𝐼‘(𝐺‘𝑆)) ⊆ ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥)) | ||
Theorem | dihglblem5 40903* | Isomorphism H of a lattice glb. (Contributed by NM, 9-Apr-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑈) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑇 ⊆ 𝐵 ∧ 𝑇 ≠ ∅)) → ∩ 𝑥 ∈ 𝑇 (𝐼‘𝑥) ∈ 𝑆) | ||
Theorem | dihmeetlem2N 40904 | Isomorphism H of a conjunction. (Contributed by NM, 22-Mar-2014.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑃 = ((oc‘𝐾)‘𝑊) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝐺 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑞) & ⊢ 0 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵)) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌))) | ||
Theorem | dihglbcpreN 40905* | Isomorphism H of a lattice glb when the glb is not under the fiducial hyperplane 𝑊. (Contributed by NM, 20-Mar-2014.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑃 = ((oc‘𝐾)‘𝑊) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝐹 = (℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑞) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → (𝐼‘(𝐺‘𝑆)) = ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥)) | ||
Theorem | dihglbcN 40906* | Isomorphism H of a lattice glb when the glb is not under the fiducial hyperplane 𝑊. (Contributed by NM, 26-Mar-2014.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ ≤ = (le‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) ∧ ¬ (𝐺‘𝑆) ≤ 𝑊) → (𝐼‘(𝐺‘𝑆)) = ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥)) | ||
Theorem | dihmeetcN 40907 | Isomorphism H of a lattice meet when the meet is not under the fiducial hyperplane 𝑊. (Contributed by NM, 26-Mar-2014.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ (𝑋 ∧ 𝑌) ≤ 𝑊) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌))) | ||
Theorem | dihmeetbN 40908 | Isomorphism H of a lattice meet when one element is under the fiducial hyperplane 𝑊. (Contributed by NM, 26-Mar-2014.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌))) | ||
Theorem | dihmeetbclemN 40909 | Lemma for isomorphism H of a lattice meet. (Contributed by NM, 30-Mar-2014.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) → (𝐼‘(𝑋 ∧ 𝑌)) = (((𝐼‘𝑋) ∩ (𝐼‘𝑌)) ∩ (𝐼‘𝑊))) | ||
Theorem | dihmeetlem3N 40910 | Lemma for isomorphism H of a lattice meet. (Contributed by NM, 30-Mar-2014.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ∨ (𝑋 ∧ 𝑊)) = 𝑋) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ (𝑅 ∨ (𝑌 ∧ 𝑊)) = 𝑌)) → 𝑄 ≠ 𝑅) | ||
Theorem | dihmeetlem4preN 40911* | Lemma for isomorphism H of a lattice meet. (Contributed by NM, 30-Mar-2014.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐺 = (℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄) & ⊢ 𝑃 = ((oc‘𝐾)‘𝑊) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵)) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → ((𝐼‘𝑄) ∩ (𝐼‘(𝑋 ∧ 𝑊))) = { 0 }) | ||
Theorem | dihmeetlem4N 40912 | Lemma for isomorphism H of a lattice meet. (Contributed by NM, 30-Mar-2014.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 0 = (0g‘𝑈) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → ((𝐼‘𝑄) ∩ (𝐼‘(𝑋 ∧ 𝑊))) = { 0 }) | ||
Theorem | dihmeetlem5 40913 | Part of proof that isomorphism H is order-preserving . (Contributed by NM, 6-Apr-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑋)) → (𝑋 ∧ (𝑌 ∨ 𝑄)) = ((𝑋 ∧ 𝑌) ∨ 𝑄)) | ||
Theorem | dihmeetlem6 40914 | Lemma for isomorphism H of a lattice meet. (Contributed by NM, 6-Apr-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑄 ≤ 𝑋)) → ¬ (𝑋 ∧ (𝑌 ∨ 𝑄)) ≤ 𝑊) | ||
Theorem | dihmeetlem7N 40915 | Lemma for isomorphism H of a lattice meet. (Contributed by NM, 6-Apr-2014.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑌)) → (((𝑋 ∧ 𝑌) ∨ 𝑝) ∧ 𝑌) = (𝑋 ∧ 𝑌)) | ||
Theorem | dihjatc1 40916 | Lemma for isomorphism H of a lattice meet. TODO: shorter proof if we change ∨ order of (𝑋 ∧ 𝑌) ∨ 𝑄 here and down? (Contributed by NM, 6-Apr-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ≤ 𝑋 ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) → (𝐼‘((𝑋 ∧ 𝑌) ∨ 𝑄)) = ((𝐼‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑌)))) | ||
Theorem | dihjatc2N 40917 | Isomorphism H of join with an atom. (Contributed by NM, 26-Aug-2014.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ≤ 𝑋 ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) → (𝐼‘(𝑄 ∨ (𝑋 ∧ 𝑌))) = ((𝐼‘𝑄) ⊕ (𝐼‘(𝑋 ∧ 𝑌)))) | ||
Theorem | dihjatc3 40918 | Isomorphism H of join with an atom. (Contributed by NM, 26-Aug-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑄 ≤ 𝑋 ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) → (𝐼‘((𝑋 ∧ 𝑌) ∨ 𝑄)) = ((𝐼‘(𝑋 ∧ 𝑌)) ⊕ (𝐼‘𝑄))) | ||
Theorem | dihmeetlem8N 40919 | Lemma for isomorphism H of a lattice meet. TODO: shorter proof if we change ∨ order of (𝑋 ∧ 𝑌) ∨ 𝑝 here and down? (Contributed by NM, 6-Apr-2014.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ (𝑝 ≤ 𝑋 ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) → (𝐼‘((𝑋 ∧ 𝑌) ∨ 𝑝)) = ((𝐼‘𝑝) ⊕ (𝐼‘(𝑋 ∧ 𝑌)))) | ||
Theorem | dihmeetlem9N 40920 | Lemma for isomorphism H of a lattice meet. (Contributed by NM, 6-Apr-2014.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐴) → (((𝐼‘𝑝) ⊕ (𝐼‘(𝑋 ∧ 𝑌))) ∩ (𝐼‘𝑌)) = ((𝐼‘(𝑋 ∧ 𝑌)) ⊕ ((𝐼‘𝑝) ∩ (𝐼‘𝑌)))) | ||
Theorem | dihmeetlem10N 40921 | Lemma for isomorphism H of a lattice meet. (Contributed by NM, 6-Apr-2014.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ 𝑝 ≤ 𝑋)) → (𝐼‘((𝑋 ∧ 𝑌) ∨ 𝑝)) = ((𝐼‘𝑋) ∩ (𝐼‘(𝑌 ∨ 𝑝)))) | ||
Theorem | dihmeetlem11N 40922 | Lemma for isomorphism H of a lattice meet. (Contributed by NM, 6-Apr-2014.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ 𝑝 ≤ 𝑋)) → ((𝐼‘((𝑋 ∧ 𝑌) ∨ 𝑝)) ∩ (𝐼‘𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌))) | ||
Theorem | dihmeetlem12N 40923 | Lemma for isomorphism H of a lattice meet. (Contributed by NM, 6-Apr-2014.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ 𝑝 ≤ 𝑋 ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) → ((𝐼‘(𝑋 ∧ 𝑌)) ⊕ ((𝐼‘𝑝) ∩ (𝐼‘𝑌))) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌))) | ||
Theorem | dihmeetlem13N 40924* | Lemma for isomorphism H of a lattice meet. (Contributed by NM, 7-Apr-2014.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑃 = ((oc‘𝐾)‘𝑊) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵)) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐹 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑄) & ⊢ 𝐺 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑅) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ 𝑄 ≠ 𝑅) → ((𝐼‘𝑄) ∩ (𝐼‘𝑅)) = { 0 }) | ||
Theorem | dihmeetlem14N 40925 | Lemma for isomorphism H of a lattice meet. (Contributed by NM, 7-Apr-2014.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑌 ∈ 𝐵 ∧ 𝑝 ∈ 𝐵) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ 𝑟 ≤ 𝑌 ∧ (𝑌 ∧ 𝑝) ≤ 𝑊)) → ((𝐼‘(𝑌 ∧ 𝑝)) ⊕ ((𝐼‘𝑟) ∩ (𝐼‘𝑝))) = ((𝐼‘𝑌) ∩ (𝐼‘𝑝))) | ||
Theorem | dihmeetlem15N 40926 | Lemma for isomorphism H of a lattice meet. (Contributed by NM, 7-Apr-2014.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ 0 = (0g‘𝑈) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑌 ∈ 𝐵 ∧ (𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ 𝑟 ≤ 𝑌 ∧ (𝑌 ∧ 𝑝) ≤ 𝑊)) → ((𝐼‘𝑟) ∩ (𝐼‘𝑝)) = { 0 }) | ||
Theorem | dihmeetlem16N 40927 | Lemma for isomorphism H of a lattice meet. (Contributed by NM, 7-Apr-2014.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑌 ∈ 𝐵 ∧ (𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊)) ∧ ((𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ 𝑟 ≤ 𝑌 ∧ (𝑌 ∧ 𝑝) ≤ 𝑊)) → (𝐼‘(𝑌 ∧ 𝑝)) = ((𝐼‘𝑌) ∩ (𝐼‘𝑝))) | ||
Theorem | dihmeetlem17N 40928 | Lemma for isomorphism H of a lattice meet. (Contributed by NM, 7-Apr-2014.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ 0 = (0.‘𝐾) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊)) ∧ (𝑌 ∈ 𝐵 ∧ (𝑋 ∧ 𝑌) ≤ 𝑊 ∧ 𝑝 ≤ 𝑋)) → (𝑌 ∧ 𝑝) = 0 ) | ||
Theorem | dihmeetlem18N 40929 | Lemma for isomorphism H of a lattice meet. (Contributed by NM, 7-Apr-2014.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ 0 = (0g‘𝑈) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ (𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑝 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌 ∧ (𝑋 ∧ 𝑌) ≤ 𝑊))) → ((𝐼‘𝑌) ∩ (𝐼‘𝑝)) = { 0 }) | ||
Theorem | dihmeetlem19N 40930 | Lemma for isomorphism H of a lattice meet. (Contributed by NM, 7-Apr-2014.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ 𝐵) ∧ ((𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊) ∧ (𝑟 ∈ 𝐴 ∧ ¬ 𝑟 ≤ 𝑊) ∧ (𝑝 ≤ 𝑋 ∧ 𝑟 ≤ 𝑌 ∧ (𝑋 ∧ 𝑌) ≤ 𝑊))) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌))) | ||
Theorem | dihmeetlem20N 40931 | Lemma for isomorphism H of a lattice meet. (Contributed by NM, 7-Apr-2014.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ ((𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊) ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌))) | ||
Theorem | dihmeetALTN 40932 | Isomorphism H of a lattice meet. This version does not depend on the atomisticity of the constructed vector space. TODO: Delete? (Contributed by NM, 7-Apr-2014.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌))) | ||
Theorem | dih1dimatlem0 40933* | Lemma for dih1dimat 40935. (Contributed by NM, 11-Apr-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐶 = (Atoms‘𝐾) & ⊢ 𝑃 = ((oc‘𝐾)‘𝑊) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵)) & ⊢ 𝐹 = (Scalar‘𝑈) & ⊢ 𝐽 = (invr‘𝐹) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐺 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = (((𝐽‘𝑠)‘𝑓)‘𝑃)) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑓 ∈ 𝑇 ∧ 𝑠 ∈ 𝐸) ∧ 𝑠 ≠ 𝑂) → ((𝑖 = (𝑝‘𝐺) ∧ 𝑝 ∈ 𝐸) ↔ ((𝑖 ∈ 𝑇 ∧ 𝑝 ∈ 𝐸) ∧ ∃𝑡 ∈ 𝐸 (𝑖 = (𝑡‘𝑓) ∧ 𝑝 = (𝑡 ∘ 𝑠))))) | ||
Theorem | dih1dimatlem 40934* | Lemma for dih1dimat 40935. (Contributed by NM, 10-Apr-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐶 = (Atoms‘𝐾) & ⊢ 𝑃 = ((oc‘𝐾)‘𝑊) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵)) & ⊢ 𝐹 = (Scalar‘𝑈) & ⊢ 𝐽 = (invr‘𝐹) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ · = ( ·𝑠 ‘𝑈) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐺 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = (((𝐽‘𝑠)‘𝑓)‘𝑃)) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐷 ∈ 𝐴) → 𝐷 ∈ ran 𝐼) | ||
Theorem | dih1dimat 40935 | Any 1-dimensional subspace is a value of isomorphism H. (Contributed by NM, 11-Apr-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑈) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ∈ 𝐴) → 𝑃 ∈ ran 𝐼) | ||
Theorem | dihlsprn 40936 | The span of a vector belongs to the range of isomorphism H. (Contributed by NM, 27-Apr-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉) → (𝑁‘{𝑋}) ∈ ran 𝐼) | ||
Theorem | dihlspsnssN 40937 | A subspace included in a 1-dim subspace belongs to the range of isomorphism H. (Contributed by NM, 26-Apr-2014.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉 ∧ 𝑇 ⊆ (𝑁‘{𝑋})) → (𝑇 ∈ 𝑆 ↔ 𝑇 ∈ ran 𝐼)) | ||
Theorem | dihlspsnat 40938 | The inverse isomorphism H of the span of a singleton is a Hilbert lattice atom. (Contributed by NM, 27-Apr-2014.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → (◡𝐼‘(𝑁‘{𝑋})) ∈ 𝐴) | ||
Theorem | dihatlat 40939 | The isomorphism H of an atom is a 1-dim subspace. (Contributed by NM, 28-Apr-2014.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ 𝐿 = (LSAtoms‘𝑈) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ 𝐴) → (𝐼‘𝑄) ∈ 𝐿) | ||
Theorem | dihat 40940 | There exists at least one atom in the subspaces of vector space H. (Contributed by NM, 12-Aug-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑃 = ((oc‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → (𝐼‘𝑃) ∈ 𝐴) | ||
Theorem | dihpN 40941* | The value of isomorphism H at the fiducial atom 𝑃 is determined by the vector 〈0, 𝑆〉 (the zero translation ltrnid 39740 and a nonzero member of the endomorphism ring). In particular, 𝑆 can be replaced with the ring unity ( I ↾ 𝑇). (Contributed by NM, 26-Aug-2014.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑃 = ((oc‘𝐾)‘𝑊) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑂 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵)) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → (𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂)) ⇒ ⊢ (𝜑 → (𝐼‘𝑃) = (𝑁‘{〈( I ↾ 𝐵), 𝑆〉})) | ||
Theorem | dihlatat 40942 | The reverse isomorphism H of a 1-dim subspace is an atom. (Contributed by NM, 28-Apr-2014.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ 𝐿 = (LSAtoms‘𝑈) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ 𝐿) → (◡𝐼‘𝑄) ∈ 𝐴) | ||
Theorem | dihatexv 40943* | There is a nonzero vector that maps to every lattice atom. (Contributed by NM, 16-Aug-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑄 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑄 ∈ 𝐴 ↔ ∃𝑥 ∈ (𝑉 ∖ { 0 })(𝐼‘𝑄) = (𝑁‘{𝑥}))) | ||
Theorem | dihatexv2 40944* | There is a nonzero vector that maps to every lattice atom. (Contributed by NM, 17-Aug-2014.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → (𝑄 ∈ 𝐴 ↔ ∃𝑥 ∈ (𝑉 ∖ { 0 })𝑄 = (◡𝐼‘(𝑁‘{𝑥})))) | ||
Theorem | dihglblem6 40945* | Isomorphism H of a lattice glb. (Contributed by NM, 9-Apr-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑃 = (LSubSp‘𝑈) & ⊢ 𝐷 = (LSAtoms‘𝑈) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) → (𝐼‘(𝐺‘𝑆)) = ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥)) | ||
Theorem | dihglb 40946* | Isomorphism H of a lattice glb. (Contributed by NM, 11-Apr-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅)) → (𝐼‘(𝐺‘𝑆)) = ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥)) | ||
Theorem | dihglb2 40947* | Isomorphism H of a lattice glb. (Contributed by NM, 11-Apr-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ⊆ 𝑉) → (𝐼‘(𝐺‘{𝑥 ∈ 𝐵 ∣ 𝑆 ⊆ (𝐼‘𝑥)})) = ∩ {𝑦 ∈ ran 𝐼 ∣ 𝑆 ⊆ 𝑦}) | ||
Theorem | dihmeet 40948 | Isomorphism H of a lattice meet. (Contributed by NM, 13-Apr-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐼‘(𝑋 ∧ 𝑌)) = ((𝐼‘𝑋) ∩ (𝐼‘𝑌))) | ||
Theorem | dihintcl 40949 | The intersection of closed subspaces (the range of isomorphism H) is a closed subspace. (Contributed by NM, 14-Apr-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) → ∩ 𝑆 ∈ ran 𝐼) | ||
Theorem | dihmeetcl 40950 | Closure of closed subspace meet for DVecH vector space. (Contributed by NM, 5-Aug-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ ran 𝐼 ∧ 𝑌 ∈ ran 𝐼)) → (𝑋 ∩ 𝑌) ∈ ran 𝐼) | ||
Theorem | dihmeet2 40951 | Reverse isomorphism H of a closed subspace intersection. (Contributed by NM, 15-Jan-2015.) |
⊢ ∧ = (meet‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝐼) & ⊢ (𝜑 → 𝑌 ∈ ran 𝐼) ⇒ ⊢ (𝜑 → (◡𝐼‘(𝑋 ∩ 𝑌)) = ((◡𝐼‘𝑋) ∧ (◡𝐼‘𝑌))) | ||
Syntax | coch 40952 | Extend class notation with subspace orthocomplement for DVecH vector space. |
class ocH | ||
Definition | df-doch 40953* | Define subspace orthocomplement for DVecH vector space. Temporarily, we are using the range of the isomorphism instead of the set of closed subspaces. Later, when inner product is introduced, we will show that these are the same. (Contributed by NM, 14-Mar-2014.) |
⊢ ocH = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((DIsoH‘𝑘)‘𝑤)‘((oc‘𝑘)‘((glb‘𝑘)‘{𝑦 ∈ (Base‘𝑘) ∣ 𝑥 ⊆ (((DIsoH‘𝑘)‘𝑤)‘𝑦)})))))) | ||
Theorem | dochffval 40954* | Subspace orthocomplement for DVecH vector space. (Contributed by NM, 14-Mar-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝑉 → (ocH‘𝐾) = (𝑤 ∈ 𝐻 ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝐾)‘𝑤)) ↦ (((DIsoH‘𝐾)‘𝑤)‘( ⊥ ‘(𝐺‘{𝑦 ∈ 𝐵 ∣ 𝑥 ⊆ (((DIsoH‘𝐾)‘𝑤)‘𝑦)})))))) | ||
Theorem | dochfval 40955* | Subspace orthocomplement for DVecH vector space. (Contributed by NM, 14-Mar-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = ((ocH‘𝐾)‘𝑊) ⇒ ⊢ ((𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻) → 𝑁 = (𝑥 ∈ 𝒫 𝑉 ↦ (𝐼‘( ⊥ ‘(𝐺‘{𝑦 ∈ 𝐵 ∣ 𝑥 ⊆ (𝐼‘𝑦)}))))) | ||
Theorem | dochval 40956* | Subspace orthocomplement for DVecH vector space. (Contributed by NM, 14-Mar-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = ((ocH‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ 𝑌 ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → (𝑁‘𝑋) = (𝐼‘( ⊥ ‘(𝐺‘{𝑦 ∈ 𝐵 ∣ 𝑋 ⊆ (𝐼‘𝑦)})))) | ||
Theorem | dochval2 40957* | Subspace orthocomplement for DVecH vector space. (Contributed by NM, 14-Apr-2014.) |
⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = ((ocH‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → (𝑁‘𝑋) = (𝐼‘( ⊥ ‘(◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧})))) | ||
Theorem | dochcl 40958 | Closure of subspace orthocomplement for DVecH vector space. (Contributed by NM, 9-Mar-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → ( ⊥ ‘𝑋) ∈ ran 𝐼) | ||
Theorem | dochlss 40959 | A subspace orthocomplement is a subspace of the DVecH vector space. (Contributed by NM, 22-Jul-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → ( ⊥ ‘𝑋) ∈ 𝑆) | ||
Theorem | dochssv 40960 | A subspace orthocomplement belongs to the DVecH vector space. (Contributed by NM, 22-Jul-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → ( ⊥ ‘𝑋) ⊆ 𝑉) | ||
Theorem | dochfN 40961 | Domain and codomain of the subspace orthocomplement for the DVecH vector space. (Contributed by NM, 27-Dec-2014.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → ⊥ :𝒫 𝑉⟶ran 𝐼) | ||
Theorem | dochvalr 40962 | Orthocomplement of a closed subspace. (Contributed by NM, 14-Mar-2014.) |
⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ 𝑁 = ((ocH‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ ran 𝐼) → (𝑁‘𝑋) = (𝐼‘( ⊥ ‘(◡𝐼‘𝑋)))) | ||
Theorem | doch0 40963 | Orthocomplement of the zero subspace. (Contributed by NM, 19-Jun-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ( ⊥ ‘{ 0 }) = 𝑉) | ||
Theorem | doch1 40964 | Orthocomplement of the unit subspace (all vectors). (Contributed by NM, 19-Jun-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ( ⊥ ‘𝑉) = { 0 }) | ||
Theorem | dochoc0 40965 | The zero subspace is closed. (Contributed by NM, 16-Feb-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 0 = (0g‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘{ 0 })) = { 0 }) | ||
Theorem | dochoc1 40966 | The unit subspace (all vectors) is closed. (Contributed by NM, 16-Feb-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘𝑉)) = 𝑉) | ||
Theorem | dochvalr2 40967 | Orthocomplement of a closed subspace. (Contributed by NM, 21-Jul-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ 𝑁 = ((ocH‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝐵) → (𝑁‘(𝐼‘𝑋)) = (𝐼‘( ⊥ ‘𝑋))) | ||
Theorem | dochvalr3 40968 | Orthocomplement of a closed subspace. (Contributed by NM, 15-Jan-2015.) |
⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ 𝑁 = ((ocH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝐼) ⇒ ⊢ (𝜑 → ( ⊥ ‘(◡𝐼‘𝑋)) = (◡𝐼‘(𝑁‘𝑋))) | ||
Theorem | doch2val2 40969* | Double orthocomplement for DVecH vector space. (Contributed by NM, 26-Jul-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ⊆ 𝑉) ⇒ ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘𝑋)) = ∩ {𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧}) | ||
Theorem | dochss 40970 | Subset law for orthocomplement. (Contributed by NM, 16-Apr-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑌 ⊆ 𝑉 ∧ 𝑋 ⊆ 𝑌) → ( ⊥ ‘𝑌) ⊆ ( ⊥ ‘𝑋)) | ||
Theorem | dochocss 40971 | Double negative law for orthocomplement of an arbitrary set of vectors. (Contributed by NM, 16-Apr-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → 𝑋 ⊆ ( ⊥ ‘( ⊥ ‘𝑋))) | ||
Theorem | dochoc 40972 | Double negative law for orthocomplement of a closed subspace. (Contributed by NM, 14-Mar-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ ran 𝐼) → ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋) | ||
Theorem | dochsscl 40973 | If a set of vectors is included in a closed set, so is its closure. (Contributed by NM, 17-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ⊆ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ ran 𝐼) ⇒ ⊢ (𝜑 → (𝑋 ⊆ 𝑌 ↔ ( ⊥ ‘( ⊥ ‘𝑋)) ⊆ 𝑌)) | ||
Theorem | dochoccl 40974 | A set of vectors is closed iff it equals its double orthocomplent. (Contributed by NM, 1-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ⊆ 𝑉) ⇒ ⊢ (𝜑 → (𝑋 ∈ ran 𝐼 ↔ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋)) | ||
Theorem | dochord 40975 | Ordering law for orthocomplement. (Contributed by NM, 12-Aug-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝐼) & ⊢ (𝜑 → 𝑌 ∈ ran 𝐼) ⇒ ⊢ (𝜑 → (𝑋 ⊆ 𝑌 ↔ ( ⊥ ‘𝑌) ⊆ ( ⊥ ‘𝑋))) | ||
Theorem | dochord2N 40976 | Ordering law for orthocomplement. (Contributed by NM, 29-Oct-2014.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝐼) & ⊢ (𝜑 → 𝑌 ∈ ran 𝐼) ⇒ ⊢ (𝜑 → (( ⊥ ‘𝑋) ⊆ 𝑌 ↔ ( ⊥ ‘𝑌) ⊆ 𝑋)) | ||
Theorem | dochord3 40977 | Ordering law for orthocomplement. (Contributed by NM, 9-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝐼) & ⊢ (𝜑 → 𝑌 ∈ ran 𝐼) ⇒ ⊢ (𝜑 → (𝑋 ⊆ ( ⊥ ‘𝑌) ↔ 𝑌 ⊆ ( ⊥ ‘𝑋))) | ||
Theorem | doch11 40978 | Orthocomplement is one-to-one. (Contributed by NM, 12-Aug-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝐼) & ⊢ (𝜑 → 𝑌 ∈ ran 𝐼) ⇒ ⊢ (𝜑 → (( ⊥ ‘𝑋) = ( ⊥ ‘𝑌) ↔ 𝑋 = 𝑌)) | ||
Theorem | dochsordN 40979 | Strict ordering law for orthocomplement. (Contributed by NM, 12-Aug-2014.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝐼) & ⊢ (𝜑 → 𝑌 ∈ ran 𝐼) ⇒ ⊢ (𝜑 → (𝑋 ⊊ 𝑌 ↔ ( ⊥ ‘𝑌) ⊊ ( ⊥ ‘𝑋))) | ||
Theorem | dochn0nv 40980 | An orthocomplement is nonzero iff the double orthocomplement is not the whole vector space. (Contributed by NM, 1-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ⊆ 𝑉) ⇒ ⊢ (𝜑 → (( ⊥ ‘𝑋) ≠ { 0 } ↔ ( ⊥ ‘( ⊥ ‘𝑋)) ≠ 𝑉)) | ||
Theorem | dihoml4c 40981 | Version of dihoml4 40982 with closed subspaces. (Contributed by NM, 15-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ ran 𝐼) & ⊢ (𝜑 → 𝑌 ∈ ran 𝐼) & ⊢ (𝜑 → 𝑋 ⊆ 𝑌) ⇒ ⊢ (𝜑 → (( ⊥ ‘(( ⊥ ‘𝑋) ∩ 𝑌)) ∩ 𝑌) = 𝑋) | ||
Theorem | dihoml4 40982 | Orthomodular law for constructed vector space H. Lemma 3.3(1) in [Holland95] p. 215. (poml4N 39558 analog.) (Contributed by NM, 15-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) & ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘𝑌)) = 𝑌) & ⊢ (𝜑 → 𝑋 ⊆ 𝑌) ⇒ ⊢ (𝜑 → (( ⊥ ‘(( ⊥ ‘𝑋) ∩ 𝑌)) ∩ 𝑌) = ( ⊥ ‘( ⊥ ‘𝑋))) | ||
Theorem | dochspss 40983 | The span of a set of vectors is included in their double orthocomplement. (Contributed by NM, 26-Jul-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ⊆ 𝑉) ⇒ ⊢ (𝜑 → (𝑁‘𝑋) ⊆ ( ⊥ ‘( ⊥ ‘𝑋))) | ||
Theorem | dochocsp 40984 | The span of an orthocomplement equals the orthocomplement of the span. (Contributed by NM, 7-Aug-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ⊆ 𝑉) ⇒ ⊢ (𝜑 → ( ⊥ ‘(𝑁‘𝑋)) = ( ⊥ ‘𝑋)) | ||
Theorem | dochspocN 40985 | The span of an orthocomplement equals the orthocomplement of the span. (Contributed by NM, 7-Aug-2014.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ⊆ 𝑉) ⇒ ⊢ (𝜑 → (𝑁‘( ⊥ ‘𝑋)) = ( ⊥ ‘(𝑁‘𝑋))) | ||
Theorem | dochocsn 40986 | The double orthocomplement of a singleton is its span. (Contributed by NM, 13-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑁 = (LSpan‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘{𝑋})) = (𝑁‘{𝑋})) | ||
Theorem | dochsncom 40987 | Swap vectors in an orthocomplement of a singleton. (Contributed by NM, 17-Jun-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑋 ∈ ( ⊥ ‘{𝑌}) ↔ 𝑌 ∈ ( ⊥ ‘{𝑋}))) | ||
Theorem | dochsat 40988 | The double orthocomplement of an atom is an atom. (Contributed by NM, 29-Oct-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 𝐴 = (LSAtoms‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑄 ∈ 𝑆) ⇒ ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘𝑄)) ∈ 𝐴 ↔ 𝑄 ∈ 𝐴)) | ||
Theorem | dochshpncl 40989 | If a hyperplane is not closed, its closure equals the vector space. (Contributed by NM, 29-Oct-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑌 = (LSHyp‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ 𝑌) ⇒ ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘𝑋)) ≠ 𝑋 ↔ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑉)) | ||
Theorem | dochlkr 40990 | Equivalent conditions for the closure of a kernel to be a hyperplane. (Contributed by NM, 29-Oct-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝑌 = (LSHyp‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ∈ 𝑌 ↔ (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺) ∧ (𝐿‘𝐺) ∈ 𝑌))) | ||
Theorem | dochkrshp 40991 | The closure of a kernel is a hyperplane iff it doesn't contain all vectors. (Contributed by NM, 1-Nov-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑌 = (LSHyp‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ 𝑉 ↔ ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ∈ 𝑌)) | ||
Theorem | dochkrshp2 40992 | Properties of the closure of the kernel of a functional. (Contributed by NM, 1-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝑌 = (LSHyp‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ 𝑉 ↔ (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺) ∧ (𝐿‘𝐺) ∈ 𝑌))) | ||
Theorem | dochkrshp3 40993 | Properties of the closure of the kernel of a functional. (Contributed by NM, 1-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ 𝑉 ↔ (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺) ∧ (𝐿‘𝐺) ≠ 𝑉))) | ||
Theorem | dochkrshp4 40994 | Properties of the closure of the kernel of a functional. (Contributed by NM, 1-Jan-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 𝐹 = (LFnl‘𝑈) & ⊢ 𝐿 = (LKer‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺) ↔ (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ 𝑉 ∨ (𝐿‘𝐺) = 𝑉))) | ||
Theorem | dochdmj1 40995 | De Morgan-like law for subspace orthocomplement. (Contributed by NM, 5-Aug-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉) → ( ⊥ ‘(𝑋 ∪ 𝑌)) = (( ⊥ ‘𝑋) ∩ ( ⊥ ‘𝑌))) | ||
Theorem | dochnoncon 40996 | Law of noncontradiction. The intersection of a subspace and its orthocomplement is the zero subspace. (Contributed by NM, 16-Apr-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆) → (𝑋 ∩ ( ⊥ ‘𝑋)) = { 0 }) | ||
Theorem | dochnel2 40997 | A nonzero member of a subspace doesn't belong to the orthocomplement of the subspace. (Contributed by NM, 28-Feb-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑇 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ (𝑇 ∖ { 0 })) ⇒ ⊢ (𝜑 → ¬ 𝑋 ∈ ( ⊥ ‘𝑇)) | ||
Theorem | dochnel 40998 | A nonzero vector doesn't belong to the orthocomplement of its singleton. (Contributed by NM, 27-Oct-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) ⇒ ⊢ (𝜑 → ¬ 𝑋 ∈ ( ⊥ ‘{𝑋})) | ||
Syntax | cdjh 40999 | Extend class notation with subspace join for DVecH vector space. |
class joinH | ||
Definition | df-djh 41000* | Define (closed) subspace join for DVecH vector space. (Contributed by NM, 19-Jul-2014.) |
⊢ joinH = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)), 𝑦 ∈ 𝒫 (Base‘((DVecH‘𝑘)‘𝑤)) ↦ (((ocH‘𝑘)‘𝑤)‘((((ocH‘𝑘)‘𝑤)‘𝑥) ∩ (((ocH‘𝑘)‘𝑤)‘𝑦)))))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |