Home | Metamath
Proof Explorer Theorem List (p. 345 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lshpkrlem5 34401* | Lemma for lshpkrex 34405. Part of showing linearity of . (Contributed by NM, 16-Jul-2014.) |
LSHyp Scalar | ||
Theorem | lshpkrlem6 34402* | Lemma for lshpkrex 34405. Show linearlity of . (Contributed by NM, 17-Jul-2014.) |
LSHyp Scalar | ||
Theorem | lshpkrcl 34403* | The set defined by hyperplane is a linear functional. (Contributed by NM, 17-Jul-2014.) |
LSHyp Scalar LFnl | ||
Theorem | lshpkr 34404* | The kernel of functional is the hyperplane defining it. (Contributed by NM, 17-Jul-2014.) |
LSHyp Scalar LKer | ||
Theorem | lshpkrex 34405* | 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 | ||
Theorem | lshpset2N 34406* | 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.) |
Scalar LSHyp LFnl LKer | ||
Theorem | islshpkrN 34407* | The predicate "is a hyperplane" (of a left module or left vector space). TODO: should it be or as in lshpkrex 34405? 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.) |
Scalar LSHyp LFnl LKer | ||
Theorem | lfl1dim 34408* | Equivalent expressions for a 1-dim subspace (ray) of functionals. (Contributed by NM, 24-Oct-2014.) |
Scalar LFnl LKer | ||
Theorem | lfl1dim2N 34409* | Equivalent expressions for a 1-dim subspace (ray) of functionals. TODO: delete this if not useful; lfl1dim 34408 may be more compatible with lspsn 19002. (Contributed by NM, 24-Oct-2014.) (New usage is discouraged.) |
Scalar LFnl LKer | ||
Syntax | cld 34410 | Extend class notation with left dualvector space. |
LDual | ||
Definition | df-ldual 34411* | 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 allows it to be a set; see ofmres 7164. 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 LFnl Scalar LFnl LFnl Scalar opprScalar Scalar LFnl Scalar | ||
Theorem | ldualset 34412* | 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.) |
LFnl LDual Scalar oppr Scalar | ||
Theorem | ldualvbase 34413 | The vectors of a dual space are functionals of the original space. (Contributed by NM, 18-Oct-2014.) |
LFnl LDual | ||
Theorem | ldualelvbase 34414 | 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 | ||
Theorem | ldualfvadd 34415 | Vector addition in the dual of a vector space. (Contributed by NM, 21-Oct-2014.) |
LFnl Scalar LDual | ||
Theorem | ldualvadd 34416 | Vector addition in the dual of a vector space. (Contributed by NM, 21-Oct-2014.) |
LFnl Scalar LDual | ||
Theorem | ldualvaddcl 34417 | The value of vector addition in the dual of a vector space is a functional. (Contributed by NM, 21-Oct-2014.) |
LFnl LDual | ||
Theorem | ldualvaddval 34418 | The value of the value of vector addition in the dual of a vector space. (Contributed by NM, 7-Jan-2015.) |
Scalar LFnl LDual | ||
Theorem | ldualsca 34419 | The ring of scalars of the dual of a vector space. (Contributed by NM, 18-Oct-2014.) |
Scalar oppr LDual Scalar | ||
Theorem | ldualsbase 34420 | Base set of scalar ring for the dual of a vector space. (Contributed by NM, 24-Oct-2014.) |
Scalar LDual Scalar | ||
Theorem | ldualsaddN 34421 | Scalar addition for the dual of a vector space. (Contributed by NM, 24-Oct-2014.) (New usage is discouraged.) |
Scalar LDual Scalar | ||
Theorem | ldualsmul 34422 | Scalar multiplication for the dual of a vector space. (Contributed by NM, 19-Oct-2014.) (Revised by Mario Carneiro, 22-Sep-2015.) |
Scalar LDual Scalar | ||
Theorem | ldualfvs 34423* | Scalar product operation for the dual of a vector space. (Contributed by NM, 18-Oct-2014.) |
LFnl Scalar LDual | ||
Theorem | ldualvs 34424 | Scalar product operation value (which is a functional) for the dual of a vector space. (Contributed by NM, 18-Oct-2014.) |
LFnl Scalar LDual | ||
Theorem | ldualvsval 34425 | Value of scalar product operation value for the dual of a vector space. (Contributed by NM, 18-Oct-2014.) |
LFnl Scalar LDual | ||
Theorem | ldualvscl 34426 | The scalar product operation value is a functional. (Contributed by NM, 18-Oct-2014.) |
LFnl Scalar LDual | ||
Theorem | ldualvaddcom 34427 | Commutative law for vector (functional) addition. (Contributed by NM, 17-Jan-2015.) |
LFnl LDual | ||
Theorem | ldualvsass 34428 | Associative law for scalar product operation. (Contributed by NM, 20-Oct-2014.) |
LFnl Scalar LDual | ||
Theorem | ldualvsass2 34429 | Associative law for scalar product operation, using operations from the dual space. (Contributed by NM, 20-Oct-2014.) |
LFnl Scalar LDual Scalar | ||
Theorem | ldualvsdi1 34430 | Distributive law for scalar product operation, using operations from the dual space. (Contributed by NM, 21-Oct-2014.) |
LFnl Scalar LDual | ||
Theorem | ldualvsdi2 34431 | Reverse distributive law for scalar product operation, using operations from the dual space. (Contributed by NM, 21-Oct-2014.) |
LFnl Scalar LDual | ||
Theorem | ldualgrplem 34432 | Lemma for ldualgrp 34433. (Contributed by NM, 22-Oct-2014.) |
LDual LFnl Scalar oppr | ||
Theorem | ldualgrp 34433 | The dual of a vector space is a group. (Contributed by NM, 21-Oct-2014.) |
LDual | ||
Theorem | ldual0 34434 | The zero scalar of the dual of a vector space. (Contributed by NM, 28-Dec-2014.) |
Scalar LDual Scalar | ||
Theorem | ldual1 34435 | The unit scalar of the dual of a vector space. (Contributed by NM, 26-Feb-2015.) |
Scalar LDual Scalar | ||
Theorem | ldualneg 34436 | The negative of a scalar of the dual of a vector space. (Contributed by NM, 26-Feb-2015.) |
Scalar LDual Scalar | ||
Theorem | ldual0v 34437 | The zero vector of the dual of a vector space. (Contributed by NM, 24-Oct-2014.) |
Scalar LDual | ||
Theorem | ldual0vcl 34438 | The dual zero vector is a functional. (Contributed by NM, 5-Mar-2015.) |
LFnl LDual | ||
Theorem | lduallmodlem 34439 | Lemma for lduallmod 34440. (Contributed by NM, 22-Oct-2014.) |
LDual LFnl Scalar oppr | ||
Theorem | lduallmod 34440 | The dual of a left module is also a left module. (Contributed by NM, 22-Oct-2014.) |
LDual | ||
Theorem | lduallvec 34441 | The dual of a left vector space is also a left vector space. Note that scalar multiplication is reversed by df-oppr 18623; otherwise, the dual would be a right vector space as is sometimes the case in the literature. (Contributed by NM, 22-Oct-2014.) |
LDual | ||
Theorem | ldualvsub 34442 | The value of vector subtraction in the dual of a vector space. (Contributed by NM, 27-Feb-2015.) |
Scalar LFnl LDual | ||
Theorem | ldualvsubcl 34443 | Closure of vector subtraction in the dual of a vector space. (Contributed by NM, 27-Feb-2015.) |
LFnl LDual | ||
Theorem | ldualvsubval 34444 | The value of the value of vector subtraction in the dual of a vector space. TODO: shorten with ldualvsub 34442? (Requires to oppr conversion.) (Contributed by NM, 26-Feb-2015.) |
Scalar LFnl LDual | ||
Theorem | ldualssvscl 34445 | Closure of scalar product in a dual subspace.) (Contributed by NM, 5-Feb-2015.) |
Scalar LDual | ||
Theorem | ldualssvsubcl 34446 | Closure of vector subtraction in a dual subspace.) (Contributed by NM, 9-Mar-2015.) |
LDual | ||
Theorem | ldual0vs 34447 | Scalar zero times a functional is the zero functional. (Contributed by NM, 17-Feb-2015.) |
LFnl Scalar LDual | ||
Theorem | lkr0f2 34448 | The kernel of the zero functional is the set of all vectors. (Contributed by NM, 4-Feb-2015.) |
LFnl LKer LDual | ||
Theorem | lduallkr3 34449 | The kernels of nonzero functionals are hyperplanes. (Contributed by NM, 22-Feb-2015.) |
LSHyp LFnl LKer LDual | ||
Theorem | lkrpssN 34450 | Proper subset relation between kernels. (Contributed by NM, 16-Feb-2015.) (New usage is discouraged.) |
LFnl LKer LDual | ||
Theorem | lkrin 34451 | Intersection of the kernels of 2 functionals is included in the kernel of their sum. (Contributed by NM, 7-Jan-2015.) |
LFnl LKer LDual | ||
Theorem | eqlkr4 34452* | Two functionals with the same kernel are the same up to a constant. (Contributed by NM, 4-Feb-2015.) |
Scalar LFnl LKer LDual | ||
Theorem | ldual1dim 34453* | Equivalent expressions for a 1-dim subspace (ray) of functionals. (Contributed by NM, 24-Oct-2014.) |
LFnl LKer LDual | ||
Theorem | ldualkrsc 34454 | The kernel of a nonzero scalar product of a functional equals the kernel of the functional. (Contributed by NM, 28-Dec-2014.) |
Scalar LFnl LKer LDual | ||
Theorem | lkrss 34455 | The kernel of a scalar product of a functional includes the kernel of the functional. (Contributed by NM, 27-Jan-2015.) |
Scalar LFnl LKer LDual | ||
Theorem | lkrss2N 34456* | Two functionals with kernels in a subset relationship. (Contributed by NM, 17-Feb-2015.) (New usage is discouraged.) |
Scalar LFnl LKer LDual | ||
Theorem | lkreqN 34457 | Proportional functionals have equal kernels. (Contributed by NM, 28-Mar-2015.) (New usage is discouraged.) |
Scalar LFnl LKer LDual | ||
Theorem | lkrlspeqN 34458 | Condition for colinear functionals to have equal kernels. (Contributed by NM, 20-Mar-2015.) (New usage is discouraged.) |
LFnl LKer LDual | ||
Syntax | cops 34459 | Extend class notation with orthoposets. |
Syntax | ccmtN 34460 | Extend class notation with the commutes relation. |
Syntax | col 34461 | Extend class notation with orthlattices. |
Syntax | coml 34462 | Extend class notation with orthomodular lattices. |
Definition | df-oposet 34463* | Define the class of orthoposets, which are bounded posets with an orthocomplementation operation. Note that p ) e. dom ( lub means there is an upper bound , and similarly for the element. (Contributed by NM, 20-Oct-2011.) (Revised by NM, 13-Sep-2018.) |
Definition | df-cmtN 34464* | Define the commutes relation for orthoposets. Definition of commutes in [Kalmbach] p. 20. (Contributed by NM, 6-Nov-2011.) |
Definition | df-ol 34465 | Define the class of ortholattices. Definition from [Kalmbach] p. 16. (Contributed by NM, 18-Sep-2011.) |
Definition | df-oml 34466* | Define the class of orthomodular lattices. Definition from [Kalmbach] p. 16. (Contributed by NM, 18-Sep-2011.) |
Theorem | isopos 34467* | The predicate "is an orthoposet." (Contributed by NM, 20-Oct-2011.) (Revised by NM, 14-Sep-2018.) |
Theorem | opposet 34468 | Every orthoposet is a poset. (Contributed by NM, 12-Oct-2011.) |
Theorem | oposlem 34469 | Lemma for orthoposet properties. (Contributed by NM, 20-Oct-2011.) |
Theorem | op01dm 34470 | Conditions necessary for zero and unit elements to exist. (Contributed by NM, 14-Sep-2018.) |
Theorem | op0cl 34471 | An orthoposet has a zero element. (h0elch 28112 analog.) (Contributed by NM, 12-Oct-2011.) |
Theorem | op1cl 34472 | An orthoposet has a unit element. (helch 28100 analog.) (Contributed by NM, 22-Oct-2011.) |
Theorem | op0le 34473 | Orthoposet zero is less than or equal to any element. (ch0le 28300 analog.) (Contributed by NM, 12-Oct-2011.) |
Theorem | ople0 34474 | An element less than or equal to zero equals zero. (chle0 28302 analog.) (Contributed by NM, 21-Oct-2011.) |
Theorem | opnlen0 34475 | An element not less than another is nonzero. TODO: Look for uses of necon3bd 2808 and op0le 34473 to see if this is useful elsewhere. (Contributed by NM, 5-May-2013.) |
Theorem | lub0N 34476 | The least upper bound of the empty set is the zero element. (Contributed by NM, 15-Sep-2013.) (New usage is discouraged.) |
Theorem | opltn0 34477 | A lattice element greater than zero is nonzero. TODO: is this needed? (Contributed by NM, 1-Jun-2012.) |
Theorem | ople1 34478 | Any element is less than the orthoposet unit. (chss 28086 analog.) (Contributed by NM, 23-Oct-2011.) |
Theorem | op1le 34479 | If the orthoposet unit is less than or equal to an element, the element equals the unit. (chle0 28302 analog.) (Contributed by NM, 5-Dec-2011.) |
Theorem | glb0N 34480 | The greatest lower bound of the empty set is the unit element. (Contributed by NM, 5-Dec-2011.) (New usage is discouraged.) |
Theorem | opoccl 34481 | Closure of orthocomplement operation. (choccl 28165 analog.) (Contributed by NM, 20-Oct-2011.) |
Theorem | opococ 34482 | Double negative law for orthoposets. (ococ 28265 analog.) (Contributed by NM, 13-Sep-2011.) |
Theorem | opcon3b 34483 | Contraposition law for orthoposets. (chcon3i 28325 analog.) (Contributed by NM, 8-Nov-2011.) |
Theorem | opcon2b 34484 | Orthocomplement contraposition law. (negcon2 10334 analog.) (Contributed by NM, 16-Jan-2012.) |
Theorem | opcon1b 34485 | Orthocomplement contraposition law. (negcon1 10333 analog.) (Contributed by NM, 24-Jan-2012.) |
Theorem | oplecon3 34486 | Contraposition law for orthoposets. (Contributed by NM, 13-Sep-2011.) |
Theorem | oplecon3b 34487 | Contraposition law for orthoposets. (chsscon3 28359 analog.) (Contributed by NM, 4-Nov-2011.) |
Theorem | oplecon1b 34488 | Contraposition law for strict ordering in orthoposets. (chsscon1 28360 analog.) (Contributed by NM, 6-Nov-2011.) |
Theorem | opoc1 34489 | Orthocomplement of orthoposet unit. (Contributed by NM, 24-Jan-2012.) |
Theorem | opoc0 34490 | Orthocomplement of orthoposet zero. (Contributed by NM, 24-Jan-2012.) |
Theorem | opltcon3b 34491 | Contraposition law for strict ordering in orthoposets. (chpsscon3 28362 analog.) (Contributed by NM, 4-Nov-2011.) |
Theorem | opltcon1b 34492 | Contraposition law for strict ordering in orthoposets. (chpsscon1 28363 analog.) (Contributed by NM, 5-Nov-2011.) |
Theorem | opltcon2b 34493 | Contraposition law for strict ordering in orthoposets. (chsscon2 28361 analog.) (Contributed by NM, 5-Nov-2011.) |
Theorem | opexmid 34494 | Law of excluded middle for orthoposets. (chjo 28374 analog.) (Contributed by NM, 13-Sep-2011.) |
Theorem | opnoncon 34495 | Law of contradiction for orthoposets. (chocin 28354 analog.) (Contributed by NM, 13-Sep-2011.) |
Theorem | riotaocN 34496* | The orthocomplement of the unique poset element such that . (riotaneg 11002 analog.) (Contributed by NM, 16-Jan-2012.) (New usage is discouraged.) |
Theorem | cmtfvalN 34497* | Value of commutes relation. (Contributed by NM, 6-Nov-2011.) (New usage is discouraged.) |
Theorem | cmtvalN 34498 | Equivalence for commutes relation. Definition of commutes in [Kalmbach] p. 20. (cmbr 28443 analog.) (Contributed by NM, 6-Nov-2011.) (New usage is discouraged.) |
Theorem | isolat 34499 | The predicate "is an ortholattice." (Contributed by NM, 18-Sep-2011.) |
Theorem | ollat 34500 | An ortholattice is a lattice. (Contributed by NM, 18-Sep-2011.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |