Home | Metamath
Proof Explorer Theorem List (p. 369 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 | lclkrlem2f 36801 | Lemma for lclkr 36822. Construct a closed hyperplane under the kernel of the sum. (Contributed by NM, 16-Jan-2015.) |
Scalar LFnl LSHyp LKer LDual | ||
Theorem | lclkrlem2g 36802 | Lemma for lclkr 36822. 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 36803 | Lemma for lclkr 36822. Eliminate the hypothesis. (Contributed by NM, 16-Jan-2015.) |
Scalar LFnl LSHyp LKer LDual | ||
Theorem | lclkrlem2i 36804 | Lemma for lclkr 36822. Eliminate the hypothesis. (Contributed by NM, 17-Jan-2015.) |
Scalar LFnl LSHyp LKer LDual | ||
Theorem | lclkrlem2j 36805 | Lemma for lclkr 36822. Kernel closure when is zero. (Contributed by NM, 18-Jan-2015.) |
Scalar LFnl LSHyp LKer LDual | ||
Theorem | lclkrlem2k 36806 | Lemma for lclkr 36822. Kernel closure when is zero. (Contributed by NM, 18-Jan-2015.) |
Scalar LFnl LSHyp LKer LDual | ||
Theorem | lclkrlem2l 36807 | Lemma for lclkr 36822. Eliminate the , hypotheses. (Contributed by NM, 18-Jan-2015.) |
Scalar LFnl LSHyp LKer LDual | ||
Theorem | lclkrlem2m 36808 | Lemma for lclkr 36822. 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 36809 | Lemma for lclkr 36822. (Contributed by NM, 12-Jan-2015.) |
Scalar LFnl LDual LKer | ||
Theorem | lclkrlem2o 36810 | Lemma for lclkr 36822. 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 36811 | Lemma for lclkr 36822. When is zero, and must colinear, so their orthocomplements must be comparable. (Contributed by NM, 17-Jan-2015.) |
Scalar LFnl LDual LKer | ||
Theorem | lclkrlem2q 36812 | Lemma for lclkr 36822. The sum has a closed kernel when is nonzero. (Contributed by NM, 18-Jan-2015.) |
Scalar LFnl LDual LKer | ||
Theorem | lclkrlem2r 36813 | Lemma for lclkr 36822. 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 36814 | Lemma for lclkr 36822. Thus, the sum has a closed kernel when is zero. (Contributed by NM, 18-Jan-2015.) |
Scalar LFnl LDual LKer | ||
Theorem | lclkrlem2t 36815 | Lemma for lclkr 36822. We eliminate all hypotheses with here. (Contributed by NM, 18-Jan-2015.) |
Scalar LFnl LDual LKer | ||
Theorem | lclkrlem2u 36816 | Lemma for lclkr 36822. lclkrlem2t 36815 with and swapped. (Contributed by NM, 18-Jan-2015.) |
Scalar LFnl LDual LKer | ||
Theorem | lclkrlem2v 36817 | Lemma for lclkr 36822. When the hypotheses of lclkrlem2u 36816 and lclkrlem2u 36816 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 36757, which requires the orthomodular law dihoml4 36666 (Lemma 3.3 of [Holland95] p. 214). (Contributed by NM, 16-Jan-2015.) |
Scalar LFnl LDual LKer | ||
Theorem | lclkrlem2w 36818 | Lemma for lclkr 36822. This is the same as lclkrlem2u 36816 and lclkrlem2u 36816 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 36819 | Lemma for lclkr 36822. Eliminate by cases the hypotheses of lclkrlem2u 36816, lclkrlem2u 36816 and lclkrlem2w 36818. (Contributed by NM, 18-Jan-2015.) |
LKer LFnl LDual | ||
Theorem | lclkrlem2y 36820 | Lemma for lclkr 36822. 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 36821* | The set of functionals having closed kernels is closed under vector (functional) addition. Lemmas lclkrlem2a 36796 through lclkrlem2y 36820 are used for the proof. Here we express lclkrlem2y 36820 in terms of membership in the set of functionals with closed kernels. (Contributed by NM, 18-Jan-2015.) |
LFnl LKer LDual | ||
Theorem | lclkr 36822* | 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 fM 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 36823* | Property of a functional with a closed kernel. (Contributed by NM, 27-Jan-2015.) |
Theorem | lcfls1N 36824* | Property of a functional with a closed kernel. (Contributed by NM, 27-Jan-2015.) (New usage is discouraged.) |
Theorem | lcfls1c 36825* | Property of a functional with a closed kernel. (Contributed by NM, 28-Jan-2015.) |
Theorem | lclkrslem1 36826* | 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 36827* | 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 36828* | 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 36822 proof. Do we achieve overall shortening by breaking them out as subtheorems? Or make lclkr 36822 a special case of this? (Contributed by NM, 29-Jan-2015.) |
LFnl LKer LDual | ||
Theorem | lclkrs2 36829* | 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 36917. (Contributed by NM, 12-Mar-2015.) |
LFnl LKer LDual | ||
Theorem | lcfrvalsnN 36830* | Reconstruction from the dual space span of a singleton. (Contributed by NM, 19-Feb-2015.) (New usage is discouraged.) |
LFnl LKer LDual | ||
Theorem | lcfrlem1 36831 | Lemma for lcfr 36874. Note that is z in Mario's notes. (Contributed by NM, 27-Feb-2015.) |
Scalar LFnl LDual | ||
Theorem | lcfrlem2 36832 | Lemma for lcfr 36874. (Contributed by NM, 27-Feb-2015.) |
Scalar LFnl LDual LKer | ||
Theorem | lcfrlem3 36833 | Lemma for lcfr 36874. (Contributed by NM, 27-Feb-2015.) |
Scalar LFnl LDual LKer | ||
Theorem | lcfrlem4 36834* | Lemma for lcfr 36874. (Contributed by NM, 10-Mar-2015.) |
LKer LDual | ||
Theorem | lcfrlem5 36835* | Lemma for lcfr 36874. The set of functionals having closed kernels and majorizing the orthocomplement of a given subspace is closed under scalar product. TODO: share hypotheses with others. Use more consistent variable names here or elsewhere when possible. (Contributed by NM, 5-Mar-2015.) |
LFnl LKer LDual Scalar | ||
Theorem | lcfrlem6 36836* | Lemma for lcfr 36874. Closure of vector sum with colinear vectors. TODO: Move down definition so top hypotheses can be shared. (Contributed by NM, 10-Mar-2015.) |
LKer LDual | ||
Theorem | lcfrlem7 36837* | Lemma for lcfr 36874. Closure of vector sum when one vector is zero. TODO: share hypotheses with others. (Contributed by NM, 11-Mar-2015.) |
LKer LDual | ||
Theorem | lcfrlem8 36838* | Lemma for lcf1o 36840 and lcfr 36874. (Contributed by NM, 21-Feb-2015.) |
Scalar LFnl LKer LDual | ||
Theorem | lcfrlem9 36839* | Lemma for lcf1o 36840. (This part has undesirable $d's on and that we remove in lcf1o 36840.) TODO: ugly proof; maybe have better subtheorems or abbreviate some expansions with ? TODO: Some redundant $d's? (Contributed by NM, 22-Feb-2015.) |
Scalar LFnl LKer LDual | ||
Theorem | lcf1o 36840* | Define a function that provides a bijection from nonzero vectors to nonzero functionals with closed kernels . (Contributed by NM, 22-Feb-2015.) |
Scalar LFnl LKer LDual | ||
Theorem | lcfrlem10 36841* | Lemma for lcfr 36874. (Contributed by NM, 23-Feb-2015.) |
Scalar LFnl LKer LDual | ||
Theorem | lcfrlem11 36842* | Lemma for lcfr 36874. (Contributed by NM, 23-Feb-2015.) |
Scalar LFnl LKer LDual | ||
Theorem | lcfrlem12N 36843* | Lemma for lcfr 36874. (Contributed by NM, 23-Feb-2015.) (New usage is discouraged.) |
Scalar LFnl LKer LDual | ||
Theorem | lcfrlem13 36844* | Lemma for lcfr 36874. (Contributed by NM, 8-Mar-2015.) |
Scalar LFnl LKer LDual | ||
Theorem | lcfrlem14 36845* | Lemma for lcfr 36874. (Contributed by NM, 10-Mar-2015.) |
Scalar LFnl LKer LDual | ||
Theorem | lcfrlem15 36846* | Lemma for lcfr 36874. (Contributed by NM, 9-Mar-2015.) |
Scalar LFnl LKer LDual | ||
Theorem | lcfrlem16 36847* | Lemma for lcfr 36874. (Contributed by NM, 8-Mar-2015.) |
Scalar LFnl LKer LDual | ||
Theorem | lcfrlem17 36848 | Lemma for lcfr 36874. Condition needed more than once. (Contributed by NM, 11-Mar-2015.) |
LSAtoms | ||
Theorem | lcfrlem18 36849 | Lemma for lcfr 36874. (Contributed by NM, 24-Feb-2015.) |
LSAtoms | ||
Theorem | lcfrlem19 36850 | Lemma for lcfr 36874. (Contributed by NM, 11-Mar-2015.) |
LSAtoms | ||
Theorem | lcfrlem20 36851 | Lemma for lcfr 36874. (Contributed by NM, 11-Mar-2015.) |
LSAtoms | ||
Theorem | lcfrlem21 36852 | Lemma for lcfr 36874. (Contributed by NM, 11-Mar-2015.) |
LSAtoms | ||
Theorem | lcfrlem22 36853 | Lemma for lcfr 36874. (Contributed by NM, 24-Feb-2015.) |
LSAtoms | ||
Theorem | lcfrlem23 36854 | Lemma for lcfr 36874. TODO: this proof was built from other proof pieces that may change into subspace sum and back unnecessarily, or similar things. (Contributed by NM, 1-Mar-2015.) |
LSAtoms | ||
Theorem | lcfrlem24 36855* | Lemma for lcfr 36874. (Contributed by NM, 24-Feb-2015.) |
LSAtoms Scalar LKer | ||
Theorem | lcfrlem25 36856* | Lemma for lcfr 36874. Special case of lcfrlem35 36866 when is zero. (Contributed by NM, 11-Mar-2015.) |
LSAtoms Scalar LKer LDual | ||
Theorem | lcfrlem26 36857* | Lemma for lcfr 36874. Special case of lcfrlem36 36867 when is zero. (Contributed by NM, 11-Mar-2015.) |
LSAtoms Scalar LKer LDual | ||
Theorem | lcfrlem27 36858* | Lemma for lcfr 36874. Special case of lcfrlem37 36868 when is zero. (Contributed by NM, 11-Mar-2015.) |
LSAtoms Scalar LKer LDual LFnl | ||
Theorem | lcfrlem28 36859* | Lemma for lcfr 36874. TODO: This can be a hypothesis since the zero version of needs it. (Contributed by NM, 9-Mar-2015.) |
LSAtoms Scalar LKer LDual | ||
Theorem | lcfrlem29 36860* | Lemma for lcfr 36874. (Contributed by NM, 9-Mar-2015.) |
LSAtoms Scalar LKer LDual | ||
Theorem | lcfrlem30 36861* | Lemma for lcfr 36874. (Contributed by NM, 6-Mar-2015.) |
LSAtoms Scalar LKer LDual LFnl | ||
Theorem | lcfrlem31 36862* | Lemma for lcfr 36874. (Contributed by NM, 10-Mar-2015.) |
LSAtoms Scalar LKer LDual | ||
Theorem | lcfrlem32 36863* | Lemma for lcfr 36874. (Contributed by NM, 10-Mar-2015.) |
LSAtoms Scalar LKer LDual | ||
Theorem | lcfrlem33 36864* | Lemma for lcfr 36874. (Contributed by NM, 10-Mar-2015.) |
LSAtoms Scalar LKer LDual | ||
Theorem | lcfrlem34 36865* | Lemma for lcfr 36874. (Contributed by NM, 10-Mar-2015.) |
LSAtoms Scalar LKer LDual | ||
Theorem | lcfrlem35 36866* | Lemma for lcfr 36874. (Contributed by NM, 2-Mar-2015.) |
LSAtoms Scalar LKer LDual | ||
Theorem | lcfrlem36 36867* | Lemma for lcfr 36874. (Contributed by NM, 6-Mar-2015.) |
LSAtoms Scalar LKer LDual | ||
Theorem | lcfrlem37 36868* | Lemma for lcfr 36874. (Contributed by NM, 8-Mar-2015.) |
LSAtoms Scalar LKer LDual LFnl | ||
Theorem | lcfrlem38 36869* | Lemma for lcfr 36874. Combine lcfrlem27 36858 and lcfrlem37 36868. (Contributed by NM, 11-Mar-2015.) |
LFnl LKer LDual LFnl Scalar | ||
Theorem | lcfrlem39 36870* | Lemma for lcfr 36874. Eliminate . (Contributed by NM, 11-Mar-2015.) |
LFnl LKer LDual LFnl | ||
Theorem | lcfrlem40 36871* | Lemma for lcfr 36874. Eliminate and . (Contributed by NM, 11-Mar-2015.) |
LFnl LKer LDual LFnl | ||
Theorem | lcfrlem41 36872* | Lemma for lcfr 36874. Eliminate span condition. (Contributed by NM, 11-Mar-2015.) |
LFnl LKer LDual LFnl | ||
Theorem | lcfrlem42 36873* | Lemma for lcfr 36874. Eliminate nonzero condition. (Contributed by NM, 11-Mar-2015.) |
LFnl LKer LDual LFnl | ||
Theorem | lcfr 36874* | Reconstruction of a subspace from a dual subspace of functionals with closed kernels. Our proof was suggested by Mario Carneiro, 20-Feb-2015. (Contributed by NM, 5-Mar-2015.) |
LFnl LKer LDual | ||
Syntax | clcd 36875 | Extend class notation with vector space of functionals with closed kernels. |
LCDual | ||
Definition | df-lcdual 36876* | Dual vector space of functionals with closed kernels. Note: we could also define this directly without mapd by using mapdrn 36938. TODO: see if it makes sense to go back and replace some of the LDual stuff with this. TODO: We could simplify df-mapd 36914 using LCDual. (Contributed by NM, 13-Mar-2015.) |
LCDual LDual ↾s LFnl LKer LKer | ||
Theorem | lcdfval 36877* | Dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015.) |
LCDual LDual ↾s LFnl LKer LKer | ||
Theorem | lcdval 36878* | Dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015.) |
LCDual LFnl LKer LDual ↾s | ||
Theorem | lcdval2 36879* | Dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015.) |
LCDual LFnl LKer LDual ↾s | ||
Theorem | lcdlvec 36880 | The dual vector space of functionals with closed kernels is a left vector space. (Contributed by NM, 14-Mar-2015.) |
LCDual | ||
Theorem | lcdlmod 36881 | The dual vector space of functionals with closed kernels is a left module. (Contributed by NM, 13-Mar-2015.) |
LCDual | ||
Theorem | lcdvbase 36882* | Vector base set of a dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015.) |
LCDual LFnl LKer | ||
Theorem | lcdvbasess 36883 | The vector base set of the closed kernel dual space is a set of functionals. (Contributed by NM, 15-Mar-2015.) |
LCDual LFnl | ||
Theorem | lcdvbaselfl 36884 | A vector in the base set of the closed kernel dual space is a functional. (Contributed by NM, 28-Mar-2015.) |
LCDual LFnl | ||
Theorem | lcdvbasecl 36885 | Closure of the value of a vector (functional) in the closed kernel dual space. (Contributed by NM, 28-Mar-2015.) |
Scalar LCDual | ||
Theorem | lcdvadd 36886 | Vector addition for the closed kernel vector space dual. (Contributed by NM, 10-Jun-2015.) |
LDual LCDual | ||
Theorem | lcdvaddval 36887 | The value of the value of vector addition in the closed kernel vector space dual. (Contributed by NM, 10-Jun-2015.) |
Scalar LCDual | ||
Theorem | lcdsca 36888 | The ring of scalars of the closed kernel dual space. (Contributed by NM, 16-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.) |
Scalar oppr LCDual Scalar | ||
Theorem | lcdsbase 36889 | Base set of scalar ring for the closed kernel dual of a vector space. (Contributed by NM, 18-Mar-2015.) |
Scalar LCDual Scalar | ||
Theorem | lcdsadd 36890 | Scalar addition for the closed kernel vector space dual. (Contributed by NM, 6-Jun-2015.) |
Scalar LCDual Scalar | ||
Theorem | lcdsmul 36891 | Scalar multiplication for the closed kernel vector space dual. (Contributed by NM, 20-Mar-2015.) |
Scalar LCDual Scalar | ||
Theorem | lcdvs 36892 | Scalar product for the closed kernel vector space dual. (Contributed by NM, 28-Mar-2015.) |
LDual LCDual | ||
Theorem | lcdvsval 36893 | Value of scalar product operation value for the closed kernel vector space dual. (Contributed by NM, 28-Mar-2015.) |
Scalar LCDual | ||
Theorem | lcdvscl 36894 | The scalar product operation value is a functional. (Contributed by NM, 20-Mar-2015.) |
Scalar LCDual | ||
Theorem | lcdlssvscl 36895 | Closure of scalar product in a closed kernel dual vector space. (Contributed by NM, 20-Mar-2015.) |
Scalar LCDual | ||
Theorem | lcdvsass 36896 | Associative law for scalar product in a closed kernel dual vector space. (Contributed by NM, 20-Mar-2015.) |
Scalar LCDual | ||
Theorem | lcd0 36897 | The zero scalar of the closed kernel dual of a vector space. (Contributed by NM, 20-Mar-2015.) |
Scalar LCDual Scalar | ||
Theorem | lcd1 36898 | The unit scalar of the closed kernel dual of a vector space. (Contributed by NM, 20-Mar-2015.) |
Scalar LCDual Scalar | ||
Theorem | lcdneg 36899 | The unit scalar of the closed kernel dual of a vector space. (Contributed by NM, 11-Jun-2015.) |
Scalar LCDual Scalar | ||
Theorem | lcd0v 36900 | The zero functional in the set of functionals with closed kernels. (Contributed by NM, 20-Mar-2015.) |
Scalar LCDual |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |