Home Metamath Proof ExplorerTheorem List (p. 322 of 323) < 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-21500) Hilbert Space Explorer (21501-23023) Users' Mathboxes (23024-32227)

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

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

Theoremhdmapevec2 32102 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 32103 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 32104 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 32105 Lemma for hdmap10 32106. (Contributed by NM, 17-May-2015.)
LCDual              mapd       HDMap                                   HVMap       HDMap1

Theoremhdmap10 32106 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 32107 Lemma for hdmapadd 32109. (Contributed by NM, 26-May-2015.)
LCDual              HDMap                                                               mapd       HVMap       HDMap1

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

Theoremhdmapadd 32109 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 32110 Part of proof of part 12 in [Baer] p. 49 line 3. (Contributed by NM, 22-May-2015.)
LCDual              HDMap

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

Theoremhdmapneg 32112 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 32113 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 32114 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 32115 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 32116 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 32117 Part of proof of part 12 in [Baer] p. 49. (Contributed by NM, 29-May-2015.) (New usage is discouraged.)
LCDual              mapd       HDMap

Theoremhdmaprnlem4tN 32118 Lemma for hdmaprnN 32130. 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 32119 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 32120 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 32121 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 32122 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 32123 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 31902 and mapdcnv11N 31922. Use better hypotheses and/or theorems? (Contributed by NM, 27-May-2015.) (New usage is discouraged.)
LCDual              mapd       HDMap

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

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

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

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

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

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

TheoremhdmaprnN 32130 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 32131 Part 12 in [Baer] p. 49. The map from vectors to functionals with closed kernels maps one-to-one onto. Combined with hdmapadd 32109, 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 32132 Prior to part 14 in [Baer] p. 49, line 25. (Contributed by NM, 31-May-2015.)
Scalar              LCDual                     Scalar              HDMap

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theoremhdmap14lem15 32148* 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 32149 Extend class notation with g-map.
HGMap

Definitiondf-hgmap 32150* 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 32151* 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 32152* 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 32153* 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 32148. (Contributed by NM, 25-Mar-2015.)
Scalar              LCDual              HDMap       HGMap

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

Theoremhgmapcl 32155 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 32156 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 32157 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 32158 Value of the scalar sigma map at zero. (Contributed by NM, 12-Jun-2015.)
Scalar              HGMap

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

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

Theoremhgmapmul 32161 Part 15 of [Baer] p. 50 line 16. The multiplication is reversed after converting to the dual space scalar to the vector space scalar. (Contributed by NM, 7-Jun-2015.)
Scalar                     HGMap

Theoremhgmaprnlem1N 32162 Lemma for hgmaprnN 32167. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.)
Scalar                            LCDual              Scalar                            HDMap       HGMap

Theoremhgmaprnlem2N 32163 Lemma for hgmaprnN 32167. Part 15 of [Baer] p. 50 line 20. We only require a subset relation, rather than equality, so that the case of zero is taken care of automatically. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.)
Scalar                            LCDual              Scalar                            HDMap       HGMap                                          mapd

Theoremhgmaprnlem3N 32164* Lemma for hgmaprnN 32167. Eliminate . (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.)
Scalar                            LCDual              Scalar                            HDMap       HGMap                                          mapd

Theoremhgmaprnlem4N 32165* Lemma for hgmaprnN 32167. Eliminate . (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.)
Scalar                            LCDual              Scalar                            HDMap       HGMap

Theoremhgmaprnlem5N 32166 Lemma for hgmaprnN 32167. Eliminate . (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.)
Scalar                            LCDual              Scalar                            HDMap       HGMap

TheoremhgmaprnN 32167 Part of proof of part 16 in [Baer] p. 50 line 23, Fs=G, except that we use the original vector space scalars for the range. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.)
Scalar              HGMap

Theoremhgmap11 32168 The scalar sigma map is one-to-one. (Contributed by NM, 7-Jun-2015.)
Scalar              HGMap

Theoremhgmapf1oN 32169 The scalar sigma map is a one-to-one onto function. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.)
Scalar              HGMap

Theoremhgmapeq0 32170 The scalar sigma map is zero iff its argument is zero. (Contributed by NM, 12-Jun-2015.)
Scalar                     HGMap

Theoremhdmapipcl 32171 The inner product (Hermitian form) will be defined as . Show closure. (Contributed by NM, 7-Jun-2015.)
Scalar              HDMap

Theoremhdmapln1 32172 Linearity property that will be used for inner product. TODO: try to combine hypotheses in hdmap*ln* series. (Contributed by NM, 7-Jun-2015.)
Scalar                            HDMap

Theoremhdmaplna1 32173 Additive property of first (inner product) argument. (Contributed by NM, 11-Jun-2015.)
Scalar              HDMap

Theoremhdmaplns1 32174 Subtraction property of first (inner product) argument. (Contributed by NM, 12-Jun-2015.)
Scalar              HDMap

Theoremhdmaplnm1 32175 Multiplicative property of first (inner product) argument. (Contributed by NM, 11-Jun-2015.)
Scalar                     HDMap

Theoremhdmaplna2 32176 Additive property of second (inner product) argument. (Contributed by NM, 10-Jun-2015.)
Scalar              HDMap

Theoremhdmapglnm2 32177 g-linear property of second (inner product) argument. Line 19 in [Holland95] p. 14. (Contributed by NM, 10-Jun-2015.)
Scalar                     HDMap       HGMap

Theoremhdmapgln2 32178 g-linear property that will be used for inner product. (Contributed by NM, 14-Jun-2015.)
Scalar                            HDMap       HGMap

Theoremhdmaplkr 32179 Kernel of the vector to dual map. Line 16 in [Holland95] p. 14. TODO: eliminate hypothesis. (Contributed by NM, 9-Jun-2015.)
LFnl       LKer       HDMap

Theoremhdmapellkr 32180 Membership in the kernel (as shown by hdmaplkr 32179) of the vector to dual map. Line 17 in [Holland95] p. 14. (Contributed by NM, 16-Jun-2015.)
Scalar              HDMap

Theoremhdmapip0 32181 Zero property that will be used for inner product. (Contributed by NM, 9-Jun-2015.)
Scalar              HDMap

Theoremhdmapip1 32182 Construct a proportional vector whose inner product with the original equals one. (Contributed by NM, 13-Jun-2015.)
Scalar                     HDMap

Theoremhdmapip0com 32183 Commutation property of Baer's sigma map (Holland's A map). Line 20 of [Holland95] p. 14. Also part of Lemma 1 of [Baer] p. 110 line 7. (Contributed by NM, 9-Jun-2015.)
Scalar              HDMap

Theoremhdmapinvlem1 32184 Line 27 in [Baer] p. 110. We use for Baer's u. Our unit vector has the required properties for his w by hdmapevec2 32102. Our means the inner product i.e. his f(u,w) (note argument reversal). (Contributed by NM, 11-Jun-2015.)
Scalar                            HDMap

Theoremhdmapinvlem2 32185 Line 28 in [Baer] p. 110, 0 = f(w,u). (Contributed by NM, 11-Jun-2015.)
Scalar                            HDMap

Theoremhdmapinvlem3 32186 Line 30 in [Baer] p. 110, f(sw + u, tw - v) = 0. (Contributed by NM, 12-Jun-2015.)
Scalar                            HDMap       HGMap

Theoremhdmapinvlem4 32187 Part 1.1 of Proposition 1 of [Baer] p. 110. We use , , , and for Baer's u, v, s, and t. Our unit vector has the required properties for his w by hdmapevec2 32102. Our means his f(u,v) (note argument reversal). (Contributed by NM, 12-Jun-2015.)
Scalar                            HDMap       HGMap

Theoremhdmapglem5 32188 Part 1.2 in [Baer] p. 110 line 34, f(u,v) alpha = f(v,u). (Contributed by NM, 12-Jun-2015.)
Scalar