Home | Metamath
Proof ExplorerTheorem List
(p. 318 of 323)
| < Previous Next > |

Browser slow? Try the
Unicode version. |

Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs

Color key: | Metamath Proof Explorer
(1-21500) |
Hilbert Space Explorer
(21501-23023) |
Users' Mathboxes
(23024-32227) |

Type | Label | Description |
---|---|---|

Statement | ||

Theorem | dvh4dimat 31701* | There is an atom that is outside the subspace sum of 3 others. (Contributed by NM, 25-Apr-2015.) |

LSAtoms | ||

Theorem | dvh3dimatN 31702* | There is an atom that is outside the subspace sum of 2 others. (Contributed by NM, 25-Apr-2015.) (New usage is discouraged.) |

LSAtoms | ||

Theorem | dvh2dimatN 31703* | Given an atom, there exists another. (Contributed by NM, 25-Apr-2015.) (New usage is discouraged.) |

LSAtoms | ||

Theorem | dvh1dimat 31704* | There exists an atom. (Contributed by NM, 25-Apr-2015.) |

LSAtoms | ||

Theorem | dvh1dim 31705* | There exists a nonzero vector. (Contributed by NM, 26-Apr-2015.) |

Theorem | dvh4dimlem 31706* | Lemma for dvh4dimN 31710. (Contributed by NM, 22-May-2015.) |

Theorem | dvhdimlem 31707* | Lemma for dvh2dim 31708 and dvh3dim 31709. TODO: make this obsolete and use dvh4dimlem 31706 directly? (Contributed by NM, 24-Apr-2015.) |

Theorem | dvh2dim 31708* | There is a vector that is outside the span of another. (Contributed by NM, 25-Apr-2015.) |

Theorem | dvh3dim 31709* | There is a vector that is outside the span of 2 others. (Contributed by NM, 24-Apr-2015.) |

Theorem | dvh4dimN 31710* | There is a vector that is outside the span of 3 others. (Contributed by NM, 22-May-2015.) (New usage is discouraged.) |

Theorem | dvh3dim2 31711* | There is a vector that is outside of 2 spans with a common vector. (Contributed by NM, 13-May-2015.) |

Theorem | dvh3dim3N 31712* | There is a vector that is outside of 2 spans. TODO: decide to use either this or dvh3dim2 31711 everywhere. If this one is needed, make dvh3dim2 31711 into a lemma. (Contributed by NM, 21-May-2015.) (New usage is discouraged.) |

Theorem | dochsnnz 31713 | The orthocomplement of a singleton is nonzero. (Contributed by NM, 13-Jun-2015.) |

Theorem | dochsatshp 31714 | The orthocomplement of a subspace atom is a hyperplane. (Contributed by NM, 27-Jul-2014.) (Revised by Mario Carneiro, 1-Oct-2014.) |

LSAtoms LSHyp | ||

Theorem | dochsatshpb 31715 | The orthocomplement of a subspace atom is a hyperplane. (Contributed by NM, 29-Oct-2014.) |

LSAtoms LSHyp | ||

Theorem | dochsnshp 31716 | The orthocomplement of a nonzero singleton is a hyperplane. (Contributed by NM, 3-Jan-2015.) |

LSHyp | ||

Theorem | dochshpsat 31717 | A hyperplane is closed iff its orthocomplement is an atom. (Contributed by NM, 29-Oct-2014.) |

LSAtoms LSHyp | ||

Theorem | dochkrsat 31718 | The orthocomplement of a kernel is an atom iff it is nonzero. (Contributed by NM, 1-Nov-2014.) |

LSAtoms LFnl LKer | ||

Theorem | dochkrsat2 31719 | 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 31720 | The orthocomplement of a kernel is either an atom or zero. (Contributed by NM, 29-Jan-2015.) |

LSAtoms LFnl LKer | ||

Theorem | dochkrsm 31721 | The subspace sum of a closed subspace and a kernel orthocomplement is closed. (djhlsmcl 31677 can be used to convert sum to join.) (Contributed by NM, 29-Jan-2015.) |

LFnl LKer | ||

Theorem | dochexmidat 31722 | Special case of excluded middle for the singleton of a vector. (Contributed by NM, 27-Oct-2014.) |

Theorem | dochexmidlem1 31723 | Lemma for dochexmid 31731. Holland's proof implicitly requires , which we prove here. (Contributed by NM, 14-Jan-2015.) |

LSAtoms | ||

Theorem | dochexmidlem2 31724 | Lemma for dochexmid 31731. (Contributed by NM, 14-Jan-2015.) |

LSAtoms | ||

Theorem | dochexmidlem3 31725 | Lemma for dochexmid 31731. Use atom exchange lsatexch1 29309 to swap and . (Contributed by NM, 14-Jan-2015.) |

LSAtoms | ||

Theorem | dochexmidlem4 31726 | Lemma for dochexmid 31731. (Contributed by NM, 15-Jan-2015.) |

LSAtoms | ||

Theorem | dochexmidlem5 31727 | Lemma for dochexmid 31731. (Contributed by NM, 15-Jan-2015.) |

LSAtoms | ||

Theorem | dochexmidlem6 31728 | Lemma for dochexmid 31731. (Contributed by NM, 15-Jan-2015.) |

LSAtoms | ||

Theorem | dochexmidlem7 31729 | Lemma for dochexmid 31731. Contradict dochexmidlem6 31728. (Contributed by NM, 15-Jan-2015.) |

LSAtoms | ||

Theorem | dochexmidlem8 31730 | Lemma for dochexmid 31731. The contradiction of dochexmidlem6 31728 and dochexmidlem7 31729 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 31731 | Excluded middle law for closed subspaces, which is equivalent to (and derived from) the orthomodular law dihoml4 31640. 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 30240 analog.) (Contributed by NM, 15-Jan-2015.) |

Theorem | dochsnkrlem1 31732 | Lemma for dochsnkr 31735. (Contributed by NM, 1-Jan-2015.) |

LFnl LKer | ||

Theorem | dochsnkrlem2 31733 | Lemma for dochsnkr 31735. (Contributed by NM, 1-Jan-2015.) |

LFnl LKer LSAtoms | ||

Theorem | dochsnkrlem3 31734 | Lemma for dochsnkr 31735. (Contributed by NM, 2-Jan-2015.) |

LFnl LKer | ||

Theorem | dochsnkr 31735 | 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 31736* | Kernel of the explicit functional determined by a nonzero vector . Compare the more general lshpkr 29380. (Contributed by NM, 27-Oct-2014.) |

LKer Scalar | ||

Theorem | dochsnkr2cl 31737* | The determining functional belongs to the atom formed by the orthocomplement of the kernel. (Contributed by NM, 4-Jan-2015.) |

LKer Scalar | ||

Theorem | dochflcl 31738* | Closure of the explicit functional determined by a nonzero vector . Compare the more general lshpkrcl 29379. (Contributed by NM, 27-Oct-2014.) |

LFnl Scalar | ||

Theorem | dochfl1 31739* | The value of the explicit functional is 1 at the that determines it. (Contributed by NM, 27-Oct-2014.) |

Scalar | ||

Theorem | dochfln0 31740 | 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 31741* | 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 29333. (Contributed by NM, 2-Jan-2015.) |

Scalar LFnl LKer | ||

Theorem | dochkr1OLDN 31742* | 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 29333. (Contributed by NM, 2-Jan-2015.) (New usage is discouraged.) |

Scalar LFnl LKer | ||

18.27.11 Construction of involution and inner
product from a Hilbert lattice | ||

Syntax | clpoN 31743 | Extend class notation with all polarities of a left module or left vector space. |

LPol | ||

Definition | df-lpolN 31744* | 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 31745* | 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 31746* | The predicate "is a polarity". (Contributed by NM, 24-Nov-2014.) (New usage is discouraged.) |

LSAtoms LSHyp LPol | ||

Theorem | islpoldN 31747* | Properties that determine a polarity. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.) |

LSAtoms LSHyp LPol | ||

Theorem | lpolfN 31748 | Functionality of a polarity. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.) |

LPol | ||

Theorem | lpolvN 31749 | The polarity of the whole space is the zero subspace. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.) |

LPol | ||

Theorem | lpolconN 31750 | Contraposition property of a polarity. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.) |

LPol | ||

Theorem | lpolsatN 31751 | The polarity of an atomic subspace is a hyperplane. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.) |

LSAtoms LSHyp LPol | ||

Theorem | lpolpolsatN 31752 | Property of a polarity. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.) |

LSAtoms LPol | ||

Theorem | dochpolN 31753 | The subspace orthocomplement for the vector space is a polarity. (Contributed by NM, 27-Dec-2014.) (New usage is discouraged.) |

LPol | ||

Theorem | lcfl1lem 31754* | Property of a functional with a closed kernel. (Contributed by NM, 28-Dec-2014.) |

Theorem | lcfl1 31755* | Property of a functional with a closed kernel. (Contributed by NM, 31-Dec-2014.) |

Theorem | lcfl2 31756* | Property of a functional with a closed kernel. (Contributed by NM, 1-Jan-2015.) |

LFnl LKer | ||

Theorem | lcfl3 31757* | Property of a functional with a closed kernel. (Contributed by NM, 1-Jan-2015.) |

LSAtoms LFnl LKer | ||

Theorem | lcfl4N 31758* | Property of a functional with a closed kernel. (Contributed by NM, 1-Jan-2015.) (New usage is discouraged.) |

LSHyp LFnl LKer | ||

Theorem | lcfl5 31759* | Property of a functional with a closed kernel. (Contributed by NM, 1-Jan-2015.) |

LFnl LKer | ||

Theorem | lcfl5a 31760 | Property of a functional with a closed kernel. TODO: Make lcfl5 31759 etc. obsolete and rewrite w/out hypothesis? (Contributed by NM, 29-Jan-2015.) |

LFnl LKer | ||

Theorem | lcfl6lem 31761* | Lemma for lcfl6 31763. A functional (whose kernel is closed by dochsnkr 31735) 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 31762* | Lemma for lcfl7N 31764. If two functionals and are equal, they are determined by the same vector. (Contributed by NM, 4-Jan-2015.) |

Scalar LFnl LKer | ||

Theorem | lcfl6 31763* | Property of a functional with a closed kernel. Note that means the functional is zero by lkr0f 29357. (Contributed by NM, 3-Jan-2015.) |

Scalar LFnl LKer | ||

Theorem | lcfl7N 31764* | 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 29357. (Contributed by NM, 4-Jan-2015.) (New usage is discouraged.) |

Scalar LFnl LKer | ||

Theorem | lcfl8 31765* | Property of a functional with a closed kernel. (Contributed by NM, 17-Jan-2015.) |

LFnl LKer | ||

Theorem | lcfl8a 31766* | Property of a functional with a closed kernel. (Contributed by NM, 17-Jan-2015.) |

LFnl LKer | ||

Theorem | lcfl8b 31767* | Property of a nonzero functional with a closed kernel. (Contributed by NM, 4-Feb-2015.) |

LFnl LKer LDual | ||

Theorem | lcfl9a 31768 | Property implying that a functional has a closed kernel. (Contributed by NM, 16-Feb-2015.) |

LFnl LKer | ||

Theorem | lclkrlem1 31769* | The set of functionals having closed kernels is closed under scalar product. (Contributed by NM, 28-Dec-2014.) |

LFnl LKer LDual Scalar | ||

Theorem | lclkrlem2a 31770 | Lemma for lclkr 31796. Use lshpat 29319 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 31771 | Lemma for lclkr 31796. (Contributed by NM, 17-Jan-2015.) |

LSAtoms | ||

Theorem | lclkrlem2c 31772 | Lemma for lclkr 31796. (Contributed by NM, 16-Jan-2015.) |

LSAtoms LSHyp | ||

Theorem | lclkrlem2d 31773 | Lemma for lclkr 31796. (Contributed by NM, 16-Jan-2015.) |

LSAtoms | ||

Theorem | lclkrlem2e 31774 | Lemma for lclkr 31796. 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 31775 | Lemma for lclkr 31796. Construct a closed hyperplane under the kernel of the sum. (Contributed by NM, 16-Jan-2015.) |

Scalar LFnl LSHyp LKer LDual | ||

Theorem | lclkrlem2g 31776 | Lemma for lclkr 31796. 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 31777 | Lemma for lclkr 31796. Eliminate the hypothesis. (Contributed by NM, 16-Jan-2015.) |

Scalar LFnl LSHyp LKer LDual | ||

Theorem | lclkrlem2i 31778 | Lemma for lclkr 31796. Eliminate the hypothesis. (Contributed by NM, 17-Jan-2015.) |

Scalar LFnl LSHyp LKer LDual | ||

Theorem | lclkrlem2j 31779 | Lemma for lclkr 31796. Kernel closure when is zero. (Contributed by NM, 18-Jan-2015.) |

Scalar LFnl LSHyp LKer LDual | ||

Theorem | lclkrlem2k 31780 | Lemma for lclkr 31796. Kernel closure when is zero. (Contributed by NM, 18-Jan-2015.) |

Scalar LFnl LSHyp LKer LDual | ||

Theorem | lclkrlem2l 31781 | Lemma for lclkr 31796. Eliminate the , hypotheses. (Contributed by NM, 18-Jan-2015.) |

Scalar LFnl LSHyp LKer LDual | ||

Theorem | lclkrlem2m 31782 | Lemma for lclkr 31796. 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 31783 | Lemma for lclkr 31796. (Contributed by NM, 12-Jan-2015.) |

Scalar LFnl LDual LKer | ||

Theorem | lclkrlem2o 31784 | Lemma for lclkr 31796. 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 31785 | Lemma for lclkr 31796. When is zero, and must colinear, so their orthocomplements must be comparable. (Contributed by NM, 17-Jan-2015.) |

Scalar LFnl LDual LKer | ||

Theorem | lclkrlem2q 31786 | Lemma for lclkr 31796. The sum has a closed kernel when is nonzero. (Contributed by NM, 18-Jan-2015.) |

Scalar LFnl LDual LKer | ||

Theorem | lclkrlem2r 31787 | Lemma for lclkr 31796. 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 31788 | Lemma for lclkr 31796. Thus, the sum has a closed kernel when is zero. (Contributed by NM, 18-Jan-2015.) |

Scalar LFnl LDual LKer | ||

Theorem | lclkrlem2t 31789 | Lemma for lclkr 31796. We eliminate all hypotheses with here. (Contributed by NM, 18-Jan-2015.) |

Scalar LFnl LDual LKer | ||

Theorem | lclkrlem2u 31790 | Lemma for lclkr 31796. lclkrlem2t 31789 with and swapped. (Contributed by NM, 18-Jan-2015.) |

Scalar LFnl LDual LKer | ||

Theorem | lclkrlem2v 31791 | Lemma for lclkr 31796. When the hypotheses of lclkrlem2u 31790 and lclkrlem2u 31790 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 31731, which requires the orthomodular law dihoml4 31640 (Lemma 3.3 of [Holland95] p. 214). (Contributed by NM, 16-Jan-2015.) |

Scalar LFnl LDual LKer | ||

Theorem | lclkrlem2w 31792 | Lemma for lclkr 31796. This is the same as lclkrlem2u 31790 and lclkrlem2u 31790 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 31793 | Lemma for lclkr 31796. Eliminate by cases the hypotheses of lclkrlem2u 31790, lclkrlem2u 31790 and lclkrlem2w 31792. (Contributed by NM, 18-Jan-2015.) |

LKer LFnl LDual < |