![]() |
Metamath
Proof Explorer Theorem List (p. 408 of 479) | < 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: | ![]() (1-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | hdmapcl 40701 | Closure of map from vectors to functionals with closed kernels. (Contributed by NM, 15-May-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) β β’ (π β (πβπ) β π·) | ||
Theorem | hdmapval2lem 40702* | Lemma for hdmapval2 40703. (Contributed by NM, 15-May-2015.) |
β’ π» = (LHypβπΎ) & β’ πΈ = β¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β© & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π½ = ((HVMapβπΎ)βπ) & β’ πΌ = ((HDMap1βπΎ)βπ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β πΉ β π·) β β’ (π β ((πβπ) = πΉ β βπ§ β π (Β¬ π§ β ((πβ{πΈ}) βͺ (πβ{π})) β πΉ = (πΌββ¨π§, (πΌββ¨πΈ, (π½βπΈ), π§β©), πβ©)))) | ||
Theorem | hdmapval2 40703 | Value of map from vectors to functionals with a specific auxiliary vector. TODO: Would shorter proofs result if the .ne hypothesis were changed to two β hypothesis? Consider hdmaplem1 40642 through hdmaplem4 40645, which would become obsolete. (Contributed by NM, 15-May-2015.) |
β’ π» = (LHypβπΎ) & β’ πΈ = β¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β© & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π½ = ((HVMapβπΎ)βπ) & β’ πΌ = ((HDMap1βπΎ)βπ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β Β¬ π β ((πβ{πΈ}) βͺ (πβ{π}))) β β’ (π β (πβπ) = (πΌββ¨π, (πΌββ¨πΈ, (π½βπΈ), πβ©), πβ©)) | ||
Theorem | hdmapval0 40704 | Value of map from vectors to functionals at zero. Note: we use dvh3dim 40317 for convenience, even though 3 dimensions aren't necessary at this point. TODO: I think either this or hdmapeq0 40715 could be derived from the other to shorten proof. (Contributed by NM, 17-May-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ 0 = (0gβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π = (0gβπΆ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β (πβ 0 ) = π) | ||
Theorem | hdmapeveclem 40705 | Lemma for hdmapevec 40706. TODO: combine with hdmapevec 40706 if it shortens overall. (Contributed by NM, 16-May-2015.) |
β’ π» = (LHypβπΎ) & β’ πΈ = β¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β© & β’ π½ = ((HVMapβπΎ)βπ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ πΌ = ((HDMap1βπΎ)βπ) & β’ (π β π β π) & β’ (π β Β¬ π β ((πβ{πΈ}) βͺ (πβ{πΈ}))) β β’ (π β (πβπΈ) = (π½βπΈ)) | ||
Theorem | hdmapevec 40706 | Value of map from vectors to functionals at the reference vector πΈ. (Contributed by NM, 16-May-2015.) |
β’ π» = (LHypβπΎ) & β’ πΈ = β¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β© & β’ π½ = ((HVMapβπΎ)βπ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β (πβπΈ) = (π½βπΈ)) | ||
Theorem | hdmapevec2 40707 | The inner product of the reference vector πΈ with itself is nonzero. This shows the inner product condition in the proof of Theorem 3.6 of [Holland95] p. 14 line 32, [ e , e ] β 0 is satisfied. TODO: remove redundant hypothesis hdmapevec.j. (Contributed by NM, 1-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ πΈ = β¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β© & β’ π½ = ((HVMapβπΎ)βπ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Scalarβπ) & β’ 1 = (1rβπ ) β β’ (π β ((πβπΈ)βπΈ) = 1 ) | ||
Theorem | hdmapval3lemN 40708 | Value of map from vectors to functionals at arguments not colinear with the reference vector πΈ. (Contributed by NM, 17-May-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ πΈ = β¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β© & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π½ = ((HVMapβπΎ)βπ) & β’ πΌ = ((HDMap1βπΎ)βπ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β (πβ{π}) β (πβ{πΈ})) & β’ (π β π β (π β {(0gβπ)})) & β’ (π β π₯ β π) & β’ (π β Β¬ π₯ β (πβ{πΈ, π})) β β’ (π β (πβπ) = (πΌββ¨πΈ, (π½βπΈ), πβ©)) | ||
Theorem | hdmapval3N 40709 | Value of map from vectors to functionals at arguments not colinear with the reference vector πΈ. (Contributed by NM, 17-May-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ πΈ = β¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β© & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π½ = ((HVMapβπΎ)βπ) & β’ πΌ = ((HDMap1βπΎ)βπ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β (πβ{π}) β (πβ{πΈ})) & β’ (π β π β π) β β’ (π β (πβπ) = (πΌββ¨πΈ, (π½βπΈ), πβ©)) | ||
Theorem | hdmap10lem 40710 | Lemma for hdmap10 40711. (Contributed by NM, 17-May-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ πΏ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ πΈ = β¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β© & β’ 0 = (0gβπ) & β’ π· = (BaseβπΆ) & β’ π½ = ((HVMapβπΎ)βπ) & β’ πΌ = ((HDMap1βπΎ)βπ) & β’ (π β π β (π β { 0 })) β β’ (π β (πβ(πβ{π})) = (πΏβ{(πβπ)})) | ||
Theorem | hdmap10 40711 | Part 10 in [Baer] p. 48 line 33, (Ft)* = G(tS) in their notation (S = sigma). (Contributed by NM, 17-May-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ πΏ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) β β’ (π β (πβ(πβ{π})) = (πΏβ{(πβπ)})) | ||
Theorem | hdmap11lem1 40712 | Lemma for hdmapadd 40714. (Contributed by NM, 26-May-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ β = (+gβπΆ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ πΈ = β¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β© & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ π· = (BaseβπΆ) & β’ πΏ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ π½ = ((HVMapβπΎ)βπ) & β’ πΌ = ((HDMap1βπΎ)βπ) & β’ (π β π§ β π) & β’ (π β Β¬ π§ β (πβ{π, π})) & β’ (π β (πβ{π§}) β (πβ{πΈ})) β β’ (π β (πβ(π + π)) = ((πβπ) β (πβπ))) | ||
Theorem | hdmap11lem2 40713 | Lemma for hdmapadd 40714. (Contributed by NM, 26-May-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ β = (+gβπΆ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ πΈ = β¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β© & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ π· = (BaseβπΆ) & β’ πΏ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ π½ = ((HVMapβπΎ)βπ) & β’ πΌ = ((HDMap1βπΎ)βπ) β β’ (π β (πβ(π + π)) = ((πβπ) β (πβπ))) | ||
Theorem | hdmapadd 40714 | 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 40715 | 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 40716 | 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 40717 | 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 40718 | 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 40719 | 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 40720 | 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 40721 | 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 40722 | 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 40723 | Lemma for hdmaprnN 40735. 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 40724 | 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 40725 | 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 40726 | 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 40727 | 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 40728 | 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 40510 and mapdcnv11N 40530. 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 40729* | Lemma for hdmaprnN 40735. (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 40730* | Lemma for hdmaprnN 40735. 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 40731* | Lemma for hdmaprnN 40735. 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 40732* | Lemma for hdmaprnN 40735. 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 40733 | Lemma for hdmaprnN 40735. 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 40734 | Lemma for hdmaprnN 40735. 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 40735 | 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 40736 | Part 12 in [Baer] p. 49. The map from vectors to functionals with closed kernels maps one-to-one onto. Combined with hdmapadd 40714, 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 40737 | 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 40738* | Prior to part 14 in [Baer] p. 49, line 25. TODO: fix to include πΉ = 0 so it can be used in hdmap14lem10 40748. (Contributed by NM, 31-May-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ β = ( Β·π βπΆ) & β’ πΏ = (LSpanβπΆ) & β’ π = (ScalarβπΆ) & β’ π΄ = (Baseβπ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β πΉ β π΅) β β’ (π β βπ β π΄ (πβ(πΉ Β· π)) = (π β (πβπ))) | ||
Theorem | hdmap14lem1 40739 | 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 40740* | Prior to part 14 in [Baer] p. 49, line 25. TODO: fix to include πΉ = π so it can be used in hdmap14lem10 40748. (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 40741* | 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 40742* | Simplify (π΄ β {π}) in hdmap14lem3 40741 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 40743* | Simplify (π΄ β {π}) in hdmap14lem3 40741 to provide a slightly simpler definition later. TODO: Use hdmap14lem4a 40742 if that one is also used directly elsewhere. Otherwise, merge hdmap14lem4a 40742 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 40744* | 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 40745* | Combine cases of πΉ. TODO: Can this be done at once in hdmap14lem3 40741, in order to get rid of hdmap14lem6 40744? Perhaps modify lspsneu 20736 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 40746 | 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 40747 | 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 40748 | 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 40749 | 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 40750* | 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 40751* | 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 40752* | 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 40753* | 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 40754 | Extend class notation with g-map. |
class HGMap | ||
Definition | df-hgmap 40755* | 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 40756* | 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 40757* | 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 40758* | 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 40753. (Contributed by NM, 25-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ β = ( Β·π βπΆ) & β’ π = ((HDMapβπΎ)βπ) & β’ πΌ = ((HGMapβπΎ)βπ) & β’ (π β (πΎ β π β§ π β π»)) & β’ (π β π β π΅) β β’ (π β (πΌβπ) = (β©π¦ β π΅ βπ£ β π (πβ(π Β· π£)) = (π¦ β (πβπ£)))) | ||
Theorem | hgmapfnN 40759 | Functionality of scalar sigma map. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ πΊ = ((HGMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β πΊ Fn π΅) | ||
Theorem | hgmapcl 40760 | 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 40761 | 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 40762 | 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 40763 | 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 40764 | 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 40765 | Part 15 of [Baer] p. 50 line 13. (Contributed by NM, 6-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) & β’ πΊ = ((HGMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (πΊβ(π + π)) = ((πΊβπ) + (πΊβπ))) | ||
Theorem | hgmapmul 40766 | 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 40767 | Lemma for hgmaprnN 40772. (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 40768 | Lemma for hgmaprnN 40772. 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 40769* | Lemma for hgmaprnN 40772. 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 40770* | Lemma for hgmaprnN 40772. 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 40771 | Lemma for hgmaprnN 40772. 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 40772 | 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 40773 | The scalar sigma map is one-to-one. (Contributed by NM, 7-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ πΊ = ((HGMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β ((πΊβπ) = (πΊβπ) β π = π)) | ||
Theorem | hgmapf1oN 40774 | 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 40775 | 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 40776 | 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 40777 | 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 40778 | Additive property of first (inner product) argument. (Contributed by NM, 11-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ π = (Scalarβπ) & ⒠⨣ = (+gβπ ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β ((πβπ)β(π + π)) = (((πβπ)βπ) ⨣ ((πβπ)βπ))) | ||
Theorem | hdmaplns1 40779 | Subtraction property of first (inner product) argument. (Contributed by NM, 12-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (Scalarβπ) & β’ π = (-gβπ ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β ((πβπ)β(π β π)) = (((πβπ)βπ)π((πβπ)βπ))) | ||
Theorem | hdmaplnm1 40780 | Multiplicative property of first (inner product) argument. (Contributed by NM, 11-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ Γ = (.rβπ ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π΄ β π΅) β β’ (π β ((πβπ)β(π΄ Β· π)) = (π΄ Γ ((πβπ)βπ))) | ||
Theorem | hdmaplna2 40781 | Additive property of second (inner product) argument. (Contributed by NM, 10-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ π = (Scalarβπ) & ⒠⨣ = (+gβπ ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β ((πβ(π + π))βπ) = (((πβπ)βπ) ⨣ ((πβπ)βπ))) | ||
Theorem | hdmapglnm2 40782 | 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 40783 | 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 40784 | 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 40785 | Membership in the kernel (as shown by hdmaplkr 40784) 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 40786 | 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 40787 | 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 40788 | 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 40789 | Line 27 in [Baer] p. 110. We use πΆ for Baer's u. Our unit vector πΈ has the required properties for his w by hdmapevec2 40707. 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 40790 | 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 40791 | 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 40792 | 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 40707. 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 40793 | 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 40794 | 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 40795 | Lemma for hgmapvv 40797. 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 40796 | Lemma for hgmapvv 40797. 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 40797 | 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 40798* | Lemma for hdmapg 40801. (Contributed by NM, 14-Jun-2015.) |
β’ π» = (LHypβπΎ) & β’ πΈ = β¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β© & β’ π = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) β β’ (π β βπ’ β (πβ{πΈ})βπ β π΅ π = ((π Β· πΈ) + π’)) | ||
Theorem | hdmapglem7b 40799 | Lemma for hdmapg 40801. (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 40800 | Lemma for hdmapg 40801. 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βπΎ)βπ) & β’ (π β π β π) β β’ (π β (πΊβ((πβπ)βπ)) = ((πβπ)βπ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |