Home | Metamath
Proof Explorer Theorem List (p. 335 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lkrssv 33401 | The kernel of a linear functional is a set of vectors. (Contributed by NM, 1-Jan-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐾 = (LKer‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐾‘𝐺) ⊆ 𝑉) | ||
Theorem | lkrsc 33402 | 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 ) ⇒ ⊢ (𝜑 → (𝐿‘(𝐺 ∘𝑓 · (𝑉 × {𝑅}))) = (𝐿‘𝐺)) | ||
Theorem | lkrscss 33403 | 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) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝑅 ∈ 𝐾) ⇒ ⊢ (𝜑 → (𝐿‘𝐺) ⊆ (𝐿‘(𝐺 ∘𝑓 · (𝑉 × {𝑅})))) | ||
Theorem | eqlkr 33404* | 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 33405* | 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 ∧ (𝐺 ∈ 𝐹 ∧ 𝐻 ∈ 𝐹) ∧ (𝐿‘𝐺) = (𝐿‘𝐻)) → ∃𝑟 ∈ 𝐾 𝐻 = (𝐺 ∘𝑓 · (𝑉 × {𝑟}))) | ||
Theorem | eqlkr3 33406 | 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 33407 | The subspace sum of a kernel and the span of a vector not in the kernel (by ellkr 33394) is the whole vector space. (Contributed by NM, 19-Apr-2014.) |
⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 0 = (0g‘𝐷) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐾 = (LKer‘𝑊) ⇒ ⊢ ((𝑊 ∈ LVec ∧ (𝑋 ∈ 𝑉 ∧ 𝐺 ∈ 𝐹) ∧ (𝐺‘𝑋) ≠ 0 ) → ((𝐾‘𝐺) ⊕ (𝑁‘{𝑋})) = 𝑉) | ||
Theorem | lkrlsp2 33408 | 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 33409 | 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 33410 | 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 33411 | The kernels of nonzero functionals are hyperplanes. (Contributed by NM, 17-Jul-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 0 = (0g‘𝐷) & ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐾 = (LKer‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → ((𝐾‘𝐺) ∈ 𝐻 ↔ 𝐺 ≠ (𝑉 × { 0 }))) | ||
Theorem | lkrshpor 33412 | 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 33413 | 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 33414* | Lemma for lshpkrex 33423. 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 3148 for 𝑎 to 𝑐? (Contributed by NM, 4-Jan-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝐻) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑍})) = 𝑉) & ⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐷) & ⊢ · = ( ·𝑠 ‘𝑊) ⇒ ⊢ (𝜑 → ∃!𝑘 ∈ 𝐾 ∃𝑦 ∈ 𝑈 𝑋 = (𝑦 + (𝑘 · 𝑍))) | ||
Theorem | lshpkrlem1 33415* | Lemma for lshpkrex 33423. 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 33416* | Lemma for lshpkrex 33423. 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 33417* | Lemma for lshpkrex 33423. Defining property of 𝐺‘𝑋. (Contributed by NM, 15-Jul-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝐻) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑍})) = 𝑉) & ⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐷) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 0 = (0g‘𝐷) & ⊢ 𝐺 = (𝑥 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝐾 ∃𝑦 ∈ 𝑈 𝑥 = (𝑦 + (𝑘 · 𝑍)))) ⇒ ⊢ (𝜑 → ∃𝑧 ∈ 𝑈 𝑋 = (𝑧 + ((𝐺‘𝑋) · 𝑍))) | ||
Theorem | lshpkrlem4 33418* | Lemma for lshpkrex 33423. 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 33419* | Lemma for lshpkrex 33423. 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 33420* | Lemma for lshpkrex 33423. Show linearlity of 𝐺. (Contributed by NM, 17-Jul-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ ⊕ = (LSSum‘𝑊) & ⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ 𝐻) & ⊢ (𝜑 → 𝑍 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → (𝑈 ⊕ (𝑁‘{𝑍})) = 𝑉) & ⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐷) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 0 = (0g‘𝐷) & ⊢ 𝐺 = (𝑥 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝐾 ∃𝑦 ∈ 𝑈 𝑥 = (𝑦 + (𝑘 · 𝑍)))) ⇒ ⊢ ((𝜑 ∧ (𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉)) → (𝐺‘((𝑙 · 𝑢) + 𝑣)) = ((𝑙(.r‘𝐷)(𝐺‘𝑢))(+g‘𝐷)(𝐺‘𝑣))) | ||
Theorem | lshpkrcl 33421* | 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 33422* | 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 33423* | 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 33424* | 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 33425* | The predicate "is a hyperplane" (of a left module or left vector space). TODO: should it be 𝑈 = (𝐾‘𝑔) or (𝐾‘𝑔) = 𝑈 as in lshpkrex 33423? 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 33426* | Equivalent expressions for a 1-dim subspace (ray) of functionals. (Contributed by NM, 24-Oct-2014.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐿 = (LKer‘𝑊) & ⊢ 𝐾 = (Base‘𝐷) & ⊢ · = (.r‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → {𝑔 ∈ 𝐹 ∣ (𝐿‘𝐺) ⊆ (𝐿‘𝑔)} = {𝑔 ∣ ∃𝑘 ∈ 𝐾 𝑔 = (𝐺 ∘𝑓 · (𝑉 × {𝑘}))}) | ||
Theorem | lfl1dim2N 33427* | Equivalent expressions for a 1-dim subspace (ray) of functionals. TODO: delete this if not useful; lfl1dim 33426 may be more compatible with lspsn 18823. (Contributed by NM, 24-Oct-2014.) (New usage is discouraged.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐿 = (LKer‘𝑊) & ⊢ 𝐾 = (Base‘𝐷) & ⊢ · = (.r‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → {𝑔 ∈ 𝐹 ∣ (𝐿‘𝐺) ⊆ (𝐿‘𝑔)} = {𝑔 ∈ 𝐹 ∣ ∃𝑘 ∈ 𝐾 𝑔 = (𝐺 ∘𝑓 · (𝑉 × {𝑘}))}) | ||
Syntax | cld 33428 | Extend class notation with left dualvector space. |
class LDual | ||
Definition | df-ldual 33429* | 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 ∘𝑓 (+g‘𝑣) allows it to be a set; see ofmres 7055. 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), ( ∘𝑓 (+g‘(Scalar‘𝑣)) ↾ ((LFnl‘𝑣) × (LFnl‘𝑣)))〉, 〈(Scalar‘ndx), (oppr‘(Scalar‘𝑣))〉} ∪ {〈( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑣)), 𝑓 ∈ (LFnl‘𝑣) ↦ (𝑓 ∘𝑓 (.r‘(Scalar‘𝑣))((Base‘𝑣) × {𝑘})))〉})) | ||
Theorem | ldualset 33430* | 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‘𝑅) & ⊢ ✚ = ( ∘𝑓 + ↾ (𝐹 × 𝐹)) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝑂 = (oppr‘𝑅) & ⊢ ∙ = (𝑘 ∈ 𝐾, 𝑓 ∈ 𝐹 ↦ (𝑓 ∘𝑓 · (𝑉 × {𝑘}))) & ⊢ (𝜑 → 𝑊 ∈ 𝑋) ⇒ ⊢ (𝜑 → 𝐷 = ({〈(Base‘ndx), 𝐹〉, 〈(+g‘ndx), ✚ 〉, 〈(Scalar‘ndx), 𝑂〉} ∪ {〈( ·𝑠 ‘ndx), ∙ 〉})) | ||
Theorem | ldualvbase 33431 | The vectors of a dual space are functionals of the original space. (Contributed by NM, 18-Oct-2014.) |
⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ 𝑉 = (Base‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ 𝑋) ⇒ ⊢ (𝜑 → 𝑉 = 𝐹) | ||
Theorem | ldualelvbase 33432 | 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 33433 | Vector addition in the dual of a vector space. (Contributed by NM, 21-Oct-2014.) |
⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ + = (+g‘𝑅) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ ✚ = (+g‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ 𝑋) & ⊢ ⨣ = ( ∘𝑓 + ↾ (𝐹 × 𝐹)) ⇒ ⊢ (𝜑 → ✚ = ⨣ ) | ||
Theorem | ldualvadd 33434 | Vector addition in the dual of a vector space. (Contributed by NM, 21-Oct-2014.) |
⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ + = (+g‘𝑅) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ ✚ = (+g‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ 𝑋) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝐻 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺 ✚ 𝐻) = (𝐺 ∘𝑓 + 𝐻)) | ||
Theorem | ldualvaddcl 33435 | 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 33436 | 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 33437 | The ring of scalars of the dual of a vector space. (Contributed by NM, 18-Oct-2014.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝑂 = (oppr‘𝐹) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ 𝑅 = (Scalar‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ 𝑋) ⇒ ⊢ (𝜑 → 𝑅 = 𝑂) | ||
Theorem | ldualsbase 33438 | 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 33439 | 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 33440 | 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 33441* | Scalar product operation for the dual of a vector space. (Contributed by NM, 18-Oct-2014.) |
⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ × = (.r‘𝑅) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ ∙ = ( ·𝑠 ‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ 𝑌) & ⊢ · = (𝑘 ∈ 𝐾, 𝑓 ∈ 𝐹 ↦ (𝑓 ∘𝑓 × (𝑉 × {𝑘}))) ⇒ ⊢ (𝜑 → ∙ = · ) | ||
Theorem | ldualvs 33442 | 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‘𝑊) & ⊢ ∙ = ( ·𝑠 ‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ 𝑌) & ⊢ (𝜑 → 𝑋 ∈ 𝐾) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝑋 ∙ 𝐺) = (𝐺 ∘𝑓 × (𝑉 × {𝑋}))) | ||
Theorem | ldualvsval 33443 | 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 33444 | The scalar product operation value is a functional. (Contributed by NM, 18-Oct-2014.) |
⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ · = ( ·𝑠 ‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝐾) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝑋 · 𝐺) ∈ 𝐹) | ||
Theorem | ldualvaddcom 33445 | Commutative law for vector (functional) addition. (Contributed by NM, 17-Jan-2015.) |
⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ + = (+g‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝐹) & ⊢ (𝜑 → 𝑌 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) = (𝑌 + 𝑋)) | ||
Theorem | ldualvsass 33446 | Associative law for scalar product operation. (Contributed by NM, 20-Oct-2014.) |
⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ × = (.r‘𝑅) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ · = ( ·𝑠 ‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝐾) & ⊢ (𝜑 → 𝑌 ∈ 𝐾) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → ((𝑌 × 𝑋) · 𝐺) = (𝑋 · (𝑌 · 𝐺))) | ||
Theorem | ldualvsass2 33447 | 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 33448 | 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 33449 | 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 33450 | Lemma for ldualgrp 33451. (Contributed by NM, 22-Oct-2014.) |
⊢ 𝐷 = (LDual‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ + = ∘𝑓 (+g‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ × = (.r‘𝑅) & ⊢ 𝑂 = (oppr‘𝑅) & ⊢ · = ( ·𝑠 ‘𝐷) ⇒ ⊢ (𝜑 → 𝐷 ∈ Grp) | ||
Theorem | ldualgrp 33451 | The dual of a vector space is a group. (Contributed by NM, 21-Oct-2014.) |
⊢ 𝐷 = (LDual‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) ⇒ ⊢ (𝜑 → 𝐷 ∈ Grp) | ||
Theorem | ldual0 33452 | 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 33453 | 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 33454 | 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 33455 | 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 33456 | The dual zero vector is a functional. (Contributed by NM, 5-Mar-2015.) |
⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ 0 = (0g‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LMod) ⇒ ⊢ (𝜑 → 0 ∈ 𝐹) | ||
Theorem | lduallmodlem 33457 | Lemma for lduallmod 33458. (Contributed by NM, 22-Oct-2014.) |
⊢ 𝐷 = (LDual‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ + = ∘𝑓 (+g‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ × = (.r‘𝑅) & ⊢ 𝑂 = (oppr‘𝑅) & ⊢ · = ( ·𝑠 ‘𝐷) ⇒ ⊢ (𝜑 → 𝐷 ∈ LMod) | ||
Theorem | lduallmod 33458 | The dual of a left module is also a left module. (Contributed by NM, 22-Oct-2014.) |
⊢ 𝐷 = (LDual‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) ⇒ ⊢ (𝜑 → 𝐷 ∈ LMod) | ||
Theorem | lduallvec 33459 | The dual of a left vector space is also a left vector space. Note that scalar multiplication is reversed by df-oppr 18446; 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 33460 | 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 33461 | Closure of vector subtraction in the dual of a vector space. (Contributed by NM, 27-Feb-2015.) |
⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ − = (-g‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝐻 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺 − 𝐻) ∈ 𝐹) | ||
Theorem | ldualvsubval 33462 | The value of the value of vector subtraction in the dual of a vector space. TODO: shorten with ldualvsub 33460? (Requires 𝐷 to oppr conversion.) (Contributed by NM, 26-Feb-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝑆 = (-g‘𝑅) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ − = (-g‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝐻 ∈ 𝐹) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝐺 − 𝐻)‘𝑋) = ((𝐺‘𝑋)𝑆(𝐻‘𝑋))) | ||
Theorem | ldualssvscl 33463 | Closure of scalar product in a dual subspace.) (Contributed by NM, 5-Feb-2015.) |
⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ · = ( ·𝑠 ‘𝐷) & ⊢ 𝑆 = (LSubSp‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐾) & ⊢ (𝜑 → 𝑌 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝑈) | ||
Theorem | ldualssvsubcl 33464 | Closure of vector subtraction in a dual subspace.) (Contributed by NM, 9-Mar-2015.) |
⊢ 𝐷 = (LDual‘𝑊) & ⊢ − = (-g‘𝐷) & ⊢ 𝑆 = (LSubSp‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝑈) & ⊢ (𝜑 → 𝑌 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝑋 − 𝑌) ∈ 𝑈) | ||
Theorem | ldual0vs 33465 | 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 33466 | 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 33467 | The kernels of nonzero functionals are hyperplanes. (Contributed by NM, 22-Feb-2015.) |
⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐾 = (LKer‘𝑊) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ 0 = (0g‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → ((𝐾‘𝐺) ∈ 𝐻 ↔ 𝐺 ≠ 0 )) | ||
Theorem | lkrpssN 33468 | 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 33469 | 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 33470* | 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 33471* | Equivalent expressions for a 1-dim subspace (ray) of functionals. (Contributed by NM, 24-Oct-2014.) |
⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐿 = (LKer‘𝑊) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ 𝑁 = (LSpan‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝑁‘{𝐺}) = {𝑔 ∈ 𝐹 ∣ (𝐿‘𝐺) ⊆ (𝐿‘𝑔)}) | ||
Theorem | ldualkrsc 33472 | 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 33473 | 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 33474* | 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 33475 | 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 33476 | 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 33477 | Extend class notation with orthoposets. |
class OP | ||
Syntax | ccmtN 33478 | Extend class notation with the commutes relation. |
class cm | ||
Syntax | col 33479 | Extend class notation with orthlattices. |
class OL | ||
Syntax | coml 33480 | Extend class notation with orthomodular lattices. |
class OML | ||
Definition | df-oposet 33481* | 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 33482* | 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 33483 | Define the class of ortholattices. Definition from [Kalmbach] p. 16. (Contributed by NM, 18-Sep-2011.) |
⊢ OL = (Lat ∩ OP) | ||
Definition | df-oml 33484* | 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 33485* | 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 33486 | Every orthoposet is a poset. (Contributed by NM, 12-Oct-2011.) |
⊢ (𝐾 ∈ OP → 𝐾 ∈ Poset) | ||
Theorem | oposlem 33487 | Lemma for orthoposet properties. (Contributed by NM, 20-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 1 = (1.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋 ≤ 𝑌 → ( ⊥ ‘𝑌) ≤ ( ⊥ ‘𝑋))) ∧ (𝑋 ∨ ( ⊥ ‘𝑋)) = 1 ∧ (𝑋 ∧ ( ⊥ ‘𝑋)) = 0 )) | ||
Theorem | op01dm 33488 | Conditions necessary for zero and unit elements to exist. (Contributed by NM, 14-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) ⇒ ⊢ (𝐾 ∈ OP → (𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺)) | ||
Theorem | op0cl 33489 | An orthoposet has a zero element. (h0elch 27496 analog.) (Contributed by NM, 12-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 0 = (0.‘𝐾) ⇒ ⊢ (𝐾 ∈ OP → 0 ∈ 𝐵) | ||
Theorem | op1cl 33490 | An orthoposet has a unit element. (helch 27484 analog.) (Contributed by NM, 22-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 1 = (1.‘𝐾) ⇒ ⊢ (𝐾 ∈ OP → 1 ∈ 𝐵) | ||
Theorem | op0le 33491 | Orthoposet zero is less than or equal to any element. (ch0le 27684 analog.) (Contributed by NM, 12-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 0 = (0.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → 0 ≤ 𝑋) | ||
Theorem | ople0 33492 | An element less than or equal to zero equals zero. (chle0 27686 analog.) (Contributed by NM, 21-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 0 = (0.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → (𝑋 ≤ 0 ↔ 𝑋 = 0 )) | ||
Theorem | opnlen0 33493 | An element not less than another is nonzero. TODO: Look for uses of necon3bd 2796 and op0le 33491 to see if this is useful elsewhere. (Contributed by NM, 5-May-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 0 = (0.‘𝐾) ⇒ ⊢ (((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋 ≤ 𝑌) → 𝑋 ≠ 0 ) | ||
Theorem | lub0N 33494 | The least upper bound of the empty set is the zero element. (Contributed by NM, 15-Sep-2013.) (New usage is discouraged.) |
⊢ 1 = (lub‘𝐾) & ⊢ 0 = (0.‘𝐾) ⇒ ⊢ (𝐾 ∈ OP → ( 1 ‘∅) = 0 ) | ||
Theorem | opltn0 33495 | A lattice element greater than zero is nonzero. TODO: is this needed? (Contributed by NM, 1-Jun-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ 0 = (0.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ( 0 < 𝑋 ↔ 𝑋 ≠ 0 )) | ||
Theorem | ople1 33496 | Any element is less than the orthoposet unit. (chss 27470 analog.) (Contributed by NM, 23-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 1 = (1.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → 𝑋 ≤ 1 ) | ||
Theorem | op1le 33497 | If the orthoposet unit is less than or equal to an element, the element equals the unit. (chle0 27686 analog.) (Contributed by NM, 5-Dec-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 1 = (1.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ( 1 ≤ 𝑋 ↔ 𝑋 = 1 )) | ||
Theorem | glb0N 33498 | The greatest lower bound of the empty set is the unit element. (Contributed by NM, 5-Dec-2011.) (New usage is discouraged.) |
⊢ 𝐺 = (glb‘𝐾) & ⊢ 1 = (1.‘𝐾) ⇒ ⊢ (𝐾 ∈ OP → (𝐺‘∅) = 1 ) | ||
Theorem | opoccl 33499 | Closure of orthocomplement operation. (choccl 27549 analog.) (Contributed by NM, 20-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ( ⊥ ‘𝑋) ∈ 𝐵) | ||
Theorem | opococ 33500 | Double negative law for orthoposets. (ococ 27649 analog.) (Contributed by NM, 13-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |