Home Metamath Proof ExplorerTheorem List (p. 324 of 328) < Previous  Next > Browser slow? Try the Unicode version.

 Color key: Metamath Proof Explorer (1-21514) Hilbert Space Explorer (21515-23037) Users' Mathboxes (23038-32776)

Theorem List for Metamath Proof Explorer - 32301-32400   *Has distinct variable group(s)
TypeLabelDescription
Statement

TheoremlpolpolsatN 32301 Property of a polarity. (Contributed by NM, 26-Nov-2014.) (New usage is discouraged.)
LSAtoms       LPol

TheoremdochpolN 32302 The subspace orthocomplement for the vector space is a polarity. (Contributed by NM, 27-Dec-2014.) (New usage is discouraged.)
LPol

Theoremlcfl1lem 32303* Property of a functional with a closed kernel. (Contributed by NM, 28-Dec-2014.)

Theoremlcfl1 32304* Property of a functional with a closed kernel. (Contributed by NM, 31-Dec-2014.)

Theoremlcfl2 32305* Property of a functional with a closed kernel. (Contributed by NM, 1-Jan-2015.)
LFnl       LKer

Theoremlcfl3 32306* Property of a functional with a closed kernel. (Contributed by NM, 1-Jan-2015.)
LSAtoms       LFnl       LKer

Theoremlcfl4N 32307* Property of a functional with a closed kernel. (Contributed by NM, 1-Jan-2015.) (New usage is discouraged.)
LSHyp       LFnl       LKer

Theoremlcfl5 32308* Property of a functional with a closed kernel. (Contributed by NM, 1-Jan-2015.)
LFnl       LKer

Theoremlcfl5a 32309 Property of a functional with a closed kernel. TODO: Make lcfl5 32308 etc. obsolete and rewrite w/out hypothesis? (Contributed by NM, 29-Jan-2015.)
LFnl       LKer

Theoremlcfl6lem 32310* Lemma for lcfl6 32312. A functional (whose kernel is closed by dochsnkr 32284) 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

Theoremlcfl7lem 32311* Lemma for lcfl7N 32313. If two functionals and are equal, they are determined by the same vector. (Contributed by NM, 4-Jan-2015.)
Scalar                     LFnl       LKer

Theoremlcfl6 32312* Property of a functional with a closed kernel. Note that means the functional is zero by lkr0f 29906. (Contributed by NM, 3-Jan-2015.)
Scalar                     LFnl       LKer

Theoremlcfl7N 32313* 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 29906. (Contributed by NM, 4-Jan-2015.) (New usage is discouraged.)
Scalar                     LFnl       LKer

Theoremlcfl8 32314* Property of a functional with a closed kernel. (Contributed by NM, 17-Jan-2015.)
LFnl       LKer

Theoremlcfl8a 32315* Property of a functional with a closed kernel. (Contributed by NM, 17-Jan-2015.)
LFnl       LKer

Theoremlcfl8b 32316* Property of a nonzero functional with a closed kernel. (Contributed by NM, 4-Feb-2015.)
LFnl       LKer       LDual

Theoremlcfl9a 32317 Property implying that a functional has a closed kernel. (Contributed by NM, 16-Feb-2015.)
LFnl       LKer

Theoremlclkrlem1 32318* The set of functionals having closed kernels is closed under scalar product. (Contributed by NM, 28-Dec-2014.)
LFnl       LKer       LDual       Scalar

Theoremlclkrlem2a 32319 Lemma for lclkr 32345. Use lshpat 29868 to show that the intersection of a hyperplane with a noncomparable sum of atoms is an atom. (Contributed by NM, 16-Jan-2015.)
LSAtoms

Theoremlclkrlem2b 32320 Lemma for lclkr 32345. (Contributed by NM, 17-Jan-2015.)
LSAtoms

Theoremlclkrlem2c 32321 Lemma for lclkr 32345. (Contributed by NM, 16-Jan-2015.)
LSAtoms                                                 LSHyp

Theoremlclkrlem2d 32322 Lemma for lclkr 32345. (Contributed by NM, 16-Jan-2015.)
LSAtoms

Theoremlclkrlem2e 32323 Lemma for lclkr 32345. 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

Theoremlclkrlem2f 32324 Lemma for lclkr 32345. Construct a closed hyperplane under the kernel of the sum. (Contributed by NM, 16-Jan-2015.)
Scalar                                   LFnl       LSHyp       LKer       LDual

Theoremlclkrlem2g 32325 Lemma for lclkr 32345. Comparable hyperplanes are equal, so the kernel of the sum is closed. (Contributed by NM, 16-Jan-2015.)
Scalar                                   LFnl       LSHyp       LKer       LDual

Theoremlclkrlem2h 32326 Lemma for lclkr 32345. Eliminate the hypothesis. (Contributed by NM, 16-Jan-2015.)
Scalar                                   LFnl       LSHyp       LKer       LDual

Theoremlclkrlem2i 32327 Lemma for lclkr 32345. Eliminate the hypothesis. (Contributed by NM, 17-Jan-2015.)
Scalar                                   LFnl       LSHyp       LKer       LDual

Theoremlclkrlem2j 32328 Lemma for lclkr 32345. Kernel closure when is zero. (Contributed by NM, 18-Jan-2015.)
Scalar                                   LFnl       LSHyp       LKer       LDual

Theoremlclkrlem2k 32329 Lemma for lclkr 32345. Kernel closure when is zero. (Contributed by NM, 18-Jan-2015.)
Scalar                                   LFnl       LSHyp       LKer       LDual

Theoremlclkrlem2l 32330 Lemma for lclkr 32345. Eliminate the , hypotheses. (Contributed by NM, 18-Jan-2015.)
Scalar                                   LFnl       LSHyp       LKer       LDual

Theoremlclkrlem2m 32331 Lemma for lclkr 32345. 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

Theoremlclkrlem2n 32332 Lemma for lclkr 32345. (Contributed by NM, 12-Jan-2015.)
Scalar                                   LFnl       LDual                                                 LKer

Theoremlclkrlem2o 32333 Lemma for lclkr 32345. 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

Theoremlclkrlem2p 32334 Lemma for lclkr 32345. When is zero, and must colinear, so their orthocomplements must be comparable. (Contributed by NM, 17-Jan-2015.)
Scalar                                   LFnl       LDual                                                 LKer

Theoremlclkrlem2q 32335 Lemma for lclkr 32345. The sum has a closed kernel when is nonzero. (Contributed by NM, 18-Jan-2015.)
Scalar                                   LFnl       LDual                                                 LKer

Theoremlclkrlem2r 32336 Lemma for lclkr 32345. 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

Theoremlclkrlem2s 32337 Lemma for lclkr 32345. Thus, the sum has a closed kernel when is zero. (Contributed by NM, 18-Jan-2015.)
Scalar                                   LFnl       LDual                                                 LKer

Theoremlclkrlem2t 32338 Lemma for lclkr 32345. We eliminate all hypotheses with here. (Contributed by NM, 18-Jan-2015.)
Scalar                                   LFnl       LDual                                                 LKer

Theoremlclkrlem2u 32339 Lemma for lclkr 32345. lclkrlem2t 32338 with and swapped. (Contributed by NM, 18-Jan-2015.)
Scalar                                   LFnl       LDual                                                 LKer

Theoremlclkrlem2v 32340 Lemma for lclkr 32345. When the hypotheses of lclkrlem2u 32339 and lclkrlem2u 32339 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 32280, which requires the orthomodular law dihoml4 32189 (Lemma 3.3 of [Holland95] p. 214). (Contributed by NM, 16-Jan-2015.)
Scalar                                   LFnl       LDual                                                 LKer

Theoremlclkrlem2w 32341 Lemma for lclkr 32345. This is the same as lclkrlem2u 32339 and lclkrlem2u 32339 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

Theoremlclkrlem2x 32342 Lemma for lclkr 32345. Eliminate by cases the hypotheses of lclkrlem2u 32339, lclkrlem2u 32339 and lclkrlem2w 32341. (Contributed by NM, 18-Jan-2015.)
LKer                                   LFnl       LDual

Theoremlclkrlem2y 32343 Lemma for lclkr 32345. 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

Theoremlclkrlem2 32344* The set of functionals having closed kernels is closed under vector (functional) addition. Lemmas lclkrlem2a 32319 through lclkrlem2y 32343 are used for the proof. Here we express lclkrlem2y 32343 in terms of membership in the set of functionals with closed kernels. (Contributed by NM, 18-Jan-2015.)
LFnl       LKer       LDual

Theoremlclkr 32345* 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

Theoremlcfls1lem 32346* Property of a functional with a closed kernel. (Contributed by NM, 27-Jan-2015.)

Theoremlcfls1N 32347* Property of a functional with a closed kernel. (Contributed by NM, 27-Jan-2015.) (New usage is discouraged.)

Theoremlcfls1c 32348* Property of a functional with a closed kernel. (Contributed by NM, 28-Jan-2015.)

Theoremlclkrslem1 32349* 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

Theoremlclkrslem2 32350* 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

Theoremlclkrs 32351* 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 32345 proof. Do we achieve overall shortening by breaking them out as subtheorems? Or make lclkr 32345 a special case of this? (Contributed by NM, 29-Jan-2015.)
LFnl       LKer       LDual

Theoremlclkrs2 32352* 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 32440. (Contributed by NM, 12-Mar-2015.)
LFnl       LKer       LDual

TheoremlcfrvalsnN 32353* Reconstruction from the dual space span of a singleton. (Contributed by NM, 19-Feb-2015.) (New usage is discouraged.)
LFnl       LKer       LDual

Theoremlcfrlem1 32354 Lemma for lcfr 32397. Note that is z in Mario's notes. (Contributed by NM, 27-Feb-2015.)
Scalar                            LFnl       LDual

Theoremlcfrlem2 32355 Lemma for lcfr 32397. (Contributed by NM, 27-Feb-2015.)
Scalar                            LFnl       LDual                                                               LKer

Theoremlcfrlem3 32356 Lemma for lcfr 32397. (Contributed by NM, 27-Feb-2015.)
Scalar                            LFnl       LDual                                                               LKer

Theoremlcfrlem4 32357* Lemma for lcfr 32397. (Contributed by NM, 10-Mar-2015.)
LKer       LDual

Theoremlcfrlem5 32358* Lemma for lcfr 32397. 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

Theoremlcfrlem6 32359* Lemma for lcfr 32397. 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

Theoremlcfrlem7 32360* Lemma for lcfr 32397. Closure of vector sum when one vector is zero. TODO: share hypotheses with others. (Contributed by NM, 11-Mar-2015.)
LKer       LDual

Theoremlcfrlem8 32361* Lemma for lcf1o 32363 and lcfr 32397. (Contributed by NM, 21-Feb-2015.)
Scalar                     LFnl       LKer       LDual

Theoremlcfrlem9 32362* Lemma for lcf1o 32363. (This part has undesirable \$d's on and that we remove in lcf1o 32363.) 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

Theoremlcf1o 32363* 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

Theoremlcfrlem10 32364* Lemma for lcfr 32397. (Contributed by NM, 23-Feb-2015.)
Scalar                     LFnl       LKer       LDual

Theoremlcfrlem11 32365* Lemma for lcfr 32397. (Contributed by NM, 23-Feb-2015.)
Scalar                     LFnl       LKer       LDual

Theoremlcfrlem12N 32366* Lemma for lcfr 32397. (Contributed by NM, 23-Feb-2015.) (New usage is discouraged.)
Scalar                     LFnl       LKer       LDual

Theoremlcfrlem13 32367* Lemma for lcfr 32397. (Contributed by NM, 8-Mar-2015.)
Scalar                     LFnl       LKer       LDual

Theoremlcfrlem14 32368* Lemma for lcfr 32397. (Contributed by NM, 10-Mar-2015.)
Scalar                     LFnl       LKer       LDual

Theoremlcfrlem15 32369* Lemma for lcfr 32397. (Contributed by NM, 9-Mar-2015.)
Scalar                     LFnl       LKer       LDual

Theoremlcfrlem16 32370* Lemma for lcfr 32397. (Contributed by NM, 8-Mar-2015.)
Scalar                     LFnl       LKer       LDual

Theoremlcfrlem17 32371 Lemma for lcfr 32397. Condition needed more than once. (Contributed by NM, 11-Mar-2015.)
LSAtoms

Theoremlcfrlem18 32372 Lemma for lcfr 32397. (Contributed by NM, 24-Feb-2015.)
LSAtoms

Theoremlcfrlem19 32373 Lemma for lcfr 32397. (Contributed by NM, 11-Mar-2015.)
LSAtoms

Theoremlcfrlem20 32374 Lemma for lcfr 32397. (Contributed by NM, 11-Mar-2015.)
LSAtoms

Theoremlcfrlem21 32375 Lemma for lcfr 32397. (Contributed by NM, 11-Mar-2015.)
LSAtoms

Theoremlcfrlem22 32376 Lemma for lcfr 32397. (Contributed by NM, 24-Feb-2015.)
LSAtoms

Theoremlcfrlem23 32377 Lemma for lcfr 32397. 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