![]() |
Metamath
Proof Explorer Theorem List (p. 406 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-30158) |
![]() (30159-31681) |
![]() (31682-47805) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mapdsn2 40501* | Value of the map defined by df-mapd 40484 at the span of a singleton. (Contributed by NM, 16-Feb-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((ocHβπΎ)βπ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β (πΏβπΊ) = (πβ{π})) β β’ (π β (πβ(πβ{π})) = {π β πΉ β£ (πΏβπΊ) β (πΏβπ)}) | ||
Theorem | mapdsn3 40502 | Value of the map defined by df-mapd 40484 at the span of a singleton. (Contributed by NM, 17-Feb-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((ocHβπΎ)βπ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π· = (LDualβπ) & β’ π = (LSpanβπ·) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β πΊ β πΉ) & β’ (π β (πΏβπΊ) = (πβ{π})) β β’ (π β (πβ(πβ{π})) = (πβ{πΊ})) | ||
Theorem | mapd1dim2lem1N 40503* | Value of the map defined by df-mapd 40484 at an atom. (Contributed by NM, 10-Feb-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π΄ = (LSAtomsβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π = ((ocHβπΎ)βπ) & β’ π = ((mapdβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π΄) β β’ (π β (πβπ) = {π β πΉ β£ βπ£ β π (πβ{π£}) = (πΏβπ)}) | ||
Theorem | mapdrvallem2 40504* | Lemma for mapdrval 40506. TODO: very long antecedents are dragged through proof in some places - see if it shortens proof to remove unused conjuncts. (Contributed by NM, 2-Feb-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((ocHβπΎ)βπ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π· = (LDualβπ) & β’ π = (LSubSpβπ·) & β’ πΆ = {π β πΉ β£ (πβ(πβ(πΏβπ))) = (πΏβπ)} & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β πΆ) & β’ π = βͺ β β π (πβ(πΏββ)) & β’ π = (Baseβπ) & β’ π΄ = (LSAtomsβπ) & β’ π = (LSpanβπ) & β’ 0 = (0gβπ) & β’ π = (0gβπ·) β β’ (π β {π β πΆ β£ (πβ(πΏβπ)) β π} β π ) | ||
Theorem | mapdrvallem3 40505* | Lemma for mapdrval 40506. (Contributed by NM, 2-Feb-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((ocHβπΎ)βπ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π· = (LDualβπ) & β’ π = (LSubSpβπ·) & β’ πΆ = {π β πΉ β£ (πβ(πβ(πΏβπ))) = (πΏβπ)} & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β πΆ) & β’ π = βͺ β β π (πβ(πΏββ)) & β’ π = (Baseβπ) & β’ π΄ = (LSAtomsβπ) & β’ π = (LSpanβπ) & β’ 0 = (0gβπ) & β’ π = (0gβπ·) β β’ (π β {π β πΆ β£ (πβ(πΏβπ)) β π} = π ) | ||
Theorem | mapdrval 40506* | Given a dual subspace π (of functionals with closed kernels), reconstruct the subspace π that maps to it. (Contributed by NM, 12-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((ocHβπΎ)βπ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π· = (LDualβπ) & β’ π = (LSubSpβπ·) & β’ πΆ = {π β πΉ β£ (πβ(πβ(πΏβπ))) = (πΏβπ)} & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β πΆ) & β’ π = βͺ β β π (πβ(πΏββ)) β β’ (π β (πβπ) = π ) | ||
Theorem | mapd1o 40507* | The map defined by df-mapd 40484 is one-to-one and onto the set of dual subspaces of functionals with closed kernels. This shows π satisfies part of the definition of projectivity of [Baer] p. 40. TODO: change theorems leading to this (lcfr 40444, mapdrval 40506, lclkrs 40398, lclkr 40392,...) to use π β© π« πΆ? TODO: maybe get rid of $d's for π versus πΎππ; propagate to mapdrn 40508 and any others. (Contributed by NM, 12-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((ocHβπΎ)βπ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π· = (LDualβπ) & β’ π = (LSubSpβπ·) & β’ πΆ = {π β πΉ β£ (πβ(πβ(πΏβπ))) = (πΏβπ)} & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β π:πβ1-1-ontoβ(π β© π« πΆ)) | ||
Theorem | mapdrn 40508* | Range of the map defined by df-mapd 40484. (Contributed by NM, 12-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((ocHβπΎ)βπ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π· = (LDualβπ) & β’ π = (LSubSpβπ·) & β’ πΆ = {π β πΉ β£ (πβ(πβ(πΏβπ))) = (πΏβπ)} & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β ran π = (π β© π« πΆ)) | ||
Theorem | mapdunirnN 40509* | Union of the range of the map defined by df-mapd 40484. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((ocHβπΎ)βπ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ πΆ = {π β πΉ β£ (πβ(πβ(πΏβπ))) = (πΏβπ)} & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β βͺ ran π = πΆ) | ||
Theorem | mapdrn2 40510 | Range of the map defined by df-mapd 40484. TODO: this seems to be needed a lot in hdmaprnlem3eN 40717 etc. Would it be better to change df-mapd 40484 theorems to use LSubSpβπΆ instead of ran π? (Contributed by NM, 13-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π = (LSubSpβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β ran π = π) | ||
Theorem | mapdcnvcl 40511 | Closure of the converse of the map defined by df-mapd 40484. (Contributed by NM, 13-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β ran π) β β’ (π β (β‘πβπ) β π) | ||
Theorem | mapdcl 40512 | Closure the value of the map defined by df-mapd 40484. (Contributed by NM, 13-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) β β’ (π β (πβπ) β ran π) | ||
Theorem | mapdcnvid1N 40513 | Converse of the value of the map defined by df-mapd 40484. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) β β’ (π β (β‘πβ(πβπ)) = π) | ||
Theorem | mapdsord 40514 | Strong ordering property of themap defined by df-mapd 40484. (Contributed by NM, 13-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β ((πβπ) β (πβπ) β π β π)) | ||
Theorem | mapdcl2 40515 | The mapping of a subspace of vector space H is a subspace in the dual space of functionals with closed kernels. (Contributed by NM, 31-Jan-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π = (LSubSpβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) β β’ (π β (πβπ ) β π) | ||
Theorem | mapdcnvid2 40516 | Value of the converse of the map defined by df-mapd 40484. (Contributed by NM, 13-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β ran π) β β’ (π β (πβ(β‘πβπ)) = π) | ||
Theorem | mapdcnvordN 40517 | Ordering property of the converse of the map defined by df-mapd 40484. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β ran π) & β’ (π β π β ran π) β β’ (π β ((β‘πβπ) β (β‘πβπ) β π β π)) | ||
Theorem | mapdcnv11N 40518 | The converse of the map defined by df-mapd 40484 is one-to-one. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β ran π) & β’ (π β π β ran π) β β’ (π β ((β‘πβπ) = (β‘πβπ) β π = π)) | ||
Theorem | mapdcv 40519 | Covering property of the converse of the map defined by df-mapd 40484. (Contributed by NM, 14-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ πΆ = ( βL βπ) & β’ π· = ((LCDualβπΎ)βπ) & β’ πΈ = ( βL βπ·) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (ππΆπ β (πβπ)πΈ(πβπ))) | ||
Theorem | mapdincl 40520 | Closure of dual subspace intersection for the map defined by df-mapd 40484. (Contributed by NM, 12-Apr-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β ran π) & β’ (π β π β ran π) β β’ (π β (π β© π) β ran π) | ||
Theorem | mapdin 40521 | Subspace intersection is preserved by the map defined by df-mapd 40484. Part of property (e) in [Baer] p. 40. (Contributed by NM, 12-Apr-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (πβ(π β© π)) = ((πβπ) β© (πβπ))) | ||
Theorem | mapdlsmcl 40522 | Closure of dual subspace sum for the map defined by df-mapd 40484. (Contributed by NM, 13-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ β = (LSSumβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β ran π) & β’ (π β π β ran π) β β’ (π β (π β π) β ran π) | ||
Theorem | mapdlsm 40523 | Subspace sum is preserved by the map defined by df-mapd 40484. Part of property (e) in [Baer] p. 40. (Contributed by NM, 13-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ β = (LSSumβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (πβ(π β π)) = ((πβπ) β (πβπ))) | ||
Theorem | mapd0 40524 | Projectivity map of the zero subspace. Part of property (f) in [Baer] p. 40. TODO: does proof need to be this long for this simple fact? (Contributed by NM, 15-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (0gβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ 0 = (0gβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β (πβ{π}) = { 0 }) | ||
Theorem | mapdcnvatN 40525 | Atoms are preserved by the map defined by df-mapd 40484. (Contributed by NM, 29-May-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π΄ = (LSAtomsβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π΅ = (LSAtomsβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π΅) β β’ (π β (β‘πβπ) β π΄) | ||
Theorem | mapdat 40526 | Atoms are preserved by the map defined by df-mapd 40484. Property (g) in [Baer] p. 41. (Contributed by NM, 14-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π΄ = (LSAtomsβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π΅ = (LSAtomsβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π΄) β β’ (π β (πβπ) β π΅) | ||
Theorem | mapdspex 40527* | The map of a span equals the dual span of some vector (functional). (Contributed by NM, 15-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π΅ = (BaseβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) β β’ (π β βπ β π΅ (πβ(πβ{π})) = (π½β{π})) | ||
Theorem | mapdn0 40528 | Transfer nonzero property from domain to range of projectivity mapd. (Contributed by NM, 12-Apr-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) & β’ 0 = (0gβπ) & β’ π = (0gβπΆ) & β’ (π β π β (π β { 0 })) β β’ (π β πΉ β (π· β {π})) | ||
Theorem | mapdncol 40529 | Transfer non-colinearity from domain to range of projectivity mapd. (Contributed by NM, 11-Apr-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β πΊ β π·) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ (π β (πβ{π}) β (πβ{π})) β β’ (π β (π½β{πΉ}) β (π½β{πΊ})) | ||
Theorem | mapdindp 40530 | Transfer (part of) vector independence condition from domain to range of projectivity mapd. (Contributed by NM, 11-Apr-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β πΊ β π·) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ (π β π β π) & β’ (π β πΈ β π·) & β’ (π β (πβ(πβ{π})) = (π½β{πΈ})) & β’ (π β Β¬ π β (πβ{π, π})) β β’ (π β Β¬ πΉ β (π½β{πΊ, πΈ})) | ||
Theorem | mapdpglem1 40531 | Lemma for mapdpg 40565. Baer p. 44, last line: "(F(x-y))* <= (Fx)*+(Fy)*." (Contributed by NM, 15-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ β = (LSSumβπΆ) β β’ (π β (πβ(πβ{(π β π)})) β ((πβ(πβ{π})) β (πβ(πβ{π})))) | ||
Theorem | mapdpglem2 40532* | Lemma for mapdpg 40565. Baer p. 45, lines 1 and 2: "we have (F(x-y))* = Gt where t necessarily belongs to (Fx)*+(Fy)*." (We scope $d π‘π locally to avoid clashes with later substitutions into π.) (Contributed by NM, 15-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ β = (LSSumβπΆ) & β’ π½ = (LSpanβπΆ) β β’ (π β βπ‘ β ((πβ(πβ{π})) β (πβ(πβ{π})))(πβ(πβ{(π β π)})) = (π½β{π‘})) | ||
Theorem | mapdpglem2a 40533* | Lemma for mapdpg 40565. (Contributed by NM, 20-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ β = (LSSumβπΆ) & β’ π½ = (LSpanβπΆ) & β’ πΉ = (BaseβπΆ) & β’ (π β π‘ β ((πβ(πβ{π})) β (πβ(πβ{π})))) β β’ (π β π‘ β πΉ) | ||
Theorem | mapdpglem3 40534* | Lemma for mapdpg 40565. Baer p. 45, line 3: "infer ... the existence of a number g in G and of an element z in (Fy)* such that t = gx'-z." (We scope $d ππ€π§π locally to avoid clashes with later substitutions into π.) (Contributed by NM, 18-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ β = (LSSumβπΆ) & β’ π½ = (LSpanβπΆ) & β’ πΉ = (BaseβπΆ) & β’ (π β π‘ β ((πβ(πβ{π})) β (πβ(πβ{π})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (-gβπΆ) & β’ (π β πΊ β πΉ) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) β β’ (π β βπ β π΅ βπ§ β (πβ(πβ{π}))π‘ = ((π Β· πΊ)π π§)) | ||
Theorem | mapdpglem4N 40535* | Lemma for mapdpg 40565. (Contributed by NM, 20-Mar-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ β = (LSSumβπΆ) & β’ π½ = (LSpanβπΆ) & β’ πΉ = (BaseβπΆ) & β’ (π β π‘ β ((πβ(πβ{π})) β (πβ(πβ{π})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (-gβπΆ) & β’ (π β πΊ β πΉ) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ π = (0gβπ) & β’ (π β (πβ{π}) β (πβ{π})) β β’ (π β (π β π) β π) | ||
Theorem | mapdpglem5N 40536* | Lemma for mapdpg 40565. (Contributed by NM, 20-Mar-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ β = (LSSumβπΆ) & β’ π½ = (LSpanβπΆ) & β’ πΉ = (BaseβπΆ) & β’ (π β π‘ β ((πβ(πβ{π})) β (πβ(πβ{π})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (-gβπΆ) & β’ (π β πΊ β πΉ) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ π = (0gβπ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{(π β π)})) = (π½β{π‘})) β β’ (π β π‘ β (0gβπΆ)) | ||
Theorem | mapdpglem6 40537* | Lemma for mapdpg 40565. Baer p. 45, line 4: "If g were 0, then t would be in (Fy)*..." (Contributed by NM, 18-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ β = (LSSumβπΆ) & β’ π½ = (LSpanβπΆ) & β’ πΉ = (BaseβπΆ) & β’ (π β π‘ β ((πβ(πβ{π})) β (πβ(πβ{π})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (-gβπΆ) & β’ (π β πΊ β πΉ) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ π = (0gβπ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{(π β π)})) = (π½β{π‘})) & β’ 0 = (0gβπ΄) & β’ (π β π β π΅) & β’ (π β π§ β (πβ(πβ{π}))) & β’ (π β π‘ = ((π Β· πΊ)π π§)) & β’ (π β π β π) & β’ (π β π = 0 ) β β’ (π β π‘ β (πβ(πβ{π}))) | ||
Theorem | mapdpglem8 40538* | Lemma for mapdpg 40565. Baer p. 45, line 4: "...so that (F(x-y))* <= (Fy)*. This would imply that F(x-y) <= F(y)..." (Contributed by NM, 20-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ β = (LSSumβπΆ) & β’ π½ = (LSpanβπΆ) & β’ πΉ = (BaseβπΆ) & β’ (π β π‘ β ((πβ(πβ{π})) β (πβ(πβ{π})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (-gβπΆ) & β’ (π β πΊ β πΉ) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ π = (0gβπ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{(π β π)})) = (π½β{π‘})) & β’ 0 = (0gβπ΄) & β’ (π β π β π΅) & β’ (π β π§ β (πβ(πβ{π}))) & β’ (π β π‘ = ((π Β· πΊ)π π§)) & β’ (π β π β π) & β’ (π β π = 0 ) β β’ (π β (πβ{(π β π)}) β (πβ{π})) | ||
Theorem | mapdpglem9 40539* | Lemma for mapdpg 40565. Baer p. 45, line 4: "...so that x would consequently belong to Fy." (Contributed by NM, 20-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ β = (LSSumβπΆ) & β’ π½ = (LSpanβπΆ) & β’ πΉ = (BaseβπΆ) & β’ (π β π‘ β ((πβ(πβ{π})) β (πβ(πβ{π})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (-gβπΆ) & β’ (π β πΊ β πΉ) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ π = (0gβπ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{(π β π)})) = (π½β{π‘})) & β’ 0 = (0gβπ΄) & β’ (π β π β π΅) & β’ (π β π§ β (πβ(πβ{π}))) & β’ (π β π‘ = ((π Β· πΊ)π π§)) & β’ (π β π β π) & β’ (π β π = 0 ) β β’ (π β π β (πβ{π})) | ||
Theorem | mapdpglem10 40540* | Lemma for mapdpg 40565. Baer p. 45, line 6: "Hence Fx=Fy, an impossibility." (Contributed by NM, 20-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ β = (LSSumβπΆ) & β’ π½ = (LSpanβπΆ) & β’ πΉ = (BaseβπΆ) & β’ (π β π‘ β ((πβ(πβ{π})) β (πβ(πβ{π})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (-gβπΆ) & β’ (π β πΊ β πΉ) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ π = (0gβπ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{(π β π)})) = (π½β{π‘})) & β’ 0 = (0gβπ΄) & β’ (π β π β π΅) & β’ (π β π§ β (πβ(πβ{π}))) & β’ (π β π‘ = ((π Β· πΊ)π π§)) & β’ (π β π β π) & β’ (π β π = 0 ) β β’ (π β (πβ{π}) = (πβ{π})) | ||
Theorem | mapdpglem11 40541* | Lemma for mapdpg 40565. (Contributed by NM, 20-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ β = (LSSumβπΆ) & β’ π½ = (LSpanβπΆ) & β’ πΉ = (BaseβπΆ) & β’ (π β π‘ β ((πβ(πβ{π})) β (πβ(πβ{π})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (-gβπΆ) & β’ (π β πΊ β πΉ) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ π = (0gβπ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{(π β π)})) = (π½β{π‘})) & β’ 0 = (0gβπ΄) & β’ (π β π β π΅) & β’ (π β π§ β (πβ(πβ{π}))) & β’ (π β π‘ = ((π Β· πΊ)π π§)) & β’ (π β π β π) β β’ (π β π β 0 ) | ||
Theorem | mapdpglem12 40542* | Lemma for mapdpg 40565. TODO: Can some commonality with mapdpglem6 40537 through mapdpglem11 40541 be exploited? Also, some consolidation of small lemmas here could be done. (Contributed by NM, 18-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ β = (LSSumβπΆ) & β’ π½ = (LSpanβπΆ) & β’ πΉ = (BaseβπΆ) & β’ (π β π‘ β ((πβ(πβ{π})) β (πβ(πβ{π})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (-gβπΆ) & β’ (π β πΊ β πΉ) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ π = (0gβπ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{(π β π)})) = (π½β{π‘})) & β’ 0 = (0gβπ΄) & β’ (π β π β π΅) & β’ (π β π§ β (πβ(πβ{π}))) & β’ (π β π‘ = ((π Β· πΊ)π π§)) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π§ = (0gβπΆ)) β β’ (π β π‘ β (πβ(πβ{π}))) | ||
Theorem | mapdpglem13 40543* | Lemma for mapdpg 40565. (Contributed by NM, 20-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ β = (LSSumβπΆ) & β’ π½ = (LSpanβπΆ) & β’ πΉ = (BaseβπΆ) & β’ (π β π‘ β ((πβ(πβ{π})) β (πβ(πβ{π})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (-gβπΆ) & β’ (π β πΊ β πΉ) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ π = (0gβπ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{(π β π)})) = (π½β{π‘})) & β’ 0 = (0gβπ΄) & β’ (π β π β π΅) & β’ (π β π§ β (πβ(πβ{π}))) & β’ (π β π‘ = ((π Β· πΊ)π π§)) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π§ = (0gβπΆ)) β β’ (π β (πβ{(π β π)}) β (πβ{π})) | ||
Theorem | mapdpglem14 40544* | Lemma for mapdpg 40565. (Contributed by NM, 20-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ β = (LSSumβπΆ) & β’ π½ = (LSpanβπΆ) & β’ πΉ = (BaseβπΆ) & β’ (π β π‘ β ((πβ(πβ{π})) β (πβ(πβ{π})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (-gβπΆ) & β’ (π β πΊ β πΉ) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ π = (0gβπ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{(π β π)})) = (π½β{π‘})) & β’ 0 = (0gβπ΄) & β’ (π β π β π΅) & β’ (π β π§ β (πβ(πβ{π}))) & β’ (π β π‘ = ((π Β· πΊ)π π§)) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π§ = (0gβπΆ)) β β’ (π β π β (πβ{π})) | ||
Theorem | mapdpglem15 40545* | Lemma for mapdpg 40565. (Contributed by NM, 20-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ β = (LSSumβπΆ) & β’ π½ = (LSpanβπΆ) & β’ πΉ = (BaseβπΆ) & β’ (π β π‘ β ((πβ(πβ{π})) β (πβ(πβ{π})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (-gβπΆ) & β’ (π β πΊ β πΉ) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ π = (0gβπ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{(π β π)})) = (π½β{π‘})) & β’ 0 = (0gβπ΄) & β’ (π β π β π΅) & β’ (π β π§ β (πβ(πβ{π}))) & β’ (π β π‘ = ((π Β· πΊ)π π§)) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π§ = (0gβπΆ)) β β’ (π β (πβ{π}) = (πβ{π})) | ||
Theorem | mapdpglem16 40546* | Lemma for mapdpg 40565. Baer p. 45, line 7: "Likewise we see that z =/= 0." (Contributed by NM, 20-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ β = (LSSumβπΆ) & β’ π½ = (LSpanβπΆ) & β’ πΉ = (BaseβπΆ) & β’ (π β π‘ β ((πβ(πβ{π})) β (πβ(πβ{π})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (-gβπΆ) & β’ (π β πΊ β πΉ) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ π = (0gβπ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{(π β π)})) = (π½β{π‘})) & β’ 0 = (0gβπ΄) & β’ (π β π β π΅) & β’ (π β π§ β (πβ(πβ{π}))) & β’ (π β π‘ = ((π Β· πΊ)π π§)) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β π§ β (0gβπΆ)) | ||
Theorem | mapdpglem17N 40547* | Lemma for mapdpg 40565. Baer p. 45, line 7: "Hence we may form y' = g^-1 z." (Contributed by NM, 20-Mar-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ β = (LSSumβπΆ) & β’ π½ = (LSpanβπΆ) & β’ πΉ = (BaseβπΆ) & β’ (π β π‘ β ((πβ(πβ{π})) β (πβ(πβ{π})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (-gβπΆ) & β’ (π β πΊ β πΉ) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ π = (0gβπ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{(π β π)})) = (π½β{π‘})) & β’ 0 = (0gβπ΄) & β’ (π β π β π΅) & β’ (π β π§ β (πβ(πβ{π}))) & β’ (π β π‘ = ((π Β· πΊ)π π§)) & β’ (π β π β π) & β’ (π β π β π) & β’ πΈ = (((invrβπ΄)βπ) Β· π§) β β’ (π β πΈ β πΉ) | ||
Theorem | mapdpglem18 40548* | Lemma for mapdpg 40565. Baer p. 45, line 7: "Then y =/= 0..." (Contributed by NM, 20-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ β = (LSSumβπΆ) & β’ π½ = (LSpanβπΆ) & β’ πΉ = (BaseβπΆ) & β’ (π β π‘ β ((πβ(πβ{π})) β (πβ(πβ{π})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (-gβπΆ) & β’ (π β πΊ β πΉ) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ π = (0gβπ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{(π β π)})) = (π½β{π‘})) & β’ 0 = (0gβπ΄) & β’ (π β π β π΅) & β’ (π β π§ β (πβ(πβ{π}))) & β’ (π β π‘ = ((π Β· πΊ)π π§)) & β’ (π β π β π) & β’ (π β π β π) & β’ πΈ = (((invrβπ΄)βπ) Β· π§) β β’ (π β πΈ β (0gβπΆ)) | ||
Theorem | mapdpglem19 40549* | Lemma for mapdpg 40565. Baer p. 45, line 8: "...is in (Fy)*..." (Contributed by NM, 20-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ β = (LSSumβπΆ) & β’ π½ = (LSpanβπΆ) & β’ πΉ = (BaseβπΆ) & β’ (π β π‘ β ((πβ(πβ{π})) β (πβ(πβ{π})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (-gβπΆ) & β’ (π β πΊ β πΉ) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ π = (0gβπ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{(π β π)})) = (π½β{π‘})) & β’ 0 = (0gβπ΄) & β’ (π β π β π΅) & β’ (π β π§ β (πβ(πβ{π}))) & β’ (π β π‘ = ((π Β· πΊ)π π§)) & β’ (π β π β π) & β’ (π β π β π) & β’ πΈ = (((invrβπ΄)βπ) Β· π§) β β’ (π β πΈ β (πβ(πβ{π}))) | ||
Theorem | mapdpglem20 40550* | Lemma for mapdpg 40565. Baer p. 45, line 8: "...so that (Fy)*=Gy'." (Contributed by NM, 20-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ β = (LSSumβπΆ) & β’ π½ = (LSpanβπΆ) & β’ πΉ = (BaseβπΆ) & β’ (π β π‘ β ((πβ(πβ{π})) β (πβ(πβ{π})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (-gβπΆ) & β’ (π β πΊ β πΉ) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ π = (0gβπ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{(π β π)})) = (π½β{π‘})) & β’ 0 = (0gβπ΄) & β’ (π β π β π΅) & β’ (π β π§ β (πβ(πβ{π}))) & β’ (π β π‘ = ((π Β· πΊ)π π§)) & β’ (π β π β π) & β’ (π β π β π) & β’ πΈ = (((invrβπ΄)βπ) Β· π§) β β’ (π β (πβ(πβ{π})) = (π½β{πΈ})) | ||
Theorem | mapdpglem21 40551* | Lemma for mapdpg 40565. (Contributed by NM, 20-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ β = (LSSumβπΆ) & β’ π½ = (LSpanβπΆ) & β’ πΉ = (BaseβπΆ) & β’ (π β π‘ β ((πβ(πβ{π})) β (πβ(πβ{π})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (-gβπΆ) & β’ (π β πΊ β πΉ) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ π = (0gβπ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{(π β π)})) = (π½β{π‘})) & β’ 0 = (0gβπ΄) & β’ (π β π β π΅) & β’ (π β π§ β (πβ(πβ{π}))) & β’ (π β π‘ = ((π Β· πΊ)π π§)) & β’ (π β π β π) & β’ (π β π β π) & β’ πΈ = (((invrβπ΄)βπ) Β· π§) β β’ (π β (((invrβπ΄)βπ) Β· π‘) = (πΊπ πΈ)) | ||
Theorem | mapdpglem22 40552* | Lemma for mapdpg 40565. Baer p. 45, line 9: "(F(x-y))* = ... = G(x'-y')." (Contributed by NM, 20-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ β = (LSSumβπΆ) & β’ π½ = (LSpanβπΆ) & β’ πΉ = (BaseβπΆ) & β’ (π β π‘ β ((πβ(πβ{π})) β (πβ(πβ{π})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (-gβπΆ) & β’ (π β πΊ β πΉ) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ π = (0gβπ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{(π β π)})) = (π½β{π‘})) & β’ 0 = (0gβπ΄) & β’ (π β π β π΅) & β’ (π β π§ β (πβ(πβ{π}))) & β’ (π β π‘ = ((π Β· πΊ)π π§)) & β’ (π β π β π) & β’ (π β π β π) & β’ πΈ = (((invrβπ΄)βπ) Β· π§) β β’ (π β (πβ(πβ{(π β π)})) = (π½β{(πΊπ πΈ)})) | ||
Theorem | mapdpglem23 40553* | Lemma for mapdpg 40565. Baer p. 45, line 10: "and so y' meets all our requirements." Our β is Baer's y'. (Contributed by NM, 20-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ β = (LSSumβπΆ) & β’ π½ = (LSpanβπΆ) & β’ πΉ = (BaseβπΆ) & β’ (π β π‘ β ((πβ(πβ{π})) β (πβ(πβ{π})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (-gβπΆ) & β’ (π β πΊ β πΉ) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ π = (0gβπ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{(π β π)})) = (π½β{π‘})) & β’ 0 = (0gβπ΄) & β’ (π β π β π΅) & β’ (π β π§ β (πβ(πβ{π}))) & β’ (π β π‘ = ((π Β· πΊ)π π§)) & β’ (π β π β π) & β’ (π β π β π) & β’ πΈ = (((invrβπ΄)βπ) Β· π§) β β’ (π β ββ β πΉ ((πβ(πβ{π})) = (π½β{β}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ β)}))) | ||
Theorem | mapdpglem30a 40554 | Lemma for mapdpg 40565. (Contributed by NM, 22-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ πΉ = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β πΊ β πΉ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) β β’ (π β πΊ β (0gβπΆ)) | ||
Theorem | mapdpglem30b 40555 | Lemma for mapdpg 40565. (Contributed by NM, 22-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ πΉ = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β πΊ β πΉ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ (π β (β β πΉ β§ ((πβ(πβ{π})) = (π½β{β}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ β)})))) & β’ (π β (π β πΉ β§ ((πβ(πβ{π})) = (π½β{π}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ π)})))) β β’ (π β π β (0gβπΆ)) | ||
Theorem | mapdpglem25 40556 | Lemma for mapdpg 40565. Baer p. 45 line 12: "Then we have Gy' = Gy'' and G(x'-y') = G(x'-y'')." (Contributed by NM, 21-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ πΉ = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β πΊ β πΉ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ (π β (β β πΉ β§ ((πβ(πβ{π})) = (π½β{β}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ β)})))) & β’ (π β (π β πΉ β§ ((πβ(πβ{π})) = (π½β{π}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ π)})))) β β’ (π β ((π½β{β}) = (π½β{π}) β§ (π½β{(πΊπ β)}) = (π½β{(πΊπ π)}))) | ||
Theorem | mapdpglem26 40557* | Lemma for mapdpg 40565. Baer p. 45 line 14: "Consequently there exist numbers u,v in G neither of which is 0 such that y = uy'' and..." (We scope $d π’π locally to avoid clashes with later substitutions into π.) (Contributed by NM, 22-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ πΉ = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β πΊ β πΉ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ (π β (β β πΉ β§ ((πβ(πβ{π})) = (π½β{β}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ β)})))) & β’ (π β (π β πΉ β§ ((πβ(πβ{π})) = (π½β{π}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ π)})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (0gβπ΄) β β’ (π β βπ’ β (π΅ β {π})β = (π’ Β· π)) | ||
Theorem | mapdpglem27 40558* | Lemma for mapdpg 40565. Baer p. 45 line 16: "v(x'-y'') = x'-y'" (with equality swapped). (Contributed by NM, 22-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ πΉ = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β πΊ β πΉ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ (π β (β β πΉ β§ ((πβ(πβ{π})) = (π½β{β}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ β)})))) & β’ (π β (π β πΉ β§ ((πβ(πβ{π})) = (π½β{π}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ π)})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (0gβπ΄) β β’ (π β βπ£ β (π΅ β {π})(πΊπ β) = (π£ Β· (πΊπ π))) | ||
Theorem | mapdpglem29 40559* | Lemma for mapdpg 40565. Baer p. 45 line 16: "But Gx' and Gy'' are distinct points and so x' and y'' are independent elements in B. (Contributed by NM, 22-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ πΉ = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β πΊ β πΉ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ (π β (β β πΉ β§ ((πβ(πβ{π})) = (π½β{β}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ β)})))) & β’ (π β (π β πΉ β§ ((πβ(πβ{π})) = (π½β{π}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ π)})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (0gβπ΄) & β’ (π β π£ β π΅) & β’ (π β β = (π’ Β· π)) & β’ (π β (πΊπ β) = (π£ Β· (πΊπ π))) β β’ (π β (π½β{πΊ}) β (π½β{π})) | ||
Theorem | mapdpglem28 40560* | Lemma for mapdpg 40565. Baer p. 45 line 18: "vx'-vy'' = x'-uy''". (Contributed by NM, 22-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ πΉ = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β πΊ β πΉ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ (π β (β β πΉ β§ ((πβ(πβ{π})) = (π½β{β}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ β)})))) & β’ (π β (π β πΉ β§ ((πβ(πβ{π})) = (π½β{π}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ π)})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (0gβπ΄) & β’ (π β π£ β π΅) & β’ (π β β = (π’ Β· π)) & β’ (π β (πΊπ β) = (π£ Β· (πΊπ π))) β β’ (π β ((π£ Β· πΊ)π (π£ Β· π)) = (πΊπ (π’ Β· π))) | ||
Theorem | mapdpglem30 40561* | Lemma for mapdpg 40565. Baer p. 45 line 18: "Hence we deduce (from mapdpglem28 40560, using lvecindp2 20744) that v = 1 and v = u...". TODO: would it be shorter to have only the π£ = (1rβπ΄) part and use mapdpglem28.u2 in mapdpglem31 40562? (Contributed by NM, 22-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ πΉ = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β πΊ β πΉ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ (π β (β β πΉ β§ ((πβ(πβ{π})) = (π½β{β}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ β)})))) & β’ (π β (π β πΉ β§ ((πβ(πβ{π})) = (π½β{π}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ π)})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (0gβπ΄) & β’ (π β π£ β π΅) & β’ (π β β = (π’ Β· π)) & β’ (π β (πΊπ β) = (π£ Β· (πΊπ π))) & β’ (π β π’ β π΅) β β’ (π β (π£ = (1rβπ΄) β§ π£ = π’)) | ||
Theorem | mapdpglem31 40562* | Lemma for mapdpg 40565. Baer p. 45 line 19: "...and we have consequently that y' = y'', as we claimed." (Contributed by NM, 23-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ πΉ = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β πΊ β πΉ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ (π β (β β πΉ β§ ((πβ(πβ{π})) = (π½β{β}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ β)})))) & β’ (π β (π β πΉ β§ ((πβ(πβ{π})) = (π½β{π}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ π)})))) & β’ π΄ = (Scalarβπ) & β’ π΅ = (Baseβπ΄) & β’ Β· = ( Β·π βπΆ) & β’ π = (0gβπ΄) & β’ (π β π£ β π΅) & β’ (π β β = (π’ Β· π)) & β’ (π β (πΊπ β) = (π£ Β· (πΊπ π))) & β’ (π β π’ β π΅) β β’ (π β β = π) | ||
Theorem | mapdpglem24 40563* | Lemma for mapdpg 40565. Existence part - consolidate hypotheses in mapdpglem23 40553. (Contributed by NM, 21-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ πΉ = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β πΊ β πΉ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) β β’ (π β ββ β πΉ ((πβ(πβ{π})) = (π½β{β}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ β)}))) | ||
Theorem | mapdpglem32 40564* | Lemma for mapdpg 40565. Uniqueness part - consolidate hypotheses in mapdpglem31 40562. (Contributed by NM, 23-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ πΉ = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β πΊ β πΉ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) β β’ ((π β§ (β β πΉ β§ π β πΉ) β§ (((πβ(πβ{π})) = (π½β{β}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ β)})) β§ ((πβ(πβ{π})) = (π½β{π}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ π)})))) β β = π) | ||
Theorem | mapdpg 40565* | Part 1 of proof of the first fundamental theorem of projective geometry. Part (1) in [Baer] p. 44. Our notation corresponds to Baer's as follows: π for *, πβ{} for F(), π½β{} for G(), π for x, πΊ for x', π for y, β for y'. TODO: Rename variables per mapdhval 40583. (Contributed by NM, 22-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ πΉ = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β πΊ β πΉ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) β β’ (π β β!β β πΉ ((πβ(πβ{π})) = (π½β{β}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ β)}))) | ||
Theorem | baerlem3lem1 40566 | Lemma for baerlem3 40572. (Contributed by NM, 9-Apr-2015.) |
β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & ⒠⨣ = (+gβπ ) & β’ πΏ = (-gβπ ) & β’ π = (0gβπ ) & β’ πΌ = (invgβπ ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π = ((π Β· π) + (π Β· π))) & β’ (π β π = ((π Β· (π β π)) + (π Β· (π β π)))) β β’ (π β π = (π Β· (π β π))) | ||
Theorem | baerlem5alem1 40567 | Lemma for baerlem5a 40573. (Contributed by NM, 13-Apr-2015.) |
β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & ⒠⨣ = (+gβπ ) & β’ πΏ = (-gβπ ) & β’ π = (0gβπ ) & β’ πΌ = (invgβπ ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π = ((π Β· (π β π)) + (π Β· π))) & β’ (π β π = ((π Β· (π β π)) + (π Β· π))) β β’ (π β π = (π Β· (π β (π + π)))) | ||
Theorem | baerlem5blem1 40568 | Lemma for baerlem5b 40574. (Contributed by NM, 9-Apr-2015.) |
β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & ⒠⨣ = (+gβπ ) & β’ πΏ = (-gβπ ) & β’ π = (0gβπ ) & β’ πΌ = (invgβπ ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π = ((π Β· π) + (π Β· π))) & β’ (π β π = ((π Β· (π β (π + π))) + (π Β· π))) β β’ (π β π = ((πΌβπ) Β· (π + π))) | ||
Theorem | baerlem3lem2 40569 | Lemma for baerlem3 40572. (Contributed by NM, 9-Apr-2015.) |
β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & ⒠⨣ = (+gβπ ) & β’ πΏ = (-gβπ ) & β’ π = (0gβπ ) & β’ πΌ = (invgβπ ) β β’ (π β (πβ{(π β π)}) = (((πβ{π}) β (πβ{π})) β© ((πβ{(π β π)}) β (πβ{(π β π)})))) | ||
Theorem | baerlem5alem2 40570 | Lemma for baerlem5a 40573. (Contributed by NM, 9-Apr-2015.) |
β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & ⒠⨣ = (+gβπ ) & β’ πΏ = (-gβπ ) & β’ π = (0gβπ ) & β’ πΌ = (invgβπ ) β β’ (π β (πβ{(π β (π + π))}) = (((πβ{(π β π)}) β (πβ{π})) β© ((πβ{(π β π)}) β (πβ{π})))) | ||
Theorem | baerlem5blem2 40571 | Lemma for baerlem5b 40574. (Contributed by NM, 13-Apr-2015.) |
β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & ⒠⨣ = (+gβπ ) & β’ πΏ = (-gβπ ) & β’ π = (0gβπ ) & β’ πΌ = (invgβπ ) β β’ (π β (πβ{(π + π)}) = (((πβ{π}) β (πβ{π})) β© ((πβ{(π β (π + π))}) β (πβ{π})))) | ||
Theorem | baerlem3 40572 | An equality that holds when π, π, π are independent (non-colinear) vectors. Part (3) in [Baer] p. 45. TODO fix ref. (Contributed by NM, 9-Apr-2015.) |
β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) β β’ (π β (πβ{(π β π)}) = (((πβ{π}) β (πβ{π})) β© ((πβ{(π β π)}) β (πβ{(π β π)})))) | ||
Theorem | baerlem5a 40573 | An equality that holds when π, π, π are independent (non-colinear) vectors. First equation of part (5) in [Baer] p. 46. (Contributed by NM, 10-Apr-2015.) |
β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) β β’ (π β (πβ{(π β (π + π))}) = (((πβ{(π β π)}) β (πβ{π})) β© ((πβ{(π β π)}) β (πβ{π})))) | ||
Theorem | baerlem5b 40574 | An equality that holds when π, π, π are independent (non-colinear) vectors. Second equation of part (5) in [Baer] p. 46. (Contributed by NM, 13-Apr-2015.) |
β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) β β’ (π β (πβ{(π + π)}) = (((πβ{π}) β (πβ{π})) β© ((πβ{(π β (π + π))}) β (πβ{π})))) | ||
Theorem | baerlem5amN 40575 | An equality that holds when π, π, π are independent (non-colinear) vectors. Subtraction version of first equation of part (5) in [Baer] p. 46. TODO: This is the subtraction version, may not be needed. TODO: delete if baerlem5abmN 40577 is used. (Contributed by NM, 24-May-2015.) (New usage is discouraged.) |
β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) β β’ (π β (πβ{(π β (π β π))}) = (((πβ{(π β π)}) β (πβ{π})) β© ((πβ{(π + π)}) β (πβ{π})))) | ||
Theorem | baerlem5bmN 40576 | An equality that holds when π, π, π are independent (non-colinear) vectors. Subtraction version of second equation of part (5) in [Baer] p. 46. TODO: This is the subtraction version, may not be needed. TODO: delete if baerlem5abmN 40577 is used. (Contributed by NM, 24-May-2015.) (New usage is discouraged.) |
β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) β β’ (π β (πβ{(π β π)}) = (((πβ{π}) β (πβ{π})) β© ((πβ{(π β (π β π))}) β (πβ{π})))) | ||
Theorem | baerlem5abmN 40577 | An equality that holds when π, π, π are independent (non-colinear) vectors. Subtraction versions of first and second equations of part (5) in [Baer] p. 46, conjoined to share commonality in their proofs. TODO: Delete if not needed. (Contributed by NM, 24-May-2015.) (New usage is discouraged.) |
β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) β β’ (π β ((πβ{(π β (π β π))}) = (((πβ{(π β π)}) β (πβ{π})) β© ((πβ{(π + π)}) β (πβ{π}))) β§ (πβ{(π β π)}) = (((πβ{π}) β (πβ{π})) β© ((πβ{(π β (π β π))}) β (πβ{π}))))) | ||
Theorem | mapdindp0 40578 | Vector independence lemma. (Contributed by NM, 29-Apr-2015.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π€ β (π β { 0 })) & β’ (π β (πβ{π}) = (πβ{π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β Β¬ π€ β (πβ{π, π})) & β’ (π β (π + π) β 0 ) β β’ (π β (πβ{(π + π)}) = (πβ{π})) | ||
Theorem | mapdindp1 40579 | Vector independence lemma. (Contributed by NM, 1-May-2015.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π€ β (π β { 0 })) & β’ (π β (πβ{π}) = (πβ{π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β Β¬ π€ β (πβ{π, π})) β β’ (π β (πβ{π}) β (πβ{(π + π)})) | ||
Theorem | mapdindp2 40580 | Vector independence lemma. (Contributed by NM, 1-May-2015.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π€ β (π β { 0 })) & β’ (π β (πβ{π}) = (πβ{π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β Β¬ π€ β (πβ{π, π})) β β’ (π β Β¬ π€ β (πβ{π, (π + π)})) | ||
Theorem | mapdindp3 40581 | Vector independence lemma. (Contributed by NM, 29-Apr-2015.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π€ β (π β { 0 })) & β’ (π β (πβ{π}) = (πβ{π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β Β¬ π€ β (πβ{π, π})) β β’ (π β (πβ{π}) β (πβ{(π€ + π)})) | ||
Theorem | mapdindp4 40582 | Vector independence lemma. (Contributed by NM, 29-Apr-2015.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π€ β (π β { 0 })) & β’ (π β (πβ{π}) = (πβ{π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β Β¬ π€ β (πβ{π, π})) β β’ (π β Β¬ π β (πβ{π, (π€ + π)})) | ||
Theorem | mapdhval 40583* | Lemmma for ~? mapdh . (Contributed by NM, 3-Apr-2015.) (Revised by Mario Carneiro, 6-May-2015.) |
β’ π = (0gβπΆ) & β’ πΌ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) & β’ (π β π β π΄) & β’ (π β πΉ β π΅) & β’ (π β π β πΈ) β β’ (π β (πΌββ¨π, πΉ, πβ©) = if(π = 0 , π, (β©β β π· ((πβ(πβ{π})) = (π½β{β}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΉπ β)}))))) | ||
Theorem | mapdhval0 40584* | Lemmma for ~? mapdh . (Contributed by NM, 3-Apr-2015.) |
β’ π = (0gβπΆ) & β’ πΌ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) & β’ 0 = (0gβπ) & β’ (π β π β π΄) & β’ (π β πΉ β π΅) β β’ (π β (πΌββ¨π, πΉ, 0 β©) = π) | ||
Theorem | mapdhval2 40585* | Lemmma for ~? mapdh . (Contributed by NM, 3-Apr-2015.) |
β’ π = (0gβπΆ) & β’ πΌ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) & β’ (π β π β π΄) & β’ (π β πΉ β π΅) & β’ (π β π β (π β { 0 })) β β’ (π β (πΌββ¨π, πΉ, πβ©) = (β©β β π· ((πβ(πβ{π})) = (π½β{β}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΉπ β)})))) | ||
Theorem | mapdhcl 40586* | Lemmma for ~? mapdh . (Contributed by NM, 3-Apr-2015.) |
β’ π = (0gβπΆ) & β’ πΌ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) & β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) & β’ (π β π β (π β { 0 })) & β’ (π β π β π) & β’ (π β (πβ{π}) β (πβ{π})) β β’ (π β (πΌββ¨π, πΉ, πβ©) β π·) | ||
Theorem | mapdheq 40587* | Lemmma for ~? mapdh . The defining equation for h(x,x',y)=y' in part (2) in [Baer] p. 45 line 24. (Contributed by NM, 4-Apr-2015.) |
β’ π = (0gβπΆ) & β’ πΌ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) & β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β πΊ β π·) & β’ (π β (πβ{π}) β (πβ{π})) β β’ (π β ((πΌββ¨π, πΉ, πβ©) = πΊ β ((πβ(πβ{π})) = (π½β{πΊ}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΉπ πΊ)})))) | ||
Theorem | mapdheq2 40588* | Lemmma for ~? mapdh . One direction of part (2) in [Baer] p. 45. (Contributed by NM, 4-Apr-2015.) |
β’ π = (0gβπΆ) & β’ πΌ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) & β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β πΊ β π·) & β’ (π β (πβ{π}) β (πβ{π})) β β’ (π β ((πΌββ¨π, πΉ, πβ©) = πΊ β (πΌββ¨π, πΊ, πβ©) = πΉ)) | ||
Theorem | mapdheq2biN 40589* | Lemmma for ~? mapdh . Part (2) in [Baer] p. 45. The bidirectional version of mapdheq2 40588 seems to require an additional hypothesis not mentioned in Baer. TODO fix ref. TODO: We probably don't need this; delete if never used. (Contributed by NM, 4-Apr-2015.) (New usage is discouraged.) |
β’ π = (0gβπΆ) & β’ πΌ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) & β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β πΊ β π·) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) β β’ (π β ((πΌββ¨π, πΉ, πβ©) = πΊ β (πΌββ¨π, πΊ, πβ©) = πΉ)) | ||
Theorem | mapdheq4lem 40590* | Lemma for mapdheq4 40591. Part (4) in [Baer] p. 46. (Contributed by NM, 12-Apr-2015.) |
β’ π = (0gβπΆ) & β’ πΌ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) & β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πΌββ¨π, πΉ, πβ©) = πΊ) & β’ (π β (πΌββ¨π, πΉ, πβ©) = πΈ) β β’ (π β (πβ(πβ{(π β π)})) = (π½β{(πΊπ πΈ)})) | ||
Theorem | mapdheq4 40591* | Lemma for ~? mapdh . Part (4) in [Baer] p. 46. (Contributed by NM, 12-Apr-2015.) |
β’ π = (0gβπΆ) & β’ πΌ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) & β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πΌββ¨π, πΉ, πβ©) = πΊ) & β’ (π β (πΌββ¨π, πΉ, πβ©) = πΈ) β β’ (π β (πΌββ¨π, πΊ, πβ©) = πΈ) | ||
Theorem | mapdh6lem1N 40592* | Lemma for mapdh6N 40606. Part (6) in [Baer] p. 47, lines 16-18. (Contributed by NM, 13-Apr-2015.) (New usage is discouraged.) |
β’ π = (0gβπΆ) & β’ πΌ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) & β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) & β’ β = (+gβπΆ) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πΌββ¨π, πΉ, πβ©) = πΊ) & β’ (π β (πΌββ¨π, πΉ, πβ©) = πΈ) β β’ (π β (πβ(πβ{(π β (π + π))})) = (π½β{(πΉπ (πΊ β πΈ))})) | ||
Theorem | mapdh6lem2N 40593* | Lemma for mapdh6N 40606. Part (6) in [Baer] p. 47, lines 20-22. (Contributed by NM, 13-Apr-2015.) (New usage is discouraged.) |
β’ π = (0gβπΆ) & β’ πΌ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) & β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) & β’ β = (+gβπΆ) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πΌββ¨π, πΉ, πβ©) = πΊ) & β’ (π β (πΌββ¨π, πΉ, πβ©) = πΈ) β β’ (π β (πβ(πβ{(π + π)})) = (π½β{(πΊ β πΈ)})) | ||
Theorem | mapdh6aN 40594* | Lemma for mapdh6N 40606. Part (6) in [Baer] p. 47, case 1. (Contributed by NM, 23-Apr-2015.) (New usage is discouraged.) |
β’ π = (0gβπΆ) & β’ πΌ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) & β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) & β’ β = (+gβπΆ) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πΌββ¨π, πΉ, πβ©) = πΊ) & β’ (π β (πΌββ¨π, πΉ, πβ©) = πΈ) β β’ (π β (πΌββ¨π, πΉ, (π + π)β©) = ((πΌββ¨π, πΉ, πβ©) β (πΌββ¨π, πΉ, πβ©))) | ||
Theorem | mapdh6b0N 40595* | Lemmma for mapdh6N 40606. (Contributed by NM, 23-Apr-2015.) (New usage is discouraged.) |
β’ π = (0gβπΆ) & β’ πΌ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) & β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) & β’ β = (+gβπΆ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β ((πβ{π}) β© (πβ{π, π})) = { 0 }) β β’ (π β Β¬ π β (πβ{π, π})) | ||
Theorem | mapdh6bN 40596* | Lemmma for mapdh6N 40606. (Contributed by NM, 24-Apr-2015.) (New usage is discouraged.) |
β’ π = (0gβπΆ) & β’ πΌ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) & β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) & β’ β = (+gβπΆ) & β’ (π β π = 0 ) & β’ (π β π β π) & β’ (π β Β¬ π β (πβ{π, π})) β β’ (π β (πΌββ¨π, πΉ, (π + π)β©) = ((πΌββ¨π, πΉ, πβ©) β (πΌββ¨π, πΉ, πβ©))) | ||
Theorem | mapdh6cN 40597* | Lemmma for mapdh6N 40606. (Contributed by NM, 24-Apr-2015.) (New usage is discouraged.) |
β’ π = (0gβπΆ) & β’ πΌ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) & β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) & β’ β = (+gβπΆ) & β’ (π β π β π) & β’ (π β π = 0 ) & β’ (π β Β¬ π β (πβ{π, π})) β β’ (π β (πΌββ¨π, πΉ, (π + π)β©) = ((πΌββ¨π, πΉ, πβ©) β (πΌββ¨π, πΉ, πβ©))) | ||
Theorem | mapdh6dN 40598* | Lemmma for mapdh6N 40606. (Contributed by NM, 1-May-2015.) (New usage is discouraged.) |
β’ π = (0gβπΆ) & β’ πΌ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) & β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) & β’ β = (+gβπΆ) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) = (πβ{π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π€ β (π β { 0 })) & β’ (π β Β¬ π€ β (πβ{π, π})) β β’ (π β (πΌββ¨π, πΉ, (π€ + (π + π))β©) = ((πΌββ¨π, πΉ, π€β©) β (πΌββ¨π, πΉ, (π + π)β©))) | ||
Theorem | mapdh6eN 40599* | Lemmma for mapdh6N 40606. Part (6) in [Baer] p. 47 line 38. (Contributed by NM, 1-May-2015.) (New usage is discouraged.) |
β’ π = (0gβπΆ) & β’ πΌ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) & β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) & β’ β = (+gβπΆ) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) = (πβ{π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π€ β (π β { 0 })) & β’ (π β Β¬ π€ β (πβ{π, π})) β β’ (π β (πΌββ¨π, πΉ, ((π€ + π) + π)β©) = ((πΌββ¨π, πΉ, (π€ + π)β©) β (πΌββ¨π, πΉ, πβ©))) | ||
Theorem | mapdh6fN 40600* | Lemmma for mapdh6N 40606. Part (6) in [Baer] p. 47 line 38. (Contributed by NM, 1-May-2015.) (New usage is discouraged.) |
β’ π = (0gβπΆ) & β’ πΌ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) & β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π· = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β πΉ β π·) & β’ (π β (πβ(πβ{π})) = (π½β{πΉ})) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) & β’ β = (+gβπΆ) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) = (πβ{π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π€ β (π β { 0 })) & β’ (π β Β¬ π€ β (πβ{π, π})) β β’ (π β (πΌββ¨π, πΉ, (π€ + π)β©) = ((πΌββ¨π, πΉ, π€β©) β (πΌββ¨π, πΉ, πβ©))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |