Home | Metamath
Proof Explorer Theorem List (p. 362 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 | lflsc0N 36101 | The scalar product with the zero functional is the zero functional. (Contributed by NM, 7-Oct-2014.) (New usage is discouraged.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐷) & ⊢ · = (.r‘𝐷) & ⊢ 0 = (0g‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝐾) ⇒ ⊢ (𝜑 → ((𝑉 × { 0 }) ∘f · (𝑉 × {𝑋})) = (𝑉 × { 0 })) | ||
Theorem | lfl1sc 36102 | The (right vector space) scalar product of a functional with one is the functional. (Contributed by NM, 21-Oct-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐾 = (Base‘𝐷) & ⊢ · = (.r‘𝐷) & ⊢ 1 = (1r‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺 ∘f · (𝑉 × { 1 })) = 𝐺) | ||
Syntax | clk 36103 | Extend class notation with the kernel of a functional (set of vectors whose functional value is zero) on a left module or left vector space. |
class LKer | ||
Definition | df-lkr 36104* | Define the kernel of a functional (set of vectors whose functional value is zero) on a left module or left vector space. (Contributed by NM, 15-Apr-2014.) |
⊢ LKer = (𝑤 ∈ V ↦ (𝑓 ∈ (LFnl‘𝑤) ↦ (◡𝑓 “ {(0g‘(Scalar‘𝑤))}))) | ||
Theorem | lkrfval 36105* | The kernel of a functional. (Contributed by NM, 15-Apr-2014.) (Revised by Mario Carneiro, 24-Jun-2014.) |
⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 0 = (0g‘𝐷) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐾 = (LKer‘𝑊) ⇒ ⊢ (𝑊 ∈ 𝑋 → 𝐾 = (𝑓 ∈ 𝐹 ↦ (◡𝑓 “ { 0 }))) | ||
Theorem | lkrval 36106 | Value of the kernel of a functional. (Contributed by NM, 15-Apr-2014.) |
⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 0 = (0g‘𝐷) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐾 = (LKer‘𝑊) ⇒ ⊢ ((𝑊 ∈ 𝑋 ∧ 𝐺 ∈ 𝐹) → (𝐾‘𝐺) = (◡𝐺 “ { 0 })) | ||
Theorem | ellkr 36107 | Membership in the kernel of a functional. (elnlfn 29633 analog.) (Contributed by NM, 16-Apr-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 0 = (0g‘𝐷) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐾 = (LKer‘𝑊) ⇒ ⊢ ((𝑊 ∈ 𝑌 ∧ 𝐺 ∈ 𝐹) → (𝑋 ∈ (𝐾‘𝐺) ↔ (𝑋 ∈ 𝑉 ∧ (𝐺‘𝑋) = 0 ))) | ||
Theorem | lkrval2 36108* | Value of the kernel of a functional. (Contributed by NM, 15-Apr-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 0 = (0g‘𝐷) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐾 = (LKer‘𝑊) ⇒ ⊢ ((𝑊 ∈ 𝑋 ∧ 𝐺 ∈ 𝐹) → (𝐾‘𝐺) = {𝑥 ∈ 𝑉 ∣ (𝐺‘𝑥) = 0 }) | ||
Theorem | ellkr2 36109 | Membership in the kernel of a functional. (Contributed by NM, 12-Jan-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 0 = (0g‘𝐷) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐾 = (LKer‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ 𝑌) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑋 ∈ (𝐾‘𝐺) ↔ (𝐺‘𝑋) = 0 )) | ||
Theorem | lkrcl 36110 | A member of the kernel of a functional is a vector. (Contributed by NM, 16-Apr-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐾 = (LKer‘𝑊) ⇒ ⊢ ((𝑊 ∈ 𝑌 ∧ 𝐺 ∈ 𝐹 ∧ 𝑋 ∈ (𝐾‘𝐺)) → 𝑋 ∈ 𝑉) | ||
Theorem | lkrf0 36111 | The value of a functional at a member of its kernel is zero. (Contributed by NM, 16-Apr-2014.) |
⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 0 = (0g‘𝐷) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐾 = (LKer‘𝑊) ⇒ ⊢ ((𝑊 ∈ 𝑌 ∧ 𝐺 ∈ 𝐹 ∧ 𝑋 ∈ (𝐾‘𝐺)) → (𝐺‘𝑋) = 0 ) | ||
Theorem | lkr0f 36112 | The kernel of the zero functional is the set of all vectors. (Contributed by NM, 17-Apr-2014.) |
⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 0 = (0g‘𝐷) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐾 = (LKer‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → ((𝐾‘𝐺) = 𝑉 ↔ 𝐺 = (𝑉 × { 0 }))) | ||
Theorem | lkrlss 36113 | The kernel of a linear functional is a subspace. (nlelshi 29765 analog.) (Contributed by NM, 16-Apr-2014.) |
⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐾 = (LKer‘𝑊) & ⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹) → (𝐾‘𝐺) ∈ 𝑆) | ||
Theorem | lkrssv 36114 | The kernel of a linear functional is a set of vectors. (Contributed by NM, 1-Jan-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐾 = (LKer‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐾‘𝐺) ⊆ 𝑉) | ||
Theorem | lkrsc 36115 | The kernel of a nonzero scalar product of a functional equals the kernel of the functional. (Contributed by NM, 9-Oct-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐷) & ⊢ · = (.r‘𝐷) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐿 = (LKer‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝑅 ∈ 𝐾) & ⊢ 0 = (0g‘𝐷) & ⊢ (𝜑 → 𝑅 ≠ 0 ) ⇒ ⊢ (𝜑 → (𝐿‘(𝐺 ∘f · (𝑉 × {𝑅}))) = (𝐿‘𝐺)) | ||
Theorem | lkrscss 36116 | The kernel of a scalar product of a functional includes the kernel of the functional. (The inclusion is proper for the zero product and equality otherwise.) (Contributed by NM, 9-Oct-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐷) & ⊢ · = (.r‘𝐷) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐿 = (LKer‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝑅 ∈ 𝐾) ⇒ ⊢ (𝜑 → (𝐿‘𝐺) ⊆ (𝐿‘(𝐺 ∘f · (𝑉 × {𝑅})))) | ||
Theorem | eqlkr 36117* | Two functionals with the same kernel are the same up to a constant. (Contributed by NM, 18-Apr-2014.) |
⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐷) & ⊢ · = (.r‘𝐷) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐿 = (LKer‘𝑊) ⇒ ⊢ ((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) → ∃𝑟 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝐻‘𝑥) = ((𝐺‘𝑥) · 𝑟)) | ||
Theorem | eqlkr2 36118* | Two functionals with the same kernel are the same up to a constant. (Contributed by NM, 10-Oct-2014.) |
⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐷) & ⊢ · = (.r‘𝐷) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐿 = (LKer‘𝑊) ⇒ ⊢ ((𝑊 ∈ LVec ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) → ∃𝑟 ∈ 𝐾 𝐻 = (𝐺 ∘f · (𝑉 × {𝑟}))) | ||
Theorem | eqlkr3 36119 | Two functionals with the same kernel are equal if they are equal at any nonzero value. (Contributed by NM, 2-Jan-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑆 = (Scalar‘𝑊) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑆) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐾 = (LKer‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝐻 ∈ 𝐹) & ⊢ (𝜑 → (𝐾‘𝐺) = (𝐾‘𝐻)) & ⊢ (𝜑 → (𝐺‘𝑋) = (𝐻‘𝑋)) & ⊢ (𝜑 → (𝐺‘𝑋) ≠ 0 ) ⇒ ⊢ (𝜑 → 𝐺 = 𝐻) | ||
Theorem | lkrlsp 36120 | The subspace sum of a kernel and the span of a vector not in the kernel (by ellkr 36107) is the whole vector space. (Contributed by NM, 19-Apr-2014.) |
⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 0 = (0g‘𝐷) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐾 = (LKer‘𝑊) ⇒ ⊢ ((𝑊 ∈ LVec ∧ (𝑋 ∈ 𝑉 ∧ 𝐺 ∈ 𝐹) ∧ (𝐺‘𝑋) ≠ 0 ) → ((𝐾‘𝐺) ⊕ (𝑁‘{𝑋})) = 𝑉) | ||
Theorem | lkrlsp2 36121 | The subspace sum of a kernel and the span of a vector not in the kernel is the whole vector space. (Contributed by NM, 12-May-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐾 = (LKer‘𝑊) ⇒ ⊢ ((𝑊 ∈ LVec ∧ (𝑋 ∈ 𝑉 ∧ 𝐺 ∈ 𝐹) ∧ ¬ 𝑋 ∈ (𝐾‘𝐺)) → ((𝐾‘𝐺) ⊕ (𝑁‘{𝑋})) = 𝑉) | ||
Theorem | lkrlsp3 36122 | The subspace sum of a kernel and the span of a vector not in the kernel is the whole vector space. (Contributed by NM, 29-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐾 = (LKer‘𝑊) ⇒ ⊢ ((𝑊 ∈ LVec ∧ (𝑋 ∈ 𝑉 ∧ 𝐺 ∈ 𝐹) ∧ ¬ 𝑋 ∈ (𝐾‘𝐺)) → (𝑁‘((𝐾‘𝐺) ∪ {𝑋})) = 𝑉) | ||
Theorem | lkrshp 36123 | The kernel of a nonzero functional is a hyperplane. (Contributed by NM, 29-Jun-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 0 = (0g‘𝐷) & ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐾 = (LKer‘𝑊) ⇒ ⊢ ((𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ (𝑉 × { 0 })) → (𝐾‘𝐺) ∈ 𝐻) | ||
Theorem | lkrshp3 36124 | The kernels of nonzero functionals are hyperplanes. (Contributed by NM, 17-Jul-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 0 = (0g‘𝐷) & ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐾 = (LKer‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → ((𝐾‘𝐺) ∈ 𝐻 ↔ 𝐺 ≠ (𝑉 × { 0 }))) | ||
Theorem | lkrshpor 36125 | The kernel of a functional is either a hyperplane or the full vector space. (Contributed by NM, 7-Oct-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐾 = (LKer‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → ((𝐾‘𝐺) ∈ 𝐻 ∨ (𝐾‘𝐺) = 𝑉)) | ||
Theorem | lkrshp4 36126 | A kernel is a hyperplane iff it doesn't contain all vectors. (Contributed by NM, 1-Nov-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐾 = (LKer‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → ((𝐾‘𝐺) ≠ 𝑉 ↔ (𝐾‘𝐺) ∈ 𝐻)) | ||
Theorem | lshpsmreu 36127* | Lemma for lshpkrex 36136. Show uniqueness of ring multiplier 𝑘 when a vector 𝑋 is broken down into components, one in a hyperplane and the other outside of it . TODO: do we need the cbvrexv 3454 for 𝑎 to 𝑐? (Contributed by NM, 4-Jan-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝐻) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑍})) = 𝑉) & ⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐷) & ⊢ · = ( ·𝑠 ‘𝑊) ⇒ ⊢ (𝜑 → ∃!𝑘 ∈ 𝐾 ∃𝑦 ∈ 𝑈 𝑋 = (𝑦 + (𝑘 · 𝑍))) | ||
Theorem | lshpkrlem1 36128* | Lemma for lshpkrex 36136. The value of tentative functional 𝐺 is zero iff its argument belongs to hyperplane 𝑈. (Contributed by NM, 14-Jul-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝐻) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑍})) = 𝑉) & ⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐷) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 0 = (0g‘𝐷) & ⊢ 𝐺 = (𝑥 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝐾 ∃𝑦 ∈ 𝑈 𝑥 = (𝑦 + (𝑘 · 𝑍)))) ⇒ ⊢ (𝜑 → (𝑋 ∈ 𝑈 ↔ (𝐺‘𝑋) = 0 )) | ||
Theorem | lshpkrlem2 36129* | Lemma for lshpkrex 36136. The value of tentative functional 𝐺 is a scalar. (Contributed by NM, 16-Jul-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝐻) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑍})) = 𝑉) & ⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐷) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 0 = (0g‘𝐷) & ⊢ 𝐺 = (𝑥 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝐾 ∃𝑦 ∈ 𝑈 𝑥 = (𝑦 + (𝑘 · 𝑍)))) ⇒ ⊢ (𝜑 → (𝐺‘𝑋) ∈ 𝐾) | ||
Theorem | lshpkrlem3 36130* | Lemma for lshpkrex 36136. Defining property of 𝐺‘𝑋. (Contributed by NM, 15-Jul-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝐻) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑍})) = 𝑉) & ⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐷) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 0 = (0g‘𝐷) & ⊢ 𝐺 = (𝑥 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝐾 ∃𝑦 ∈ 𝑈 𝑥 = (𝑦 + (𝑘 · 𝑍)))) ⇒ ⊢ (𝜑 → ∃𝑧 ∈ 𝑈 𝑋 = (𝑧 + ((𝐺‘𝑋) · 𝑍))) | ||
Theorem | lshpkrlem4 36131* | Lemma for lshpkrex 36136. Part of showing linearity of 𝐺. (Contributed by NM, 16-Jul-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝐻) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑍})) = 𝑉) & ⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐷) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 0 = (0g‘𝐷) & ⊢ 𝐺 = (𝑥 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝐾 ∃𝑦 ∈ 𝑈 𝑥 = (𝑦 + (𝑘 · 𝑍)))) ⇒ ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑉 ∧ 𝑠 ∈ 𝑉) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)))) → ((𝑙 · 𝑢) + 𝑣) = (((𝑙 · 𝑟) + 𝑠) + (((𝑙(.r‘𝐷)(𝐺‘𝑢))(+g‘𝐷)(𝐺‘𝑣)) · 𝑍))) | ||
Theorem | lshpkrlem5 36132* | Lemma for lshpkrex 36136. Part of showing linearity of 𝐺. (Contributed by NM, 16-Jul-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝐻) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑍})) = 𝑉) & ⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐷) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 0 = (0g‘𝐷) & ⊢ 𝐺 = (𝑥 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝐾 ∃𝑦 ∈ 𝑈 𝑥 = (𝑦 + (𝑘 · 𝑍)))) ⇒ ⊢ (((𝜑 ∧ 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉) ∧ (𝑣 ∈ 𝑉 ∧ 𝑟 ∈ 𝑈 ∧ (𝑠 ∈ 𝑈 ∧ 𝑧 ∈ 𝑈)) ∧ (𝑢 = (𝑟 + ((𝐺‘𝑢) · 𝑍)) ∧ 𝑣 = (𝑠 + ((𝐺‘𝑣) · 𝑍)) ∧ ((𝑙 · 𝑢) + 𝑣) = (𝑧 + ((𝐺‘((𝑙 · 𝑢) + 𝑣)) · 𝑍)))) → (𝐺‘((𝑙 · 𝑢) + 𝑣)) = ((𝑙(.r‘𝐷)(𝐺‘𝑢))(+g‘𝐷)(𝐺‘𝑣))) | ||
Theorem | lshpkrlem6 36133* | Lemma for lshpkrex 36136. Show linearlity of 𝐺. (Contributed by NM, 17-Jul-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝐻) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑍})) = 𝑉) & ⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐷) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 0 = (0g‘𝐷) & ⊢ 𝐺 = (𝑥 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝐾 ∃𝑦 ∈ 𝑈 𝑥 = (𝑦 + (𝑘 · 𝑍)))) ⇒ ⊢ ((𝜑 ∧ (𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉)) → (𝐺‘((𝑙 · 𝑢) + 𝑣)) = ((𝑙(.r‘𝐷)(𝐺‘𝑢))(+g‘𝐷)(𝐺‘𝑣))) | ||
Theorem | lshpkrcl 36134* | The set 𝐺 defined by hyperplane 𝑈 is a linear functional. (Contributed by NM, 17-Jul-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝐻) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑍})) = 𝑉) & ⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐷) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐺 = (𝑥 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝐾 ∃𝑦 ∈ 𝑈 𝑥 = (𝑦 + (𝑘 · 𝑍)))) & ⊢ 𝐹 = (LFnl‘𝑊) ⇒ ⊢ (𝜑 → 𝐺 ∈ 𝐹) | ||
Theorem | lshpkr 36135* | The kernel of functional 𝐺 is the hyperplane defining it. (Contributed by NM, 17-Jul-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝐻) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑍})) = 𝑉) & ⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐷) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐺 = (𝑥 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝐾 ∃𝑦 ∈ 𝑈 𝑥 = (𝑦 + (𝑘 · 𝑍)))) & ⊢ 𝐿 = (LKer‘𝑊) ⇒ ⊢ (𝜑 → (𝐿‘𝐺) = 𝑈) | ||
Theorem | lshpkrex 36136* | There exists a functional whose kernel equals a given hyperplane. Part of Th. 1.27 of Barbu and Precupanu, Convexity and Optimization in Banach Spaces. (Contributed by NM, 17-Jul-2014.) |
⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐾 = (LKer‘𝑊) ⇒ ⊢ ((𝑊 ∈ LVec ∧ 𝑈 ∈ 𝐻) → ∃𝑔 ∈ 𝐹 (𝐾‘𝑔) = 𝑈) | ||
Theorem | lshpset2N 36137* | The set of all hyperplanes of a left module or left vector space equals the set of all kernels of nonzero functionals. (Contributed by NM, 17-Jul-2014.) (New usage is discouraged.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 0 = (0g‘𝐷) & ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐾 = (LKer‘𝑊) ⇒ ⊢ (𝑊 ∈ LVec → 𝐻 = {𝑠 ∣ ∃𝑔 ∈ 𝐹 (𝑔 ≠ (𝑉 × { 0 }) ∧ 𝑠 = (𝐾‘𝑔))}) | ||
Theorem | islshpkrN 36138* | The predicate "is a hyperplane" (of a left module or left vector space). TODO: should it be 𝑈 = (𝐾‘𝑔) or (𝐾‘𝑔) = 𝑈 as in lshpkrex 36136? Both standards seem to be used randomly throughout set.mm; we should decide on a preferred one. (Contributed by NM, 7-Oct-2014.) (New usage is discouraged.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 0 = (0g‘𝐷) & ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐾 = (LKer‘𝑊) ⇒ ⊢ (𝑊 ∈ LVec → (𝑈 ∈ 𝐻 ↔ ∃𝑔 ∈ 𝐹 (𝑔 ≠ (𝑉 × { 0 }) ∧ 𝑈 = (𝐾‘𝑔)))) | ||
Theorem | lfl1dim 36139* | Equivalent expressions for a 1-dim subspace (ray) of functionals. (Contributed by NM, 24-Oct-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐿 = (LKer‘𝑊) & ⊢ 𝐾 = (Base‘𝐷) & ⊢ · = (.r‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → {𝑔 ∈ 𝐹 ∣ (𝐿‘𝐺) ⊆ (𝐿‘𝑔)} = {𝑔 ∣ ∃𝑘 ∈ 𝐾 𝑔 = (𝐺 ∘f · (𝑉 × {𝑘}))}) | ||
Theorem | lfl1dim2N 36140* | Equivalent expressions for a 1-dim subspace (ray) of functionals. TODO: delete this if not useful; lfl1dim 36139 may be more compatible with lspsn 19705. (Contributed by NM, 24-Oct-2014.) (New usage is discouraged.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐿 = (LKer‘𝑊) & ⊢ 𝐾 = (Base‘𝐷) & ⊢ · = (.r‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → {𝑔 ∈ 𝐹 ∣ (𝐿‘𝐺) ⊆ (𝐿‘𝑔)} = {𝑔 ∈ 𝐹 ∣ ∃𝑘 ∈ 𝐾 𝑔 = (𝐺 ∘f · (𝑉 × {𝑘}))}) | ||
Syntax | cld 36141 | Extend class notation with left dualvector space. |
class LDual | ||
Definition | df-ldual 36142* | Define the (left) dual of a left vector space (or module) in which the vectors are functionals. In many texts, this is defined as a right vector space, but by reversing the multiplication we achieve a left vector space, as is done in definition of dual vector space in [Holland95] p. 218. This allows us to reuse our existing collection of left vector space theorems. The restriction on ∘f (+g‘𝑣) allows it to be a set; see ofmres 7676. Note the operation reversal in the scalar product to allow us to use the original scalar ring instead of the oppr ring, for convenience. (Contributed by NM, 18-Oct-2014.) |
⊢ LDual = (𝑣 ∈ V ↦ ({〈(Base‘ndx), (LFnl‘𝑣)〉, 〈(+g‘ndx), ( ∘f (+g‘(Scalar‘𝑣)) ↾ ((LFnl‘𝑣) × (LFnl‘𝑣)))〉, 〈(Scalar‘ndx), (oppr‘(Scalar‘𝑣))〉} ∪ {〈( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑣)), 𝑓 ∈ (LFnl‘𝑣) ↦ (𝑓 ∘f (.r‘(Scalar‘𝑣))((Base‘𝑣) × {𝑘})))〉})) | ||
Theorem | ldualset 36143* | Define the (left) dual of a left vector space (or module) in which the vectors are functionals. In many texts, this is defined as a right vector space, but by reversing the multiplication we achieve a left vector space, as is done in definition of dual vector space in [Holland95] p. 218. This allows us to reuse our existing collection of left vector space theorems. Note the operation reversal in the scalar product to allow us to use the original scalar ring instead of the oppr ring, for convenience. (Contributed by NM, 18-Oct-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑅) & ⊢ ✚ = ( ∘f + ↾ (𝐹 × 𝐹)) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝑂 = (oppr‘𝑅) & ⊢ ∙ = (𝑘 ∈ 𝐾, 𝑓 ∈ 𝐹 ↦ (𝑓 ∘f · (𝑉 × {𝑘}))) & ⊢ (𝜑 → 𝑊 ∈ 𝑋) ⇒ ⊢ (𝜑 → 𝐷 = ({〈(Base‘ndx), 𝐹〉, 〈(+g‘ndx), ✚ 〉, 〈(Scalar‘ndx), 𝑂〉} ∪ {〈( ·𝑠 ‘ndx), ∙ 〉})) | ||
Theorem | ldualvbase 36144 | The vectors of a dual space are functionals of the original space. (Contributed by NM, 18-Oct-2014.) |
⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ 𝑉 = (Base‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ 𝑋) ⇒ ⊢ (𝜑 → 𝑉 = 𝐹) | ||
Theorem | ldualelvbase 36145 | Utility theorem for converting a functional to a vector of the dual space in order to use standard vector theorems. (Contributed by NM, 6-Jan-2015.) |
⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ 𝑉 = (Base‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ 𝑋) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → 𝐺 ∈ 𝑉) | ||
Theorem | ldualfvadd 36146 | Vector addition in the dual of a vector space. (Contributed by NM, 21-Oct-2014.) |
⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ + = (+g‘𝑅) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ ✚ = (+g‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ 𝑋) & ⊢ ⨣ = ( ∘f + ↾ (𝐹 × 𝐹)) ⇒ ⊢ (𝜑 → ✚ = ⨣ ) | ||
Theorem | ldualvadd 36147 | Vector addition in the dual of a vector space. (Contributed by NM, 21-Oct-2014.) |
⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ + = (+g‘𝑅) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ ✚ = (+g‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ 𝑋) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝐻 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺 ✚ 𝐻) = (𝐺 ∘f + 𝐻)) | ||
Theorem | ldualvaddcl 36148 | The value of vector addition in the dual of a vector space is a functional. (Contributed by NM, 21-Oct-2014.) |
⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ + = (+g‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝐻 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺 + 𝐻) ∈ 𝐹) | ||
Theorem | ldualvaddval 36149 | The value of the value of vector addition in the dual of a vector space. (Contributed by NM, 7-Jan-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ + = (+g‘𝑅) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ ✚ = (+g‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝐻 ∈ 𝐹) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝐺 ✚ 𝐻)‘𝑋) = ((𝐺‘𝑋) + (𝐻‘𝑋))) | ||
Theorem | ldualsca 36150 | The ring of scalars of the dual of a vector space. (Contributed by NM, 18-Oct-2014.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝑂 = (oppr‘𝐹) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ 𝑅 = (Scalar‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ 𝑋) ⇒ ⊢ (𝜑 → 𝑅 = 𝑂) | ||
Theorem | ldualsbase 36151 | Base set of scalar ring for the dual of a vector space. (Contributed by NM, 24-Oct-2014.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐿 = (Base‘𝐹) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ 𝑅 = (Scalar‘𝐷) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ (𝜑 → 𝑊 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐾 = 𝐿) | ||
Theorem | ldualsaddN 36152 | Scalar addition for the dual of a vector space. (Contributed by NM, 24-Oct-2014.) (New usage is discouraged.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ + = (+g‘𝐹) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ 𝑅 = (Scalar‘𝐷) & ⊢ ✚ = (+g‘𝑅) & ⊢ (𝜑 → 𝑊 ∈ 𝑉) ⇒ ⊢ (𝜑 → ✚ = + ) | ||
Theorem | ldualsmul 36153 | Scalar multiplication for the dual of a vector space. (Contributed by NM, 19-Oct-2014.) (Revised by Mario Carneiro, 22-Sep-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ · = (.r‘𝐹) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ 𝑅 = (Scalar‘𝐷) & ⊢ ∙ = (.r‘𝑅) & ⊢ (𝜑 → 𝑊 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐾) & ⊢ (𝜑 → 𝑌 ∈ 𝐾) ⇒ ⊢ (𝜑 → (𝑋 ∙ 𝑌) = (𝑌 · 𝑋)) | ||
Theorem | ldualfvs 36154* | Scalar product operation for the dual of a vector space. (Contributed by NM, 18-Oct-2014.) |
⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ × = (.r‘𝑅) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ ∙ = ( ·𝑠 ‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ 𝑌) & ⊢ · = (𝑘 ∈ 𝐾, 𝑓 ∈ 𝐹 ↦ (𝑓 ∘f × (𝑉 × {𝑘}))) ⇒ ⊢ (𝜑 → ∙ = · ) | ||
Theorem | ldualvs 36155 | Scalar product operation value (which is a functional) for the dual of a vector space. (Contributed by NM, 18-Oct-2014.) |
⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ × = (.r‘𝑅) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ ∙ = ( ·𝑠 ‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ 𝑌) & ⊢ (𝜑 → 𝑋 ∈ 𝐾) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝑋 ∙ 𝐺) = (𝐺 ∘f × (𝑉 × {𝑋}))) | ||
Theorem | ldualvsval 36156 | Value of scalar product operation value for the dual of a vector space. (Contributed by NM, 18-Oct-2014.) |
⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ × = (.r‘𝑅) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ ∙ = ( ·𝑠 ‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ 𝑌) & ⊢ (𝜑 → 𝑋 ∈ 𝐾) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝑋 ∙ 𝐺)‘𝐴) = ((𝐺‘𝐴) × 𝑋)) | ||
Theorem | ldualvscl 36157 | The scalar product operation value is a functional. (Contributed by NM, 18-Oct-2014.) |
⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ · = ( ·𝑠 ‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝐾) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝑋 · 𝐺) ∈ 𝐹) | ||
Theorem | ldualvaddcom 36158 | Commutative law for vector (functional) addition. (Contributed by NM, 17-Jan-2015.) |
⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ + = (+g‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝐹) & ⊢ (𝜑 → 𝑌 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) = (𝑌 + 𝑋)) | ||
Theorem | ldualvsass 36159 | Associative law for scalar product operation. (Contributed by NM, 20-Oct-2014.) |
⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ × = (.r‘𝑅) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ · = ( ·𝑠 ‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝐾) & ⊢ (𝜑 → 𝑌 ∈ 𝐾) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → ((𝑌 × 𝑋) · 𝐺) = (𝑋 · (𝑌 · 𝐺))) | ||
Theorem | ldualvsass2 36160 | Associative law for scalar product operation, using operations from the dual space. (Contributed by NM, 20-Oct-2014.) |
⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ 𝑄 = (Scalar‘𝐷) & ⊢ × = (.r‘𝑄) & ⊢ · = ( ·𝑠 ‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝐾) & ⊢ (𝜑 → 𝑌 ∈ 𝐾) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → ((𝑋 × 𝑌) · 𝐺) = (𝑋 · (𝑌 · 𝐺))) | ||
Theorem | ldualvsdi1 36161 | Distributive law for scalar product operation, using operations from the dual space. (Contributed by NM, 21-Oct-2014.) |
⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ + = (+g‘𝐷) & ⊢ · = ( ·𝑠 ‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝐾) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝐻 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝑋 · (𝐺 + 𝐻)) = ((𝑋 · 𝐺) + (𝑋 · 𝐻))) | ||
Theorem | ldualvsdi2 36162 | Reverse distributive law for scalar product operation, using operations from the dual space. (Contributed by NM, 21-Oct-2014.) |
⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ + = (+g‘𝑅) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ ✚ = (+g‘𝐷) & ⊢ · = ( ·𝑠 ‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝐾) & ⊢ (𝜑 → 𝑌 ∈ 𝐾) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → ((𝑋 + 𝑌) · 𝐺) = ((𝑋 · 𝐺) ✚ (𝑌 · 𝐺))) | ||
Theorem | ldualgrplem 36163 | Lemma for ldualgrp 36164. (Contributed by NM, 22-Oct-2014.) |
⊢ 𝐷 = (LDual‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ + = ∘f (+g‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ × = (.r‘𝑅) & ⊢ 𝑂 = (oppr‘𝑅) & ⊢ · = ( ·𝑠 ‘𝐷) ⇒ ⊢ (𝜑 → 𝐷 ∈ Grp) | ||
Theorem | ldualgrp 36164 | The dual of a vector space is a group. (Contributed by NM, 21-Oct-2014.) |
⊢ 𝐷 = (LDual‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) ⇒ ⊢ (𝜑 → 𝐷 ∈ Grp) | ||
Theorem | ldual0 36165 | The zero scalar of the dual of a vector space. (Contributed by NM, 28-Dec-2014.) |
⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ 𝑆 = (Scalar‘𝐷) & ⊢ 𝑂 = (0g‘𝑆) & ⊢ (𝜑 → 𝑊 ∈ LMod) ⇒ ⊢ (𝜑 → 𝑂 = 0 ) | ||
Theorem | ldual1 36166 | The unit scalar of the dual of a vector space. (Contributed by NM, 26-Feb-2015.) |
⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ 𝑆 = (Scalar‘𝐷) & ⊢ 𝐼 = (1r‘𝑆) & ⊢ (𝜑 → 𝑊 ∈ LMod) ⇒ ⊢ (𝜑 → 𝐼 = 1 ) | ||
Theorem | ldualneg 36167 | The negative of a scalar of the dual of a vector space. (Contributed by NM, 26-Feb-2015.) |
⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝑀 = (invg‘𝑅) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ 𝑆 = (Scalar‘𝐷) & ⊢ 𝑁 = (invg‘𝑆) & ⊢ (𝜑 → 𝑊 ∈ LMod) ⇒ ⊢ (𝜑 → 𝑁 = 𝑀) | ||
Theorem | ldual0v 36168 | The zero vector of the dual of a vector space. (Contributed by NM, 24-Oct-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ 𝑂 = (0g‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LMod) ⇒ ⊢ (𝜑 → 𝑂 = (𝑉 × { 0 })) | ||
Theorem | ldual0vcl 36169 | The dual zero vector is a functional. (Contributed by NM, 5-Mar-2015.) |
⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ 0 = (0g‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LMod) ⇒ ⊢ (𝜑 → 0 ∈ 𝐹) | ||
Theorem | lduallmodlem 36170 | Lemma for lduallmod 36171. (Contributed by NM, 22-Oct-2014.) |
⊢ 𝐷 = (LDual‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ + = ∘f (+g‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ × = (.r‘𝑅) & ⊢ 𝑂 = (oppr‘𝑅) & ⊢ · = ( ·𝑠 ‘𝐷) ⇒ ⊢ (𝜑 → 𝐷 ∈ LMod) | ||
Theorem | lduallmod 36171 | The dual of a left module is also a left module. (Contributed by NM, 22-Oct-2014.) |
⊢ 𝐷 = (LDual‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) ⇒ ⊢ (𝜑 → 𝐷 ∈ LMod) | ||
Theorem | lduallvec 36172 | The dual of a left vector space is also a left vector space. Note that scalar multiplication is reversed by df-oppr 19304; otherwise, the dual would be a right vector space as is sometimes the case in the literature. (Contributed by NM, 22-Oct-2014.) |
⊢ 𝐷 = (LDual‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) ⇒ ⊢ (𝜑 → 𝐷 ∈ LVec) | ||
Theorem | ldualvsub 36173 | The value of vector subtraction in the dual of a vector space. (Contributed by NM, 27-Feb-2015.) |
⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝑁 = (invg‘𝑅) & ⊢ 1 = (1r‘𝑅) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ + = (+g‘𝐷) & ⊢ · = ( ·𝑠 ‘𝐷) & ⊢ − = (-g‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝐻 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺 − 𝐻) = (𝐺 + ((𝑁‘ 1 ) · 𝐻))) | ||
Theorem | ldualvsubcl 36174 | Closure of vector subtraction in the dual of a vector space. (Contributed by NM, 27-Feb-2015.) |
⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ − = (-g‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝐻 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺 − 𝐻) ∈ 𝐹) | ||
Theorem | ldualvsubval 36175 | The value of the value of vector subtraction in the dual of a vector space. TODO: shorten with ldualvsub 36173? (Requires 𝐷 to oppr conversion.) (Contributed by NM, 26-Feb-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝑆 = (-g‘𝑅) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ − = (-g‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝐻 ∈ 𝐹) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝐺 − 𝐻)‘𝑋) = ((𝐺‘𝑋)𝑆(𝐻‘𝑋))) | ||
Theorem | ldualssvscl 36176 | Closure of scalar product in a dual subspace.) (Contributed by NM, 5-Feb-2015.) |
⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ · = ( ·𝑠 ‘𝐷) & ⊢ 𝑆 = (LSubSp‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐾) & ⊢ (𝜑 → 𝑌 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝑈) | ||
Theorem | ldualssvsubcl 36177 | Closure of vector subtraction in a dual subspace.) (Contributed by NM, 9-Mar-2015.) |
⊢ 𝐷 = (LDual‘𝑊) & ⊢ − = (-g‘𝐷) & ⊢ 𝑆 = (LSubSp‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝑈) & ⊢ (𝜑 → 𝑌 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝑋 − 𝑌) ∈ 𝑈) | ||
Theorem | ldual0vs 36178 | Scalar zero times a functional is the zero functional. (Contributed by NM, 17-Feb-2015.) |
⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ · = ( ·𝑠 ‘𝐷) & ⊢ 𝑂 = (0g‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → ( 0 · 𝐺) = 𝑂) | ||
Theorem | lkr0f2 36179 | The kernel of the zero functional is the set of all vectors. (Contributed by NM, 4-Feb-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐾 = (LKer‘𝑊) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ 0 = (0g‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → ((𝐾‘𝐺) = 𝑉 ↔ 𝐺 = 0 )) | ||
Theorem | lduallkr3 36180 | The kernels of nonzero functionals are hyperplanes. (Contributed by NM, 22-Feb-2015.) |
⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐾 = (LKer‘𝑊) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ 0 = (0g‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → ((𝐾‘𝐺) ∈ 𝐻 ↔ 𝐺 ≠ 0 )) | ||
Theorem | lkrpssN 36181 | Proper subset relation between kernels. (Contributed by NM, 16-Feb-2015.) (New usage is discouraged.) |
⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐾 = (LKer‘𝑊) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ 0 = (0g‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝐻 ∈ 𝐹) ⇒ ⊢ (𝜑 → ((𝐾‘𝐺) ⊊ (𝐾‘𝐻) ↔ (𝐺 ≠ 0 ∧ 𝐻 = 0 ))) | ||
Theorem | lkrin 36182 | Intersection of the kernels of 2 functionals is included in the kernel of their sum. (Contributed by NM, 7-Jan-2015.) |
⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐾 = (LKer‘𝑊) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ + = (+g‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝐻 ∈ 𝐹) ⇒ ⊢ (𝜑 → ((𝐾‘𝐺) ∩ (𝐾‘𝐻)) ⊆ (𝐾‘(𝐺 + 𝐻))) | ||
Theorem | eqlkr4 36183* | Two functionals with the same kernel are the same up to a constant. (Contributed by NM, 4-Feb-2015.) |
⊢ 𝑆 = (Scalar‘𝑊) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐾 = (LKer‘𝑊) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ · = ( ·𝑠 ‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝐻 ∈ 𝐹) & ⊢ (𝜑 → (𝐾‘𝐺) = (𝐾‘𝐻)) ⇒ ⊢ (𝜑 → ∃𝑟 ∈ 𝑅 𝐻 = (𝑟 · 𝐺)) | ||
Theorem | ldual1dim 36184* | Equivalent expressions for a 1-dim subspace (ray) of functionals. (Contributed by NM, 24-Oct-2014.) |
⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐿 = (LKer‘𝑊) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ 𝑁 = (LSpan‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝑁‘{𝐺}) = {𝑔 ∈ 𝐹 ∣ (𝐿‘𝐺) ⊆ (𝐿‘𝑔)}) | ||
Theorem | ldualkrsc 36185 | The kernel of a nonzero scalar product of a functional equals the kernel of the functional. (Contributed by NM, 28-Dec-2014.) |
⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐿 = (LKer‘𝑊) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ · = ( ·𝑠 ‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝑋 ∈ 𝐾) & ⊢ (𝜑 → 𝑋 ≠ 0 ) ⇒ ⊢ (𝜑 → (𝐿‘(𝑋 · 𝐺)) = (𝐿‘𝐺)) | ||
Theorem | lkrss 36186 | The kernel of a scalar product of a functional includes the kernel of the functional. (Contributed by NM, 27-Jan-2015.) |
⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐿 = (LKer‘𝑊) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ · = ( ·𝑠 ‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝑋 ∈ 𝐾) ⇒ ⊢ (𝜑 → (𝐿‘𝐺) ⊆ (𝐿‘(𝑋 · 𝐺))) | ||
Theorem | lkrss2N 36187* | Two functionals with kernels in a subset relationship. (Contributed by NM, 17-Feb-2015.) (New usage is discouraged.) |
⊢ 𝑆 = (Scalar‘𝑊) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐾 = (LKer‘𝑊) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ · = ( ·𝑠 ‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝐻 ∈ 𝐹) ⇒ ⊢ (𝜑 → ((𝐾‘𝐺) ⊆ (𝐾‘𝐻) ↔ ∃𝑟 ∈ 𝑅 𝐻 = (𝑟 · 𝐺))) | ||
Theorem | lkreqN 36188 | Proportional functionals have equal kernels. (Contributed by NM, 28-Mar-2015.) (New usage is discouraged.) |
⊢ 𝑆 = (Scalar‘𝑊) & ⊢ 𝑅 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑆) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐾 = (LKer‘𝑊) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ · = ( ·𝑠 ‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝐴 ∈ (𝑅 ∖ { 0 })) & ⊢ (𝜑 → 𝐻 ∈ 𝐹) & ⊢ (𝜑 → 𝐺 = (𝐴 · 𝐻)) ⇒ ⊢ (𝜑 → (𝐾‘𝐺) = (𝐾‘𝐻)) | ||
Theorem | lkrlspeqN 36189 | Condition for colinear functionals to have equal kernels. (Contributed by NM, 20-Mar-2015.) (New usage is discouraged.) |
⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐿 = (LKer‘𝑊) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ 0 = (0g‘𝐷) & ⊢ 𝑁 = (LSpan‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝐻 ∈ 𝐹) & ⊢ (𝜑 → 𝐺 ∈ ((𝑁‘{𝐻}) ∖ { 0 })) ⇒ ⊢ (𝜑 → (𝐿‘𝐺) = (𝐿‘𝐻)) | ||
Syntax | cops 36190 | Extend class notation with orthoposets. |
class OP | ||
Syntax | ccmtN 36191 | Extend class notation with the commutes relation. |
class cm | ||
Syntax | col 36192 | Extend class notation with orthlattices. |
class OL | ||
Syntax | coml 36193 | Extend class notation with orthomodular lattices. |
class OML | ||
Definition | df-oposet 36194* | Define the class of orthoposets, which are bounded posets with an orthocomplementation operation. Note that (Base p ) e. dom ( lub 𝑝) means there is an upper bound 1., and similarly for the 0. element. (Contributed by NM, 20-Oct-2011.) (Revised by NM, 13-Sep-2018.) |
⊢ OP = {𝑝 ∈ Poset ∣ (((Base‘𝑝) ∈ dom (lub‘𝑝) ∧ (Base‘𝑝) ∈ dom (glb‘𝑝)) ∧ ∃𝑜(𝑜 = (oc‘𝑝) ∧ ∀𝑎 ∈ (Base‘𝑝)∀𝑏 ∈ (Base‘𝑝)(((𝑜‘𝑎) ∈ (Base‘𝑝) ∧ (𝑜‘(𝑜‘𝑎)) = 𝑎 ∧ (𝑎(le‘𝑝)𝑏 → (𝑜‘𝑏)(le‘𝑝)(𝑜‘𝑎))) ∧ (𝑎(join‘𝑝)(𝑜‘𝑎)) = (1.‘𝑝) ∧ (𝑎(meet‘𝑝)(𝑜‘𝑎)) = (0.‘𝑝))))} | ||
Definition | df-cmtN 36195* | Define the commutes relation for orthoposets. Definition of commutes in [Kalmbach] p. 20. (Contributed by NM, 6-Nov-2011.) |
⊢ cm = (𝑝 ∈ V ↦ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (Base‘𝑝) ∧ 𝑦 ∈ (Base‘𝑝) ∧ 𝑥 = ((𝑥(meet‘𝑝)𝑦)(join‘𝑝)(𝑥(meet‘𝑝)((oc‘𝑝)‘𝑦))))}) | ||
Definition | df-ol 36196 | Define the class of ortholattices. Definition from [Kalmbach] p. 16. (Contributed by NM, 18-Sep-2011.) |
⊢ OL = (Lat ∩ OP) | ||
Definition | df-oml 36197* | Define the class of orthomodular lattices. Definition from [Kalmbach] p. 16. (Contributed by NM, 18-Sep-2011.) |
⊢ OML = {𝑙 ∈ OL ∣ ∀𝑎 ∈ (Base‘𝑙)∀𝑏 ∈ (Base‘𝑙)(𝑎(le‘𝑙)𝑏 → 𝑏 = (𝑎(join‘𝑙)(𝑏(meet‘𝑙)((oc‘𝑙)‘𝑎))))} | ||
Theorem | isopos 36198* | The predicate "is an orthoposet." (Contributed by NM, 20-Oct-2011.) (Revised by NM, 14-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 1 = (1.‘𝐾) ⇒ ⊢ (𝐾 ∈ OP ↔ ((𝐾 ∈ Poset ∧ 𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((( ⊥ ‘𝑥) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑥)) = 𝑥 ∧ (𝑥 ≤ 𝑦 → ( ⊥ ‘𝑦) ≤ ( ⊥ ‘𝑥))) ∧ (𝑥 ∨ ( ⊥ ‘𝑥)) = 1 ∧ (𝑥 ∧ ( ⊥ ‘𝑥)) = 0 ))) | ||
Theorem | opposet 36199 | Every orthoposet is a poset. (Contributed by NM, 12-Oct-2011.) |
⊢ (𝐾 ∈ OP → 𝐾 ∈ Poset) | ||
Theorem | oposlem 36200 | Lemma for orthoposet properties. (Contributed by NM, 20-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 1 = (1.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋 ≤ 𝑌 → ( ⊥ ‘𝑌) ≤ ( ⊥ ‘𝑋))) ∧ (𝑋 ∨ ( ⊥ ‘𝑋)) = 1 ∧ (𝑋 ∧ ( ⊥ ‘𝑋)) = 0 )) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |