Home | Metamath
Proof Explorer Theorem List (p. 403 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | hdmapadd 40201 | Part 11 in [Baer] p. 48 line 35, (a+b)S = aS+bS in their notation (S = sigma). (Contributed by NM, 22-May-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ β = (+gβπΆ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (πβ(π + π)) = ((πβπ) β (πβπ))) | ||
Theorem | hdmapeq0 40202 | Part of proof of part 12 in [Baer] p. 49 line 3. (Contributed by NM, 22-May-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π = (0gβπΆ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) β β’ (π β ((πβπ) = π β π = 0 )) | ||
Theorem | hdmapnzcl 40203 | Nonzero vector closure of map from vectors to functionals with closed kernels. (Contributed by NM, 27-May-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π = (0gβπΆ) & β’ π· = (BaseβπΆ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) β β’ (π β (πβπ) β (π· β {π})) | ||
Theorem | hdmapneg 40204 | 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.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (invgβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ πΌ = (invgβπΆ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) β β’ (π β (πβ(πβπ)) = (πΌβ(πβπ))) | ||
Theorem | hdmapsub 40205 | 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.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π = (-gβπΆ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (πβ(π β π)) = ((πβπ)π(πβπ))) | ||
Theorem | hdmap11 40206 | 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.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β ((πβπ) = (πβπ) β π = π)) | ||
Theorem | hdmaprnlem1N 40207 | 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.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ πΏ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π· β {π})) & β’ (π β π£ β π) & β’ (π β (πβ(πβ{π£})) = (πΏβ{π })) & β’ (π β π’ β π) & β’ (π β Β¬ π’ β (πβ{π£})) β β’ (π β (πΏβ{(πβπ’)}) β (πΏβ{π })) | ||
Theorem | hdmaprnlem3N 40208 | 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.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ πΏ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π· β {π})) & β’ (π β π£ β π) & β’ (π β (πβ(πβ{π£})) = (πΏβ{π })) & β’ (π β π’ β π) & β’ (π β Β¬ π’ β (πβ{π£})) & β’ π· = (BaseβπΆ) & β’ π = (0gβπΆ) & β’ 0 = (0gβπ) & β’ β = (+gβπΆ) β β’ (π β (πβ{π£}) β (β‘πβ(πΏβ{((πβπ’) β π )}))) | ||
Theorem | hdmaprnlem3uN 40209 | Part of proof of part 12 in [Baer] p. 49. (Contributed by NM, 29-May-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ πΏ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π· β {π})) & β’ (π β π£ β π) & β’ (π β (πβ(πβ{π£})) = (πΏβ{π })) & β’ (π β π’ β π) & β’ (π β Β¬ π’ β (πβ{π£})) & β’ π· = (BaseβπΆ) & β’ π = (0gβπΆ) & β’ 0 = (0gβπ) & β’ β = (+gβπΆ) β β’ (π β (πβ{π’}) β (β‘πβ(πΏβ{((πβπ’) β π )}))) | ||
Theorem | hdmaprnlem4tN 40210 | Lemma for hdmaprnN 40222. TODO: This lemma doesn't quite pay for itself even though used six times. Maybe prove this directly instead. (Contributed by NM, 27-May-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ πΏ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π· β {π})) & β’ (π β π£ β π) & β’ (π β (πβ(πβ{π£})) = (πΏβ{π })) & β’ (π β π’ β π) & β’ (π β Β¬ π’ β (πβ{π£})) & β’ π· = (BaseβπΆ) & β’ π = (0gβπΆ) & β’ 0 = (0gβπ) & β’ β = (+gβπΆ) & β’ (π β π‘ β ((πβ{π£}) β { 0 })) β β’ (π β π‘ β π) | ||
Theorem | hdmaprnlem4N 40211 | 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.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ πΏ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π· β {π})) & β’ (π β π£ β π) & β’ (π β (πβ(πβ{π£})) = (πΏβ{π })) & β’ (π β π’ β π) & β’ (π β Β¬ π’ β (πβ{π£})) & β’ π· = (BaseβπΆ) & β’ π = (0gβπΆ) & β’ 0 = (0gβπ) & β’ β = (+gβπΆ) & β’ (π β π‘ β ((πβ{π£}) β { 0 })) β β’ (π β (πβ(πβ{π‘})) = (πΏβ{π })) | ||
Theorem | hdmaprnlem6N 40212 | 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.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ πΏ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π· β {π})) & β’ (π β π£ β π) & β’ (π β (πβ(πβ{π£})) = (πΏβ{π })) & β’ (π β π’ β π) & β’ (π β Β¬ π’ β (πβ{π£})) & β’ π· = (BaseβπΆ) & β’ π = (0gβπΆ) & β’ 0 = (0gβπ) & β’ β = (+gβπΆ) & β’ (π β π‘ β ((πβ{π£}) β { 0 })) & β’ + = (+gβπ) & β’ (π β (πΏβ{((πβπ’) β π )}) = (πβ(πβ{(π’ + π‘)}))) β β’ (π β (πΏβ{((πβπ’) β π )}) = (πΏβ{((πβπ’) β (πβπ‘))})) | ||
Theorem | hdmaprnlem7N 40213 | 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.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ πΏ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π· β {π})) & β’ (π β π£ β π) & β’ (π β (πβ(πβ{π£})) = (πΏβ{π })) & β’ (π β π’ β π) & β’ (π β Β¬ π’ β (πβ{π£})) & β’ π· = (BaseβπΆ) & β’ π = (0gβπΆ) & β’ 0 = (0gβπ) & β’ β = (+gβπΆ) & β’ (π β π‘ β ((πβ{π£}) β { 0 })) & β’ + = (+gβπ) & β’ (π β (πΏβ{((πβπ’) β π )}) = (πβ(πβ{(π’ + π‘)}))) β β’ (π β (π (-gβπΆ)(πβπ‘)) β (πΏβ{((πβπ’) β π )})) | ||
Theorem | hdmaprnlem8N 40214 | 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.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ πΏ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π· β {π})) & β’ (π β π£ β π) & β’ (π β (πβ(πβ{π£})) = (πΏβ{π })) & β’ (π β π’ β π) & β’ (π β Β¬ π’ β (πβ{π£})) & β’ π· = (BaseβπΆ) & β’ π = (0gβπΆ) & β’ 0 = (0gβπ) & β’ β = (+gβπΆ) & β’ (π β π‘ β ((πβ{π£}) β { 0 })) & β’ + = (+gβπ) & β’ (π β (πΏβ{((πβπ’) β π )}) = (πβ(πβ{(π’ + π‘)}))) β β’ (π β (π (-gβπΆ)(πβπ‘)) β (πβ(πβ{π‘}))) | ||
Theorem | hdmaprnlem9N 40215 | 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 39997 and mapdcnv11N 40017. Use better hypotheses and/or theorems? (Contributed by NM, 27-May-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ πΏ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π· β {π})) & β’ (π β π£ β π) & β’ (π β (πβ(πβ{π£})) = (πΏβ{π })) & β’ (π β π’ β π) & β’ (π β Β¬ π’ β (πβ{π£})) & β’ π· = (BaseβπΆ) & β’ π = (0gβπΆ) & β’ 0 = (0gβπ) & β’ β = (+gβπΆ) & β’ (π β π‘ β ((πβ{π£}) β { 0 })) & β’ + = (+gβπ) & β’ (π β (πΏβ{((πβπ’) β π )}) = (πβ(πβ{(π’ + π‘)}))) β β’ (π β π = (πβπ‘)) | ||
Theorem | hdmaprnlem3eN 40216* | Lemma for hdmaprnN 40222. (Contributed by NM, 29-May-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ πΏ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π· β {π})) & β’ (π β π£ β π) & β’ (π β (πβ(πβ{π£})) = (πΏβ{π })) & β’ (π β π’ β π) & β’ (π β Β¬ π’ β (πβ{π£})) & β’ π· = (BaseβπΆ) & β’ π = (0gβπΆ) & β’ 0 = (0gβπ) & β’ β = (+gβπΆ) & β’ + = (+gβπ) β β’ (π β βπ‘ β ((πβ{π£}) β { 0 })(πΏβ{((πβπ’) β π )}) = (πβ(πβ{(π’ + π‘)}))) | ||
Theorem | hdmaprnlem10N 40217* | Lemma for hdmaprnN 40222. Show π is in the range of π. (Contributed by NM, 29-May-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ πΏ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π· β {π})) & β’ (π β π£ β π) & β’ (π β (πβ(πβ{π£})) = (πΏβ{π })) & β’ (π β π’ β π) & β’ (π β Β¬ π’ β (πβ{π£})) & β’ π· = (BaseβπΆ) & β’ π = (0gβπΆ) & β’ 0 = (0gβπ) & β’ β = (+gβπΆ) & β’ + = (+gβπ) β β’ (π β βπ‘ β π (πβπ‘) = π ) | ||
Theorem | hdmaprnlem11N 40218* | Lemma for hdmaprnN 40222. Show π is in the range of π. (Contributed by NM, 29-May-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ πΏ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π· β {π})) & β’ (π β π£ β π) & β’ (π β (πβ(πβ{π£})) = (πΏβ{π })) & β’ (π β π’ β π) & β’ (π β Β¬ π’ β (πβ{π£})) & β’ π· = (BaseβπΆ) & β’ π = (0gβπΆ) & β’ 0 = (0gβπ) & β’ β = (+gβπΆ) & β’ + = (+gβπ) β β’ (π β π β ran π) | ||
Theorem | hdmaprnlem15N 40219* | Lemma for hdmaprnN 40222. Eliminate π’. (Contributed by NM, 30-May-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ 0 = (0gβπΆ) & β’ πΏ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π· β { 0 })) & β’ (π β π£ β π) & β’ (π β (πβ(πβ{π£})) = (πΏβ{π })) β β’ (π β π β ran π) | ||
Theorem | hdmaprnlem16N 40220 | Lemma for hdmaprnN 40222. Eliminate π£. (Contributed by NM, 30-May-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ 0 = (0gβπΆ) & β’ πΏ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π· β { 0 })) β β’ (π β π β ran π) | ||
Theorem | hdmaprnlem17N 40221 | Lemma for hdmaprnN 40222. Include zero. (Contributed by NM, 30-May-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ 0 = (0gβπΆ) & β’ πΏ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π·) β β’ (π β π β ran π) | ||
Theorem | hdmaprnN 40222 | Part of proof of part 12 in [Baer] p. 49 line 21, As=B. (Contributed by NM, 30-May-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β ran π = π·) | ||
Theorem | hdmapf1oN 40223 | Part 12 in [Baer] p. 49. The map from vectors to functionals with closed kernels maps one-to-one onto. Combined with hdmapadd 40201, 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.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β π:πβ1-1-ontoβπ·) | ||
Theorem | hdmap14lem1a 40224 | Prior to part 14 in [Baer] p. 49, line 25. (Contributed by NM, 31-May-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ β = ( Β·π βπΆ) & β’ πΏ = (LSpanβπΆ) & β’ π = (ScalarβπΆ) & β’ π΄ = (Baseβπ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β πΉ β π΅) & β’ 0 = (0gβπ ) & β’ (π β πΉ β 0 ) β β’ (π β (πΏβ{(πβπ)}) = (πΏβ{(πβ(πΉ Β· π))})) | ||
Theorem | hdmap14lem2a 40225* | Prior to part 14 in [Baer] p. 49, line 25. TODO: fix to include πΉ = 0 so it can be used in hdmap14lem10 40235. (Contributed by NM, 31-May-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ β = ( Β·π βπΆ) & β’ πΏ = (LSpanβπΆ) & β’ π = (ScalarβπΆ) & β’ π΄ = (Baseβπ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β πΉ β π΅) β β’ (π β βπ β π΄ (πβ(πΉ Β· π)) = (π β (πβπ))) | ||
Theorem | hdmap14lem1 40226 | Prior to part 14 in [Baer] p. 49, line 25. (Contributed by NM, 31-May-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ 0 = (0gβπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ π = (0gβπ ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ β = ( Β·π βπΆ) & β’ πΏ = (LSpanβπΆ) & β’ π = (ScalarβπΆ) & β’ π΄ = (Baseβπ) & β’ π = (0gβπ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β πΉ β (π΅ β {π})) β β’ (π β (πΏβ{(πβπ)}) = (πΏβ{(πβ(πΉ Β· π))})) | ||
Theorem | hdmap14lem2N 40227* | Prior to part 14 in [Baer] p. 49, line 25. TODO: fix to include πΉ = π so it can be used in hdmap14lem10 40235. (Contributed by NM, 31-May-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ 0 = (0gβπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ π = (0gβπ ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ β = ( Β·π βπΆ) & β’ πΏ = (LSpanβπΆ) & β’ π = (ScalarβπΆ) & β’ π΄ = (Baseβπ) & β’ π = (0gβπ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β πΉ β (π΅ β {π})) β β’ (π β βπ β (π΄ β {π})(πβ(πΉ Β· π)) = (π β (πβπ))) | ||
Theorem | hdmap14lem3 40228* | Prior to part 14 in [Baer] p. 49, line 26. (Contributed by NM, 31-May-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ 0 = (0gβπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ π = (0gβπ ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ β = ( Β·π βπΆ) & β’ πΏ = (LSpanβπΆ) & β’ π = (ScalarβπΆ) & β’ π΄ = (Baseβπ) & β’ π = (0gβπ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β πΉ β (π΅ β {π})) β β’ (π β β!π β (π΄ β {π})(πβ(πΉ Β· π)) = (π β (πβπ))) | ||
Theorem | hdmap14lem4a 40229* | Simplify (π΄ β {π}) in hdmap14lem3 40228 to provide a slightly simpler definition later. (Contributed by NM, 31-May-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ 0 = (0gβπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ π = (0gβπ ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ β = ( Β·π βπΆ) & β’ πΏ = (LSpanβπΆ) & β’ π = (ScalarβπΆ) & β’ π΄ = (Baseβπ) & β’ π = (0gβπ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β πΉ β (π΅ β {π})) β β’ (π β (β!π β (π΄ β {π})(πβ(πΉ Β· π)) = (π β (πβπ)) β β!π β π΄ (πβ(πΉ Β· π)) = (π β (πβπ)))) | ||
Theorem | hdmap14lem4 40230* | Simplify (π΄ β {π}) in hdmap14lem3 40228 to provide a slightly simpler definition later. TODO: Use hdmap14lem4a 40229 if that one is also used directly elsewhere. Otherwise, merge hdmap14lem4a 40229 into this one. (Contributed by NM, 31-May-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ 0 = (0gβπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ π = (0gβπ ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ β = ( Β·π βπΆ) & β’ πΏ = (LSpanβπΆ) & β’ π = (ScalarβπΆ) & β’ π΄ = (Baseβπ) & β’ π = (0gβπ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β πΉ β (π΅ β {π})) β β’ (π β β!π β π΄ (πβ(πΉ Β· π)) = (π β (πβπ))) | ||
Theorem | hdmap14lem6 40231* | Case where πΉ is zero. (Contributed by NM, 1-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ 0 = (0gβπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ π = (0gβπ ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ β = ( Β·π βπΆ) & β’ πΏ = (LSpanβπΆ) & β’ π = (ScalarβπΆ) & β’ π΄ = (Baseβπ) & β’ π = (0gβπ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β πΉ = π) β β’ (π β β!π β π΄ (πβ(πΉ Β· π)) = (π β (πβπ))) | ||
Theorem | hdmap14lem7 40232* | Combine cases of πΉ. TODO: Can this be done at once in hdmap14lem3 40228, in order to get rid of hdmap14lem6 40231? Perhaps modify lspsneu 20507 to become β!π β πΎ instead of β!π β (πΎ β { 0 })? (Contributed by NM, 1-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ 0 = (0gβπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ β = ( Β·π βπΆ) & β’ π = (ScalarβπΆ) & β’ π΄ = (Baseβπ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β πΉ β π΅) β β’ (π β β!π β π΄ (πβ(πΉ Β· π)) = (π β (πβπ))) | ||
Theorem | hdmap14lem8 40233 | Part of proof of part 14 in [Baer] p. 49 lines 33-35. (Contributed by NM, 1-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ β = (+gβπΆ) & β’ β = ( Β·π βπΆ) & β’ π = (ScalarβπΆ) & β’ π΄ = (Baseβπ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΄) & β’ (π β πΌ β π΄) & β’ (π β (πβ(πΉ Β· π)) = (πΊ β (πβπ))) & β’ (π β (πβ(πΉ Β· π)) = (πΌ β (πβπ))) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β π½ β π΄) & β’ (π β (πβ(πΉ Β· (π + π))) = (π½ β (πβ(π + π)))) β β’ (π β ((π½ β (πβπ)) β (π½ β (πβπ))) = ((πΊ β (πβπ)) β (πΌ β (πβπ)))) | ||
Theorem | hdmap14lem9 40234 | Part of proof of part 14 in [Baer] p. 49 line 38. (Contributed by NM, 1-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ β = (+gβπΆ) & β’ β = ( Β·π βπΆ) & β’ π = (ScalarβπΆ) & β’ π΄ = (Baseβπ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΄) & β’ (π β πΌ β π΄) & β’ (π β (πβ(πΉ Β· π)) = (πΊ β (πβπ))) & β’ (π β (πβ(πΉ Β· π)) = (πΌ β (πβπ))) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β π½ β π΄) & β’ (π β (πβ(πΉ Β· (π + π))) = (π½ β (πβ(π + π)))) β β’ (π β πΊ = πΌ) | ||
Theorem | hdmap14lem10 40235 | Part of proof of part 14 in [Baer] p. 49 line 38. (Contributed by NM, 3-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ β = (+gβπΆ) & β’ β = ( Β·π βπΆ) & β’ π = (ScalarβπΆ) & β’ π΄ = (Baseβπ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΄) & β’ (π β πΌ β π΄) & β’ (π β (πβ(πΉ Β· π)) = (πΊ β (πβπ))) & β’ (π β (πβ(πΉ Β· π)) = (πΌ β (πβπ))) & β’ (π β (πβ{π}) β (πβ{π})) β β’ (π β πΊ = πΌ) | ||
Theorem | hdmap14lem11 40236 | Part of proof of part 14 in [Baer] p. 50 line 3. (Contributed by NM, 3-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ β = (+gβπΆ) & β’ β = ( Β·π βπΆ) & β’ π = (ScalarβπΆ) & β’ π΄ = (Baseβπ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΄) & β’ (π β πΌ β π΄) & β’ (π β (πβ(πΉ Β· π)) = (πΊ β (πβπ))) & β’ (π β (πβ(πΉ Β· π)) = (πΌ β (πβπ))) β β’ (π β πΊ = πΌ) | ||
Theorem | hdmap14lem12 40237* | Lemma for proof of part 14 in [Baer] p. 50. (Contributed by NM, 6-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ β = ( Β·π βπΆ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π΅) & β’ π = (ScalarβπΆ) & β’ π΄ = (Baseβπ) & β’ 0 = (0gβπ) & β’ (π β π β (π β { 0 })) & β’ (π β πΊ β π΄) β β’ (π β ((πβ(πΉ Β· π)) = (πΊ β (πβπ)) β βπ¦ β (π β { 0 })(πβ(πΉ Β· π¦)) = (πΊ β (πβπ¦)))) | ||
Theorem | hdmap14lem13 40238* | Lemma for proof of part 14 in [Baer] p. 50. (Contributed by NM, 6-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ β = ( Β·π βπΆ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π΅) & β’ π = (ScalarβπΆ) & β’ π΄ = (Baseβπ) & β’ 0 = (0gβπ) & β’ (π β π β (π β { 0 })) & β’ (π β πΊ β π΄) β β’ (π β ((πβ(πΉ Β· π)) = (πΊ β (πβπ)) β βπ¦ β π (πβ(πΉ Β· π¦)) = (πΊ β (πβπ¦)))) | ||
Theorem | hdmap14lem14 40239* | Part of proof of part 14 in [Baer] p. 50 line 3. (Contributed by NM, 6-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ β = ( Β·π βπΆ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π΅) & β’ π = (ScalarβπΆ) & β’ π΄ = (Baseβπ) β β’ (π β β!π β π΄ βπ₯ β π (πβ(πΉ Β· π₯)) = (π β (πβπ₯))) | ||
Theorem | hdmap14lem15 40240* | 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.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ β = ( Β·π βπΆ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π΅) β β’ (π β β!π β π΅ βπ₯ β π (πβ(πΉ Β· π₯)) = (π β (πβπ₯))) | ||
Syntax | chg 40241 | Extend class notation with g-map. |
class HGMap | ||
Definition | df-hgmap 40242* | 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 = (π β V β¦ (π€ β (LHypβπ) β¦ {π β£ [((DVecHβπ)βπ€) / π’][(Baseβ(Scalarβπ’)) / π][((HDMapβπ)βπ€) / π]π β (π₯ β π β¦ (β©π¦ β π βπ£ β (Baseβπ’)(πβ(π₯( Β·π βπ’)π£)) = (π¦( Β·π β((LCDualβπ)βπ€))(πβπ£))))})) | ||
Theorem | hgmapffval 40243* | 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.) |
β’ π» = (LHypβπΎ) β β’ (πΎ β π β (HGMapβπΎ) = (π€ β π» β¦ {π β£ [((DVecHβπΎ)βπ€) / π’][(Baseβ(Scalarβπ’)) / π][((HDMapβπΎ)βπ€) / π]π β (π₯ β π β¦ (β©π¦ β π βπ£ β (Baseβπ’)(πβ(π₯( Β·π βπ’)π£)) = (π¦( Β·π β((LCDualβπΎ)βπ€))(πβπ£))))})) | ||
Theorem | hgmapfval 40244* | 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.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ β = ( Β·π βπΆ) & β’ π = ((HDMapβπΎ)βπ) & β’ πΌ = ((HGMapβπΎ)βπ) & β’ (π β (πΎ β π β§ π β π»)) β β’ (π β πΌ = (π₯ β π΅ β¦ (β©π¦ β π΅ βπ£ β π (πβ(π₯ Β· π£)) = (π¦ β (πβπ£))))) | ||
Theorem | hgmapval 40245* | 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 40240. (Contributed by NM, 25-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ β = ( Β·π βπΆ) & β’ π = ((HDMapβπΎ)βπ) & β’ πΌ = ((HGMapβπΎ)βπ) & β’ (π β (πΎ β π β§ π β π»)) & β’ (π β π β π΅) β β’ (π β (πΌβπ) = (β©π¦ β π΅ βπ£ β π (πβ(π Β· π£)) = (π¦ β (πβπ£)))) | ||
Theorem | hgmapfnN 40246 | Functionality of scalar sigma map. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ πΊ = ((HGMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β πΊ Fn π΅) | ||
Theorem | hgmapcl 40247 | 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.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ πΊ = ((HGMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π΅) β β’ (π β (πΊβπΉ) β π΅) | ||
Theorem | hgmapdcl 40248 | Closure of the vector space to dual space scalar map, in the scalar sigma map. (Contributed by NM, 6-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π = (ScalarβπΆ) & β’ π΄ = (Baseβπ) & β’ πΊ = ((HGMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π΅) β β’ (π β (πΊβπΉ) β π΄) | ||
Theorem | hgmapvs 40249 | Part 15 of [Baer] p. 50 line 6. Also line 15 in [Holland95] p. 14. (Contributed by NM, 6-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ β = ( Β·π βπΆ) & β’ π = ((HDMapβπΎ)βπ) & β’ πΊ = ((HGMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β πΉ β π΅) β β’ (π β (πβ(πΉ Β· π)) = ((πΊβπΉ) β (πβπ))) | ||
Theorem | hgmapval0 40250 | Value of the scalar sigma map at zero. (Contributed by NM, 12-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Scalarβπ) & β’ 0 = (0gβπ ) & β’ πΊ = ((HGMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β (πΊβ 0 ) = 0 ) | ||
Theorem | hgmapval1 40251 | Value of the scalar sigma map at one. (Contributed by NM, 12-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Scalarβπ) & β’ 1 = (1rβπ ) & β’ πΊ = ((HGMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β (πΊβ 1 ) = 1 ) | ||
Theorem | hgmapadd 40252 | Part 15 of [Baer] p. 50 line 13. (Contributed by NM, 6-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) & β’ πΊ = ((HGMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (πΊβ(π + π)) = ((πΊβπ) + (πΊβπ))) | ||
Theorem | hgmapmul 40253 | 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.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ πΊ = ((HGMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (πΊβ(π Β· π)) = ((πΊβπ) Β· (πΊβπ))) | ||
Theorem | hgmaprnlem1N 40254 | Lemma for hgmaprnN 40259. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ Β· = ( Β·π βπ) & β’ 0 = (0gβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (ScalarβπΆ) & β’ π΄ = (Baseβπ) & β’ β = ( Β·π βπΆ) & β’ π = (0gβπΆ) & β’ π = ((HDMapβπΎ)βπ) & β’ πΊ = ((HGMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π§ β π΄) & β’ (π β π‘ β (π β { 0 })) & β’ (π β π β π) & β’ (π β (πβπ ) = (π§ β (πβπ‘))) & β’ (π β π β π΅) & β’ (π β π = (π Β· π‘)) β β’ (π β π§ β ran πΊ) | ||
Theorem | hgmaprnlem2N 40255 | Lemma for hgmaprnN 40259. 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.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ Β· = ( Β·π βπ) & β’ 0 = (0gβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (ScalarβπΆ) & β’ π΄ = (Baseβπ) & β’ β = ( Β·π βπΆ) & β’ π = (0gβπΆ) & β’ π = ((HDMapβπΎ)βπ) & β’ πΊ = ((HGMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π§ β π΄) & β’ (π β π‘ β (π β { 0 })) & β’ (π β π β π) & β’ (π β (πβπ ) = (π§ β (πβπ‘))) & β’ π = ((mapdβπΎ)βπ) & β’ π = (LSpanβπ) & β’ πΏ = (LSpanβπΆ) β β’ (π β (πβ{π }) β (πβ{π‘})) | ||
Theorem | hgmaprnlem3N 40256* | Lemma for hgmaprnN 40259. Eliminate π. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ Β· = ( Β·π βπ) & β’ 0 = (0gβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (ScalarβπΆ) & β’ π΄ = (Baseβπ) & β’ β = ( Β·π βπΆ) & β’ π = (0gβπΆ) & β’ π = ((HDMapβπΎ)βπ) & β’ πΊ = ((HGMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π§ β π΄) & β’ (π β π‘ β (π β { 0 })) & β’ (π β π β π) & β’ (π β (πβπ ) = (π§ β (πβπ‘))) & β’ π = ((mapdβπΎ)βπ) & β’ π = (LSpanβπ) & β’ πΏ = (LSpanβπΆ) β β’ (π β π§ β ran πΊ) | ||
Theorem | hgmaprnlem4N 40257* | Lemma for hgmaprnN 40259. Eliminate π . (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ Β· = ( Β·π βπ) & β’ 0 = (0gβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (ScalarβπΆ) & β’ π΄ = (Baseβπ) & β’ β = ( Β·π βπΆ) & β’ π = (0gβπΆ) & β’ π = ((HDMapβπΎ)βπ) & β’ πΊ = ((HGMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π§ β π΄) & β’ (π β π‘ β (π β { 0 })) β β’ (π β π§ β ran πΊ) | ||
Theorem | hgmaprnlem5N 40258 | Lemma for hgmaprnN 40259. Eliminate π‘. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ Β· = ( Β·π βπ) & β’ 0 = (0gβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (ScalarβπΆ) & β’ π΄ = (Baseβπ) & β’ β = ( Β·π βπΆ) & β’ π = (0gβπΆ) & β’ π = ((HDMapβπΎ)βπ) & β’ πΊ = ((HGMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π§ β π΄) β β’ (π β π§ β ran πΊ) | ||
Theorem | hgmaprnN 40259 | 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.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ πΊ = ((HGMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β ran πΊ = π΅) | ||
Theorem | hgmap11 40260 | The scalar sigma map is one-to-one. (Contributed by NM, 7-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ πΊ = ((HGMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β ((πΊβπ) = (πΊβπ) β π = π)) | ||
Theorem | hgmapf1oN 40261 | The scalar sigma map is a one-to-one onto function. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ πΊ = ((HGMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β πΊ:π΅β1-1-ontoβπ΅) | ||
Theorem | hgmapeq0 40262 | The scalar sigma map is zero iff its argument is zero. (Contributed by NM, 12-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ πΊ = ((HGMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π΅) β β’ (π β ((πΊβπ) = 0 β π = 0 )) | ||
Theorem | hdmapipcl 40263 | The inner product (Hermitian form) (π, π) will be defined as ((πβπ)βπ). Show closure. (Contributed by NM, 7-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β ((πβπ)βπ) β π΅) | ||
Theorem | hdmapln1 40264 | Linearity property that will be used for inner product. TODO: try to combine hypotheses in hdmap*ln* series. (Contributed by NM, 7-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & ⒠⨣ = (+gβπ ) & β’ Γ = (.rβπ ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π΄ β π΅) β β’ (π β ((πβπ)β((π΄ Β· π) + π)) = ((π΄ Γ ((πβπ)βπ)) ⨣ ((πβπ)βπ))) | ||
Theorem | hdmaplna1 40265 | Additive property of first (inner product) argument. (Contributed by NM, 11-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ π = (Scalarβπ) & ⒠⨣ = (+gβπ ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β ((πβπ)β(π + π)) = (((πβπ)βπ) ⨣ ((πβπ)βπ))) | ||
Theorem | hdmaplns1 40266 | Subtraction property of first (inner product) argument. (Contributed by NM, 12-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (Scalarβπ) & β’ π = (-gβπ ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β ((πβπ)β(π β π)) = (((πβπ)βπ)π((πβπ)βπ))) | ||
Theorem | hdmaplnm1 40267 | Multiplicative property of first (inner product) argument. (Contributed by NM, 11-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ Γ = (.rβπ ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π΄ β π΅) β β’ (π β ((πβπ)β(π΄ Β· π)) = (π΄ Γ ((πβπ)βπ))) | ||
Theorem | hdmaplna2 40268 | Additive property of second (inner product) argument. (Contributed by NM, 10-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ π = (Scalarβπ) & ⒠⨣ = (+gβπ ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β ((πβ(π + π))βπ) = (((πβπ)βπ) ⨣ ((πβπ)βπ))) | ||
Theorem | hdmapglnm2 40269 | g-linear property of second (inner product) argument. Line 19 in [Holland95] p. 14. (Contributed by NM, 10-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ Γ = (.rβπ ) & β’ π = ((HDMapβπΎ)βπ) & β’ πΊ = ((HGMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π΄ β π΅) β β’ (π β ((πβ(π΄ Β· π))βπ) = (((πβπ)βπ) Γ (πΊβπ΄))) | ||
Theorem | hdmapgln2 40270 | g-linear property that will be used for inner product. (Contributed by NM, 14-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & ⒠⨣ = (+gβπ ) & β’ Γ = (.rβπ ) & β’ π = ((HDMapβπΎ)βπ) & β’ πΊ = ((HGMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π΄ β π΅) β β’ (π β ((πβ((π΄ Β· π) + π))βπ) = ((((πβπ)βπ) Γ (πΊβπ΄)) ⨣ ((πβπ)βπ))) | ||
Theorem | hdmaplkr 40271 | Kernel of the vector to dual map. Line 16 in [Holland95] p. 14. TODO: eliminate πΉ hypothesis. (Contributed by NM, 9-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ πΉ = (LFnlβπ) & β’ π = (LKerβπ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) β β’ (π β (πβ(πβπ)) = (πβ{π})) | ||
Theorem | hdmapellkr 40272 | Membership in the kernel (as shown by hdmaplkr 40271) of the vector to dual map. Line 17 in [Holland95] p. 14. (Contributed by NM, 16-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (Scalarβπ) & β’ 0 = (0gβπ ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (((πβπ)βπ) = 0 β π β (πβ{π}))) | ||
Theorem | hdmapip0 40273 | Zero property that will be used for inner product. (Contributed by NM, 9-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ π = (Scalarβπ) & β’ π = (0gβπ ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) β β’ (π β (((πβπ)βπ) = π β π = 0 )) | ||
Theorem | hdmapip1 40274 | Construct a proportional vector π whose inner product with the original π equals one. (Contributed by NM, 13-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ 0 = (0gβπ) & β’ π = (Scalarβπ) & β’ 1 = (1rβπ ) & β’ π = (invrβπ ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ π = ((πβ((πβπ)βπ)) Β· π) β β’ (π β ((πβπ)βπ) = 1 ) | ||
Theorem | hdmapip0com 40275 | 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.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (Scalarβπ) & β’ 0 = (0gβπ ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (((πβπ)βπ) = 0 β ((πβπ)βπ) = 0 )) | ||
Theorem | hdmapinvlem1 40276 | Line 27 in [Baer] p. 110. We use πΆ for Baer's u. Our unit vector πΈ has the required properties for his w by hdmapevec2 40194. Our ((πβπΈ)βπΆ) means the inner product β¨πΆ, πΈβ© i.e. his f(u,w) (note argument reversal). (Contributed by NM, 11-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ πΈ = β¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β© & β’ π = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 0 = (0gβπ ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΆ β (πβ{πΈ})) β β’ (π β ((πβπΈ)βπΆ) = 0 ) | ||
Theorem | hdmapinvlem2 40277 | Line 28 in [Baer] p. 110, 0 = f(w,u). (Contributed by NM, 11-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ πΈ = β¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β© & β’ π = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 0 = (0gβπ ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΆ β (πβ{πΈ})) β β’ (π β ((πβπΆ)βπΈ) = 0 ) | ||
Theorem | hdmapinvlem3 40278 | Line 30 in [Baer] p. 110, f(sw + u, tw - v) = 0. (Contributed by NM, 12-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ πΈ = β¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β© & β’ π = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ β = (-gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ Γ = (.rβπ ) & β’ 0 = (0gβπ ) & β’ π = ((HDMapβπΎ)βπ) & β’ πΊ = ((HGMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΆ β (πβ{πΈ})) & β’ (π β π· β (πβ{πΈ})) & β’ (π β πΌ β π΅) & β’ (π β π½ β π΅) & β’ (π β (πΌ Γ (πΊβπ½)) = ((πβπ·)βπΆ)) β β’ (π β ((πβ((π½ Β· πΈ) β π·))β((πΌ Β· πΈ) + πΆ)) = 0 ) | ||
Theorem | hdmapinvlem4 40279 | 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 40194. Our ((πβπ·)βπΆ) means his f(u,v) (note argument reversal). (Contributed by NM, 12-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ πΈ = β¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β© & β’ π = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ β = (-gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ Γ = (.rβπ ) & β’ 0 = (0gβπ ) & β’ π = ((HDMapβπΎ)βπ) & β’ πΊ = ((HGMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΆ β (πβ{πΈ})) & β’ (π β π· β (πβ{πΈ})) & β’ (π β πΌ β π΅) & β’ (π β π½ β π΅) & β’ (π β (πΌ Γ (πΊβπ½)) = ((πβπ·)βπΆ)) β β’ (π β (π½ Γ (πΊβπΌ)) = ((πβπΆ)βπ·)) | ||
Theorem | hdmapglem5 40280 | Part 1.2 in [Baer] p. 110 line 34, f(u,v) alpha = f(v,u). (Contributed by NM, 12-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ πΈ = β¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β© & β’ π = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ β = (-gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ Γ = (.rβπ ) & β’ 0 = (0gβπ ) & β’ π = ((HDMapβπΎ)βπ) & β’ πΊ = ((HGMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΆ β (πβ{πΈ})) & β’ (π β π· β (πβ{πΈ})) & β’ (π β πΌ β π΅) & β’ (π β π½ β π΅) β β’ (π β (πΊβ((πβπ·)βπΆ)) = ((πβπΆ)βπ·)) | ||
Theorem | hgmapvvlem1 40281 | Involution property of scalar sigma map. Line 10 in [Baer] p. 111, t sigma squared = t. Our πΈ, πΆ, π·, π, π correspond to Baer's w, h, k, s, t. (Contributed by NM, 13-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ πΈ = β¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β© & β’ π = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ Γ = (.rβπ ) & β’ 0 = (0gβπ ) & β’ 1 = (1rβπ ) & β’ π = (invrβπ ) & β’ π = ((HDMapβπΎ)βπ) & β’ πΊ = ((HGMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π΅ β { 0 })) & β’ (π β πΆ β (πβ{πΈ})) & β’ (π β π· β (πβ{πΈ})) & β’ (π β ((πβπ·)βπΆ) = 1 ) & β’ (π β π β (π΅ β { 0 })) & β’ (π β (π Γ (πΊβπ)) = 1 ) β β’ (π β (πΊβ(πΊβπ)) = π) | ||
Theorem | hgmapvvlem2 40282 | Lemma for hgmapvv 40284. Eliminate π (Baer's s). (Contributed by NM, 13-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ πΈ = β¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β© & β’ π = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ Γ = (.rβπ ) & β’ 0 = (0gβπ ) & β’ 1 = (1rβπ ) & β’ π = (invrβπ ) & β’ π = ((HDMapβπΎ)βπ) & β’ πΊ = ((HGMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π΅ β { 0 })) & β’ (π β πΆ β (πβ{πΈ})) & β’ (π β π· β (πβ{πΈ})) & β’ (π β ((πβπ·)βπΆ) = 1 ) β β’ (π β (πΊβ(πΊβπ)) = π) | ||
Theorem | hgmapvvlem3 40283 | Lemma for hgmapvv 40284. Eliminate ((πβπ·)βπΆ) = 1 (Baer's f(h,k)=1). (Contributed by NM, 13-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ πΈ = β¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β© & β’ π = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ Γ = (.rβπ ) & β’ 0 = (0gβπ ) & β’ 1 = (1rβπ ) & β’ π = (invrβπ ) & β’ π = ((HDMapβπΎ)βπ) & β’ πΊ = ((HGMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π΅ β { 0 })) β β’ (π β (πΊβ(πΊβπ)) = π) | ||
Theorem | hgmapvv 40284 | Value of a double involution. Part 1.2 of [Baer] p. 110 line 37. (Contributed by NM, 13-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ πΊ = ((HGMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π΅) β β’ (π β (πΊβ(πΊβπ)) = π) | ||
Theorem | hdmapglem7a 40285* | Lemma for hdmapg 40288. (Contributed by NM, 14-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ πΈ = β¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β© & β’ π = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) β β’ (π β βπ’ β (πβ{πΈ})βπ β π΅ π = ((π Β· πΈ) + π’)) | ||
Theorem | hdmapglem7b 40286 | Lemma for hdmapg 40288. (Contributed by NM, 14-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ πΈ = β¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β© & β’ π = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ Γ = (.rβπ ) & β’ 0 = (0gβπ ) & β’ β = (+gβπ ) & β’ π = ((HDMapβπΎ)βπ) & β’ πΊ = ((HGMapβπΎ)βπ) & β’ (π β π₯ β (πβ{πΈ})) & β’ (π β π¦ β (πβ{πΈ})) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β ((πβ((π Β· πΈ) + π₯))β((π Β· πΈ) + π¦)) = ((π Γ (πΊβπ)) β ((πβπ₯)βπ¦))) | ||
Theorem | hdmapglem7 40287 | Lemma for hdmapg 40288. Line 15 in [Baer] p. 111, f(x,y) alpha = f(y,x). In the proof, our πΈ, (πβ{πΈ}), π, π, π, π’, π, and π£ correspond respectively to Baer's w, H, x, y, x', x'', y', and y'', and our ((πβπ)βπ) corresponds to Baer's f(x,y). (Contributed by NM, 14-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ πΈ = β¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β© & β’ π = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ Γ = (.rβπ ) & β’ 0 = (0gβπ ) & β’ β = (+gβπ ) & β’ π = ((HDMapβπΎ)βπ) & β’ πΊ = ((HGMapβπΎ)βπ) & β’ (π β π β π) β β’ (π β (πΊβ((πβπ)βπ)) = ((πβπ)βπ)) | ||
Theorem | hdmapg 40288 | Apply the scalar sigma function (involution) πΊ to an inner product reverses the arguments. The inner product of π and π is represented by ((πβπ)βπ). Line 15 in [Baer] p. 111, f(x,y) alpha = f(y,x). (Contributed by NM, 14-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = ((HDMapβπΎ)βπ) & β’ πΊ = ((HGMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (πΊβ((πβπ)βπ)) = ((πβπ)βπ)) | ||
Theorem | hdmapoc 40289* | Express our constructed orthocomplement (polarity) in terms of the Hilbert space definition of orthocomplement. Lines 24 and 25 in [Holland95] p. 14. (Contributed by NM, 17-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (Scalarβπ) & β’ 0 = (0gβπ ) & β’ π = ((ocHβπΎ)βπ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) β β’ (π β (πβπ) = {π¦ β π β£ βπ§ β π ((πβπ§)βπ¦) = 0 }) | ||
Syntax | chlh 40290 | Extend class notation with the final constructed Hilbert space. |
class HLHil | ||
Definition | df-hlhil 40291* | Define our final Hilbert space constructed from a Hilbert lattice. (Contributed by NM, 21-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) |
β’ HLHil = (π β V β¦ (π€ β (LHypβπ) β¦ β¦((DVecHβπ)βπ€) / π’β¦β¦(Baseβπ’) / π£β¦({β¨(Baseβndx), π£β©, β¨(+gβndx), (+gβπ’)β©, β¨(Scalarβndx), (((EDRingβπ)βπ€) sSet β¨(*πβndx), ((HGMapβπ)βπ€)β©)β©} βͺ {β¨( Β·π βndx), ( Β·π βπ’)β©, β¨(Β·πβndx), (π₯ β π£, π¦ β π£ β¦ ((((HDMapβπ)βπ€)βπ¦)βπ₯))β©}))) | ||
Theorem | hlhilset 40292* | The final Hilbert space constructed from a Hilbert lattice πΎ and an arbitrary hyperplane π in πΎ. (Contributed by NM, 21-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ πΏ = ((HLHilβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ πΈ = ((EDRingβπΎ)βπ) & β’ πΊ = ((HGMapβπΎ)βπ) & β’ π = (πΈ sSet β¨(*πβndx), πΊβ©) & β’ Β· = ( Β·π βπ) & β’ π = ((HDMapβπΎ)βπ) & β’ , = (π₯ β π, π¦ β π β¦ ((πβπ¦)βπ₯)) & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β πΏ = ({β¨(Baseβndx), πβ©, β¨(+gβndx), + β©, β¨(Scalarβndx), π β©} βͺ {β¨( Β·π βndx), Β· β©, β¨(Β·πβndx), , β©})) | ||
Theorem | hlhilsca 40293 | The scalar of the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((HLHilβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ πΈ = ((EDRingβπΎ)βπ) & β’ πΊ = ((HGMapβπΎ)βπ) & β’ π = (πΈ sSet β¨(*πβndx), πΊβ©) β β’ (π β π = (Scalarβπ)) | ||
Theorem | hlhilbase 40294 | The base set of the final constructed Hilbert space. (Contributed by NM, 21-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((HLHilβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ πΏ = ((DVecHβπΎ)βπ) & β’ π = (BaseβπΏ) β β’ (π β π = (Baseβπ)) | ||
Theorem | hlhilplus 40295 | The vector addition for the final constructed Hilbert space. (Contributed by NM, 21-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((HLHilβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ πΏ = ((DVecHβπΎ)βπ) & β’ + = (+gβπΏ) β β’ (π β + = (+gβπ)) | ||
Theorem | hlhilslem 40296 | Lemma for hlhilsbase 40298 etc. (Contributed by Mario Carneiro, 28-Jun-2015.) (Revised by AV, 6-Nov-2024.) |
β’ π» = (LHypβπΎ) & β’ πΈ = ((EDRingβπΎ)βπ) & β’ π = ((HLHilβπΎ)βπ) & β’ π = (Scalarβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ πΉ = Slot (πΉβndx) & β’ (πΉβndx) β (*πβndx) & β’ πΆ = (πΉβπΈ) β β’ (π β πΆ = (πΉβπ )) | ||
Theorem | hlhilslemOLD 40297 | Obsolete version of hlhilslem 40296 as of 6-Nov-2024. Lemma for hlhilsbase 40298. (Contributed by Mario Carneiro, 28-Jun-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π» = (LHypβπΎ) & β’ πΈ = ((EDRingβπΎ)βπ) & β’ π = ((HLHilβπΎ)βπ) & β’ π = (Scalarβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ πΉ = Slot π & β’ π β β & β’ π < 4 & β’ πΆ = (πΉβπΈ) β β’ (π β πΆ = (πΉβπ )) | ||
Theorem | hlhilsbase 40298 | The scalar base set of the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) (Revised by AV, 6-Nov-2024.) |
β’ π» = (LHypβπΎ) & β’ πΈ = ((EDRingβπΎ)βπ) & β’ π = ((HLHilβπΎ)βπ) & β’ π = (Scalarβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ πΆ = (BaseβπΈ) β β’ (π β πΆ = (Baseβπ )) | ||
Theorem | hlhilsbaseOLD 40299 | Obsolete version of hlhilsbase 40298 as of 6-Nov-2024. The scalar base set of the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π» = (LHypβπΎ) & β’ πΈ = ((EDRingβπΎ)βπ) & β’ π = ((HLHilβπΎ)βπ) & β’ π = (Scalarβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ πΆ = (BaseβπΈ) β β’ (π β πΆ = (Baseβπ )) | ||
Theorem | hlhilsplus 40300 | Scalar addition for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) (Revised by AV, 6-Nov-2024.) |
β’ π» = (LHypβπΎ) & β’ πΈ = ((EDRingβπΎ)βπ) & β’ π = ((HLHilβπΎ)βπ) & β’ π = (Scalarβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ + = (+gβπΈ) β β’ (π β + = (+gβπ )) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |