Home | Metamath
Proof Explorer Theorem List (p. 382 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dvhbase 38101 | The ring base set of the constructed full vector space H. (Contributed by NM, 29-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑈) & ⊢ 𝐶 = (Base‘𝐹) ⇒ ⊢ ((𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻) → 𝐶 = 𝐸) | ||
Theorem | dvhfplusr 38102* | Ring addition operation for the constructed full vector space H. (Contributed by NM, 29-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑈) & ⊢ + = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓)))) & ⊢ ✚ = (+g‘𝐹) ⇒ ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → ✚ = + ) | ||
Theorem | dvhfmulr 38103* | Ring multiplication operation for the constructed full vector space H. (Contributed by NM, 29-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑈) & ⊢ · = (.r‘𝐹) ⇒ ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → · = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑠 ∘ 𝑡))) | ||
Theorem | dvhmulr 38104 | Ring multiplication operation for the constructed full vector space H. (Contributed by NM, 29-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑈) & ⊢ · = (.r‘𝐹) ⇒ ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐸 ∧ 𝑆 ∈ 𝐸)) → (𝑅 · 𝑆) = (𝑅 ∘ 𝑆)) | ||
Theorem | dvhvbase 38105 | The vectors (vector base set) of the constructed full vector space H are all translations (for a fiducial co-atom 𝑊). (Contributed by NM, 2-Nov-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) ⇒ ⊢ ((𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻) → 𝑉 = (𝑇 × 𝐸)) | ||
Theorem | dvhelvbasei 38106 | Vector membership in the constructed full vector space H. (Contributed by NM, 20-Feb-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) ⇒ ⊢ (((𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸)) → 〈𝐹, 𝑆〉 ∈ 𝑉) | ||
Theorem | dvhvaddcbv 38107* | Change bound variables to isolate them later. (Contributed by NM, 3-Nov-2013.) |
⊢ + = (𝑓 ∈ (𝑇 × 𝐸), 𝑔 ∈ (𝑇 × 𝐸) ↦ 〈((1st ‘𝑓) ∘ (1st ‘𝑔)), ((2nd ‘𝑓) ⨣ (2nd ‘𝑔))〉) ⇒ ⊢ + = (ℎ ∈ (𝑇 × 𝐸), 𝑖 ∈ (𝑇 × 𝐸) ↦ 〈((1st ‘ℎ) ∘ (1st ‘𝑖)), ((2nd ‘ℎ) ⨣ (2nd ‘𝑖))〉) | ||
Theorem | dvhvaddval 38108* | The vector sum operation for the constructed full vector space H. (Contributed by NM, 26-Oct-2013.) |
⊢ + = (𝑓 ∈ (𝑇 × 𝐸), 𝑔 ∈ (𝑇 × 𝐸) ↦ 〈((1st ‘𝑓) ∘ (1st ‘𝑔)), ((2nd ‘𝑓) ⨣ (2nd ‘𝑔))〉) ⇒ ⊢ ((𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸)) → (𝐹 + 𝐺) = 〈((1st ‘𝐹) ∘ (1st ‘𝐺)), ((2nd ‘𝐹) ⨣ (2nd ‘𝐺))〉) | ||
Theorem | dvhfvadd 38109* | The vector sum operation for the constructed full vector space H. (Contributed by NM, 26-Oct-2013.) (Revised by Mario Carneiro, 23-Jun-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐷 = (Scalar‘𝑈) & ⊢ ⨣ = (+g‘𝐷) & ⊢ ✚ = (𝑓 ∈ (𝑇 × 𝐸), 𝑔 ∈ (𝑇 × 𝐸) ↦ 〈((1st ‘𝑓) ∘ (1st ‘𝑔)), ((2nd ‘𝑓) ⨣ (2nd ‘𝑔))〉) & ⊢ + = (+g‘𝑈) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → + = ✚ ) | ||
Theorem | dvhvadd 38110 | The vector sum operation for the constructed full vector space H. (Contributed by NM, 11-Feb-2014.) (Revised by Mario Carneiro, 23-Jun-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐷 = (Scalar‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ ⨣ = (+g‘𝐷) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸))) → (𝐹 + 𝐺) = 〈((1st ‘𝐹) ∘ (1st ‘𝐺)), ((2nd ‘𝐹) ⨣ (2nd ‘𝐺))〉) | ||
Theorem | dvhopvadd 38111 | The vector sum operation for the constructed full vector space H. (Contributed by NM, 21-Feb-2014.) (Revised by Mario Carneiro, 6-May-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐷 = (Scalar‘𝑈) & ⊢ + = (+g‘𝑈) & ⊢ ⨣ = (+g‘𝐷) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑄 ∈ 𝐸) ∧ (𝐺 ∈ 𝑇 ∧ 𝑅 ∈ 𝐸)) → (〈𝐹, 𝑄〉 + 〈𝐺, 𝑅〉) = 〈(𝐹 ∘ 𝐺), (𝑄 ⨣ 𝑅)〉) | ||
Theorem | dvhopvadd2 38112* | The vector sum operation for the constructed full vector space H. TODO: check if this will shorten proofs that use dvhopvadd 38111 and/or dvhfplusr 38102. (Contributed by NM, 26-Sep-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ + = (𝑠 ∈ 𝐸, 𝑡 ∈ 𝐸 ↦ (𝑓 ∈ 𝑇 ↦ ((𝑠‘𝑓) ∘ (𝑡‘𝑓)))) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ✚ = (+g‘𝑈) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑄 ∈ 𝐸) ∧ (𝐺 ∈ 𝑇 ∧ 𝑅 ∈ 𝐸)) → (〈𝐹, 𝑄〉 ✚ 〈𝐺, 𝑅〉) = 〈(𝐹 ∘ 𝐺), (𝑄 + 𝑅)〉) | ||
Theorem | dvhvaddcl 38113 | Closure of the vector sum operation for the constructed full vector space H. (Contributed by NM, 26-Oct-2013.) (Revised by Mario Carneiro, 23-Jun-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐷 = (Scalar‘𝑈) & ⊢ ⨣ = (+g‘𝐷) & ⊢ + = (+g‘𝑈) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸))) → (𝐹 + 𝐺) ∈ (𝑇 × 𝐸)) | ||
Theorem | dvhvaddcomN 38114 | Commutativity of vector sum. (Contributed by NM, 26-Oct-2013.) (Revised by Mario Carneiro, 23-Jun-2014.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐷 = (Scalar‘𝑈) & ⊢ ⨣ = (+g‘𝐷) & ⊢ + = (+g‘𝑈) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸))) → (𝐹 + 𝐺) = (𝐺 + 𝐹)) | ||
Theorem | dvhvaddass 38115 | Associativity of vector sum. (Contributed by NM, 31-Oct-2013.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐷 = (Scalar‘𝑈) & ⊢ ⨣ = (+g‘𝐷) & ⊢ + = (+g‘𝑈) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸) ∧ 𝐼 ∈ (𝑇 × 𝐸))) → ((𝐹 + 𝐺) + 𝐼) = (𝐹 + (𝐺 + 𝐼))) | ||
Theorem | dvhvscacbv 38116* | Change bound variables to isolate them later. (Contributed by NM, 20-Nov-2013.) |
⊢ · = (𝑠 ∈ 𝐸, 𝑓 ∈ (𝑇 × 𝐸) ↦ 〈(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))〉) ⇒ ⊢ · = (𝑡 ∈ 𝐸, 𝑔 ∈ (𝑇 × 𝐸) ↦ 〈(𝑡‘(1st ‘𝑔)), (𝑡 ∘ (2nd ‘𝑔))〉) | ||
Theorem | dvhvscaval 38117* | The scalar product operation for the constructed full vector space H. (Contributed by NM, 20-Nov-2013.) |
⊢ · = (𝑠 ∈ 𝐸, 𝑓 ∈ (𝑇 × 𝐸) ↦ 〈(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))〉) ⇒ ⊢ ((𝑈 ∈ 𝐸 ∧ 𝐹 ∈ (𝑇 × 𝐸)) → (𝑈 · 𝐹) = 〈(𝑈‘(1st ‘𝐹)), (𝑈 ∘ (2nd ‘𝐹))〉) | ||
Theorem | dvhfvsca 38118* | Scalar product operation for the constructed full vector space H. (Contributed by NM, 2-Nov-2013.) (Revised by Mario Carneiro, 23-Jun-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑈) ⇒ ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → · = (𝑠 ∈ 𝐸, 𝑓 ∈ (𝑇 × 𝐸) ↦ 〈(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))〉)) | ||
Theorem | dvhvsca 38119 | Scalar product operation for the constructed full vector space H. (Contributed by NM, 2-Nov-2013.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑈) ⇒ ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐸 ∧ 𝐹 ∈ (𝑇 × 𝐸))) → (𝑅 · 𝐹) = 〈(𝑅‘(1st ‘𝐹)), (𝑅 ∘ (2nd ‘𝐹))〉) | ||
Theorem | dvhopvsca 38120 | Scalar product operation for the constructed full vector space H. (Contributed by NM, 20-Feb-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑈) ⇒ ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐸 ∧ 𝐹 ∈ 𝑇 ∧ 𝑋 ∈ 𝐸)) → (𝑅 · 〈𝐹, 𝑋〉) = 〈(𝑅‘𝐹), (𝑅 ∘ 𝑋)〉) | ||
Theorem | dvhvscacl 38121 | Closure of the scalar product operation for the constructed full vector space H. (Contributed by NM, 12-Feb-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑈) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅 ∈ 𝐸 ∧ 𝐹 ∈ (𝑇 × 𝐸))) → (𝑅 · 𝐹) ∈ (𝑇 × 𝐸)) | ||
Theorem | tendoinvcl 38122* | Closure of multiplicative inverse for endomorphism. We use the scalar inverse of the vector space since it is much simpler than the direct inverse of cdleml8 38001. (Contributed by NM, 10-Apr-2014.) (Revised by Mario Carneiro, 23-Jun-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵)) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑈) & ⊢ 𝑁 = (invr‘𝐹) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂) → ((𝑁‘𝑆) ∈ 𝐸 ∧ (𝑁‘𝑆) ≠ 𝑂)) | ||
Theorem | tendolinv 38123* | Left multiplicative inverse for endomorphism. (Contributed by NM, 10-Apr-2014.) (Revised by Mario Carneiro, 23-Jun-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵)) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑈) & ⊢ 𝑁 = (invr‘𝐹) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂) → ((𝑁‘𝑆) ∘ 𝑆) = ( I ↾ 𝑇)) | ||
Theorem | tendorinv 38124* | Right multiplicative inverse for endomorphism. (Contributed by NM, 10-Apr-2014.) (Revised by Mario Carneiro, 23-Jun-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵)) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑈) & ⊢ 𝑁 = (invr‘𝐹) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ 𝐸 ∧ 𝑆 ≠ 𝑂) → (𝑆 ∘ (𝑁‘𝑆)) = ( I ↾ 𝑇)) | ||
Theorem | dvhgrp 38125 | The full vector space 𝑈 constructed from a Hilbert lattice 𝐾 (given a fiducial hyperplane 𝑊) is a group. (Contributed by NM, 19-Oct-2013.) (Revised by Mario Carneiro, 24-Jun-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐷 = (Scalar‘𝑈) & ⊢ ⨣ = (+g‘𝐷) & ⊢ + = (+g‘𝑈) & ⊢ 0 = (0g‘𝐷) & ⊢ 𝐼 = (invg‘𝐷) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑈 ∈ Grp) | ||
Theorem | dvhlveclem 38126 | Lemma for dvhlvec 38127. TODO: proof substituting inner part first shorter/longer than substituting outer part first? TODO: break up into smaller lemmas? TODO: does 𝜑 → method shorten proof? (Contributed by NM, 22-Oct-2013.) (Proof shortened by Mario Carneiro, 24-Jun-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐷 = (Scalar‘𝑈) & ⊢ ⨣ = (+g‘𝐷) & ⊢ + = (+g‘𝑈) & ⊢ 0 = (0g‘𝐷) & ⊢ 𝐼 = (invg‘𝐷) & ⊢ × = (.r‘𝐷) & ⊢ · = ( ·𝑠 ‘𝑈) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑈 ∈ LVec) | ||
Theorem | dvhlvec 38127 | The full vector space 𝑈 constructed from a Hilbert lattice 𝐾 (given a fiducial hyperplane 𝑊) is a left module. (Contributed by NM, 23-May-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → 𝑈 ∈ LVec) | ||
Theorem | dvhlmod 38128 | The full vector space 𝑈 constructed from a Hilbert lattice 𝐾 (given a fiducial hyperplane 𝑊) is a left module. (Contributed by NM, 23-May-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → 𝑈 ∈ LMod) | ||
Theorem | dvh0g 38129* | The zero vector of vector space H has the zero translation as its first member and the zero trace-preserving endomorphism as the second. (Contributed by NM, 9-Mar-2014.) (Revised by Mario Carneiro, 24-Jun-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝑂 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵)) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 0 = 〈( I ↾ 𝐵), 𝑂〉) | ||
Theorem | dvheveccl 38130 | Properties of a unit vector that we will use later as a convenient reference vector. This vector is called "e" in the remark after Lemma M of [Crawley] p. 121. line 17. See also dvhopN 38134 and dihpN 38354. (Contributed by NM, 27-Mar-2015.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) & ⊢ 0 = (0g‘𝑈) & ⊢ 𝐸 = 〈( I ↾ 𝐵), ( I ↾ 𝑇)〉 & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) ⇒ ⊢ (𝜑 → 𝐸 ∈ (𝑉 ∖ { 0 })) | ||
Theorem | dvhopclN 38131 | Closure of a DVecH vector expressed as ordered pair. (Contributed by NM, 20-Nov-2013.) (New usage is discouraged.) |
⊢ ((𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸) → 〈𝐹, 𝑈〉 ∈ (𝑇 × 𝐸)) | ||
Theorem | dvhopaddN 38132* | Sum of DVecH vectors expressed as ordered pair. (Contributed by NM, 20-Nov-2013.) (New usage is discouraged.) |
⊢ 𝐴 = (𝑓 ∈ (𝑇 × 𝐸), 𝑔 ∈ (𝑇 × 𝐸) ↦ 〈((1st ‘𝑓) ∘ (1st ‘𝑔)), ((2nd ‘𝑓)𝑃(2nd ‘𝑔))〉) ⇒ ⊢ (((𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸) ∧ (𝐺 ∈ 𝑇 ∧ 𝑉 ∈ 𝐸)) → (〈𝐹, 𝑈〉𝐴〈𝐺, 𝑉〉) = 〈(𝐹 ∘ 𝐺), (𝑈𝑃𝑉)〉) | ||
Theorem | dvhopspN 38133* | Scalar product of DVecH vector expressed as ordered pair. (Contributed by NM, 20-Nov-2013.) (New usage is discouraged.) |
⊢ 𝑆 = (𝑠 ∈ 𝐸, 𝑓 ∈ (𝑇 × 𝐸) ↦ 〈(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))〉) ⇒ ⊢ ((𝑅 ∈ 𝐸 ∧ (𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸)) → (𝑅𝑆〈𝐹, 𝑈〉) = 〈(𝑅‘𝐹), (𝑅 ∘ 𝑈)〉) | ||
Theorem | dvhopN 38134* | Decompose a DVecH vector expressed as an ordered pair into the sum of two components, the first from the translation group vector base of DVecA and the other from the one-dimensional vector subspace 𝐸. Part of Lemma M of [Crawley] p. 121, line 18. We represent their e, sigma, f by 〈( I ↾ 𝐵), ( I ↾ 𝑇)〉, 𝑈, 〈𝐹, 𝑂〉. We swapped the order of vector sum (their juxtaposition i.e. composition) to show 〈𝐹, 𝑂〉 first. Note that 𝑂 and ( I ↾ 𝑇) are the zero and one of the division ring 𝐸, and ( I ↾ 𝐵) is the zero of the translation group. 𝑆 is the scalar product. (Contributed by NM, 21-Nov-2013.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑃 = (𝑎 ∈ 𝐸, 𝑏 ∈ 𝐸 ↦ (𝑐 ∈ 𝑇 ↦ ((𝑎‘𝑐) ∘ (𝑏‘𝑐)))) & ⊢ 𝐴 = (𝑓 ∈ (𝑇 × 𝐸), 𝑔 ∈ (𝑇 × 𝐸) ↦ 〈((1st ‘𝑓) ∘ (1st ‘𝑔)), ((2nd ‘𝑓)𝑃(2nd ‘𝑔))〉) & ⊢ 𝑆 = (𝑠 ∈ 𝐸, 𝑓 ∈ (𝑇 × 𝐸) ↦ 〈(𝑠‘(1st ‘𝑓)), (𝑠 ∘ (2nd ‘𝑓))〉) & ⊢ 𝑂 = (𝑐 ∈ 𝑇 ↦ ( I ↾ 𝐵)) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑈 ∈ 𝐸)) → 〈𝐹, 𝑈〉 = (〈𝐹, 𝑂〉𝐴(𝑈𝑆〈( I ↾ 𝐵), ( I ↾ 𝑇)〉))) | ||
Theorem | dvhopellsm 38135* | Ordered pair membership in a subspace sum. (Contributed by NM, 12-Mar-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ + = (+g‘𝑈) & ⊢ 𝑆 = (LSubSp‘𝑈) & ⊢ ⊕ = (LSSum‘𝑈) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) → (〈𝐹, 𝑇〉 ∈ (𝑋 ⊕ 𝑌) ↔ ∃𝑥∃𝑦∃𝑧∃𝑤((〈𝑥, 𝑦〉 ∈ 𝑋 ∧ 〈𝑧, 𝑤〉 ∈ 𝑌) ∧ 〈𝐹, 𝑇〉 = (〈𝑥, 𝑦〉 + 〈𝑧, 𝑤〉)))) | ||
Theorem | cdlemm10N 38136* | The image of the map 𝐺 is the entire one-dimensional subspace (𝐼‘𝑉). Remark after Lemma M of [Crawley] p. 121 line 23. (Contributed by NM, 24-Nov-2013.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) & ⊢ 𝐶 = {𝑟 ∈ 𝐴 ∣ (𝑟 ≤ (𝑃 ∨ 𝑉) ∧ ¬ 𝑟 ≤ 𝑊)} & ⊢ 𝐹 = (℩𝑓 ∈ 𝑇 (𝑓‘𝑃) = 𝑠) & ⊢ 𝐺 = (𝑞 ∈ 𝐶 ↦ (℩𝑓 ∈ 𝑇 (𝑓‘𝑃) = 𝑞)) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) → ran 𝐺 = (𝐼‘𝑉)) | ||
Syntax | cocaN 38137 | Extend class notation with subspace orthocomplement for DVecA partial vector space. |
class ocA | ||
Definition | df-docaN 38138* | Define subspace orthocomplement for DVecA partial 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, 6-Dec-2013.) |
⊢ ocA = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤) ↦ (((DIsoA‘𝑘)‘𝑤)‘((((oc‘𝑘)‘(◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤))))) | ||
Theorem | docaffvalN 38139* | Subspace orthocomplement for DVecA partial vector space. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝑉 → (ocA‘𝐾) = (𝑤 ∈ 𝐻 ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝐾)‘𝑤) ↦ (((DIsoA‘𝐾)‘𝑤)‘((( ⊥ ‘(◡((DIsoA‘𝐾)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝐾)‘𝑤) ∣ 𝑥 ⊆ 𝑧})) ∨ ( ⊥ ‘𝑤)) ∧ 𝑤))))) | ||
Theorem | docafvalN 38140* | Subspace orthocomplement for DVecA partial vector space. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) & ⊢ 𝑁 = ((ocA‘𝐾)‘𝑊) ⇒ ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → 𝑁 = (𝑥 ∈ 𝒫 𝑇 ↦ (𝐼‘((( ⊥ ‘(◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ 𝑥 ⊆ 𝑧})) ∨ ( ⊥ ‘𝑊)) ∧ 𝑊)))) | ||
Theorem | docavalN 38141* | Subspace orthocomplement for DVecA partial vector space. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) & ⊢ 𝑁 = ((ocA‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑇) → (𝑁‘𝑋) = (𝐼‘((( ⊥ ‘(◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ 𝑋 ⊆ 𝑧})) ∨ ( ⊥ ‘𝑊)) ∧ 𝑊))) | ||
Theorem | docaclN 38142 | Closure of subspace orthocomplement for DVecA partial vector space. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocA‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑇) → ( ⊥ ‘𝑋) ∈ ran 𝐼) | ||
Theorem | diaocN 38143 | Value of partial isomorphism A at lattice orthocomplement (using a Sasaki projection to get orthocomplement relative to the fiducial co-atom 𝑊). (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) & ⊢ 𝑁 = ((ocA‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → (𝐼‘((( ⊥ ‘𝑋) ∨ ( ⊥ ‘𝑊)) ∧ 𝑊)) = (𝑁‘(𝐼‘𝑋))) | ||
Theorem | doca2N 38144 | Double orthocomplement of partial isomorphism A. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocA‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → ( ⊥ ‘( ⊥ ‘(𝐼‘𝑋))) = (𝐼‘𝑋)) | ||
Theorem | doca3N 38145 | Double orthocomplement of partial isomorphism A. (Contributed by NM, 17-Jan-2014.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocA‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ ran 𝐼) → ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋) | ||
Theorem | dvadiaN 38146 | Any closed subspace is a member of the range of partial isomorphism A, showing the isomorphism maps onto the set of closed subspaces of partial vector space A. (Contributed by NM, 17-Jan-2014.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecA‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocA‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑈) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝑆 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋)) → 𝑋 ∈ ran 𝐼) | ||
Theorem | diarnN 38147* | Partial isomorphism A maps onto the set of all closed subspaces of partial vector space A. Part of Lemma M of [Crawley] p. 121 line 12, with closed subspaces rather than subspaces. (Contributed by NM, 17-Jan-2014.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecA‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocA‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑈) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ran 𝐼 = {𝑥 ∈ 𝑆 ∣ ( ⊥ ‘( ⊥ ‘𝑥)) = 𝑥}) | ||
Theorem | diaf1oN 38148* | The partial isomorphism A for a lattice 𝐾 is a one-to-one, onto function. Part of Lemma M of [Crawley] p. 121 line 12, with closed subspaces rather than subspaces. See diadm 38053 for the domain. (Contributed by NM, 17-Jan-2014.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecA‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocA‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑈) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝐼:dom 𝐼–1-1-onto→{𝑥 ∈ 𝑆 ∣ ( ⊥ ‘( ⊥ ‘𝑥)) = 𝑥}) | ||
Syntax | cdjaN 38149 | Extend class notation with subspace join for DVecA partial vector space. |
class vA | ||
Definition | df-djaN 38150* | Define (closed) subspace join for DVecA partial vector space. (Contributed by NM, 6-Dec-2013.) |
⊢ vA = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤), 𝑦 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤) ↦ (((ocA‘𝑘)‘𝑤)‘((((ocA‘𝑘)‘𝑤)‘𝑥) ∩ (((ocA‘𝑘)‘𝑤)‘𝑦)))))) | ||
Theorem | djaffvalN 38151* | Subspace join for DVecA partial vector space. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝑉 → (vA‘𝐾) = (𝑤 ∈ 𝐻 ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝐾)‘𝑤), 𝑦 ∈ 𝒫 ((LTrn‘𝐾)‘𝑤) ↦ (((ocA‘𝐾)‘𝑤)‘((((ocA‘𝐾)‘𝑤)‘𝑥) ∩ (((ocA‘𝐾)‘𝑤)‘𝑦)))))) | ||
Theorem | djafvalN 38152* | Subspace join for DVecA partial vector space. TODO: take out hypothesis .i, no longer used. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocA‘𝐾)‘𝑊) & ⊢ 𝐽 = ((vA‘𝐾)‘𝑊) ⇒ ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → 𝐽 = (𝑥 ∈ 𝒫 𝑇, 𝑦 ∈ 𝒫 𝑇 ↦ ( ⊥ ‘(( ⊥ ‘𝑥) ∩ ( ⊥ ‘𝑦))))) | ||
Theorem | djavalN 38153 | Subspace join for DVecA partial vector space. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) & ⊢ ⊥ = ((ocA‘𝐾)‘𝑊) & ⊢ 𝐽 = ((vA‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ⊆ 𝑇 ∧ 𝑌 ⊆ 𝑇)) → (𝑋𝐽𝑌) = ( ⊥ ‘(( ⊥ ‘𝑋) ∩ ( ⊥ ‘𝑌)))) | ||
Theorem | djaclN 38154 | Closure of subspace join for DVecA partial vector space. (Contributed by NM, 5-Dec-2013.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) & ⊢ 𝐽 = ((vA‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ⊆ 𝑇 ∧ 𝑌 ⊆ 𝑇)) → (𝑋𝐽𝑌) ∈ ran 𝐼) | ||
Theorem | djajN 38155 | Transfer lattice join to DVecA partial vector space closed subspace join. Part of Lemma M of [Crawley] p. 120 line 29, with closed subspace join rather than subspace sum. (Contributed by NM, 5-Dec-2013.) (New usage is discouraged.) |
⊢ ∨ = (join‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) & ⊢ 𝐽 = ((vA‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ dom 𝐼 ∧ 𝑌 ∈ dom 𝐼)) → (𝐼‘(𝑋 ∨ 𝑌)) = ((𝐼‘𝑋)𝐽(𝐼‘𝑌))) | ||
Syntax | cdib 38156 | Extend class notation with isomorphism B. |
class DIsoB | ||
Definition | df-dib 38157* | Isomorphism B is isomorphism A extended with an extra dimension set to the zero vector component i.e. the zero endormorphism. Its domain is lattice elements less than or equal to the fiducial co-atom 𝑤. (Contributed by NM, 8-Dec-2013.) |
⊢ DIsoB = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ dom ((DIsoA‘𝑘)‘𝑤) ↦ ((((DIsoA‘𝑘)‘𝑤)‘𝑥) × {(𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ↦ ( I ↾ (Base‘𝑘)))})))) | ||
Theorem | dibffval 38158* | The partial isomorphism B for a lattice 𝐾. (Contributed by NM, 8-Dec-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝑉 → (DIsoB‘𝐾) = (𝑤 ∈ 𝐻 ↦ (𝑥 ∈ dom ((DIsoA‘𝐾)‘𝑤) ↦ ((((DIsoA‘𝐾)‘𝑤)‘𝑥) × {(𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ↦ ( I ↾ 𝐵))})))) | ||
Theorem | dibfval 38159* | The partial isomorphism B for a lattice 𝐾. (Contributed by NM, 8-Dec-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 0 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵)) & ⊢ 𝐽 = ((DIsoA‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊) ⇒ ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → 𝐼 = (𝑥 ∈ dom 𝐽 ↦ ((𝐽‘𝑥) × { 0 }))) | ||
Theorem | dibval 38160* | The partial isomorphism B for a lattice 𝐾. (Contributed by NM, 8-Dec-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 0 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵)) & ⊢ 𝐽 = ((DIsoA‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐽) → (𝐼‘𝑋) = ((𝐽‘𝑋) × { 0 })) | ||
Theorem | dibopelvalN 38161* | Member of the partial isomorphism B. (Contributed by NM, 18-Jan-2014.) (Revised by Mario Carneiro, 6-May-2015.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 0 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵)) & ⊢ 𝐽 = ((DIsoA‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐽) → (〈𝐹, 𝑆〉 ∈ (𝐼‘𝑋) ↔ (𝐹 ∈ (𝐽‘𝑋) ∧ 𝑆 = 0 ))) | ||
Theorem | dibval2 38162* | Value of the partial isomorphism B. (Contributed by NM, 18-Jan-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 0 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵)) & ⊢ 𝐽 = ((DIsoA‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐼‘𝑋) = ((𝐽‘𝑋) × { 0 })) | ||
Theorem | dibopelval2 38163* | Member of the partial isomorphism B. (Contributed by NM, 3-Mar-2014.) (Revised by Mario Carneiro, 6-May-2015.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 0 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵)) & ⊢ 𝐽 = ((DIsoA‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (〈𝐹, 𝑆〉 ∈ (𝐼‘𝑋) ↔ (𝐹 ∈ (𝐽‘𝑋) ∧ 𝑆 = 0 ))) | ||
Theorem | dibval3N 38164* | Value of the partial isomorphism B for a lattice 𝐾. (Contributed by NM, 24-Feb-2014.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) & ⊢ 0 = (𝑔 ∈ 𝑇 ↦ ( I ↾ 𝐵)) & ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐼‘𝑋) = ({𝑓 ∈ 𝑇 ∣ (𝑅‘𝑓) ≤ 𝑋} × { 0 })) | ||
Theorem | dibelval3 38165* | Member of the partial isomorphism B. (Contributed by NM, 26-Feb-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) & ⊢ 0 = (𝑔 ∈ 𝑇 ↦ ( I ↾ 𝐵)) & ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝑌 ∈ (𝐼‘𝑋) ↔ ∃𝑓 ∈ 𝑇 (𝑌 = 〈𝑓, 0 〉 ∧ (𝑅‘𝑓) ≤ 𝑋))) | ||
Theorem | dibopelval3 38166* | Member of the partial isomorphism B. (Contributed by NM, 3-Mar-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) & ⊢ 0 = (𝑔 ∈ 𝑇 ↦ ( I ↾ 𝐵)) & ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (〈𝐹, 𝑆〉 ∈ (𝐼‘𝑋) ↔ ((𝐹 ∈ 𝑇 ∧ (𝑅‘𝐹) ≤ 𝑋) ∧ 𝑆 = 0 ))) | ||
Theorem | dibelval1st 38167 | Membership in value of the partial isomorphism B for a lattice 𝐾. (Contributed by NM, 13-Feb-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐽 = ((DIsoA‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ (𝐼‘𝑋)) → (1st ‘𝑌) ∈ (𝐽‘𝑋)) | ||
Theorem | dibelval1st1 38168 | Membership in value of the partial isomorphism B for a lattice 𝐾. (Contributed by NM, 13-Feb-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ (𝐼‘𝑋)) → (1st ‘𝑌) ∈ 𝑇) | ||
Theorem | dibelval1st2N 38169 | Membership in value of the partial isomorphism B for a lattice 𝐾. (Contributed by NM, 13-Feb-2014.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ (𝐼‘𝑋)) → (𝑅‘(1st ‘𝑌)) ≤ 𝑋) | ||
Theorem | dibelval2nd 38170* | Membership in value of the partial isomorphism B for a lattice 𝐾. (Contributed by NM, 13-Feb-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 0 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵)) & ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ 𝑌 ∈ (𝐼‘𝑋)) → (2nd ‘𝑌) = 0 ) | ||
Theorem | dibn0 38171 | The value of the partial isomorphism B is not empty. (Contributed by NM, 18-Jan-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐼‘𝑋) ≠ ∅) | ||
Theorem | dibfna 38172 | Functionality and domain of the partial isomorphism B. (Contributed by NM, 17-Jan-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐽 = ((DIsoA‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊) ⇒ ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → 𝐼 Fn dom 𝐽) | ||
Theorem | dibdiadm 38173 | Domain of the partial isomorphism B. (Contributed by NM, 17-Jan-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐽 = ((DIsoA‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊) ⇒ ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → dom 𝐼 = dom 𝐽) | ||
Theorem | dibfnN 38174* | Functionality and domain of the partial isomorphism B. (Contributed by NM, 17-Jan-2014.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊) ⇒ ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → 𝐼 Fn {𝑥 ∈ 𝐵 ∣ 𝑥 ≤ 𝑊}) | ||
Theorem | dibdmN 38175* | Domain of the partial isomorphism A. (Contributed by NM, 8-Mar-2014.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊) ⇒ ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → dom 𝐼 = {𝑥 ∈ 𝐵 ∣ 𝑥 ≤ 𝑊}) | ||
Theorem | dibeldmN 38176 | Member of domain of the partial isomorphism B. (Contributed by NM, 17-Jan-2014.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊) ⇒ ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → (𝑋 ∈ dom 𝐼 ↔ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊))) | ||
Theorem | dibord 38177 | The isomorphism B for a lattice 𝐾 is order-preserving in the region under co-atom 𝑊. (Contributed by NM, 24-Feb-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → ((𝐼‘𝑋) ⊆ (𝐼‘𝑌) ↔ 𝑋 ≤ 𝑌)) | ||
Theorem | dib11N 38178 | The isomorphism B for a lattice 𝐾 is one-to-one in the region under co-atom 𝑊. (Contributed by NM, 24-Feb-2014.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) → ((𝐼‘𝑋) = (𝐼‘𝑌) ↔ 𝑋 = 𝑌)) | ||
Theorem | dibf11N 38179 | The partial isomorphism A for a lattice 𝐾 is a one-to-one function. Part of Lemma M of [Crawley] p. 120 line 27. (Contributed by NM, 4-Dec-2013.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝐼:dom 𝐼–1-1-onto→ran 𝐼) | ||
Theorem | dibclN 38180 | Closure of partial isomorphism B for a lattice 𝐾. (Contributed by NM, 8-Mar-2014.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ dom 𝐼) → (𝐼‘𝑋) ∈ ran 𝐼) | ||
Theorem | dibvalrel 38181 | The value of partial isomorphism B is a relation. (Contributed by NM, 8-Mar-2014.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊) ⇒ ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → Rel (𝐼‘𝑋)) | ||
Theorem | dib0 38182 | The value of partial isomorphism B at the lattice zero is the singleton of the zero vector i.e. the zero subspace. (Contributed by NM, 27-Mar-2014.) |
⊢ 0 = (0.‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑂 = (0g‘𝑈) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝐼‘ 0 ) = {𝑂}) | ||
Theorem | dib1dim 38183* | Two expressions for the 1-dimensional subspaces of vector space H. (Contributed by NM, 24-Feb-2014.) (Revised by Mario Carneiro, 24-Jun-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵)) & ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝐼‘(𝑅‘𝐹)) = {𝑔 ∈ (𝑇 × 𝐸) ∣ ∃𝑠 ∈ 𝐸 𝑔 = 〈(𝑠‘𝐹), 𝑂〉}) | ||
Theorem | dibglbN 38184* | Partial isomorphism B of a lattice glb. (Contributed by NM, 9-Mar-2014.) (New usage is discouraged.) |
⊢ 𝐺 = (glb‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ dom 𝐼 ∧ 𝑆 ≠ ∅)) → (𝐼‘(𝐺‘𝑆)) = ∩ 𝑥 ∈ 𝑆 (𝐼‘𝑥)) | ||
Theorem | dibintclN 38185 | The intersection of partial isomorphism B closed subspaces is a closed subspace. (Contributed by NM, 8-Mar-2014.) (New usage is discouraged.) |
⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ ran 𝐼 ∧ 𝑆 ≠ ∅)) → ∩ 𝑆 ∈ ran 𝐼) | ||
Theorem | dib1dim2 38186* | Two expressions for a 1-dimensional subspace of vector space H (when 𝐹 is a nonzero vector i.e. non-identity translation). (Contributed by NM, 24-Feb-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑅 = ((trL‘𝐾)‘𝑊) & ⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵)) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑈) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇) → (𝐼‘(𝑅‘𝐹)) = (𝑁‘{〈𝐹, 𝑂〉})) | ||
Theorem | dibss 38187 | The partial isomorphism B maps to a set of vectors in full vector space H. (Contributed by NM, 1-Jan-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝑉 = (Base‘𝑈) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐼‘𝑋) ⊆ 𝑉) | ||
Theorem | diblss 38188 | The value of partial isomorphism B is a subspace of partial vector space H. TODO: use dib* specific theorems instead of dia* ones to shorten proof? (Contributed by NM, 11-Feb-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑈) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐼‘𝑋) ∈ 𝑆) | ||
Theorem | diblsmopel 38189* | Membership in subspace sum for partial isomorphism B. (Contributed by NM, 21-Sep-2014.) (Revised by Mario Carneiro, 6-May-2015.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝑂 = (𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵)) & ⊢ 𝑉 = ((DVecA‘𝐾)‘𝑊) & ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) & ⊢ ⊕ = (LSSum‘𝑉) & ⊢ ✚ = (LSSum‘𝑈) & ⊢ 𝐽 = ((DIsoA‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊) & ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) & ⊢ (𝜑 → (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) & ⊢ (𝜑 → (𝑌 ∈ 𝐵 ∧ 𝑌 ≤ 𝑊)) ⇒ ⊢ (𝜑 → (〈𝐹, 𝑆〉 ∈ ((𝐼‘𝑋) ✚ (𝐼‘𝑌)) ↔ (𝐹 ∈ ((𝐽‘𝑋) ⊕ (𝐽‘𝑌)) ∧ 𝑆 = 𝑂))) | ||
Syntax | cdic 38190 | Extend class notation with isomorphism C. |
class DIsoC | ||
Definition | df-dic 38191* | Isomorphism C has domain of lattice atoms that are not less than or equal to the fiducial co-atom 𝑤. The value is a one-dimensional subspace generated by the pair consisting of the ℩ vector below and the endomorphism ring unit. Definition of phi(q) in [Crawley] p. 121. Note that we use the fixed atom ((oc k ) 𝑤) to represent the p in their "Choose an atom p..." on line 21. (Contributed by NM, 15-Dec-2013.) |
⊢ DIsoC = (𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑞 ∈ {𝑟 ∈ (Atoms‘𝑘) ∣ ¬ 𝑟(le‘𝑘)𝑤} ↦ {〈𝑓, 𝑠〉 ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ ((LTrn‘𝑘)‘𝑤)(𝑔‘((oc‘𝑘)‘𝑤)) = 𝑞)) ∧ 𝑠 ∈ ((TEndo‘𝑘)‘𝑤))}))) | ||
Theorem | dicffval 38192* | The partial isomorphism C for a lattice 𝐾. (Contributed by NM, 15-Dec-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝑉 → (DIsoC‘𝐾) = (𝑤 ∈ 𝐻 ↦ (𝑞 ∈ {𝑟 ∈ 𝐴 ∣ ¬ 𝑟 ≤ 𝑤} ↦ {〈𝑓, 𝑠〉 ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ ((LTrn‘𝐾)‘𝑤)(𝑔‘((oc‘𝐾)‘𝑤)) = 𝑞)) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑤))}))) | ||
Theorem | dicfval 38193* | The partial isomorphism C for a lattice 𝐾. (Contributed by NM, 15-Dec-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑃 = ((oc‘𝐾)‘𝑊) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoC‘𝐾)‘𝑊) ⇒ ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → 𝐼 = (𝑞 ∈ {𝑟 ∈ 𝐴 ∣ ¬ 𝑟 ≤ 𝑊} ↦ {〈𝑓, 𝑠〉 ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑞)) ∧ 𝑠 ∈ 𝐸)})) | ||
Theorem | dicval 38194* | The partial isomorphism C for a lattice 𝐾. (Contributed by NM, 15-Dec-2013.) (Revised by Mario Carneiro, 22-Sep-2015.) |
⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑃 = ((oc‘𝐾)‘𝑊) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoC‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝐼‘𝑄) = {〈𝑓, 𝑠〉 ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) ∧ 𝑠 ∈ 𝐸)}) | ||
Theorem | dicopelval 38195* | Membership in value of the partial isomorphism C for a lattice 𝐾. (Contributed by NM, 15-Feb-2014.) |
⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑃 = ((oc‘𝐾)‘𝑊) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoC‘𝐾)‘𝑊) & ⊢ 𝐹 ∈ V & ⊢ 𝑆 ∈ V ⇒ ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (〈𝐹, 𝑆〉 ∈ (𝐼‘𝑄) ↔ (𝐹 = (𝑆‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) ∧ 𝑆 ∈ 𝐸))) | ||
Theorem | dicelvalN 38196* | Membership in value of the partial isomorphism C for a lattice 𝐾. (Contributed by NM, 25-Feb-2014.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑃 = ((oc‘𝐾)‘𝑊) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoC‘𝐾)‘𝑊) ⇒ ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝑌 ∈ (𝐼‘𝑄) ↔ (𝑌 ∈ (V × V) ∧ ((1st ‘𝑌) = ((2nd ‘𝑌)‘(℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄)) ∧ (2nd ‘𝑌) ∈ 𝐸)))) | ||
Theorem | dicval2 38197* | The partial isomorphism C for a lattice 𝐾. (Contributed by NM, 20-Feb-2014.) |
⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑃 = ((oc‘𝐾)‘𝑊) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoC‘𝐾)‘𝑊) & ⊢ 𝐺 = (℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄) ⇒ ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝐼‘𝑄) = {〈𝑓, 𝑠〉 ∣ (𝑓 = (𝑠‘𝐺) ∧ 𝑠 ∈ 𝐸)}) | ||
Theorem | dicelval3 38198* | Member of the partial isomorphism C. (Contributed by NM, 26-Feb-2014.) |
⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑃 = ((oc‘𝐾)‘𝑊) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoC‘𝐾)‘𝑊) & ⊢ 𝐺 = (℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄) ⇒ ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝑌 ∈ (𝐼‘𝑄) ↔ ∃𝑠 ∈ 𝐸 𝑌 = 〈(𝑠‘𝐺), 𝑠〉)) | ||
Theorem | dicopelval2 38199* | Membership in value of the partial isomorphism C for a lattice 𝐾. (Contributed by NM, 20-Feb-2014.) |
⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑃 = ((oc‘𝐾)‘𝑊) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoC‘𝐾)‘𝑊) & ⊢ 𝐺 = (℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄) & ⊢ 𝐹 ∈ V & ⊢ 𝑆 ∈ V ⇒ ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (〈𝐹, 𝑆〉 ∈ (𝐼‘𝑄) ↔ (𝐹 = (𝑆‘𝐺) ∧ 𝑆 ∈ 𝐸))) | ||
Theorem | dicelval2N 38200* | Membership in value of the partial isomorphism C for a lattice 𝐾. (Contributed by NM, 25-Feb-2014.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑃 = ((oc‘𝐾)‘𝑊) & ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) & ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) & ⊢ 𝐼 = ((DIsoC‘𝐾)‘𝑊) & ⊢ 𝐺 = (℩𝑔 ∈ 𝑇 (𝑔‘𝑃) = 𝑄) ⇒ ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝑌 ∈ (𝐼‘𝑄) ↔ (𝑌 ∈ (V × V) ∧ ((1st ‘𝑌) = ((2nd ‘𝑌)‘𝐺) ∧ (2nd ‘𝑌) ∈ 𝐸)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |