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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | hdmaprnlem4tN 40201 | Lemma for hdmaprnN 40213. 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 40202 | 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 40203 | 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 40204 | 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 40205 | 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 40206 | 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 39988 and mapdcnv11N 40008. 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 40207* | Lemma for hdmaprnN 40213. (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 40208* | Lemma for hdmaprnN 40213. 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 40209* | Lemma for hdmaprnN 40213. 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 40210* | Lemma for hdmaprnN 40213. 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 40211 | Lemma for hdmaprnN 40213. 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 40212 | Lemma for hdmaprnN 40213. 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 40213 | 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 40214 | Part 12 in [Baer] p. 49. The map from vectors to functionals with closed kernels maps one-to-one onto. Combined with hdmapadd 40192, 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 40215 | 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 40216* | Prior to part 14 in [Baer] p. 49, line 25. TODO: fix to include πΉ = 0 so it can be used in hdmap14lem10 40226. (Contributed by NM, 31-May-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ β = ( Β·π βπΆ) & β’ πΏ = (LSpanβπΆ) & β’ π = (ScalarβπΆ) & β’ π΄ = (Baseβπ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β πΉ β π΅) β β’ (π β βπ β π΄ (πβ(πΉ Β· π)) = (π β (πβπ))) | ||
Theorem | hdmap14lem1 40217 | 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 40218* | Prior to part 14 in [Baer] p. 49, line 25. TODO: fix to include πΉ = π so it can be used in hdmap14lem10 40226. (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 40219* | 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 40220* | Simplify (π΄ β {π}) in hdmap14lem3 40219 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 40221* | Simplify (π΄ β {π}) in hdmap14lem3 40219 to provide a slightly simpler definition later. TODO: Use hdmap14lem4a 40220 if that one is also used directly elsewhere. Otherwise, merge hdmap14lem4a 40220 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 40222* | 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 40223* | Combine cases of πΉ. TODO: Can this be done at once in hdmap14lem3 40219, in order to get rid of hdmap14lem6 40222? 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 40224 | 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 40225 | 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 40226 | 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 40227 | 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 40228* | 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 40229* | 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 40230* | 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 40231* | 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 40232 | Extend class notation with g-map. |
class HGMap | ||
Definition | df-hgmap 40233* | 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 40234* | 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 40235* | 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 40236* | 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 40231. (Contributed by NM, 25-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ β = ( Β·π βπΆ) & β’ π = ((HDMapβπΎ)βπ) & β’ πΌ = ((HGMapβπΎ)βπ) & β’ (π β (πΎ β π β§ π β π»)) & β’ (π β π β π΅) β β’ (π β (πΌβπ) = (β©π¦ β π΅ βπ£ β π (πβ(π Β· π£)) = (π¦ β (πβπ£)))) | ||
Theorem | hgmapfnN 40237 | Functionality of scalar sigma map. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ πΊ = ((HGMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β πΊ Fn π΅) | ||
Theorem | hgmapcl 40238 | 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 40239 | 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 40240 | 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 40241 | 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 40242 | 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 40243 | Part 15 of [Baer] p. 50 line 13. (Contributed by NM, 6-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) & β’ πΊ = ((HGMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (πΊβ(π + π)) = ((πΊβπ) + (πΊβπ))) | ||
Theorem | hgmapmul 40244 | 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 40245 | Lemma for hgmaprnN 40250. (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 40246 | Lemma for hgmaprnN 40250. 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 40247* | Lemma for hgmaprnN 40250. 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 40248* | Lemma for hgmaprnN 40250. 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 40249 | Lemma for hgmaprnN 40250. 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 40250 | 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 40251 | The scalar sigma map is one-to-one. (Contributed by NM, 7-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ πΊ = ((HGMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β ((πΊβπ) = (πΊβπ) β π = π)) | ||
Theorem | hgmapf1oN 40252 | 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 40253 | 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 40254 | 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 40255 | 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 40256 | Additive property of first (inner product) argument. (Contributed by NM, 11-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ π = (Scalarβπ) & ⒠⨣ = (+gβπ ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β ((πβπ)β(π + π)) = (((πβπ)βπ) ⨣ ((πβπ)βπ))) | ||
Theorem | hdmaplns1 40257 | Subtraction property of first (inner product) argument. (Contributed by NM, 12-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (Scalarβπ) & β’ π = (-gβπ ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β ((πβπ)β(π β π)) = (((πβπ)βπ)π((πβπ)βπ))) | ||
Theorem | hdmaplnm1 40258 | Multiplicative property of first (inner product) argument. (Contributed by NM, 11-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ Γ = (.rβπ ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π΄ β π΅) β β’ (π β ((πβπ)β(π΄ Β· π)) = (π΄ Γ ((πβπ)βπ))) | ||
Theorem | hdmaplna2 40259 | Additive property of second (inner product) argument. (Contributed by NM, 10-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ π = (Scalarβπ) & ⒠⨣ = (+gβπ ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β ((πβ(π + π))βπ) = (((πβπ)βπ) ⨣ ((πβπ)βπ))) | ||
Theorem | hdmapglnm2 40260 | 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 40261 | 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 40262 | 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 40263 | Membership in the kernel (as shown by hdmaplkr 40262) 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 40264 | 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 40265 | 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 40266 | 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 40267 | Line 27 in [Baer] p. 110. We use πΆ for Baer's u. Our unit vector πΈ has the required properties for his w by hdmapevec2 40185. 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 40268 | 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 40269 | 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 40270 | 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 40185. 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 40271 | 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 40272 | 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 40273 | Lemma for hgmapvv 40275. 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 40274 | Lemma for hgmapvv 40275. 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 40275 | 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 40276* | Lemma for hdmapg 40279. (Contributed by NM, 14-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ πΈ = β¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β© & β’ π = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) β β’ (π β βπ’ β (πβ{πΈ})βπ β π΅ π = ((π Β· πΈ) + π’)) | ||
Theorem | hdmapglem7b 40277 | Lemma for hdmapg 40279. (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 40278 | Lemma for hdmapg 40279. 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 40279 | 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 40280* | 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 40281 | Extend class notation with the final constructed Hilbert space. |
class HLHil | ||
Definition | df-hlhil 40282* | 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 40283* | 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 40284 | 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 40285 | 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 40286 | The vector addition for the final constructed Hilbert space. (Contributed by NM, 21-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((HLHilβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ πΏ = ((DVecHβπΎ)βπ) & β’ + = (+gβπΏ) β β’ (π β + = (+gβπ)) | ||
Theorem | hlhilslem 40287 | Lemma for hlhilsbase 40289 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 40288 | Obsolete version of hlhilslem 40287 as of 6-Nov-2024. Lemma for hlhilsbase 40289. (Contributed by Mario Carneiro, 28-Jun-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π» = (LHypβπΎ) & β’ πΈ = ((EDRingβπΎ)βπ) & β’ π = ((HLHilβπΎ)βπ) & β’ π = (Scalarβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ πΉ = Slot π & β’ π β β & β’ π < 4 & β’ πΆ = (πΉβπΈ) β β’ (π β πΆ = (πΉβπ )) | ||
Theorem | hlhilsbase 40289 | 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 40290 | Obsolete version of hlhilsbase 40289 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 40291 | 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βπ )) | ||
Theorem | hlhilsplusOLD 40292 | Obsolete version of hlhilsplus 40291 as of 6-Nov-2024. The scalar addition for 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 β§ π β π»)) & β’ + = (+gβπΈ) β β’ (π β + = (+gβπ )) | ||
Theorem | hlhilsmul 40293 | Scalar multiplication 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 β§ π β π»)) & β’ Β· = (.rβπΈ) β β’ (π β Β· = (.rβπ )) | ||
Theorem | hlhilsmulOLD 40294 | Obsolete version of hlhilsmul 40293 as of 6-Nov-2024. The scalar multiplication for 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 β§ π β π»)) & β’ Β· = (.rβπΈ) β β’ (π β Β· = (.rβπ )) | ||
Theorem | hlhilsbase2 40295 | The scalar base set of the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ πΏ = ((DVecHβπΎ)βπ) & β’ π = (ScalarβπΏ) & β’ π = ((HLHilβπΎ)βπ) & β’ π = (Scalarβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ πΆ = (Baseβπ) β β’ (π β πΆ = (Baseβπ )) | ||
Theorem | hlhilsplus2 40296 | Scalar addition for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ πΏ = ((DVecHβπΎ)βπ) & β’ π = (ScalarβπΏ) & β’ π = ((HLHilβπΎ)βπ) & β’ π = (Scalarβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ + = (+gβπ) β β’ (π β + = (+gβπ )) | ||
Theorem | hlhilsmul2 40297 | Scalar multiplication for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ πΏ = ((DVecHβπΎ)βπ) & β’ π = (ScalarβπΏ) & β’ π = ((HLHilβπΎ)βπ) & β’ π = (Scalarβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ Β· = (.rβπ) β β’ (π β Β· = (.rβπ )) | ||
Theorem | hlhils0 40298 | The scalar ring zero for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 29-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ πΏ = ((DVecHβπΎ)βπ) & β’ π = (ScalarβπΏ) & β’ π = ((HLHilβπΎ)βπ) & β’ π = (Scalarβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ 0 = (0gβπ) β β’ (π β 0 = (0gβπ )) | ||
Theorem | hlhils1N 40299 | The scalar ring unity for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 29-Jun-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ πΏ = ((DVecHβπΎ)βπ) & β’ π = (ScalarβπΏ) & β’ π = ((HLHilβπΎ)βπ) & β’ π = (Scalarβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ 1 = (1rβπ) β β’ (π β 1 = (1rβπ )) | ||
Theorem | hlhilvsca 40300 | The scalar product for the final constructed Hilbert space. (Contributed by NM, 21-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ πΏ = ((DVecHβπΎ)βπ) & β’ Β· = ( Β·π βπΏ) & β’ π = ((HLHilβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β Β· = ( Β·π βπ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |