Home Metamath Proof ExplorerTheorem List (p. 328 of 330) < 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-22459) Hilbert Space Explorer (22460-23982) Users' Mathboxes (23983-32936)

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

Theoremmapdheq2 32701* Lemmma for ~? mapdh . One direction of part (2) in [Baer] p. 45. (Contributed by NM, 4-Apr-2015.)
mapd                                          LCDual

Theoremmapdheq2biN 32702* Lemmma for ~? mapdh . Part (2) in [Baer] p. 45. The bidirectional version of mapdheq2 32701 seems to require an additional hypothesis not mentioned in Baer. TODO fix ref. TODO: We probably don't need this; delete if never used. (Contributed by NM, 4-Apr-2015.) (New usage is discouraged.)
mapd                                          LCDual

Theoremmapdheq4lem 32703* Lemma for mapdheq4 32704. Part (4) in [Baer] p. 46. (Contributed by NM, 12-Apr-2015.)
mapd                                          LCDual

Theoremmapdheq4 32704* Lemma for ~? mapdh . Part (4) in [Baer] p. 46. (Contributed by NM, 12-Apr-2015.)
mapd                                          LCDual

Theoremmapdh6lem1N 32705* Lemma for mapdh6N 32719. Part (6) in [Baer] p. 47, lines 16-18. (Contributed by NM, 13-Apr-2015.) (New usage is discouraged.)
mapd                                          LCDual

Theoremmapdh6lem2N 32706* Lemma for mapdh6N 32719. Part (6) in [Baer] p. 47, lines 20-22. (Contributed by NM, 13-Apr-2015.) (New usage is discouraged.)
mapd                                          LCDual

Theoremmapdh6aN 32707* Lemma for mapdh6N 32719. Part (6) in [Baer] p. 47, case 1. (Contributed by NM, 23-Apr-2015.) (New usage is discouraged.)
mapd                                          LCDual

Theoremmapdh6b0N 32708* Lemmma for mapdh6N 32719. (Contributed by NM, 23-Apr-2015.) (New usage is discouraged.)
mapd                                          LCDual

Theoremmapdh6bN 32709* Lemmma for mapdh6N 32719. (Contributed by NM, 24-Apr-2015.) (New usage is discouraged.)
mapd                                          LCDual

Theoremmapdh6cN 32710* Lemmma for mapdh6N 32719. (Contributed by NM, 24-Apr-2015.) (New usage is discouraged.)
mapd                                          LCDual

Theoremmapdh6dN 32711* Lemmma for mapdh6N 32719. (Contributed by NM, 1-May-2015.) (New usage is discouraged.)
mapd                                          LCDual

Theoremmapdh6eN 32712* Lemmma for mapdh6N 32719. Part (6) in [Baer] p. 47 line 38. (Contributed by NM, 1-May-2015.) (New usage is discouraged.)
mapd                                          LCDual

Theoremmapdh6fN 32713* Lemmma for mapdh6N 32719. Part (6) in [Baer] p. 47 line 38. (Contributed by NM, 1-May-2015.) (New usage is discouraged.)
mapd                                          LCDual

Theoremmapdh6gN 32714* Lemmma for mapdh6N 32719. Part (6) of [Baer] p. 47 line 39. (Contributed by NM, 1-May-2015.) (New usage is discouraged.)
mapd                                          LCDual

Theoremmapdh6hN 32715* Lemmma for mapdh6N 32719. Part (6) of [Baer] p. 48 line 2. (Contributed by NM, 1-May-2015.) (New usage is discouraged.)
mapd                                          LCDual

Theoremmapdh6iN 32716* Lemmma for mapdh6N 32719. Eliminate auxiliary vector . (Contributed by NM, 1-May-2015.) (New usage is discouraged.)
mapd                                          LCDual

Theoremmapdh6jN 32717* Lemmma for mapdh6N 32719. Eliminate { Y } ) = ( N hypothesis. (Contributed by NM, 1-May-2015.) (New usage is discouraged.)
mapd                                          LCDual

Theoremmapdh6kN 32718* Lemmma for mapdh6N 32719. Eliminate nonzero vector requirement. (Contributed by NM, 1-May-2015.) (New usage is discouraged.)
mapd                                          LCDual

Theoremmapdh6N 32719* Part (6) of [Baer] p. 47 line 6. Note that we use which is equivalent to Baer's "Fx (Fy + Fz)" by lspdisjb 16236. TODO: If \$ds with and becomes a problem later, cbv's on variables here to get rid of them. . Maybe reorder hypotheses in lemmas to the more consistent order of this theorem, so they can be shared with this theorem. (Contributed by NM, 1-May-2015.) (New usage is discouraged.)
LCDual                                          mapd

Theoremmapdh7eN 32720* Part (7) of [Baer] p. 48 line 10 (5 of 6 cases). (Note: 1 of 6 and 2 of 6 are hypotheses a and b.) (Contributed by NM, 2-May-2015.) (New usage is discouraged.)
LCDual                                   mapd

Theoremmapdh7cN 32721* Part (7) of [Baer] p. 48 line 10 (3 of 6 cases). (Contributed by NM, 2-May-2015.) (New usage is discouraged.)
LCDual                                   mapd

Theoremmapdh7dN 32722* Part (7) of [Baer] p. 48 line 10 (4 of 6 cases). (Contributed by NM, 2-May-2015.) (New usage is discouraged.)
LCDual                                   mapd

Theoremmapdh7fN 32723* Part (7) of [Baer] p. 48 line 10 (6 of 6 cases). (Contributed by NM, 2-May-2015.) (New usage is discouraged.)
LCDual                                   mapd

Theoremmapdh75e 32724* Part (7) of [Baer] p. 48 line 10 (5 of 6 cases). , , are Baer's u, v, w. (Note: Cases 1 of 6 and 2 of 6 are hypotheses mapdh75b here and mapdh75a in mapdh75cN 32725.) (Contributed by NM, 2-May-2015.)
LCDual                                   mapd

Theoremmapdh75cN 32725* Part (7) of [Baer] p. 48 line 10 (3 of 6 cases). (Contributed by NM, 2-May-2015.) (New usage is discouraged.)
LCDual                                   mapd

Theoremmapdh75d 32726* Part (7) of [Baer] p. 48 line 10 (4 of 6 cases). (Contributed by NM, 2-May-2015.)
LCDual                                   mapd

Theoremmapdh75fN 32727* Part (7) of [Baer] p. 48 line 10 (6 of 6 cases). (Contributed by NM, 2-May-2015.) (New usage is discouraged.)
LCDual                                   mapd

Syntaxchvm 32728 Extend class notation with vector to dual map.
HVMap

Definitiondf-hvmap 32729* Extend class notation with a map from each nonzero vector to a unique nonzero functional in the closed kernel dual space. (We could extend it to include the zero vector, but that is unnecessary for our purposes.) TODO: This pattern is used several times earlier e.g. lcf1o 32523, dochfl1 32448- should we update those to use this definition? (Contributed by NM, 23-Mar-2015.)
HVMap Scalar

Theoremhvmapffval 32730* Map from nonzero vectors to nonzero functionals in the closed kernel dual space. (Contributed by NM, 23-Mar-2015.)
HVMap Scalar

Theoremhvmapfval 32731* Map from nonzero vectors to nonzero functionals in the closed kernel dual space. (Contributed by NM, 23-Mar-2015.)
Scalar              HVMap

Theoremhvmapval 32732* Value of map from nonzero vectors to nonzero functionals in the closed kernel dual space. (Contributed by NM, 23-Mar-2015.)
Scalar              HVMap

TheoremhvmapvalvalN 32733* Value of value of map (i.e. functional value) from nonzero vectors to nonzero functionals in the closed kernel dual space. (Contributed by NM, 23-Mar-2015.) (New usage is discouraged.)
Scalar              HVMap

TheoremhvmapidN 32734 The value of the vector to functional map, at the vector, is one. (Contributed by NM, 23-Mar-2015.) (New usage is discouraged.)
Scalar              HVMap

Theoremhvmap1o 32735* The vector to functional map provides a bijection from nonzero vectors to nonzero functionals with closed kernels . (Contributed by NM, 27-Mar-2015.)
LFnl       LKer       LDual                     HVMap

TheoremhvmapclN 32736* Closure of the vector to functional map. (Contributed by NM, 27-Mar-2015.) (New usage is discouraged.)
LFnl       LKer       LDual                     HVMap

Theoremhvmap1o2 32737 The vector to functional map provides a bijection from nonzero vectors to nonzero functionals with closed kernels . (Contributed by NM, 27-Mar-2015.)
LCDual                     HVMap

Theoremhvmapcl2 32738 Closure of the vector to functional map. (Contributed by NM, 27-Mar-2015.)
LCDual                     HVMap

Theoremhvmaplfl 32739 The vector to functional map value is a functional. (Contributed by NM, 28-Mar-2015.)
LFnl       HVMap

Theoremhvmaplkr 32740 Kernel of the vector to functional map. TODO: make this become lcfrlem11 32525. (Contributed by NM, 29-Mar-2015.)
LKer       HVMap

Theoremmapdhvmap 32741 Relationship between mapd and HVMap, which can be used to satify the last hypothesis of mapdpg 32678. Equation 10 of [Baer] p. 48. (Contributed by NM, 29-Mar-2015.)
LCDual              mapd       HVMap

Theoremlspindp5 32742 Obtain an independent vector set from a vector dependent on and and another independent set . (Here we don't show the part of the independence, which passes straight through. We also don't show nonzero vector requirements that are redundant for this theorem. Different orderings can be obtained using lspexch 16239 and prcom 3911.) (Contributed by NM, 4-May-2015.)

Theoremhdmaplem1 32743 Lemma to convert a frequently-used union condition. TODO: see if this can be applied to other hdmap* theorems. (Contributed by NM, 17-May-2015.)

Theoremhdmaplem2N 32744 Lemma to convert a frequently-used union condition. TODO: see if this can be applied to other hdmap* theorems. (Contributed by NM, 17-May-2015.) (New usage is discouraged.)

Theoremhdmaplem3 32745 Lemma to convert a frequently-used union condition. TODO: see if this can be applied to other hdmap* theorems. (Contributed by NM, 17-May-2015.)

Theoremhdmaplem4 32746 Lemma to convert a frequently-used union condition. TODO: see if this can be applied to other hdmap* theorems. (Contributed by NM, 17-May-2015.)

Theoremmapdh8a 32747* Part of Part (8) in [Baer] p. 48. (Contributed by NM, 5-May-2015.)
LCDual                                   mapd

Theoremmapdh8aa 32748* Part of Part (8) in [Baer] p. 48. (Contributed by NM, 12-May-2015.)
LCDual                                   mapd

Theoremmapdh8ab 32749* Part of Part (8) in [Baer] p. 48. (Contributed by NM, 13-May-2015.)
LCDual                                   mapd

Theoremmapdh8ac 32750* Part of Part (8) in [Baer] p. 48. (Contributed by NM, 13-May-2015.)
LCDual                                   mapd

Theoremmapdh8ad 32751* Part of Part (8) in [Baer] p. 48. (Contributed by NM, 13-May-2015.)
LCDual                                   mapd

Theoremmapdh8b 32752* Part of Part (8) in [Baer] p. 48. (Contributed by NM, 6-May-2015.)
LCDual                                   mapd

Theoremmapdh8c 32753* Part of Part (8) in [Baer] p. 48. (Contributed by NM, 6-May-2015.)
LCDual                                   mapd