Home Metamath Proof ExplorerTheorem List (p. 322 of 325) < 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-22374) Hilbert Space Explorer (22375-23897) Users' Mathboxes (23898-32447)

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

Theoremlcdvsubval 32101 The value of the value of vector addition in the closed kernel vector space dual. (Contributed by NM, 11-Jun-2015.)
Scalar              LCDual

Theoremlcdlss 32102* Subspaces of a dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015.)
LCDual                     LFnl       LKer       LDual

Theoremlcdlss2N 32103 Subspaces of a dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.)
LCDual                            LDual

Theoremlcdlsp 32104 Span in the set of functionals with closed kernels. (Contributed by NM, 28-Mar-2015.)
LDual              LCDual

TheoremlcdlkreqN 32105 Colinear functionals have equal kernels. (Contributed by NM, 28-Mar-2015.) (New usage is discouraged.)
LKer       LCDual

Theoremlcdlkreq2N 32106 Colinear functionals have equal kernels. (Contributed by NM, 28-Mar-2015.) (New usage is discouraged.)
Scalar                     LKer       LCDual

Syntaxcmpd 32107 Extend class notation with projectivity from subspaces of vector space H to subspaces of functionals with closed kernels.
mapd

Definitiondf-mapd 32108* Extend class notation with a one-to-one onto (mapd1o 32131), order-preserving (mapdord 32121) map, called a projectivity (definition of projectivity in [Baer] p. 40), from subspaces of vector space H to those subspaces of the dual space having functionals with closed kernels. (Contributed by NM, 25-Jan-2015.)
mapd LFnl LKer LKer LKer

Theoremmapdffval 32109* Projectivity from vector space H to dual space. (Contributed by NM, 25-Jan-2015.)
mapd LFnl LKer LKer LKer

Theoremmapdfval 32110* Projectivity from vector space H to dual space. (Contributed by NM, 25-Jan-2015.)
LFnl       LKer              mapd

Theoremmapdval 32111* Value of projectivity from vector space H to dual space. (Contributed by NM, 27-Jan-2015.)
LFnl       LKer              mapd

Theoremmapdvalc 32112* Value of projectivity from vector space H to dual space. (Contributed by NM, 27-Jan-2015.)
LFnl       LKer              mapd

Theoremmapdval2N 32113* Value of projectivity from vector space H to dual space. (Contributed by NM, 31-Jan-2015.) (New usage is discouraged.)
LFnl       LKer              mapd

Theoremmapdval3N 32114* Value of projectivity from vector space H to dual space. (Contributed by NM, 31-Jan-2015.) (New usage is discouraged.)
LFnl       LKer              mapd

Theoremmapdval4N 32115* Value of projectivity from vector space H to dual space. TODO: 1. This is shorter than others - make it the official def? (but is not as obvious that it is ) 2. The unneeded direction of lcfl8a 31986 has awkward - add another thm with only one direction of it? 3. Swap and ? (Contributed by NM, 31-Jan-2015.) (New usage is discouraged.)
LFnl       LKer              mapd

Theoremmapdval5N 32116* Value of projectivity from vector space H to dual space. (Contributed by NM, 31-Jan-2015.) (New usage is discouraged.)
LFnl       LKer              mapd

Theoremmapdordlem1a 32117* Lemma for mapdord 32121. (Contributed by NM, 27-Jan-2015.)
LSHyp       LFnl       LKer

Theoremmapdordlem1bN 32118* Lemma for mapdord 32121. (Contributed by NM, 27-Jan-2015.) (New usage is discouraged.)

Theoremmapdordlem1 32119* Lemma for mapdord 32121. (Contributed by NM, 27-Jan-2015.)

Theoremmapdordlem2 32120* Lemma for mapdord 32121. Ordering property of projectivity . TODO: This was proved using some hacked-up older proofs. Maybe simplify; get rid of the hypothesis. (Contributed by NM, 27-Jan-2015.)
mapd                                   LSAtoms       LFnl       LSHyp       LKer

Theoremmapdord 32121 Ordering property of the map defined by df-mapd 32108. Property (b) of [Baer] p. 40. (Contributed by NM, 27-Jan-2015.)
mapd

Theoremmapd11 32122 The map defined by df-mapd 32108 is one-to-one. Property (c) of [Baer] p. 40. (Contributed by NM, 12-Mar-2015.)
mapd

TheoremmapddlssN 32123 The mapping of a subspace of vector space H to the dual space is a subspace of the dual space. TODO: Make this obsolete, use mapdcl2 32139 instead. (Contributed by NM, 31-Jan-2015.) (New usage is discouraged.)
mapd                     LDual

Theoremmapdsn 32124* Value of the map defined by df-mapd 32108 at the span of a singleton. (Contributed by NM, 16-Feb-2015.)
mapd                            LFnl       LKer

Theoremmapdsn2 32125* Value of the map defined by df-mapd 32108 at the span of a singleton. (Contributed by NM, 16-Feb-2015.)
mapd                            LFnl       LKer

Theoremmapdsn3 32126 Value of the map defined by df-mapd 32108 at the span of a singleton. (Contributed by NM, 17-Feb-2015.)
mapd                            LFnl       LKer       LDual

Theoremmapd1dim2lem1N 32127* Value of the map defined by df-mapd 32108 at an atom. (Contributed by NM, 10-Feb-2015.) (New usage is discouraged.)
LSAtoms       LFnl       LKer              mapd

Theoremmapdrvallem2 32128* Lemma for ~? mapdrval . TODO: very long antecendents are dragged through proof in some places - see if it shortens proof to remove unused conjuncts. (Contributed by NM, 2-Feb-2015.)
mapd                     LFnl       LKer       LDual                                                        LSAtoms

Theoremmapdrvallem3 32129* Lemma for ~? mapdrval . (Contributed by NM, 2-Feb-2015.)
mapd                     LFnl       LKer       LDual                                                        LSAtoms

Theoremmapdrval 32130* Given a dual subspace (of functionals with closed kernels), reconstruct the subspace that maps to it. (Contributed by NM, 12-Mar-2015.)
mapd                     LFnl       LKer       LDual

Theoremmapd1o 32131* The map defined by df-mapd 32108 is one-to-one and onto the set of dual subspaces of functionals with closed kernels. This shows satisfies part of the definition of projectivity of [Baer] p. 40. TODO: change theorems leading to this (lcfr 32068, mapdrval 32130, lclkrs 32022, lclkr 32016,...) to use ? TODO: maybe get rid of \$d's for vs. ,. propagate to mapdrn 32132 and any others. (Contributed by NM, 12-Mar-2015.)
mapd                     LFnl       LKer       LDual

Theoremmapdrn 32132* Range of the map defined by df-mapd 32108. (Contributed by NM, 12-Mar-2015.)
mapd              LFnl       LKer       LDual

TheoremmapdunirnN 32133* Union of the range of the map defined by df-mapd 32108. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.)
mapd              LFnl       LKer

Theoremmapdrn2 32134 Range of the map defined by df-mapd 32108. TODO: this seems to be needed a lot in hdmaprnlem3eN 32344 etc. Would it be better to change df-mapd 32108 theorems to use instead of ? (Contributed by NM, 13-Mar-2015.)
mapd       LCDual

Theoremmapdcnvcl 32135 Closure of the converse of the map defined by df-mapd 32108. (Contributed by NM, 13-Mar-2015.)
mapd

Theoremmapdcl 32136 Closure the value of the map defined by df-mapd 32108. (Contributed by NM, 13-Mar-2015.)
mapd

Theoremmapdcnvid1N 32137 Converse of the value of the map defined by df-mapd 32108. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.)
mapd

Theoremmapdsord 32138 Strong ordering property of themap defined by df-mapd 32108. (Contributed by NM, 13-Mar-2015.)
mapd

Theoremmapdcl2 32139 The mapping of a subspace of vector space H is a subspace in the dual space of functionals with closed kernels. (Contributed by NM, 31-Jan-2015.)
mapd                     LCDual

Theoremmapdcnvid2 32140 Value of the converse of the map defined by df-mapd 32108. (Contributed by NM, 13-Mar-2015.)
mapd

TheoremmapdcnvordN 32141 Ordering property of the converse of the map defined by df-mapd 32108. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.)
mapd

Theoremmapdcnv11N 32142 The converse of the map defined by df-mapd 32108 is one-to-one. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.)
mapd

Theoremmapdcv 32143 Covering property of the converse of the map defined by df-mapd 32108. (Contributed by NM, 14-Mar-2015.)
mapd                     L        LCDual       L

Theoremmapdincl 32144 Closure of dual subspace intersection for the map defined by df-mapd 32108. (Contributed by NM, 12-Apr-2015.)
mapd              LCDual

Theoremmapdin 32145 Subspace intersection is preserved by the map defined by df-mapd 32108. Part of property (e) in [Baer] p. 40. (Contributed by NM, 12-Apr-2015.)
mapd

Theoremmapdlsmcl 32146 Closure of dual subspace sum for the map defined by df-mapd 32108. (Contributed by NM, 13-Mar-2015.)
mapd              LCDual

Theoremmapdlsm 32147 Subspace sum is preserved by the map defined by df-mapd 32108. Part of property (e) in [Baer] p. 40. (Contributed by NM, 13-Mar-2015.)
mapd                            LCDual

Theoremmapd0 32148 Projectivity map of the zero subspace. Part of property (f) in [Baer] p. 40. TODO: does proof need to be this long for this simple fact? (Contributed by NM, 15-Mar-2015.)
mapd                     LCDual

TheoremmapdcnvatN 32149 Atoms are preserved by the map defined by df-mapd 32108. (Contributed by NM, 29-May-2015.) (New usage is discouraged.)
mapd              LSAtoms       LCDual       LSAtoms

Theoremmapdat 32150 Atoms are preserved by the map defined by df-mapd 32108. Property (g) in [Baer] p. 41. (Contributed by NM, 14-Mar-2015.)
mapd              LSAtoms       LCDual       LSAtoms

Theoremmapdspex 32151* The map of a span equals the dual span of some vector (functional). (Contributed by NM, 15-Mar-2015.)
mapd                            LCDual

Theoremmapdn0 32152 Transfer non-zero property from domain to range of projectivity mapd. (Contributed by NM, 12-Apr-2015.)
mapd                            LCDual

Theoremmapdncol 32153 Transfer non-colinearity from domain to range of projectivity mapd. (Contributed by NM, 11-Apr-2015.)
mapd                            LCDual

Theoremmapdindp 32154 Transfer (part of) vector independence condition from domain to range of projectivity mapd. (Contributed by NM, 11-Apr-2015.)
mapd                            LCDual

Theoremmapdpglem1 32155 Lemma for mapdpg 32189. Baer p. 44, last line: "(F(x-y))* =< (Fx)*+(Fy)*." (Contributed by NM, 15-Mar-2015.)
mapd                                   LCDual

Theoremmapdpglem2 32156* Lemma for mapdpg 32189. Baer p. 45, lines 1 and 2: "we have (F(x-y))* = Gt where t necessarily belongs to (Fx)*+(Fy)*." (We scope \$d locally to avoid clashes with later substitutions into .) (Contributed by NM, 15-Mar-2015.)
mapd                                   LCDual

Theoremmapdpglem2a 32157* Lemma for mapdpg 32189. (Contributed by NM, 20-Mar-2015.)
mapd                                   LCDual

Theoremmapdpglem3 32158* Lemma for mapdpg 32189. Baer p. 45, line 3: "infer...the existence of a number g in G and of an element z in (Fy)* such that t = gx'-z." (We scope \$d locally to avoid clashes with later substitutions into .) (Contributed by NM, 18-Mar-2015.)
mapd                                   LCDual                                                        Scalar

Theoremmapdpglem4N 32159* Lemma for mapdpg 32189. (Contributed by NM, 20-Mar-2015.) (New usage is discouraged.)
mapd                                   LCDual                                                        Scalar

Theoremmapdpglem5N 32160* Lemma for mapdpg 32189. (Contributed by NM, 20-Mar-2015.) (New usage is discouraged.)
mapd                                   LCDual                                                        Scalar

Theoremmapdpglem6 32161* Lemma for mapdpg 32189. Baer p. 45, line 4: "If g were 0, then t would be in (Fy)*..." (Contributed by NM, 18-Mar-2015.)
mapd                                   LCDual                                                        Scalar

Theoremmapdpglem8 32162* Lemma for mapdpg 32189. Baer p. 45, line 4: "...so that (F(x-y))* =< (Fy)*. This would imply that F(x-y) =< F(y)..." (Contributed by NM, 20-Mar-2015.)
mapd                                   LCDual                                                        Scalar

Theoremmapdpglem9 32163* Lemma for mapdpg 32189. Baer p. 45, line 4: "...so that x would consequently belong to Fy." (Contributed by NM, 20-Mar-2015.)
mapd                                   LCDual                                                        Scalar

Theoremmapdpglem10 32164* Lemma for mapdpg 32189. Baer p. 45, line 6: "Hence Fx=Fy, an impossibility." (Contributed by NM, 20-Mar-2015.)
mapd                                   LCDual                                                        Scalar

Theoremmapdpglem11 32165* Lemma for mapdpg 32189. (Contributed by NM, 20-Mar-2015.)
mapd                                   LCDual                                                        Scalar

Theoremmapdpglem12 32166* Lemma for mapdpg 32189. TODO: Can some commonality with mapdpglem6 32161 through mapdpglem11 32165 be exploited? Also, some consolidation of small lemmas here could be done. (Contributed by NM, 18-Mar-2015.)
mapd                                   LCDual                                                        Scalar

Theoremmapdpglem13 32167* Lemma for mapdpg 32189. (Contributed by NM, 20-Mar-2015.)
mapd                                   LCDual                                                        Scalar

Theoremmapdpglem14 32168* Lemma for mapdpg 32189. (Contributed by NM, 20-Mar-2015.)
mapd                                   LCDual                                                        Scalar

Theoremmapdpglem15 32169* Lemma for mapdpg 32189. (Contributed by NM, 20-Mar-2015.)
mapd                                   LCDual                                                        Scalar

Theoremmapdpglem16 32170* Lemma for mapdpg 32189. Baer p. 45, line 7: "Likewise we see that z =/= 0." (Contributed by NM, 20-Mar-2015.)
mapd                                   LCDual                                                        Scalar

Theoremmapdpglem17N 32171* Lemma for mapdpg 32189. Baer p. 45, line 7: "Hence we may form y' = g^-1 z." (Contributed by NM, 20-Mar-2015.) (New usage is discouraged.)
mapd                                   LCDual                                                        Scalar

Theoremmapdpglem18 32172* Lemma for mapdpg 32189. Baer p. 45, line 7: "Then y =/= 0..." (Contributed by NM, 20-Mar-2015.)
mapd                                   LCDual                                                        Scalar

Theoremmapdpglem19 32173* Lemma for mapdpg 32189. Baer p. 45, line 8: "...is in (Fy)*..." (Contributed by NM, 20-Mar-2015.)
mapd                                   LCDual                                                        Scalar

Theoremmapdpglem20 32174* Lemma for mapdpg 32189. Baer p. 45, line 8: "...so that (Fy)*=Gy'." (Contributed by NM, 20-Mar-2015.)
mapd                                   LCDual                                                        Scalar

Theoremmapdpglem21 32175* Lemma for mapdpg 32189. (Contributed by NM, 20-Mar-2015.)
mapd                                   LCDual                                                        Scalar

Theoremmapdpglem22 32176* Lemma for mapdpg 32189. Baer p. 45, line 9: "(F(x-y))* = ... = G(x'-y')." (Contributed by NM, 20-Mar-2015.)
mapd                                   LCDual                                                        Scalar

Theoremmapdpglem23 32177* Lemma for mapdpg 32189. Baer p. 45, line 10: "and so y' meets all our requirements." Our is Baer's y'. (Contributed by NM, 20-Mar-2015.)
mapd                                   LCDual                                                        Scalar

Theoremmapdpglem30a 32178 Lemma for mapdpg 32189. (Contributed by NM, 22-Mar-2015.)
mapd                                          LCDual

Theoremmapdpglem30b 32179 Lemma for mapdpg 32189. (Contributed by NM, 22-Mar-2015.)
mapd                                          LCDual

Theoremmapdpglem25 32180 Lemma for mapdpg 32189. Baer p. 45 line 12: "Then we have Gy' = Gy'' and G(x'-y') = G(x'-y'')." (Contributed by NM, 21-Mar-2015.)
mapd                                          LCDual

Theoremmapdpglem26 32181* Lemma for mapdpg 32189. Baer p. 45 line 14: "Consequently there exist numbers u,v in G neither of which is 0 such that y = uy'' and..." (We scope \$d locally to avoid clashes with later substitutions into .) (Contributed by NM, 22-Mar-2015.)
mapd