Home | Metamath
Proof Explorer Theorem List (p. 305 of 310) | < Previous Next > |
Browser slow? Try the
Unicode version. |
Color key: | Metamath Proof Explorer
(1-21328) |
Hilbert Space Explorer
(21329-22851) |
Users' Mathboxes
(22852-30913) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dochsatshpb 30401 | The orthocomplement of a subspace atom is a hyperplane. (Contributed by NM, 29-Oct-2014.) |
LSAtoms LSHyp | ||
Theorem | dochsnshp 30402 | The orthocomplement of a nonzero singleton is a hyperplane. (Contributed by NM, 3-Jan-2015.) |
LSHyp | ||
Theorem | dochshpsat 30403 | A hyperplane is closed iff its orthocomplement is an atom. (Contributed by NM, 29-Oct-2014.) |
LSAtoms LSHyp | ||
Theorem | dochkrsat 30404 | The orthocomplement of a kernel is an atom iff it is nonzero. (Contributed by NM, 1-Nov-2014.) |
LSAtoms LFnl LKer | ||
Theorem | dochkrsat2 30405 | The orthocomplement of a kernel is an atom iff the double orthocomplement is not the vector space. (Contributed by NM, 1-Jan-2015.) |
LSAtoms LFnl LKer | ||
Theorem | dochsat0 30406 | The orthocomplement of a kernel is either an atom or zero. (Contributed by NM, 29-Jan-2015.) |
LSAtoms LFnl LKer | ||
Theorem | dochkrsm 30407 | The subspace sum of a closed subspace and a kernel orthocomplement is closed. (djhlsmcl 30363 can be used to convert sum to join.) (Contributed by NM, 29-Jan-2015.) |
LFnl LKer | ||
Theorem | dochexmidat 30408 | Special case of excluded middle for the singleton of a vector. (Contributed by NM, 27-Oct-2014.) |
Theorem | dochexmidlem1 30409 | Lemma for dochexmid 30417. Holland's proof implicitly requires , which we prove here. (Contributed by NM, 14-Jan-2015.) |
LSAtoms | ||
Theorem | dochexmidlem2 30410 | Lemma for dochexmid 30417. (Contributed by NM, 14-Jan-2015.) |
LSAtoms | ||
Theorem | dochexmidlem3 30411 | Lemma for dochexmid 30417. Use atom exchange lsatexch1 27995 to swap and . (Contributed by NM, 14-Jan-2015.) |
LSAtoms | ||
Theorem | dochexmidlem4 30412 | Lemma for dochexmid 30417. (Contributed by NM, 15-Jan-2015.) |
LSAtoms | ||
Theorem | dochexmidlem5 30413 | Lemma for dochexmid 30417. (Contributed by NM, 15-Jan-2015.) |
LSAtoms | ||
Theorem | dochexmidlem6 30414 | Lemma for dochexmid 30417. (Contributed by NM, 15-Jan-2015.) |
LSAtoms | ||
Theorem | dochexmidlem7 30415 | Lemma for dochexmid 30417. Contradict dochexmidlem6 30414. (Contributed by NM, 15-Jan-2015.) |
LSAtoms | ||
Theorem | dochexmidlem8 30416 | Lemma for dochexmid 30417. The contradiction of dochexmidlem6 30414 and dochexmidlem7 30415 shows that there can be no atom that is not in , which is therefore the whole atom space. (Contributed by NM, 15-Jan-2015.) |
LSAtoms | ||
Theorem | dochexmid 30417 | Excluded middle law for closed subspaces, which is equivalent to (and derived from) the orthomodular law dihoml4 30326. Lemma 3.3(2) in [Holland95] p. 215. In our proof, we use the variables , , , , in place of Hollands' l, m, P, Q, L respectively. (pexmidALTN 28926 analog.) (Contributed by NM, 15-Jan-2015.) |
Theorem | dochsnkrlem1 30418 | Lemma for dochsnkr 30421. (Contributed by NM, 1-Jan-2015.) |
LFnl LKer | ||
Theorem | dochsnkrlem2 30419 | Lemma for dochsnkr 30421. (Contributed by NM, 1-Jan-2015.) |
LFnl LKer LSAtoms | ||
Theorem | dochsnkrlem3 30420 | Lemma for dochsnkr 30421. (Contributed by NM, 2-Jan-2015.) |
LFnl LKer | ||
Theorem | dochsnkr 30421 | A (closed) kernel expressed in terms of a nonzero vector in its orthocomplement. TODO: consolidate lemmas unless they're needed for something else (in which case break out as theorems) (Contributed by NM, 2-Jan-2015.) |
LFnl LKer | ||
Theorem | dochsnkr2 30422* | Kernel of the explicit functional determined by a nonzero vector . Compare the more general lshpkr 28066. (Contributed by NM, 27-Oct-2014.) |
LKer Scalar | ||
Theorem | dochsnkr2cl 30423* | The determining functional belongs to the atom formed by the orthocomplement of the kernel. (Contributed by NM, 4-Jan-2015.) |
LKer Scalar | ||
Theorem | dochflcl 30424* | Closure of the explicit functional determined by a nonzero vector . Compare the more general lshpkrcl 28065. (Contributed by NM, 27-Oct-2014.) |
LFnl Scalar | ||
Theorem | dochfl1 30425* | The value of the explicit functional is 1 at the that determines it. (Contributed by NM, 27-Oct-2014.) |
Scalar | ||
Theorem | dochfln0 30426 | The value of a functional is nonzero at a nonzero vector in the orthocomplement of its kernel. (Contributed by NM, 2-Jan-2015.) |
Scalar LFnl LKer | ||
Theorem | dochkr1 30427* | A non-zero functional has a value of 1 at some argument belonging to the orthocomplement of its kernel (when its kernel is a closed hyperplane). Tighter version of lfl1 28019. (Contributed by NM, 2-Jan-2015.) |
Scalar LFnl LKer | ||
Theorem | dochkr1OLDN 30428* | A non-zero functional has a value of 1 at some argument belonging to the orthocomplement of its kernel (when its kernel is a closed hyperplane). Tighter version of lfl1 28019. (Contributed by NM, 2-Jan-2015.) (New usage is discouraged.) |
Scalar LFnl LKer | ||
Syntax | clpoN 30429 | Extend class notation with all polarities of a left module or left vector space. |
LPol | ||
Definition | df-lpolN 30430* | Define the set of all polarities of a left module or left vector space. A polarity is a kind of complementation operation on a subspace. The double polarity of a subspace is a closure operation. Based on Definition 3.2 of [Holland95] p. 214 for projective geometry polarities. For convenience, we open up the domain to include all vector subsets and not just subspaces, but any more restricted polarity can be converted to this one by taking the span of its argument. (Contributed by NM, 24-Nov-2014.) |
LPol LSAtoms LSHyp | ||
Theorem | lpolsetN 30431* | The set of polarities of a left module or left vector space. (Contributed by NM, 24-Nov-2014.) (New usage is discouraged.) |
LSAtoms LSHyp LPol | ||
Theorem | islpolN 30432* | The predicate "is a polarity". (Contributed by NM, 24-Nov-2014.) (New usage is discouraged.) |
LSAtoms LSHyp LPol | ||
Theorem | islpoldN 30433* | Properties that determine a polarity. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.) |
LSAtoms LSHyp LPol | ||
Theorem | lpolfN 30434 | Functionality of a polarity. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.) |
LPol | ||
Theorem | lpolvN 30435 | The polarity of the whole space is the zero subspace. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.) |
LPol | ||
Theorem | lpolconN 30436 | Contraposition property of a polarity. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.) |
LPol | ||
Theorem | lpolsatN 30437 | The polarity of an atomic subspace is a hyperplane. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.) |
LSAtoms LSHyp LPol | ||
Theorem | lpolpolsatN 30438 | Property of a polarity. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.) |
LSAtoms LPol | ||
Theorem | dochpolN 30439 | The subspace orthocomplement for the vector space is a polarity. (Contributed by NM, 27-Dec-2014.) (New usage is discouraged.) |
LPol | ||
Theorem | lcfl1lem 30440* | Property of a functional with a closed kernel. (Contributed by NM, 28-Dec-2014.) |
Theorem | lcfl1 30441* | Property of a functional with a closed kernel. (Contributed by NM, 31-Dec-2014.) |
Theorem | lcfl2 30442* | Property of a functional with a closed kernel. (Contributed by NM, 1-Jan-2015.) |
LFnl LKer | ||
Theorem | lcfl3 30443* | Property of a functional with a closed kernel. (Contributed by NM, 1-Jan-2015.) |
LSAtoms LFnl LKer | ||
Theorem | lcfl4N 30444* | Property of a functional with a closed kernel. (Contributed by NM, 1-Jan-2015.) (New usage is discouraged.) |
LSHyp LFnl LKer | ||
Theorem | lcfl5 30445* | Property of a functional with a closed kernel. (Contributed by NM, 1-Jan-2015.) |
LFnl LKer | ||
Theorem | lcfl5a 30446 | Property of a functional with a closed kernel. TODO: Make lcfl5 30445 etc. obsolete and rewrite w/out hypothesis? (Contributed by NM, 29-Jan-2015.) |
LFnl LKer | ||
Theorem | lcfl6lem 30447* | Lemma for lcfl6 30449. A functional (whose kernel is closed by dochsnkr 30421) is comletely determined by a vector in the orthocomplement in its kernel at which the functional value is 1. Note that the in the hypothesis is redundant by the last hypothesis but allows easier use of other theorems. (Contributed by NM, 3-Jan-2015.) |
Scalar LFnl LKer | ||
Theorem | lcfl7lem 30448* | Lemma for lcfl7N 30450. If two functionals and are equal, they are determined by the same vector. (Contributed by NM, 4-Jan-2015.) |
Scalar LFnl LKer | ||
Theorem | lcfl6 30449* | Property of a functional with a closed kernel. Note that means the functional is zero by lkr0f 28043. (Contributed by NM, 3-Jan-2015.) |
Scalar LFnl LKer | ||
Theorem | lcfl7N 30450* | Property of a functional with a closed kernel. Every nonzero functional is determined by a unique nonzero vector. Note that means the functional is zero by lkr0f 28043. (Contributed by NM, 4-Jan-2015.) (New usage is discouraged.) |
Scalar LFnl LKer | ||
Theorem | lcfl8 30451* | Property of a functional with a closed kernel. (Contributed by NM, 17-Jan-2015.) |
LFnl LKer | ||
Theorem | lcfl8a 30452* | Property of a functional with a closed kernel. (Contributed by NM, 17-Jan-2015.) |
LFnl LKer | ||
Theorem | lcfl8b 30453* | Property of a nonzero functional with a closed kernel. (Contributed by NM, 4-Feb-2015.) |
LFnl LKer LDual | ||
Theorem | lcfl9a 30454 | Property implying that a functional has a closed kernel. (Contributed by NM, 16-Feb-2015.) |
LFnl LKer | ||
Theorem | lclkrlem1 30455* | The set of functionals having closed kernels is closed under scalar product. (Contributed by NM, 28-Dec-2014.) |
LFnl LKer LDual Scalar | ||
Theorem | lclkrlem2a 30456 | Lemma for lclkr 30482. Use lshpat 28005 to show that the intersection of a hyperplane with a noncomparable sum of atoms is an atom. (Contributed by NM, 16-Jan-2015.) |
LSAtoms | ||
Theorem | lclkrlem2b 30457 | Lemma for lclkr 30482. (Contributed by NM, 17-Jan-2015.) |
LSAtoms | ||
Theorem | lclkrlem2c 30458 | Lemma for lclkr 30482. (Contributed by NM, 16-Jan-2015.) |
LSAtoms LSHyp | ||
Theorem | lclkrlem2d 30459 | Lemma for lclkr 30482. (Contributed by NM, 16-Jan-2015.) |
LSAtoms | ||
Theorem | lclkrlem2e 30460 | Lemma for lclkr 30482. The kernel of the sum is closed when the kernels of the summands are equal and closed. (Contributed by NM, 17-Jan-2015.) |
LFnl LKer LDual | ||
Theorem | lclkrlem2f 30461 | Lemma for lclkr 30482. Construct a closed hyperplane under the kernel of the sum. (Contributed by NM, 16-Jan-2015.) |
Scalar LFnl LSHyp LKer LDual | ||
Theorem | lclkrlem2g 30462 | Lemma for lclkr 30482. Comparable hyperplanes are equal, so the kernel of the sum is closed. (Contributed by NM, 16-Jan-2015.) |
Scalar LFnl LSHyp LKer LDual | ||
Theorem | lclkrlem2h 30463 | Lemma for lclkr 30482. Eliminate the hypothesis. (Contributed by NM, 16-Jan-2015.) |
Scalar LFnl LSHyp LKer LDual | ||
Theorem | lclkrlem2i 30464 | Lemma for lclkr 30482. Eliminate the hypothesis. (Contributed by NM, 17-Jan-2015.) |
Scalar LFnl LSHyp LKer LDual | ||
Theorem | lclkrlem2j 30465 | Lemma for lclkr 30482. Kernel closure when is zero. (Contributed by NM, 18-Jan-2015.) |
Scalar LFnl LSHyp LKer LDual | ||
Theorem | lclkrlem2k 30466 | Lemma for lclkr 30482. Kernel closure when is zero. (Contributed by NM, 18-Jan-2015.) |
Scalar LFnl LSHyp LKer LDual | ||
Theorem | lclkrlem2l 30467 | Lemma for lclkr 30482. Eliminate the , hypotheses. (Contributed by NM, 18-Jan-2015.) |
Scalar LFnl LSHyp LKer LDual | ||
Theorem | lclkrlem2m 30468 | Lemma for lclkr 30482. Construct a vector that makes the sum of functionals zero. Combine with to shorten overall proof. (Contributed by NM, 17-Jan-2015.) |
Scalar LFnl LDual | ||
Theorem | lclkrlem2n 30469 | Lemma for lclkr 30482. (Contributed by NM, 12-Jan-2015.) |
Scalar LFnl LDual LKer | ||
Theorem | lclkrlem2o 30470 | Lemma for lclkr 30482. When is nonzero, the vectors and can't both belong to the hyperplane generated by . (Contributed by NM, 17-Jan-2015.) |
Scalar LFnl LDual LKer | ||
Theorem | lclkrlem2p 30471 | Lemma for lclkr 30482. When is zero, and must colinear, so their orthocomplements must be comparable. (Contributed by NM, 17-Jan-2015.) |
Scalar LFnl LDual LKer | ||
Theorem | lclkrlem2q 30472 | Lemma for lclkr 30482. The sum has a closed kernel when is nonzero. (Contributed by NM, 18-Jan-2015.) |
Scalar LFnl LDual LKer | ||
Theorem | lclkrlem2r 30473 | Lemma for lclkr 30482. When is zero, i.e. when and are colinear, the intersection of the kernels of and equal the kernel of , so the kernels of and the sum are comparable. (Contributed by NM, 18-Jan-2015.) |
Scalar LFnl LDual LKer | ||
Theorem | lclkrlem2s 30474 | Lemma for lclkr 30482. Thus the sum has a closed kernel when is zero. (Contributed by NM, 18-Jan-2015.) |
Scalar LFnl LDual LKer | ||
Theorem | lclkrlem2t 30475 | Lemma for lclkr 30482. We eliminate all hypotheses with here. (Contributed by NM, 18-Jan-2015.) |
Scalar LFnl LDual LKer | ||
Theorem | lclkrlem2u 30476 | Lemma for lclkr 30482. lclkrlem2t 30475 with and swapped. (Contributed by NM, 18-Jan-2015.) |
Scalar LFnl LDual LKer | ||
Theorem | lclkrlem2v 30477 | Lemma for lclkr 30482. When the hypotheses of lclkrlem2u 30476 and lclkrlem2u 30476 are negated, the functional sum must be zero, so the kernel is the vector space. We make use of the law of excluded middle, dochexmid 30417, which requires the orthomodular law dihoml4 30326 (Lemma 3.3 of [Holland95] p. 214). (Contributed by NM, 16-Jan-2015.) |
Scalar LFnl LDual LKer | ||
Theorem | lclkrlem2w 30478 | Lemma for lclkr 30482. This is the same as lclkrlem2u 30476 and lclkrlem2u 30476 with the inequality hypotheses negated. When the sum of two functionals is zero at each generating vector, the kernel is the vector space and therefore closed. (Contributed by NM, 16-Jan-2015.) |
Scalar LFnl LDual LKer | ||
Theorem | lclkrlem2x 30479 | Lemma for lclkr 30482. Eliminate by cases the hypotheses of lclkrlem2u 30476, lclkrlem2u 30476 and lclkrlem2w 30478. (Contributed by NM, 18-Jan-2015.) |
LKer LFnl LDual | ||
Theorem | lclkrlem2y 30480 | Lemma for lclkr 30482. Restate the hypotheses for and to say their kernels are closed, in order to eliminate the generating vectors and . (Contributed by NM, 18-Jan-2015.) |
LKer LFnl LDual | ||
Theorem | lclkrlem2 30481* | The set of functionals having closed kernels is closed under vector (functional) addition. Lemmas lclkrlem2a 30456 through lclkrlem2y 30480 are used for the proof. Here we express lclkrlem2y 30480 in terms of membership in the set of functionals with closed kernels. (Contributed by NM, 18-Jan-2015.) |
LFnl LKer LDual | ||
Theorem | lclkr 30482* | The set of functionals with closed kernels is a subspace. Part of proof of Theorem 3.6 of [Holland95] p. 218, line 20, stating "The f_{M} that arise this way generate a subspace F of E'". Our proof was suggested by Mario Carneiro, 5-Jan-2015. (Contributed by NM, 18-Jan-2015.) |
LFnl LKer LDual | ||
Theorem | lcfls1lem 30483* | Property of a functional with a closed kernel. (Contributed by NM, 27-Jan-2015.) |
Theorem | lcfls1N 30484* | Property of a functional with a closed kernel. (Contributed by NM, 27-Jan-2015.) (New usage is discouraged.) |
Theorem | lcfls1c 30485* | Property of a functional with a closed kernel. (Contributed by NM, 28-Jan-2015.) |
Theorem | lclkrslem1 30486* | The set of functionals having closed kernels and majorizing the orthocomplement of a given subspace is closed under scalar product. (Contributed by NM, 27-Jan-2015.) |
LFnl LKer LDual Scalar | ||
Theorem | lclkrslem2 30487* | The set of functionals having closed kernels and majorizing the orthocomplement of a given subspace is closed under scalar product. (Contributed by NM, 28-Jan-2015.) |
LFnl LKer LDual Scalar | ||
Theorem | lclkrs 30488* | The set of functionals having closed kernels and majorizing the orthocomplement of a given subspace is a subspace of the dual space. TODO: This proof repeats large parts of the lclkr 30482 proof. Do we achieve overall shortening by breaking them out as subtheorems? Or make lclkr 30482 a special case of this? (Contributed by NM, 29-Jan-2015.) |
LFnl LKer LDual | ||
Theorem | lclkrs2 30489* | The set of functionals with closed kernels and majorizing the orthocomplement of a given subspace is a subspace of the dual space containing functionals with closed kernels. Note that is the value given by mapdval 30577. (Contributed by NM, 12-Mar-2015.) |
LFnl LKer |