![]() |
Metamath
Proof Explorer Theorem List (p. 413 of 482) | < 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-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | chdma1 41201 | Extend class notation with preliminary map from vectors to functionals in the closed kernel dual space. |
class HDMap1 | ||
Syntax | chdma 41202 | Extend class notation with map from vectors to functionals in the closed kernel dual space. |
class HDMap | ||
Definition | df-hdmap1 41203* | Define preliminary map from vectors to functionals in the closed kernel dual space. See hdmap1fval 41206 description for more details. (Contributed by NM, 14-May-2015.) |
β’ HDMap1 = (π β V β¦ (π€ β (LHypβπ) β¦ {π β£ [((DVecHβπ)βπ€) / π’][(Baseβπ’) / π£][(LSpanβπ’) / π][((LCDualβπ)βπ€) / π][(Baseβπ) / π][(LSpanβπ) / π][((mapdβπ)βπ€) / π]π β (π₯ β ((π£ Γ π) Γ π£) β¦ if((2nd βπ₯) = (0gβπ’), (0gβπ), (β©β β π ((πβ(πβ{(2nd βπ₯)})) = (πβ{β}) β§ (πβ(πβ{((1st β(1st βπ₯))(-gβπ’)(2nd βπ₯))})) = (πβ{((2nd β(1st βπ₯))(-gβπ)β)})))))})) | ||
Definition | df-hdmap 41204* | Define map from vectors to functionals in the closed kernel dual space. See hdmapfval 41237 description for more details. (Contributed by NM, 15-May-2015.) |
β’ HDMap = (π β V β¦ (π€ β (LHypβπ) β¦ {π β£ [β¨( I βΎ (Baseβπ)), ( I βΎ ((LTrnβπ)βπ€))β© / π][((DVecHβπ)βπ€) / π’][(Baseβπ’) / π£][((HDMap1βπ)βπ€) / π]π β (π‘ β π£ β¦ (β©π¦ β (Baseβ((LCDualβπ)βπ€))βπ§ β π£ (Β¬ π§ β (((LSpanβπ’)β{π}) βͺ ((LSpanβπ’)β{π‘})) β π¦ = (πββ¨π§, (πββ¨π, (((HVMapβπ)βπ€)βπ), π§β©), π‘β©))))})) | ||
Theorem | hdmap1ffval 41205* | Preliminary map from vectors to functionals in the closed kernel dual space. (Contributed by NM, 14-May-2015.) |
β’ π» = (LHypβπΎ) β β’ (πΎ β π β (HDMap1βπΎ) = (π€ β π» β¦ {π β£ [((DVecHβπΎ)βπ€) / π’][(Baseβπ’) / π£][(LSpanβπ’) / π][((LCDualβπΎ)βπ€) / π][(Baseβπ) / π][(LSpanβπ) / π][((mapdβπΎ)βπ€) / π]π β (π₯ β ((π£ Γ π) Γ π£) β¦ if((2nd βπ₯) = (0gβπ’), (0gβπ), (β©β β π ((πβ(πβ{(2nd βπ₯)})) = (πβ{β}) β§ (πβ(πβ{((1st β(1st βπ₯))(-gβπ’)(2nd βπ₯))})) = (πβ{((2nd β(1st βπ₯))(-gβπ)β)})))))})) | ||
Theorem | hdmap1fval 41206* | Preliminary map from vectors to functionals in the closed kernel dual space. TODO: change span π½ to the convention πΏ for this section. (Contributed by NM, 15-May-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π = (0gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ πΌ = ((HDMap1βπΎ)βπ) & β’ (π β (πΎ β π΄ β§ π β π»)) β β’ (π β πΌ = (π₯ β ((π Γ π·) Γ π) β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)})))))) | ||
Theorem | hdmap1vallem 41207* | Value of preliminary map from vectors to functionals in the closed kernel dual space. (Contributed by NM, 15-May-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π = (0gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ πΌ = ((HDMap1βπΎ)βπ) & β’ (π β (πΎ β π΄ β§ π β π»)) & β’ (π β π β ((π Γ π·) Γ π)) β β’ (π β (πΌβπ) = if((2nd βπ) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ)) β (2nd βπ))})) = (π½β{((2nd β(1st βπ))π β)}))))) | ||
Theorem | hdmap1val 41208* | Value of preliminary map from vectors to functionals in the closed kernel dual space. (Restatement of mapdhval 41134.) TODO: change πΌ = (π₯ β V β¦... to (π β (πΌββ¨π, πΉ, π > ) =... in e.g. mapdh8 41198 to shorten proofs with no $d on π₯. (Contributed by NM, 15-May-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π = (0gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ πΌ = ((HDMap1βπΎ)βπ) & β’ (π β (πΎ β π΄ β§ π β π»)) & β’ (π β π β π) & β’ (π β πΉ β π·) & β’ (π β π β π) β β’ (π β (πΌββ¨π, πΉ, πβ©) = if(π = 0 , π, (β©β β π· ((πβ(πβ{π})) = (π½β{β}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΉπ β)}))))) | ||
Theorem | hdmap1val0 41209 | Value of preliminary map from vectors to functionals at zero. (Restated mapdhval0 41135.) (Contributed by NM, 17-May-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (0gβπΆ) & β’ πΌ = ((HDMap1βπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β π β π) β β’ (π β (πΌββ¨π, πΉ, 0 β©) = π) | ||
Theorem | hdmap1val2 41210* | Value of preliminary map from vectors to functionals in the closed kernel dual space, for nonzero π. (Contributed by NM, 16-May-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ πΏ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ πΌ = ((HDMap1βπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β πΉ β π·) & β’ (π β π β (π β { 0 })) β β’ (π β (πΌββ¨π, πΉ, πβ©) = (β©β β π· ((πβ(πβ{π})) = (πΏβ{β}) β§ (πβ(πβ{(π β π)})) = (πΏβ{(πΉπ β)})))) | ||
Theorem | hdmap1eq 41211 | The defining equation for h(x,x',y)=y' in part (2) in [Baer] p. 45 line 24. (Contributed by NM, 16-May-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ πΏ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ πΌ = ((HDMap1βπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β πΉ β π·) & β’ (π β π β (π β { 0 })) & β’ (π β πΊ β π·) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{π})) = (πΏβ{πΉ})) β β’ (π β ((πΌββ¨π, πΉ, πβ©) = πΊ β ((πβ(πβ{π})) = (πΏβ{πΊ}) β§ (πβ(πβ{(π β π)})) = (πΏβ{(πΉπ πΊ)})))) | ||
Theorem | hdmap1cbv 41212* | Frequently used lemma to change bound variables in πΏ hypothesis. (Contributed by NM, 15-May-2015.) |
β’ πΏ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) β β’ πΏ = (π¦ β V β¦ if((2nd βπ¦) = 0 , π, (β©π β π· ((πβ(πβ{(2nd βπ¦)})) = (π½β{π}) β§ (πβ(πβ{((1st β(1st βπ¦)) β (2nd βπ¦))})) = (π½β{((2nd β(1st βπ¦))π π)}))))) | ||
Theorem | hdmap1valc 41213* | Connect the value of the preliminary map from vectors to functionals πΌ to the hypothesis πΏ used by earlier theorems. Note: the π β (π β { 0 }) hypothesis could be the more general π β π but the former will be easier to use. TODO: use the πΌ function directly in those theorems, so this theorem becomes unnecessary? TODO: The hdmap1cbv 41212 is probably unnecessary, but it would mean different $d's later on. (Contributed by NM, 15-May-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π = (0gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ πΌ = ((HDMap1βπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β πΉ β π·) & β’ (π β π β π) & β’ πΏ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) β β’ (π β (πΌββ¨π, πΉ, πβ©) = (πΏββ¨π, πΉ, πβ©)) | ||
Theorem | hdmap1cl 41214 | Convert closure theorem mapdhcl 41137 to use HDMap1 function. (Contributed by NM, 15-May-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ πΏ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ πΌ = ((HDMap1βπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β (πβ(πβ{π})) = (πΏβ{πΉ})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β π) β β’ (π β (πΌββ¨π, πΉ, πβ©) β π·) | ||
Theorem | hdmap1eq2 41215 | Convert mapdheq2 41139 to use HDMap1 function. (Contributed by NM, 16-May-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ πΏ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ πΌ = ((HDMap1βπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β (πβ(πβ{π})) = (πΏβ{πΉ})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β (πΌββ¨π, πΉ, πβ©) = πΊ) β β’ (π β (πΌββ¨π, πΊ, πβ©) = πΉ) | ||
Theorem | hdmap1eq4N 41216 | Convert mapdheq4 41142 to use HDMap1 function. (Contributed by NM, 17-May-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ πΏ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ πΌ = ((HDMap1βπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β (πβ(πβ{π})) = (πΏβ{πΉ})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πΌββ¨π, πΉ, πβ©) = πΊ) & β’ (π β (πΌββ¨π, πΉ, πβ©) = π΅) β β’ (π β (πΌββ¨π, πΊ, πβ©) = π΅) | ||
Theorem | hdmap1l6lem1 41217 | Lemma for hdmap1l6 41231. Part (6) in [Baer] p. 47, lines 16-18. (Contributed by NM, 13-Apr-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ β = (+gβπΆ) & β’ π = (-gβπΆ) & β’ π = (0gβπΆ) & β’ πΏ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ πΌ = ((HDMap1βπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β π β (π β { 0 })) & β’ (π β (πβ(πβ{π})) = (πΏβ{πΉ})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πΌββ¨π, πΉ, πβ©) = πΊ) & β’ (π β (πΌββ¨π, πΉ, πβ©) = πΈ) β β’ (π β (πβ(πβ{(π β (π + π))})) = (πΏβ{(πΉπ (πΊ β πΈ))})) | ||
Theorem | hdmap1l6lem2 41218 | Lemma for hdmap1l6 41231. Part (6) in [Baer] p. 47, lines 20-22. (Contributed by NM, 13-Apr-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ β = (+gβπΆ) & β’ π = (-gβπΆ) & β’ π = (0gβπΆ) & β’ πΏ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ πΌ = ((HDMap1βπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β π β (π β { 0 })) & β’ (π β (πβ(πβ{π})) = (πΏβ{πΉ})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πΌββ¨π, πΉ, πβ©) = πΊ) & β’ (π β (πΌββ¨π, πΉ, πβ©) = πΈ) β β’ (π β (πβ(πβ{(π + π)})) = (πΏβ{(πΊ β πΈ)})) | ||
Theorem | hdmap1l6a 41219 | Lemma for hdmap1l6 41231. Part (6) in [Baer] p. 47, case 1. (Contributed by NM, 23-Apr-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ β = (+gβπΆ) & β’ π = (-gβπΆ) & β’ π = (0gβπΆ) & β’ πΏ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ πΌ = ((HDMap1βπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β π β (π β { 0 })) & β’ (π β (πβ(πβ{π})) = (πΏβ{πΉ})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πΌββ¨π, πΉ, πβ©) = πΊ) & β’ (π β (πΌββ¨π, πΉ, πβ©) = πΈ) β β’ (π β (πΌββ¨π, πΉ, (π + π)β©) = ((πΌββ¨π, πΉ, πβ©) β (πΌββ¨π, πΉ, πβ©))) | ||
Theorem | hdmap1l6b0N 41220 | Lemmma for hdmap1l6 41231. (Contributed by NM, 23-Apr-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ β = (+gβπΆ) & β’ π = (-gβπΆ) & β’ π = (0gβπΆ) & β’ πΏ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ πΌ = ((HDMap1βπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β π β (π β { 0 })) & β’ (π β (πβ(πβ{π})) = (πΏβ{πΉ})) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β ((πβ{π}) β© (πβ{π, π})) = { 0 }) β β’ (π β Β¬ π β (πβ{π, π})) | ||
Theorem | hdmap1l6b 41221 | Lemmma for hdmap1l6 41231. (Contributed by NM, 24-Apr-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ β = (+gβπΆ) & β’ π = (-gβπΆ) & β’ π = (0gβπΆ) & β’ πΏ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ πΌ = ((HDMap1βπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β π β (π β { 0 })) & β’ (π β (πβ(πβ{π})) = (πΏβ{πΉ})) & β’ (π β π = 0 ) & β’ (π β π β π) & β’ (π β Β¬ π β (πβ{π, π})) β β’ (π β (πΌββ¨π, πΉ, (π + π)β©) = ((πΌββ¨π, πΉ, πβ©) β (πΌββ¨π, πΉ, πβ©))) | ||
Theorem | hdmap1l6c 41222 | Lemmma for hdmap1l6 41231. (Contributed by NM, 24-Apr-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ β = (+gβπΆ) & β’ π = (-gβπΆ) & β’ π = (0gβπΆ) & β’ πΏ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ πΌ = ((HDMap1βπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β π β (π β { 0 })) & β’ (π β (πβ(πβ{π})) = (πΏβ{πΉ})) & β’ (π β π β π) & β’ (π β π = 0 ) & β’ (π β Β¬ π β (πβ{π, π})) β β’ (π β (πΌββ¨π, πΉ, (π + π)β©) = ((πΌββ¨π, πΉ, πβ©) β (πΌββ¨π, πΉ, πβ©))) | ||
Theorem | hdmap1l6d 41223 | Lemmma for hdmap1l6 41231. (Contributed by NM, 1-May-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ β = (+gβπΆ) & β’ π = (-gβπΆ) & β’ π = (0gβπΆ) & β’ πΏ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ πΌ = ((HDMap1βπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β π β (π β { 0 })) & β’ (π β (πβ(πβ{π})) = (πΏβ{πΉ})) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) = (πβ{π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π€ β (π β { 0 })) & β’ (π β Β¬ π€ β (πβ{π, π})) β β’ (π β (πΌββ¨π, πΉ, (π€ + (π + π))β©) = ((πΌββ¨π, πΉ, π€β©) β (πΌββ¨π, πΉ, (π + π)β©))) | ||
Theorem | hdmap1l6e 41224 | Lemmma for hdmap1l6 41231. Part (6) in [Baer] p. 47 line 38. (Contributed by NM, 1-May-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ β = (+gβπΆ) & β’ π = (-gβπΆ) & β’ π = (0gβπΆ) & β’ πΏ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ πΌ = ((HDMap1βπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β π β (π β { 0 })) & β’ (π β (πβ(πβ{π})) = (πΏβ{πΉ})) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) = (πβ{π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π€ β (π β { 0 })) & β’ (π β Β¬ π€ β (πβ{π, π})) β β’ (π β (πΌββ¨π, πΉ, ((π€ + π) + π)β©) = ((πΌββ¨π, πΉ, (π€ + π)β©) β (πΌββ¨π, πΉ, πβ©))) | ||
Theorem | hdmap1l6f 41225 | Lemmma for hdmap1l6 41231. Part (6) in [Baer] p. 47 line 38. (Contributed by NM, 1-May-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ β = (+gβπΆ) & β’ π = (-gβπΆ) & β’ π = (0gβπΆ) & β’ πΏ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ πΌ = ((HDMap1βπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β π β (π β { 0 })) & β’ (π β (πβ(πβ{π})) = (πΏβ{πΉ})) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) = (πβ{π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π€ β (π β { 0 })) & β’ (π β Β¬ π€ β (πβ{π, π})) β β’ (π β (πΌββ¨π, πΉ, (π€ + π)β©) = ((πΌββ¨π, πΉ, π€β©) β (πΌββ¨π, πΉ, πβ©))) | ||
Theorem | hdmap1l6g 41226 | Lemmma for hdmap1l6 41231. Part (6) of [Baer] p. 47 line 39. (Contributed by NM, 1-May-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ β = (+gβπΆ) & β’ π = (-gβπΆ) & β’ π = (0gβπΆ) & β’ πΏ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ πΌ = ((HDMap1βπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β π β (π β { 0 })) & β’ (π β (πβ(πβ{π})) = (πΏβ{πΉ})) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) = (πβ{π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π€ β (π β { 0 })) & β’ (π β Β¬ π€ β (πβ{π, π})) β β’ (π β ((πΌββ¨π, πΉ, π€β©) β (πΌββ¨π, πΉ, (π + π)β©)) = (((πΌββ¨π, πΉ, π€β©) β (πΌββ¨π, πΉ, πβ©)) β (πΌββ¨π, πΉ, πβ©))) | ||
Theorem | hdmap1l6h 41227 | Lemmma for hdmap1l6 41231. Part (6) of [Baer] p. 48 line 2. (Contributed by NM, 1-May-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ β = (+gβπΆ) & β’ π = (-gβπΆ) & β’ π = (0gβπΆ) & β’ πΏ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ πΌ = ((HDMap1βπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β π β (π β { 0 })) & β’ (π β (πβ(πβ{π})) = (πΏβ{πΉ})) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) = (πβ{π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π€ β (π β { 0 })) & β’ (π β Β¬ π€ β (πβ{π, π})) β β’ (π β (πΌββ¨π, πΉ, (π + π)β©) = ((πΌββ¨π, πΉ, πβ©) β (πΌββ¨π, πΉ, πβ©))) | ||
Theorem | hdmap1l6i 41228 | Lemmma for hdmap1l6 41231. Eliminate auxiliary vector π€. (Contributed by NM, 1-May-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ β = (+gβπΆ) & β’ π = (-gβπΆ) & β’ π = (0gβπΆ) & β’ πΏ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ πΌ = ((HDMap1βπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β π β (π β { 0 })) & β’ (π β (πβ(πβ{π})) = (πΏβ{πΉ})) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β (πβ{π}) = (πβ{π})) β β’ (π β (πΌββ¨π, πΉ, (π + π)β©) = ((πΌββ¨π, πΉ, πβ©) β (πΌββ¨π, πΉ, πβ©))) | ||
Theorem | hdmap1l6j 41229 | Lemmma for hdmap1l6 41231. Eliminate (π { Y } ) = ( N {π}) hypothesis. (Contributed by NM, 1-May-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ β = (+gβπΆ) & β’ π = (-gβπΆ) & β’ π = (0gβπΆ) & β’ πΏ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ πΌ = ((HDMap1βπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β π β (π β { 0 })) & β’ (π β (πβ(πβ{π})) = (πΏβ{πΉ})) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) β β’ (π β (πΌββ¨π, πΉ, (π + π)β©) = ((πΌββ¨π, πΉ, πβ©) β (πΌββ¨π, πΉ, πβ©))) | ||
Theorem | hdmap1l6k 41230 | Lemmma for hdmap1l6 41231. Eliminate nonzero vector requirement. (Contributed by NM, 1-May-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ β = (+gβπΆ) & β’ π = (-gβπΆ) & β’ π = (0gβπΆ) & β’ πΏ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ πΌ = ((HDMap1βπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β π β (π β { 0 })) & β’ (π β (πβ(πβ{π})) = (πΏβ{πΉ})) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β Β¬ π β (πβ{π, π})) β β’ (π β (πΌββ¨π, πΉ, (π + π)β©) = ((πΌββ¨π, πΉ, πβ©) β (πΌββ¨π, πΉ, πβ©))) | ||
Theorem | hdmap1l6 41231 | Part (6) of [Baer] p. 47 line 6. Note that we use Β¬ π β (πβ{π, π}) which is equivalent to Baer's "Fx β© (Fy + Fz)" by lspdisjb 21003. (Convert mapdh6N 41157 to use the function HDMap1.) (Contributed by NM, 17-May-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ β = (+gβπΆ) & β’ πΏ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ πΌ = ((HDMap1βπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β π β (π β { 0 })) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ(πβ{π})) = (πΏβ{πΉ})) β β’ (π β (πΌββ¨π, πΉ, (π + π)β©) = ((πΌββ¨π, πΉ, πβ©) β (πΌββ¨π, πΉ, πβ©))) | ||
Theorem | hdmap1eulem 41232* | Lemma for hdmap1eu 41234. TODO: combine with hdmap1eu 41234 or at least share some hypotheses. (Contributed by NM, 15-May-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π = (0gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ πΌ = ((HDMap1βπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) & β’ (π β π β (π β { 0 })) & β’ (π β πΉ β π·) & β’ (π β π β π) & β’ πΏ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) β β’ (π β β!π¦ β π· βπ§ β π (Β¬ π§ β ((πβ{π}) βͺ (πβ{π})) β π¦ = (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©))) | ||
Theorem | hdmap1eulemOLDN 41233* | Lemma for hdmap1euOLDN 41235. TODO: combine with hdmap1euOLDN 41235 or at least share some hypotheses. (Contributed by NM, 15-May-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π = (0gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ πΌ = ((HDMap1βπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) & β’ (π β π β (π β { 0 })) & β’ (π β πΉ β π·) & β’ (π β π β π) & β’ πΏ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) β β’ (π β β!π¦ β π· βπ§ β π (Β¬ π§ β (πβ{π, π}) β π¦ = (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©))) | ||
Theorem | hdmap1eu 41234* | Convert mapdh9a 41199 to use the HDMap1 notation. (Contributed by NM, 15-May-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ πΏ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ πΌ = ((HDMap1βπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β (πβ(πβ{π})) = (πΏβ{πΉ})) & β’ (π β π β (π β { 0 })) & β’ (π β πΉ β π·) & β’ (π β π β π) β β’ (π β β!π¦ β π· βπ§ β π (Β¬ π§ β ((πβ{π}) βͺ (πβ{π})) β π¦ = (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©))) | ||
Theorem | hdmap1euOLDN 41235* | Convert mapdh9aOLDN 41200 to use the HDMap1 notation. (Contributed by NM, 15-May-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ πΏ = (LSpanβπΆ) & β’ π = ((mapdβπΎ)βπ) & β’ πΌ = ((HDMap1βπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β (πβ(πβ{π})) = (πΏβ{πΉ})) & β’ (π β π β (π β { 0 })) & β’ (π β πΉ β π·) & β’ (π β π β π) β β’ (π β β!π¦ β π· βπ§ β π (Β¬ π§ β (πβ{π, π}) β π¦ = (πΌββ¨π§, (πΌββ¨π, πΉ, π§β©), πβ©))) | ||
Theorem | hdmapffval 41236* | Map from vectors to functionals in the closed kernel dual space. (Contributed by NM, 15-May-2015.) |
β’ π» = (LHypβπΎ) β β’ (πΎ β π β (HDMapβπΎ) = (π€ β π» β¦ {π β£ [β¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ€))β© / π][((DVecHβπΎ)βπ€) / π’][(Baseβπ’) / π£][((HDMap1βπΎ)βπ€) / π]π β (π‘ β π£ β¦ (β©π¦ β (Baseβ((LCDualβπΎ)βπ€))βπ§ β π£ (Β¬ π§ β (((LSpanβπ’)β{π}) βͺ ((LSpanβπ’)β{π‘})) β π¦ = (πββ¨π§, (πββ¨π, (((HVMapβπΎ)βπ€)βπ), π§β©), π‘β©))))})) | ||
Theorem | hdmapfval 41237* | Map from vectors to functionals in the closed kernel dual space. (Contributed by NM, 15-May-2015.) |
β’ π» = (LHypβπΎ) & β’ πΈ = β¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β© & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π½ = ((HVMapβπΎ)βπ) & β’ πΌ = ((HDMap1βπΎ)βπ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β π΄ β§ π β π»)) β β’ (π β π = (π‘ β π β¦ (β©π¦ β π· βπ§ β π (Β¬ π§ β ((πβ{πΈ}) βͺ (πβ{π‘})) β π¦ = (πΌββ¨π§, (πΌββ¨πΈ, (π½βπΈ), π§β©), π‘β©))))) | ||
Theorem | hdmapval 41238* | Value of map from vectors to functionals in the closed kernel dual space. This is the function sigma on line 27 above part 9 in [Baer] p. 48. We select a convenient fixed reference vector πΈ to be β¨0, 1β© (corresponding to vector u on p. 48 line 7) whose span is the lattice isomorphism map of the fiducial atom π = ((ocβπΎ)βπ) (see dvheveccl 40522). (π½βπΈ) is a fixed reference functional determined by this vector (corresponding to u' on line 8; mapdhvmap 41179 shows in Baer's notation (Fu)* = Gu'). Baer's independent vectors v and w on line 7 correspond to our π§ that the βπ§ β π ranges over. The middle term (πΌββ¨πΈ, (π½βπΈ), π§β©) provides isolation to allow πΈ and π to assume the same value without conflict. Closure is shown by hdmapcl 41240. If a separate auxiliary vector is known, hdmapval2 41242 provides a version without quantification. (Contributed by NM, 15-May-2015.) |
β’ π» = (LHypβπΎ) & β’ πΈ = β¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β© & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π½ = ((HVMapβπΎ)βπ) & β’ πΌ = ((HDMap1βπΎ)βπ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β π΄ β§ π β π»)) & β’ (π β π β π) β β’ (π β (πβπ) = (β©π¦ β π· βπ§ β π (Β¬ π§ β ((πβ{πΈ}) βͺ (πβ{π})) β π¦ = (πΌββ¨π§, (πΌββ¨πΈ, (π½βπΈ), π§β©), πβ©)))) | ||
Theorem | hdmapfnN 41239 | Functionality of map from vectors to functionals with closed kernels. (Contributed by NM, 30-May-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β π Fn π) | ||
Theorem | hdmapcl 41240 | 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 41241* | Lemma for hdmapval2 41242. (Contributed by NM, 15-May-2015.) |
β’ π» = (LHypβπΎ) & β’ πΈ = β¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β© & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π½ = ((HVMapβπΎ)βπ) & β’ πΌ = ((HDMap1βπΎ)βπ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β πΉ β π·) β β’ (π β ((πβπ) = πΉ β βπ§ β π (Β¬ π§ β ((πβ{πΈ}) βͺ (πβ{π})) β πΉ = (πΌββ¨π§, (πΌββ¨πΈ, (π½βπΈ), π§β©), πβ©)))) | ||
Theorem | hdmapval2 41242 | 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 41181 through hdmaplem4 41184, 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 41243 | Value of map from vectors to functionals at zero. Note: we use dvh3dim 40856 for convenience, even though 3 dimensions aren't necessary at this point. TODO: I think either this or hdmapeq0 41254 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 41244 | Lemma for hdmapevec 41245. TODO: combine with hdmapevec 41245 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 41245 | 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 41246 | 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 41247 | 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 41248 | 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 41249 | Lemma for hdmap10 41250. (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 41250 | 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 41251 | Lemma for hdmapadd 41253. (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 41252 | Lemma for hdmapadd 41253. (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 41253 | 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 41254 | 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 41255 | 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 41256 | 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 41257 | 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 41258 | 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 41259 | 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 41260 | 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 41261 | 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 41262 | Lemma for hdmaprnN 41274. 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 41263 | 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 41264 | 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 41265 | 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 41266 | 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 41267 | 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 41049 and mapdcnv11N 41069. 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 41268* | Lemma for hdmaprnN 41274. (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 41269* | Lemma for hdmaprnN 41274. 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 41270* | Lemma for hdmaprnN 41274. 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 41271* | Lemma for hdmaprnN 41274. 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 41272 | Lemma for hdmaprnN 41274. 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 41273 | Lemma for hdmaprnN 41274. 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 41274 | 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 41275 | Part 12 in [Baer] p. 49. The map from vectors to functionals with closed kernels maps one-to-one onto. Combined with hdmapadd 41253, 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 41276 | 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 41277* | Prior to part 14 in [Baer] p. 49, line 25. TODO: fix to include πΉ = 0 so it can be used in hdmap14lem10 41287. (Contributed by NM, 31-May-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ β = ( Β·π βπΆ) & β’ πΏ = (LSpanβπΆ) & β’ π = (ScalarβπΆ) & β’ π΄ = (Baseβπ) & β’ π = ((HDMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β πΉ β π΅) β β’ (π β βπ β π΄ (πβ(πΉ Β· π)) = (π β (πβπ))) | ||
Theorem | hdmap14lem1 41278 | 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 41279* | Prior to part 14 in [Baer] p. 49, line 25. TODO: fix to include πΉ = π so it can be used in hdmap14lem10 41287. (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 41280* | 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 41281* | Simplify (π΄ β {π}) in hdmap14lem3 41280 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 41282* | Simplify (π΄ β {π}) in hdmap14lem3 41280 to provide a slightly simpler definition later. TODO: Use hdmap14lem4a 41281 if that one is also used directly elsewhere. Otherwise, merge hdmap14lem4a 41281 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 41283* | 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 41284* | Combine cases of πΉ. TODO: Can this be done at once in hdmap14lem3 41280, in order to get rid of hdmap14lem6 41283? Perhaps modify lspsneu 21000 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 41285 | 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 41286 | 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 41287 | 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 41288 | 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 41289* | 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 41290* | 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 41291* | 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 41292* | 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 41293 | Extend class notation with g-map. |
class HGMap | ||
Definition | df-hgmap 41294* | 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 41295* | 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 41296* | 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 41297* | 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 41292. (Contributed by NM, 25-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ β = ( Β·π βπΆ) & β’ π = ((HDMapβπΎ)βπ) & β’ πΌ = ((HGMapβπΎ)βπ) & β’ (π β (πΎ β π β§ π β π»)) & β’ (π β π β π΅) β β’ (π β (πΌβπ) = (β©π¦ β π΅ βπ£ β π (πβ(π Β· π£)) = (π¦ β (πβπ£)))) | ||
Theorem | hgmapfnN 41298 | Functionality of scalar sigma map. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & β’ πΊ = ((HGMapβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β πΊ Fn π΅) | ||
Theorem | hgmapcl 41299 | 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 41300 | 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 β§ π β π»)) & β’ (π β πΉ β π΅) β β’ (π β (πΊβπΉ) β π΄) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |