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

 Color key: Metamath Proof Explorer (1-22374) Hilbert Space Explorer (22375-23897) Users' Mathboxes (23898-32447)

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

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

Theoremlclkrlem2m 32002 Lemma for lclkr 32016. 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 32003 Lemma for lclkr 32016. (Contributed by NM, 12-Jan-2015.)
Scalar                                   LFnl       LDual                                                 LKer

Theoremlclkrlem2o 32004 Lemma for lclkr 32016. 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 32005 Lemma for lclkr 32016. When is zero, and must colinear, so their orthocomplements must be comparable. (Contributed by NM, 17-Jan-2015.)
Scalar                                   LFnl       LDual                                                 LKer

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

Theoremlclkrlem2r 32007 Lemma for lclkr 32016. 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 32008 Lemma for lclkr 32016. Thus, the sum has a closed kernel when is zero. (Contributed by NM, 18-Jan-2015.)
Scalar                                   LFnl       LDual                                                 LKer

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

Theoremlclkrlem2u 32010 Lemma for lclkr 32016. lclkrlem2t 32009 with and swapped. (Contributed by NM, 18-Jan-2015.)
Scalar                                   LFnl       LDual                                                 LKer

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

Theoremlclkrlem2w 32012 Lemma for lclkr 32016. This is the same as lclkrlem2u 32010 and lclkrlem2u 32010 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 32013 Lemma for lclkr 32016. Eliminate by cases the hypotheses of lclkrlem2u 32010, lclkrlem2u 32010 and lclkrlem2w 32012. (Contributed by NM, 18-Jan-2015.)
LKer                                   LFnl       LDual

Theoremlclkrlem2y 32014 Lemma for lclkr 32016. 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 32015* The set of functionals having closed kernels is closed under vector (functional) addition. Lemmas lclkrlem2a 31990 through lclkrlem2y 32014 are used for the proof. Here we express lclkrlem2y 32014 in terms of membership in the set of functionals with closed kernels. (Contributed by NM, 18-Jan-2015.)
LFnl       LKer       LDual

Theoremlclkr 32016* 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 32017* Property of a functional with a closed kernel. (Contributed by NM, 27-Jan-2015.)

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

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

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

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

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

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

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

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

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

Theoremlcfrlem5 32029* Lemma for lcfr 32068. 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 32030* Lemma for lcfr 32068. 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 32031* Lemma for lcfr 32068. Closure of vector sum when one vector is zero. TODO: share hypotheses with others. (Contributed by NM, 11-Mar-2015.)
LKer       LDual

Theoremlcfrlem8 32032* Lemma for lcf1o 32034 and lcfr 32068. (Contributed by NM, 21-Feb-2015.)
Scalar                     LFnl       LKer       LDual

Theoremlcfrlem9 32033* Lemma for lcf1o 32034. (This part has undesirable \$d's on and that we remove in lcf1o 32034.) 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 32034* 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 32035* Lemma for lcfr 32068. (Contributed by NM, 23-Feb-2015.)
Scalar                     LFnl       LKer       LDual

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

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

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

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

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

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

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

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

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

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

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

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

Theoremlcfrlem23 32048 Lemma for lcfr 32068. 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

Theoremlcfrlem24 32049* Lemma for lcfr 32068. (Contributed by NM, 24-Feb-2015.)
LSAtoms                                                 Scalar                                   LKer

Theoremlcfrlem25 32050* Lemma for lcfr 32068. Special case of lcfrlem35 32060 when is zero. (Contributed by NM, 11-Mar-2015.)
LSAtoms                                                 Scalar                                   LKer       LDual

Theoremlcfrlem26 32051* Lemma for lcfr 32068. Special case of lcfrlem36 32061 when is zero. (Contributed by NM, 11-Mar-2015.)
LSAtoms                                                 Scalar                                   LKer       LDual

Theoremlcfrlem27 32052* Lemma for lcfr 32068. Special case of lcfrlem37 32062 when is zero. (Contributed by NM, 11-Mar-2015.)
LSAtoms                                                 Scalar                                   LKer       LDual                            LFnl

Theoremlcfrlem28 32053* Lemma for lcfr 32068. TODO: This can be a hypothesis since the zero version of needs it. (Contributed by NM, 9-Mar-2015.)
LSAtoms                                                 Scalar                                   LKer       LDual

Theoremlcfrlem29 32054* Lemma for lcfr 32068. (Contributed by NM, 9-Mar-2015.)
LSAtoms                                                 Scalar                                   LKer       LDual

Theoremlcfrlem30 32055* Lemma for lcfr 32068. (Contributed by NM, 6-Mar-2015.)
LSAtoms                                                 Scalar                                   LKer       LDual                                   LFnl

Theoremlcfrlem31 32056* Lemma for lcfr 32068. (Contributed by NM, 10-Mar-2015.)
LSAtoms                                                 Scalar                                   LKer       LDual

Theoremlcfrlem32 32057* Lemma for lcfr 32068. (Contributed by NM, 10-Mar-2015.)
LSAtoms                                                 Scalar                                   LKer       LDual

Theoremlcfrlem33 32058* Lemma for lcfr 32068. (Contributed by NM, 10-Mar-2015.)
LSAtoms                                                 Scalar                                   LKer       LDual

Theoremlcfrlem34 32059* Lemma for lcfr 32068. (Contributed by NM, 10-Mar-2015.)
LSAtoms                                                 Scalar                                   LKer       LDual

Theoremlcfrlem35 32060* Lemma for lcfr 32068. (Contributed by NM, 2-Mar-2015.)
LSAtoms                                                 Scalar                                   LKer       LDual

Theoremlcfrlem36 32061* Lemma for lcfr 32068. (Contributed by NM, 6-Mar-2015.)
LSAtoms                                                 Scalar                                   LKer       LDual

Theoremlcfrlem37 32062* Lemma for lcfr 32068. (Contributed by NM, 8-Mar-2015.)
LSAtoms                                                 Scalar                                   LKer       LDual                                          LFnl

Theoremlcfrlem38 32063* Lemma for lcfr 32068. Combine lcfrlem27 32052 and lcfrlem37 32062. (Contributed by NM, 11-Mar-2015.)
LFnl       LKer       LDual              LFnl                                                                                                                        Scalar

Theoremlcfrlem39 32064* Lemma for lcfr 32068. Eliminate . (Contributed by NM, 11-Mar-2015.)
LFnl       LKer       LDual              LFnl