![]() |
Metamath
Proof Explorer Theorem List (p. 392 of 491) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | islshpkrN 39101* | The predicate "is a hyperplane" (of a left module or left vector space). TODO: should it be 𝑈 = (𝐾‘𝑔) or (𝐾‘𝑔) = 𝑈 as in lshpkrex 39099? 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 39102* | 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 39103* | Equivalent expressions for a 1-dim subspace (ray) of functionals. TODO: delete this if not useful; lfl1dim 39102 may be more compatible with lspsn 21017. (Contributed by NM, 24-Oct-2014.) (New usage is discouraged.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐿 = (LKer‘𝑊) & ⊢ 𝐾 = (Base‘𝐷) & ⊢ · = (.r‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → {𝑔 ∈ 𝐹 ∣ (𝐿‘𝐺) ⊆ (𝐿‘𝑔)} = {𝑔 ∈ 𝐹 ∣ ∃𝑘 ∈ 𝐾 𝑔 = (𝐺 ∘f · (𝑉 × {𝑘}))}) | ||
Syntax | cld 39104 | Extend class notation with left dualvector space. |
class LDual | ||
Definition | df-ldual 39105* | 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 to reuse our existing collection of left vector space theorems. The restriction on ∘f (+g‘𝑣) allows it to be a set; see ofmres 8007. Note the operation reversal in the scalar product to allow 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 39106* | 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 to reuse our existing collection of left vector space theorems. Note the operation reversal in the scalar product to allow 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 39107 | The vectors of a dual space are functionals of the original space. (Contributed by NM, 18-Oct-2014.) |
⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ 𝑉 = (Base‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ 𝑋) ⇒ ⊢ (𝜑 → 𝑉 = 𝐹) | ||
Theorem | ldualelvbase 39108 | 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 39109 | Vector addition in the dual of a vector space. (Contributed by NM, 21-Oct-2014.) |
⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ + = (+g‘𝑅) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ ✚ = (+g‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ 𝑋) & ⊢ ⨣ = ( ∘f + ↾ (𝐹 × 𝐹)) ⇒ ⊢ (𝜑 → ✚ = ⨣ ) | ||
Theorem | ldualvadd 39110 | Vector addition in the dual of a vector space. (Contributed by NM, 21-Oct-2014.) |
⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ + = (+g‘𝑅) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ ✚ = (+g‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ 𝑋) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝐻 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺 ✚ 𝐻) = (𝐺 ∘f + 𝐻)) | ||
Theorem | ldualvaddcl 39111 | 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 39112 | 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 39113 | The ring of scalars of the dual of a vector space. (Contributed by NM, 18-Oct-2014.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝑂 = (oppr‘𝐹) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ 𝑅 = (Scalar‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ 𝑋) ⇒ ⊢ (𝜑 → 𝑅 = 𝑂) | ||
Theorem | ldualsbase 39114 | 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 39115 | 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 39116 | 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 39117* | 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 39118 | 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 39119 | 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 39120 | The scalar product operation value is a functional. (Contributed by NM, 18-Oct-2014.) |
⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ · = ( ·𝑠 ‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝐾) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝑋 · 𝐺) ∈ 𝐹) | ||
Theorem | ldualvaddcom 39121 | Commutative law for vector (functional) addition. (Contributed by NM, 17-Jan-2015.) |
⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ + = (+g‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝐹) & ⊢ (𝜑 → 𝑌 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) = (𝑌 + 𝑋)) | ||
Theorem | ldualvsass 39122 | Associative law for scalar product operation. (Contributed by NM, 20-Oct-2014.) |
⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ × = (.r‘𝑅) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ · = ( ·𝑠 ‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑋 ∈ 𝐾) & ⊢ (𝜑 → 𝑌 ∈ 𝐾) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → ((𝑌 × 𝑋) · 𝐺) = (𝑋 · (𝑌 · 𝐺))) | ||
Theorem | ldualvsass2 39123 | 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 39124 | 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 39125 | 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 39126 | Lemma for ldualgrp 39127. (Contributed by NM, 22-Oct-2014.) |
⊢ 𝐷 = (LDual‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ + = ∘f (+g‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ × = (.r‘𝑅) & ⊢ 𝑂 = (oppr‘𝑅) & ⊢ · = ( ·𝑠 ‘𝐷) ⇒ ⊢ (𝜑 → 𝐷 ∈ Grp) | ||
Theorem | ldualgrp 39127 | The dual of a vector space is a group. (Contributed by NM, 21-Oct-2014.) |
⊢ 𝐷 = (LDual‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) ⇒ ⊢ (𝜑 → 𝐷 ∈ Grp) | ||
Theorem | ldual0 39128 | 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 39129 | 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 39130 | 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 39131 | 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 39132 | The dual zero vector is a functional. (Contributed by NM, 5-Mar-2015.) |
⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ 0 = (0g‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LMod) ⇒ ⊢ (𝜑 → 0 ∈ 𝐹) | ||
Theorem | lduallmodlem 39133 | Lemma for lduallmod 39134. (Contributed by NM, 22-Oct-2014.) |
⊢ 𝐷 = (LDual‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ + = ∘f (+g‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ × = (.r‘𝑅) & ⊢ 𝑂 = (oppr‘𝑅) & ⊢ · = ( ·𝑠 ‘𝐷) ⇒ ⊢ (𝜑 → 𝐷 ∈ LMod) | ||
Theorem | lduallmod 39134 | The dual of a left module is also a left module. (Contributed by NM, 22-Oct-2014.) |
⊢ 𝐷 = (LDual‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) ⇒ ⊢ (𝜑 → 𝐷 ∈ LMod) | ||
Theorem | lduallvec 39135 | The dual of a left vector space is also a left vector space. Note that scalar multiplication is reversed by df-oppr 20350; 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 39136 | 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 39137 | Closure of vector subtraction in the dual of a vector space. (Contributed by NM, 27-Feb-2015.) |
⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ − = (-g‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝐻 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝐺 − 𝐻) ∈ 𝐹) | ||
Theorem | ldualvsubval 39138 | The value of the value of vector subtraction in the dual of a vector space. TODO: shorten with ldualvsub 39136? (Requires 𝐷 to oppr conversion.) (Contributed by NM, 26-Feb-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝑆 = (-g‘𝑅) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ − = (-g‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) & ⊢ (𝜑 → 𝐻 ∈ 𝐹) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝐺 − 𝐻)‘𝑋) = ((𝐺‘𝑋)𝑆(𝐻‘𝑋))) | ||
Theorem | ldualssvscl 39139 | Closure of scalar product in a dual subspace.) (Contributed by NM, 5-Feb-2015.) |
⊢ 𝑅 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ · = ( ·𝑠 ‘𝐷) & ⊢ 𝑆 = (LSubSp‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐾) & ⊢ (𝜑 → 𝑌 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝑈) | ||
Theorem | ldualssvsubcl 39140 | Closure of vector subtraction in a dual subspace.) (Contributed by NM, 9-Mar-2015.) |
⊢ 𝐷 = (LDual‘𝑊) & ⊢ − = (-g‘𝐷) & ⊢ 𝑆 = (LSubSp‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝑈) & ⊢ (𝜑 → 𝑌 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝑋 − 𝑌) ∈ 𝑈) | ||
Theorem | ldual0vs 39141 | 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 39142 | 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 39143 | The kernels of nonzero functionals are hyperplanes. (Contributed by NM, 22-Feb-2015.) |
⊢ 𝐻 = (LSHyp‘𝑊) & ⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐾 = (LKer‘𝑊) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ 0 = (0g‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → ((𝐾‘𝐺) ∈ 𝐻 ↔ 𝐺 ≠ 0 )) | ||
Theorem | lkrpssN 39144 | 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 39145 | 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 39146* | 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 39147* | Equivalent expressions for a 1-dim subspace (ray) of functionals. (Contributed by NM, 24-Oct-2014.) |
⊢ 𝐹 = (LFnl‘𝑊) & ⊢ 𝐿 = (LKer‘𝑊) & ⊢ 𝐷 = (LDual‘𝑊) & ⊢ 𝑁 = (LSpan‘𝐷) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝐺 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝑁‘{𝐺}) = {𝑔 ∈ 𝐹 ∣ (𝐿‘𝐺) ⊆ (𝐿‘𝑔)}) | ||
Theorem | ldualkrsc 39148 | 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 39149 | 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 39150* | 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 39151 | 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 39152 | 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 39153 | Extend class notation with orthoposets. |
class OP | ||
Syntax | ccmtN 39154 | Extend class notation with the commutes relation. |
class cm | ||
Syntax | col 39155 | Extend class notation with orthlattices. |
class OL | ||
Syntax | coml 39156 | Extend class notation with orthomodular lattices. |
class OML | ||
Definition | df-oposet 39157* | 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 39158* | 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 39159 | Define the class of ortholattices. Definition from [Kalmbach] p. 16. (Contributed by NM, 18-Sep-2011.) |
⊢ OL = (Lat ∩ OP) | ||
Definition | df-oml 39160* | 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 39161* | 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 39162 | Every orthoposet is a poset. (Contributed by NM, 12-Oct-2011.) |
⊢ (𝐾 ∈ OP → 𝐾 ∈ Poset) | ||
Theorem | oposlem 39163 | Lemma for orthoposet properties. (Contributed by NM, 20-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 1 = (1.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋 ≤ 𝑌 → ( ⊥ ‘𝑌) ≤ ( ⊥ ‘𝑋))) ∧ (𝑋 ∨ ( ⊥ ‘𝑋)) = 1 ∧ (𝑋 ∧ ( ⊥ ‘𝑋)) = 0 )) | ||
Theorem | op01dm 39164 | Conditions necessary for zero and unity elements to exist. (Contributed by NM, 14-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) ⇒ ⊢ (𝐾 ∈ OP → (𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺)) | ||
Theorem | op0cl 39165 | An orthoposet has a zero element. (h0elch 31283 analog.) (Contributed by NM, 12-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 0 = (0.‘𝐾) ⇒ ⊢ (𝐾 ∈ OP → 0 ∈ 𝐵) | ||
Theorem | op1cl 39166 | An orthoposet has a unity element. (helch 31271 analog.) (Contributed by NM, 22-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 1 = (1.‘𝐾) ⇒ ⊢ (𝐾 ∈ OP → 1 ∈ 𝐵) | ||
Theorem | op0le 39167 | Orthoposet zero is less than or equal to any element. (ch0le 31469 analog.) (Contributed by NM, 12-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 0 = (0.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → 0 ≤ 𝑋) | ||
Theorem | ople0 39168 | An element less than or equal to zero equals zero. (chle0 31471 analog.) (Contributed by NM, 21-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 0 = (0.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → (𝑋 ≤ 0 ↔ 𝑋 = 0 )) | ||
Theorem | opnlen0 39169 | An element not less than another is nonzero. TODO: Look for uses of necon3bd 2951 and op0le 39167 to see if this is useful elsewhere. (Contributed by NM, 5-May-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 0 = (0.‘𝐾) ⇒ ⊢ (((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ¬ 𝑋 ≤ 𝑌) → 𝑋 ≠ 0 ) | ||
Theorem | lub0N 39170 | 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 39171 | 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 39172 | Any element is less than the orthoposet unity. (chss 31257 analog.) (Contributed by NM, 23-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 1 = (1.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → 𝑋 ≤ 1 ) | ||
Theorem | op1le 39173 | If the orthoposet unity is less than or equal to an element, the element equals the unit. (chle0 31471 analog.) (Contributed by NM, 5-Dec-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 1 = (1.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ( 1 ≤ 𝑋 ↔ 𝑋 = 1 )) | ||
Theorem | glb0N 39174 | The greatest lower bound of the empty set is the unity element. (Contributed by NM, 5-Dec-2011.) (New usage is discouraged.) |
⊢ 𝐺 = (glb‘𝐾) & ⊢ 1 = (1.‘𝐾) ⇒ ⊢ (𝐾 ∈ OP → (𝐺‘∅) = 1 ) | ||
Theorem | opoccl 39175 | Closure of orthocomplement operation. (choccl 31334 analog.) (Contributed by NM, 20-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ( ⊥ ‘𝑋) ∈ 𝐵) | ||
Theorem | opococ 39176 | Double negative law for orthoposets. (ococ 31434 analog.) (Contributed by NM, 13-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋) | ||
Theorem | opcon3b 39177 | Contraposition law for orthoposets. (chcon3i 31494 analog.) (Contributed by NM, 8-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 = 𝑌 ↔ ( ⊥ ‘𝑌) = ( ⊥ ‘𝑋))) | ||
Theorem | opcon2b 39178 | Orthocomplement contraposition law. (negcon2 11559 analog.) (Contributed by NM, 16-Jan-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 = ( ⊥ ‘𝑌) ↔ 𝑌 = ( ⊥ ‘𝑋))) | ||
Theorem | opcon1b 39179 | Orthocomplement contraposition law. (negcon1 11558 analog.) (Contributed by NM, 24-Jan-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (( ⊥ ‘𝑋) = 𝑌 ↔ ( ⊥ ‘𝑌) = 𝑋)) | ||
Theorem | oplecon3 39180 | Contraposition law for orthoposets. (Contributed by NM, 13-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → ( ⊥ ‘𝑌) ≤ ( ⊥ ‘𝑋))) | ||
Theorem | oplecon3b 39181 | Contraposition law for orthoposets. (chsscon3 31528 analog.) (Contributed by NM, 4-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ↔ ( ⊥ ‘𝑌) ≤ ( ⊥ ‘𝑋))) | ||
Theorem | oplecon1b 39182 | Contraposition law for strict ordering in orthoposets. (chsscon1 31529 analog.) (Contributed by NM, 6-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (( ⊥ ‘𝑋) ≤ 𝑌 ↔ ( ⊥ ‘𝑌) ≤ 𝑋)) | ||
Theorem | opoc1 39183 | Orthocomplement of orthoposet unity. (Contributed by NM, 24-Jan-2012.) |
⊢ 0 = (0.‘𝐾) & ⊢ 1 = (1.‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ (𝐾 ∈ OP → ( ⊥ ‘ 1 ) = 0 ) | ||
Theorem | opoc0 39184 | Orthocomplement of orthoposet zero. (Contributed by NM, 24-Jan-2012.) |
⊢ 0 = (0.‘𝐾) & ⊢ 1 = (1.‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ (𝐾 ∈ OP → ( ⊥ ‘ 0 ) = 1 ) | ||
Theorem | opltcon3b 39185 | Contraposition law for strict ordering in orthoposets. (chpsscon3 31531 analog.) (Contributed by NM, 4-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 < 𝑌 ↔ ( ⊥ ‘𝑌) < ( ⊥ ‘𝑋))) | ||
Theorem | opltcon1b 39186 | Contraposition law for strict ordering in orthoposets. (chpsscon1 31532 analog.) (Contributed by NM, 5-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (( ⊥ ‘𝑋) < 𝑌 ↔ ( ⊥ ‘𝑌) < 𝑋)) | ||
Theorem | opltcon2b 39187 | Contraposition law for strict ordering in orthoposets. (chsscon2 31530 analog.) (Contributed by NM, 5-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 < ( ⊥ ‘𝑌) ↔ 𝑌 < ( ⊥ ‘𝑋))) | ||
Theorem | opexmid 39188 | Law of excluded middle for orthoposets. (chjo 31543 analog.) (Contributed by NM, 13-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 1 = (1.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → (𝑋 ∨ ( ⊥ ‘𝑋)) = 1 ) | ||
Theorem | opnoncon 39189 | Law of contradiction for orthoposets. (chocin 31523 analog.) (Contributed by NM, 13-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 0 = (0.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → (𝑋 ∧ ( ⊥ ‘𝑋)) = 0 ) | ||
Theorem | riotaocN 39190* | The orthocomplement of the unique poset element such that 𝜓. (riotaneg 12244 analog.) (Contributed by NM, 16-Jan-2012.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ (𝑥 = ( ⊥ ‘𝑦) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐾 ∈ OP ∧ ∃!𝑥 ∈ 𝐵 𝜑) → (℩𝑥 ∈ 𝐵 𝜑) = ( ⊥ ‘(℩𝑦 ∈ 𝐵 𝜓))) | ||
Theorem | cmtfvalN 39191* | Value of commutes relation. (Contributed by NM, 6-Nov-2011.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐴 → 𝐶 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑥 = ((𝑥 ∧ 𝑦) ∨ (𝑥 ∧ ( ⊥ ‘𝑦))))}) | ||
Theorem | cmtvalN 39192 | Equivalence for commutes relation. Definition of commutes in [Kalmbach] p. 20. (cmbr 31612 analog.) (Contributed by NM, 6-Nov-2011.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ 𝑋 = ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ ( ⊥ ‘𝑌))))) | ||
Theorem | isolat 39193 | The predicate "is an ortholattice." (Contributed by NM, 18-Sep-2011.) |
⊢ (𝐾 ∈ OL ↔ (𝐾 ∈ Lat ∧ 𝐾 ∈ OP)) | ||
Theorem | ollat 39194 | An ortholattice is a lattice. (Contributed by NM, 18-Sep-2011.) |
⊢ (𝐾 ∈ OL → 𝐾 ∈ Lat) | ||
Theorem | olop 39195 | An ortholattice is an orthoposet. (Contributed by NM, 18-Sep-2011.) |
⊢ (𝐾 ∈ OL → 𝐾 ∈ OP) | ||
Theorem | olposN 39196 | An ortholattice is a poset. (Contributed by NM, 16-Oct-2011.) (New usage is discouraged.) |
⊢ (𝐾 ∈ OL → 𝐾 ∈ Poset) | ||
Theorem | isolatiN 39197 | Properties that determine an ortholattice. (Contributed by NM, 18-Sep-2011.) (New usage is discouraged.) |
⊢ 𝐾 ∈ Lat & ⊢ 𝐾 ∈ OP ⇒ ⊢ 𝐾 ∈ OL | ||
Theorem | oldmm1 39198 | De Morgan's law for meet in an ortholattice. (chdmm1 31553 analog.) (Contributed by NM, 6-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(𝑋 ∧ 𝑌)) = (( ⊥ ‘𝑋) ∨ ( ⊥ ‘𝑌))) | ||
Theorem | oldmm2 39199 | De Morgan's law for meet in an ortholattice. (chdmm2 31554 analog.) (Contributed by NM, 6-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(( ⊥ ‘𝑋) ∧ 𝑌)) = (𝑋 ∨ ( ⊥ ‘𝑌))) | ||
Theorem | oldmm3N 39200 | De Morgan's law for meet in an ortholattice. (chdmm3 31555 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) = (( ⊥ ‘𝑋) ∨ 𝑌)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |