Home Metamath Proof ExplorerTheorem List (p. 324 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 - 32301-32400   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremhdmap1l6h 32301 Lemmma for hdmap1l6 32305. Part (6) of [Baer] p. 48 line 2. (Contributed by NM, 1-May-2015.)
LCDual                                          mapd       HDMap1

Theoremhdmap1l6i 32302 Lemmma for hdmap1l6 32305. Eliminate auxiliary vector . (Contributed by NM, 1-May-2015.)
LCDual                                          mapd       HDMap1

Theoremhdmap1l6j 32303 Lemmma for hdmap1l6 32305. Eliminate { Y } ) = ( N hypothesis. (Contributed by NM, 1-May-2015.)
LCDual                                          mapd       HDMap1

Theoremhdmap1l6k 32304 Lemmma for hdmap1l6 32305. Eliminate nonzero vector requirement. (Contributed by NM, 1-May-2015.)
LCDual                                          mapd       HDMap1

Theoremhdmap1l6 32305 Part (6) of [Baer] p. 47 line 6. Note that we use which is equivalent to Baer's "Fx (Fy + Fz)" by lspdisjb 16153. (Contributed by NM, 17-May-2015.)
LCDual                            mapd       HDMap1

Theoremhdmap1p6N 32306 (Convert mapdh6N 32230 to use HDMap1 function.) Part (6) of [Baer] p. 47 line 6. Note that we use which is equivalent to Baer's "Fx (Fy + Fz)" by lspdisjb 16153. TODO: No longer used and should be deleted. Use hdmap1l6 32305 instead. Also delete unused mapdh6N 32230 etc. leading up to this. (Contributed by NM, 17-May-2015.) (New usage is discouraged.)
LCDual                            mapd       HDMap1

Theoremhdmap1eulem 32307* Lemma for hdmap1eu 32309. TODO: combine with hdmap1eu 32309 or at least share some hypotheses. (Contributed by NM, 15-May-2015.)
LCDual                                   mapd       HDMap1

Theoremhdmap1eulemOLDN 32308* Lemma for hdmap1euOLDN 32310. TODO: combine with hdmap1euOLDN 32310 or at least share some hypotheses. (Contributed by NM, 15-May-2015.) (New usage is discouraged.)
LCDual                                   mapd       HDMap1

Theoremhdmap1eu 32309* Convert mapdh9a 32273 to use the HDMap1 notation. (Contributed by NM, 15-May-2015.)
LCDual                     mapd       HDMap1

Theoremhdmap1euOLDN 32310* Convert mapdh9aOLDN 32274 to use the HDMap1 notation. (Contributed by NM, 15-May-2015.) (New usage is discouraged.)
LCDual                     mapd       HDMap1

Theoremhdmap1neglem1N 32311 Lemma for hdmapneg 32332. TODO: Not used; delete. (Contributed by NM, 23-May-2015.) (New usage is discouraged.)
LCDual                            mapd       HDMap1

Theoremhdmapffval 32312* Map from vectors to functionals in the closed kernel dual space. (Contributed by NM, 15-May-2015.)
HDMap HDMap1 LCDual HVMap

Theoremhdmapfval 32313* Map from vectors to functionals in the closed kernel dual space. (Contributed by NM, 15-May-2015.)
LCDual              HVMap       HDMap1       HDMap

Theoremhdmapval 32314* Value of map from vectors to functionals in the closed kernel dual space. This is the function sigma on line 27 above part 9 in [Baer] p. 48. We select a convenient fixed reference vector to be (corresponding to vector u on p. 48 line 7) whose span is the lattice isomorphism map of the fiducial atom (see dvheveccl 31595). is a fixed reference functional determined by this vector (corresponding to u' on line 8; mapdhvmap 32252 shows in Baer's notation (Fu)* = Gu'). Baer's independent vectors v and w on line 7 correspond to our that the ranges over. The middle term provides isolation to allow and to assume the same value without conflict. Closure is shown by hdmapcl 32316. If a separate auxiliary vector is known, hdmapval2 32318 provides a version without quantification. (Contributed by NM, 15-May-2015.)
LCDual              HVMap       HDMap1       HDMap

TheoremhdmapfnN 32315 Functionality of map from vectors to functionals with closed kernels. (Contributed by NM, 30-May-2015.) (New usage is discouraged.)
HDMap

Theoremhdmapcl 32316 Closure of map from vectors to functionals with closed kernels. (Contributed by NM, 15-May-2015.)
LCDual              HDMap

Theoremhdmapval2lem 32317* Lemma for hdmapval2 32318. (Contributed by NM, 15-May-2015.)
LCDual              HVMap       HDMap1       HDMap

Theoremhdmapval2 32318 Value of map from vectors to functionals with a specific auxiliary vector. TODO: Would shorter proofs result if the .ne hypothesis were changed to two hypothesis? Consider hdmaplem1 32254 through hdmaplem4 32257, which would become obsolete. (Contributed by NM, 15-May-2015.)
LCDual              HVMap       HDMap1       HDMap

Theoremhdmapval0 32319 Value of map from vectors to functionals at zero. Note: we use dvh3dim 31929 for convenience, even though 3 dimensions aren't necessary at this point. TODO: I think either this or hdmapeq0 32330 could be derived from the other to shorten proof. (Contributed by NM, 17-May-2015.)
LCDual              HDMap

Theoremhdmapeveclem 32320 Lemma for hdmapevec 32321. TODO: combine with hdmapevec 32321 if it shortens overall. (Contributed by NM, 16-May-2015.)
HVMap       HDMap                                   LCDual              HDMap1

Theoremhdmapevec 32321 Value of map from vectors to functionals at the reference vector . (Contributed by NM, 16-May-2015.)
HVMap       HDMap

Theoremhdmapevec2 32322 The inner product of the reference vector with itself is nonzero. This shows the inner product condition in the proof of Theorem 3.6 of [Holland95] p. 14 line 32, e , e is satisfied. TODO: remove redundant hypothesis hdmapevec.j. (Contributed by NM, 1-Jun-2015.)
HVMap       HDMap                     Scalar

Theoremhdmapval3lemN 32323 Value of map from vectors to functionals at arguments not colinear with the reference vector . (Contributed by NM, 17-May-2015.) (New usage is discouraged.)
LCDual              HVMap       HDMap1       HDMap

Theoremhdmapval3N 32324 Value of map from vectors to functionals at arguments not colinear with the reference vector . (Contributed by NM, 17-May-2015.) (New usage is discouraged.)
LCDual              HVMap       HDMap1       HDMap

Theoremhdmap10lem 32325 Lemma for hdmap10 32326. (Contributed by NM, 17-May-2015.)
LCDual              mapd       HDMap                                   HVMap       HDMap1

Theoremhdmap10 32326 Part 10 in [Baer] p. 48 line 33, (Ft)* = G(tS) in their notation (S = sigma). (Contributed by NM, 17-May-2015.)
LCDual              mapd       HDMap

Theoremhdmap11lem1 32327 Lemma for hdmapadd 32329. (Contributed by NM, 26-May-2015.)
LCDual              HDMap                                                               mapd       HVMap       HDMap1

Theoremhdmap11lem2 32328 Lemma for hdmapadd 32329. (Contributed by NM, 26-May-2015.)
LCDual              HDMap                                                               mapd       HVMap       HDMap1

Theoremhdmapadd 32329 Part 11 in [Baer] p. 48 line 35, (a+b)S = aS+bS in their notation (S = sigma). (Contributed by NM, 22-May-2015.)
LCDual              HDMap

Theoremhdmapeq0 32330 Part of proof of part 12 in [Baer] p. 49 line 3. (Contributed by NM, 22-May-2015.)
LCDual              HDMap

Theoremhdmapnzcl 32331 Nonzero vector closure of map from vectors to functionals with closed kernels. (Contributed by NM, 27-May-2015.)
LCDual                     HDMap

Theoremhdmapneg 32332 Part of proof of part 12 in [Baer] p. 49 line 4. The sigma map of a negative is the negative of the sigma map. (Contributed by NM, 24-May-2015.)
LCDual              HDMap

Theoremhdmapsub 32333 Part of proof of part 12 in [Baer] p. 49 line 5, (a-b)S = aS-bS in their notation (S = sigma). (Contributed by NM, 26-May-2015.)
LCDual              HDMap

Theoremhdmap11 32334 Part of proof of part 12 in [Baer] p. 49 line 4, aS=bS iff a=b in their notation (S = sigma). The sigma map is one-to-one. (Contributed by NM, 26-May-2015.)
HDMap

Theoremhdmaprnlem1N 32335 Part of proof of part 12 in [Baer] p. 49 line 10, Gu' Gs. Our is Baer's T. (Contributed by NM, 26-May-2015.) (New usage is discouraged.)
LCDual              mapd       HDMap

Theoremhdmaprnlem3N 32336 Part of proof of part 12 in [Baer] p. 49 line 15, T P. Our is Baer's P, where P* = G(u'+s). (Contributed by NM, 27-May-2015.) (New usage is discouraged.)
LCDual              mapd       HDMap

Theoremhdmaprnlem3uN 32337 Part of proof of part 12 in [Baer] p. 49. (Contributed by NM, 29-May-2015.) (New usage is discouraged.)
LCDual              mapd       HDMap

Theoremhdmaprnlem4tN 32338 Lemma for hdmaprnN 32350. TODO: This lemma doesn't quite pay for itself even though used 4 times. Maybe prove this directly instead. (Contributed by NM, 27-May-2015.) (New usage is discouraged.)
LCDual              mapd       HDMap

Theoremhdmaprnlem4N 32339 Part of proof of part 12 in [Baer] p. 49 line 19. (T* =) (Ft)* = Gs. (Contributed by NM, 27-May-2015.) (New usage is discouraged.)
LCDual              mapd       HDMap

Theoremhdmaprnlem6N 32340 Part of proof of part 12 in [Baer] p. 49 line 18, G(u'+s) = G(u'+t). (Contributed by NM, 27-May-2015.) (New usage is discouraged.)
LCDual              mapd       HDMap

Theoremhdmaprnlem7N 32341 Part of proof of part 12 in [Baer] p. 49 line 19, s-St G(u'+s) = P*. (Contributed by NM, 27-May-2015.) (New usage is discouraged.)
LCDual              mapd       HDMap

Theoremhdmaprnlem8N 32342 Part of proof of part 12 in [Baer] p. 49 line 19, s-St (Ft)* = T*. (Contributed by NM, 27-May-2015.) (New usage is discouraged.)
LCDual              mapd       HDMap

Theoremhdmaprnlem9N 32343 Part of proof of part 12 in [Baer] p. 49 line 21, s=S(t). TODO: we seem to be going back and forth with mapd11 32122 and mapdcnv11N 32142. Use better hypotheses and/or theorems? (Contributed by NM, 27-May-2015.) (New usage is discouraged.)
LCDual              mapd       HDMap

Theoremhdmaprnlem3eN 32344* Lemma for hdmaprnN 32350. (Contributed by NM, 29-May-2015.) (New usage is discouraged.)
LCDual              mapd       HDMap

Theoremhdmaprnlem10N 32345* Lemma for hdmaprnN 32350. Show is in the range of . (Contributed by NM, 29-May-2015.) (New usage is discouraged.)
LCDual              mapd       HDMap

Theoremhdmaprnlem11N 32346* Lemma for hdmaprnN 32350. Show is in the range of . (Contributed by NM, 29-May-2015.) (New usage is discouraged.)
LCDual              mapd       HDMap

Theoremhdmaprnlem15N 32347* Lemma for hdmaprnN 32350. Eliminate . (Contributed by NM, 30-May-2015.) (New usage is discouraged.)
LCDual                            mapd       HDMap

Theoremhdmaprnlem16N 32348 Lemma for hdmaprnN 32350. Eliminate . (Contributed by NM, 30-May-2015.) (New usage is discouraged.)
LCDual                            mapd       HDMap

Theoremhdmaprnlem17N 32349 Lemma for hdmaprnN 32350. Include zero. (Contributed by NM, 30-May-2015.) (New usage is discouraged.)
LCDual                            mapd       HDMap

TheoremhdmaprnN 32350 Part of proof of part 12 in [Baer] p. 49 line 21, As=B. (Contributed by NM, 30-May-2015.) (New usage is discouraged.)
LCDual              HDMap

Theoremhdmapf1oN 32351 Part 12 in [Baer] p. 49. The map from vectors to functionals with closed kernels maps one-to-one onto. Combined with hdmapadd 32329, this shows the map is an automorphism from the additive group of vectors to the additive group of functionals with closed kernels. (Contributed by NM, 30-May-2015.) (New usage is discouraged.)
LCDual              HDMap

Theoremhdmap14lem1a 32352 Prior to part 14 in [Baer] p. 49, line 25. (Contributed by NM, 31-May-2015.)
Scalar              LCDual                     Scalar              HDMap

Theoremhdmap14lem2a 32353* Prior to part 14 in [Baer] p. 49, line 25. TODO: fix to include so it can be used in hdmap14lem10 32363. (Contributed by NM, 31-May-2015.)
Scalar              LCDual                     Scalar              HDMap

Theoremhdmap14lem1 32354 Prior to part 14 in [Baer] p. 49, line 25. (Contributed by NM, 31-May-2015.)
Scalar                     LCDual                     Scalar                     HDMap

Theoremhdmap14lem2N 32355* Prior to part 14 in [Baer] p. 49, line 25. TODO: fix to include so it can be used in hdmap14lem10 32363. (Contributed by NM, 31-May-2015.) (New usage is discouraged.)
Scalar                     LCDual                     Scalar                     HDMap

Theoremhdmap14lem3 32356* Prior to part 14 in [Baer] p. 49, line 26. (Contributed by NM, 31-May-2015.)
Scalar                     LCDual                     Scalar                     HDMap

Theoremhdmap14lem4a 32357* Simplify in hdmap14lem3 32356 to provide a slightly simpler definition later. (Contributed by NM, 31-May-2015.)
Scalar                     LCDual                     Scalar                     HDMap

Theoremhdmap14lem4 32358* Simplify in hdmap14lem3 32356 to provide a slightly simpler definition later. TODO: Use hdmap14lem4a 32357 if that one is also used directly elsewhere. Otherwise, merge hdmap14lem4a 32357 into this one. (Contributed by NM, 31-May-2015.)
Scalar                     LCDual                     Scalar                     HDMap

Theoremhdmap14lem6 32359* Case where is zero. (Contributed by NM, 1-Jun-2015.)
Scalar                     LCDual                     Scalar                     HDMap

Theoremhdmap14lem7 32360* Combine cases of . TODO: Can this be done at once in hdmap14lem3 32356, in order to get rid of hdmap14lem6 32359? Perhaps modify lspsneu 16150 to become instead of ? (Contributed by NM, 1-Jun-2015.)
Scalar              LCDual              Scalar              HDMap

Theoremhdmap14lem8 32361 Part of proof of part 14 in [Baer] p. 49 lines 33-35. (Contributed by NM, 1-Jun-2015.)
Scalar              LCDual                     Scalar              HDMap

Theoremhdmap14lem9 32362 Part of proof of part 14 in [Baer] p. 49 line 38. (Contributed by NM, 1-Jun-2015.)
Scalar              LCDual                     Scalar              HDMap

Theoremhdmap14lem10 32363 Part of proof of part 14 in [Baer] p. 49 line 38. (Contributed by NM, 3-Jun-2015.)
Scalar              LCDual                     Scalar              HDMap

Theoremhdmap14lem11 32364 Part of proof of part 14 in [Baer] p. 50 line 3. (Contributed by NM, 3-Jun-2015.)
Scalar              LCDual                     Scalar              HDMap

Theoremhdmap14lem12 32365* Lemma for proof of part 14 in [Baer] p. 50. (Contributed by NM, 6-Jun-2015.)
Scalar              LCDual              HDMap                     Scalar

Theoremhdmap14lem13 32366* Lemma for proof of part 14 in [Baer] p. 50. (Contributed by NM, 6-Jun-2015.)
Scalar              LCDual              HDMap                     Scalar

Theoremhdmap14lem14 32367* Part of proof of part 14 in [Baer] p. 50 line 3. (Contributed by NM, 6-Jun-2015.)
Scalar              LCDual              HDMap                     Scalar

Theoremhdmap14lem15 32368* Part of proof of part 14 in [Baer] p. 50 line 3. Convert scalar base of dual to scalar base of vector space. (Contributed by NM, 6-Jun-2015.)
Scalar              LCDual              HDMap

Syntaxchg 32369 Extend class notation with g-map.
HGMap

Definitiondf-hgmap 32370* Define map from the scalar division ring of the vector space to the scalar division ring of its closed kernel dual. (Contributed by NM, 25-Mar-2015.)
HGMap Scalar HDMap LCDual

Theoremhgmapffval 32371* Map from the scalar division ring of the vector space to the scalar division ring of its closed kernel dual. (Contributed by NM, 25-Mar-2015.)
HGMap Scalar HDMap LCDual

Theoremhgmapfval 32372* Map from the scalar division ring of the vector space to the scalar division ring of its closed kernel dual. (Contributed by NM, 25-Mar-2015.)
Scalar              LCDual              HDMap       HGMap

Theoremhgmapval 32373* Value of map from the scalar division ring of the vector space to the scalar division ring of its closed kernel dual. Function sigma of scalar f in part 14 of [Baer] p. 50 line 4. TODO: variable names are inherited from older version. Maybe make more consistent with hdmap14lem15 32368. (Contributed by NM, 25-Mar-2015.)
Scalar              LCDual              HDMap       HGMap

TheoremhgmapfnN 32374 Functionality of scalar sigma map. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.)
Scalar              HGMap

Theoremhgmapcl 32375 Closure of scalar sigma map i.e. the map from the vector space scalar base to the dual space scalar base. (Contributed by NM, 6-Jun-2015.)
Scalar              HGMap

Theoremhgmapdcl 32376 Closure of the vector space to dual space scalar map, in the scalar sigma map. (Contributed by NM, 6-Jun-2015.)
Scalar              LCDual       Scalar              HGMap

Theoremhgmapvs 32377 Part 15 of [Baer] p. 50 line 6. Also line 15 in [Holland95] p. 14. (Contributed by NM, 6-Jun-2015.)
Scalar              LCDual              HDMap       HGMap

Theoremhgmapval0 32378 Value of the scalar sigma map at zero. (Contributed by NM, 12-Jun-2015.)
Scalar              HGMap

Theoremhgmapval1 32379 Value of the scalar sigma map at one. (Contributed by NM, 12-Jun-2015.)
Scalar              HGMap

Theoremhgmapadd 32380 Part 15 of [Baer] p. 50 line 13. (Contributed by NM, 6-Jun-2015.)