![]() |
Metamath
Proof Explorer Theorem List (p. 409 of 480) | < 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-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mapdffval 40801* | Projectivity from vector space H to dual space. (Contributed by NM, 25-Jan-2015.) |
β’ π» = (LHypβπΎ) β β’ (πΎ β π β (mapdβπΎ) = (π€ β π» β¦ (π β (LSubSpβ((DVecHβπΎ)βπ€)) β¦ {π β (LFnlβ((DVecHβπΎ)βπ€)) β£ ((((ocHβπΎ)βπ€)β(((ocHβπΎ)βπ€)β((LKerβ((DVecHβπΎ)βπ€))βπ))) = ((LKerβ((DVecHβπΎ)βπ€))βπ) β§ (((ocHβπΎ)βπ€)β((LKerβ((DVecHβπΎ)βπ€))βπ)) β π )}))) | ||
Theorem | mapdfval 40802* | Projectivity from vector space H to dual space. (Contributed by NM, 25-Jan-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π = ((ocHβπΎ)βπ) & β’ π = ((mapdβπΎ)βπ) β β’ ((πΎ β π β§ π β π») β π = (π β π β¦ {π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π )})) | ||
Theorem | mapdval 40803* | Value of projectivity from vector space H to dual space. (Contributed by NM, 27-Jan-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π = ((ocHβπΎ)βπ) & β’ π = ((mapdβπΎ)βπ) & β’ (π β (πΎ β π β§ π β π»)) & β’ (π β π β π) β β’ (π β (πβπ) = {π β πΉ β£ ((πβ(πβ(πΏβπ))) = (πΏβπ) β§ (πβ(πΏβπ)) β π)}) | ||
Theorem | mapdvalc 40804* | Value of projectivity from vector space H to dual space. (Contributed by NM, 27-Jan-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π = ((ocHβπΎ)βπ) & β’ π = ((mapdβπΎ)βπ) & β’ (π β (πΎ β π β§ π β π»)) & β’ (π β π β π) & β’ πΆ = {π β πΉ β£ (πβ(πβ(πΏβπ))) = (πΏβπ)} β β’ (π β (πβπ) = {π β πΆ β£ (πβ(πΏβπ)) β π}) | ||
Theorem | mapdval2N 40805* | Value of projectivity from vector space H to dual space. (Contributed by NM, 31-Jan-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π = ((ocHβπΎ)βπ) & β’ π = ((mapdβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ πΆ = {π β πΉ β£ (πβ(πβ(πΏβπ))) = (πΏβπ)} β β’ (π β (πβπ) = {π β πΆ β£ βπ£ β π (πβ(πΏβπ)) = (πβ{π£})}) | ||
Theorem | mapdval3N 40806* | Value of projectivity from vector space H to dual space. (Contributed by NM, 31-Jan-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π = ((ocHβπΎ)βπ) & β’ π = ((mapdβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ πΆ = {π β πΉ β£ (πβ(πβ(πΏβπ))) = (πΏβπ)} β β’ (π β (πβπ) = βͺ π£ β π {π β πΆ β£ (πβ(πΏβπ)) = (πβ{π£})}) | ||
Theorem | mapdval4N 40807* | Value of projectivity from vector space H to dual space. TODO: 1. This is shorter than others - make it the official def? (but is not as obvious that it is β πΆ) 2. The unneeded direction of lcfl8a 40678 has awkward β- add another thm with only one direction of it? 3. Swap πβ{π£} and πΏβπ? (Contributed by NM, 31-Jan-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π = ((ocHβπΎ)βπ) & β’ π = ((mapdβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) β β’ (π β (πβπ) = {π β πΉ β£ βπ£ β π (πβ{π£}) = (πΏβπ)}) | ||
Theorem | mapdval5N 40808* | Value of projectivity from vector space H to dual space. (Contributed by NM, 31-Jan-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π = ((ocHβπΎ)βπ) & β’ π = ((mapdβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) β β’ (π β (πβπ) = βͺ π£ β π {π β πΉ β£ (πβ{π£}) = (πΏβπ)}) | ||
Theorem | mapdordlem1a 40809* | Lemma for mapdord 40813. (Contributed by NM, 27-Jan-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((ocHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (LSHypβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π = {π β πΉ β£ (πβ(πβ(πΏβπ))) β π} & β’ πΆ = {π β πΉ β£ (πβ(πβ(πΏβπ))) = (πΏβπ)} & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β (π½ β π β (π½ β πΆ β§ (πβ(πβ(πΏβπ½))) β π))) | ||
Theorem | mapdordlem1bN 40810* | Lemma for mapdord 40813. (Contributed by NM, 27-Jan-2015.) (New usage is discouraged.) |
β’ πΆ = {π β πΉ β£ (πβ(πβ(πΏβπ))) = (πΏβπ)} β β’ (π½ β πΆ β (π½ β πΉ β§ (πβ(πβ(πΏβπ½))) = (πΏβπ½))) | ||
Theorem | mapdordlem1 40811* | Lemma for mapdord 40813. (Contributed by NM, 27-Jan-2015.) |
β’ π = {π β πΉ β£ (πβ(πβ(πΏβπ))) β π} β β’ (π½ β π β (π½ β πΉ β§ (πβ(πβ(πΏβπ½))) β π)) | ||
Theorem | mapdordlem2 40812* | Lemma for mapdord 40813. Ordering property of projectivity π. TODO: This was proved using some hacked-up older proofs. Maybe simplify; get rid of the π hypothesis. (Contributed by NM, 27-Jan-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ π = ((mapdβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ π = ((ocHβπΎ)βπ) & β’ π΄ = (LSAtomsβπ) & β’ πΉ = (LFnlβπ) & β’ π½ = (LSHypβπ) & β’ πΏ = (LKerβπ) & β’ π = {π β πΉ β£ (πβ(πβ(πΏβπ))) β π½} & β’ πΆ = {π β πΉ β£ (πβ(πβ(πΏβπ))) = (πΏβπ)} β β’ (π β ((πβπ) β (πβπ) β π β π)) | ||
Theorem | mapdord 40813 | Ordering property of the map defined by df-mapd 40800. Property (b) of [Baer] p. 40. (Contributed by NM, 27-Jan-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ π = ((mapdβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β ((πβπ) β (πβπ) β π β π)) | ||
Theorem | mapd11 40814 | The map defined by df-mapd 40800 is one-to-one. Property (c) of [Baer] p. 40. (Contributed by NM, 12-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ π = ((mapdβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β ((πβπ) = (πβπ) β π = π)) | ||
Theorem | mapddlssN 40815 | The mapping of a subspace of vector space H to the dual space is a subspace of the dual space. TODO: Make this obsolete, use mapdcl2 40831 instead. (Contributed by NM, 31-Jan-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ π· = (LDualβπ) & β’ π = (LSubSpβπ·) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) β β’ (π β (πβπ ) β π) | ||
Theorem | mapdsn 40816* | Value of the map defined by df-mapd 40800 at the span of a singleton. (Contributed by NM, 16-Feb-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((ocHβπΎ)βπ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) β β’ (π β (πβ(πβ{π})) = {π β πΉ β£ (πβ{π}) β (πΏβπ)}) | ||
Theorem | mapdsn2 40817* | Value of the map defined by df-mapd 40800 at the span of a singleton. (Contributed by NM, 16-Feb-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((ocHβπΎ)βπ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β (πΏβπΊ) = (πβ{π})) β β’ (π β (πβ(πβ{π})) = {π β πΉ β£ (πΏβπΊ) β (πΏβπ)}) | ||
Theorem | mapdsn3 40818 | Value of the map defined by df-mapd 40800 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 40819* | Value of the map defined by df-mapd 40800 at an atom. (Contributed by NM, 10-Feb-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π΄ = (LSAtomsβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π = ((ocHβπΎ)βπ) & β’ π = ((mapdβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π΄) β β’ (π β (πβπ) = {π β πΉ β£ βπ£ β π (πβ{π£}) = (πΏβπ)}) | ||
Theorem | mapdrvallem2 40820* | Lemma for mapdrval 40822. 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 40821* | Lemma for mapdrval 40822. (Contributed by NM, 2-Feb-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((ocHβπΎ)βπ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π· = (LDualβπ) & β’ π = (LSubSpβπ·) & β’ πΆ = {π β πΉ β£ (πβ(πβ(πΏβπ))) = (πΏβπ)} & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β πΆ) & β’ π = βͺ β β π (πβ(πΏββ)) & β’ π = (Baseβπ) & β’ π΄ = (LSAtomsβπ) & β’ π = (LSpanβπ) & β’ 0 = (0gβπ) & β’ π = (0gβπ·) β β’ (π β {π β πΆ β£ (πβ(πΏβπ)) β π} = π ) | ||
Theorem | mapdrval 40822* | 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 40823* | The map defined by df-mapd 40800 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 40760, mapdrval 40822, lclkrs 40714, lclkr 40708,...) to use π β© π« πΆ? TODO: maybe get rid of $d's for π versus πΎππ; propagate to mapdrn 40824 and any others. (Contributed by NM, 12-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((ocHβπΎ)βπ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π· = (LDualβπ) & β’ π = (LSubSpβπ·) & β’ πΆ = {π β πΉ β£ (πβ(πβ(πΏβπ))) = (πΏβπ)} & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β π:πβ1-1-ontoβ(π β© π« πΆ)) | ||
Theorem | mapdrn 40824* | Range of the map defined by df-mapd 40800. (Contributed by NM, 12-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((ocHβπΎ)βπ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ π· = (LDualβπ) & β’ π = (LSubSpβπ·) & β’ πΆ = {π β πΉ β£ (πβ(πβ(πΏβπ))) = (πΏβπ)} & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β ran π = (π β© π« πΆ)) | ||
Theorem | mapdunirnN 40825* | Union of the range of the map defined by df-mapd 40800. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((ocHβπΎ)βπ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΉ = (LFnlβπ) & β’ πΏ = (LKerβπ) & β’ πΆ = {π β πΉ β£ (πβ(πβ(πΏβπ))) = (πΏβπ)} & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β βͺ ran π = πΆ) | ||
Theorem | mapdrn2 40826 | Range of the map defined by df-mapd 40800. TODO: this seems to be needed a lot in hdmaprnlem3eN 41033 etc. Would it be better to change df-mapd 40800 theorems to use LSubSpβπΆ instead of ran π? (Contributed by NM, 13-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π = (LSubSpβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β ran π = π) | ||
Theorem | mapdcnvcl 40827 | Closure of the converse of the map defined by df-mapd 40800. (Contributed by NM, 13-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β ran π) β β’ (π β (β‘πβπ) β π) | ||
Theorem | mapdcl 40828 | Closure the value of the map defined by df-mapd 40800. (Contributed by NM, 13-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) β β’ (π β (πβπ) β ran π) | ||
Theorem | mapdcnvid1N 40829 | Converse of the value of the map defined by df-mapd 40800. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) β β’ (π β (β‘πβ(πβπ)) = π) | ||
Theorem | mapdsord 40830 | Strong ordering property of themap defined by df-mapd 40800. (Contributed by NM, 13-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β ((πβπ) β (πβπ) β π β π)) | ||
Theorem | mapdcl2 40831 | 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 40832 | Value of the converse of the map defined by df-mapd 40800. (Contributed by NM, 13-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β ran π) β β’ (π β (πβ(β‘πβπ)) = π) | ||
Theorem | mapdcnvordN 40833 | Ordering property of the converse of the map defined by df-mapd 40800. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β ran π) & β’ (π β π β ran π) β β’ (π β ((β‘πβπ) β (β‘πβπ) β π β π)) | ||
Theorem | mapdcnv11N 40834 | The converse of the map defined by df-mapd 40800 is one-to-one. (Contributed by NM, 13-Mar-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β ran π) & β’ (π β π β ran π) β β’ (π β ((β‘πβπ) = (β‘πβπ) β π = π)) | ||
Theorem | mapdcv 40835 | Covering property of the converse of the map defined by df-mapd 40800. (Contributed by NM, 14-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ πΆ = ( βL βπ) & β’ π· = ((LCDualβπΎ)βπ) & β’ πΈ = ( βL βπ·) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (ππΆπ β (πβπ)πΈ(πβπ))) | ||
Theorem | mapdincl 40836 | Closure of dual subspace intersection for the map defined by df-mapd 40800. (Contributed by NM, 12-Apr-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β ran π) & β’ (π β π β ran π) β β’ (π β (π β© π) β ran π) | ||
Theorem | mapdin 40837 | Subspace intersection is preserved by the map defined by df-mapd 40800. Part of property (e) in [Baer] p. 40. (Contributed by NM, 12-Apr-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (πβ(π β© π)) = ((πβπ) β© (πβπ))) | ||
Theorem | mapdlsmcl 40838 | Closure of dual subspace sum for the map defined by df-mapd 40800. (Contributed by NM, 13-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ β = (LSSumβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β ran π) & β’ (π β π β ran π) β β’ (π β (π β π) β ran π) | ||
Theorem | mapdlsm 40839 | Subspace sum is preserved by the map defined by df-mapd 40800. Part of property (e) in [Baer] p. 40. (Contributed by NM, 13-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ β = (LSSumβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (πβ(π β π)) = ((πβπ) β (πβπ))) | ||
Theorem | mapd0 40840 | 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 40841 | Atoms are preserved by the map defined by df-mapd 40800. (Contributed by NM, 29-May-2015.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π΄ = (LSAtomsβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π΅ = (LSAtomsβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π΅) β β’ (π β (β‘πβπ) β π΄) | ||
Theorem | mapdat 40842 | Atoms are preserved by the map defined by df-mapd 40800. Property (g) in [Baer] p. 41. (Contributed by NM, 14-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π΄ = (LSAtomsβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ π΅ = (LSAtomsβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π΄) β β’ (π β (πβπ) β π΅) | ||
Theorem | mapdspex 40843* | 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 40844 | 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 40845 | 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 40846 | 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 40847 | Lemma for mapdpg 40881. 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 40848* | Lemma for mapdpg 40881. 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 40849* | Lemma for mapdpg 40881. (Contributed by NM, 20-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) & β’ (π β π β π) & β’ β = (LSSumβπΆ) & β’ π½ = (LSpanβπΆ) & β’ πΉ = (BaseβπΆ) & β’ (π β π‘ β ((πβ(πβ{π})) β (πβ(πβ{π})))) β β’ (π β π‘ β πΉ) | ||
Theorem | mapdpglem3 40850* | Lemma for mapdpg 40881. 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 40851* | Lemma for mapdpg 40881. (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 40852* | Lemma for mapdpg 40881. (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 40853* | Lemma for mapdpg 40881. 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 40854* | Lemma for mapdpg 40881. 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 40855* | Lemma for mapdpg 40881. 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 40856* | Lemma for mapdpg 40881. 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 40857* | Lemma for mapdpg 40881. (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 40858* | Lemma for mapdpg 40881. TODO: Can some commonality with mapdpglem6 40853 through mapdpglem11 40857 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 40859* | Lemma for mapdpg 40881. (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 40860* | Lemma for mapdpg 40881. (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 40861* | Lemma for mapdpg 40881. (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 40862* | Lemma for mapdpg 40881. 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 40863* | Lemma for mapdpg 40881. 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 40864* | Lemma for mapdpg 40881. 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 40865* | Lemma for mapdpg 40881. 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 40866* | Lemma for mapdpg 40881. 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 40867* | Lemma for mapdpg 40881. (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 40868* | Lemma for mapdpg 40881. 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 40869* | Lemma for mapdpg 40881. 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 40870 | Lemma for mapdpg 40881. (Contributed by NM, 22-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ πΉ = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β πΊ β πΉ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) β β’ (π β πΊ β (0gβπΆ)) | ||
Theorem | mapdpglem30b 40871 | Lemma for mapdpg 40881. (Contributed by NM, 22-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ πΉ = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β πΊ β πΉ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) & β’ (π β (β β πΉ β§ ((πβ(πβ{π})) = (π½β{β}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ β)})))) & β’ (π β (π β πΉ β§ ((πβ(πβ{π})) = (π½β{π}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ π)})))) β β’ (π β π β (0gβπΆ)) | ||
Theorem | mapdpglem25 40872 | Lemma for mapdpg 40881. 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 40873* | Lemma for mapdpg 40881. 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 40874* | Lemma for mapdpg 40881. 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 40875* | Lemma for mapdpg 40881. 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 40876* | Lemma for mapdpg 40881. 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 40877* | Lemma for mapdpg 40881. Baer p. 45 line 18: "Hence we deduce (from mapdpglem28 40876, using lvecindp2 20898) that v = 1 and v = u...". TODO: would it be shorter to have only the π£ = (1rβπ΄) part and use mapdpglem28.u2 in mapdpglem31 40878? (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 40878* | Lemma for mapdpg 40881. 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 40879* | Lemma for mapdpg 40881. Existence part - consolidate hypotheses in mapdpglem23 40869. (Contributed by NM, 21-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ πΉ = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β πΊ β πΉ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) β β’ (π β ββ β πΉ ((πβ(πβ{π})) = (π½β{β}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ β)}))) | ||
Theorem | mapdpglem32 40880* | Lemma for mapdpg 40881. Uniqueness part - consolidate hypotheses in mapdpglem31 40878. (Contributed by NM, 23-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ πΉ = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β πΊ β πΉ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) β β’ ((π β§ (β β πΉ β§ π β πΉ) β§ (((πβ(πβ{π})) = (π½β{β}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ β)})) β§ ((πβ(πβ{π})) = (π½β{π}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ π)})))) β β = π) | ||
Theorem | mapdpg 40881* | 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 40899. (Contributed by NM, 22-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((mapdβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΆ = ((LCDualβπΎ)βπ) & β’ πΉ = (BaseβπΆ) & β’ π = (-gβπΆ) & β’ π½ = (LSpanβπΆ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β πΊ β πΉ) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) β β’ (π β β!β β πΉ ((πβ(πβ{π})) = (π½β{β}) β§ (πβ(πβ{(π β π)})) = (π½β{(πΊπ β)}))) | ||
Theorem | baerlem3lem1 40882 | Lemma for baerlem3 40888. (Contributed by NM, 9-Apr-2015.) |
β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & ⒠⨣ = (+gβπ ) & β’ πΏ = (-gβπ ) & β’ π = (0gβπ ) & β’ πΌ = (invgβπ ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π = ((π Β· π) + (π Β· π))) & β’ (π β π = ((π Β· (π β π)) + (π Β· (π β π)))) β β’ (π β π = (π Β· (π β π))) | ||
Theorem | baerlem5alem1 40883 | Lemma for baerlem5a 40889. (Contributed by NM, 13-Apr-2015.) |
β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & ⒠⨣ = (+gβπ ) & β’ πΏ = (-gβπ ) & β’ π = (0gβπ ) & β’ πΌ = (invgβπ ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π = ((π Β· (π β π)) + (π Β· π))) & β’ (π β π = ((π Β· (π β π)) + (π Β· π))) β β’ (π β π = (π Β· (π β (π + π)))) | ||
Theorem | baerlem5blem1 40884 | Lemma for baerlem5b 40890. (Contributed by NM, 9-Apr-2015.) |
β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & ⒠⨣ = (+gβπ ) & β’ πΏ = (-gβπ ) & β’ π = (0gβπ ) & β’ πΌ = (invgβπ ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π = ((π Β· π) + (π Β· π))) & β’ (π β π = ((π Β· (π β (π + π))) + (π Β· π))) β β’ (π β π = ((πΌβπ) Β· (π + π))) | ||
Theorem | baerlem3lem2 40885 | Lemma for baerlem3 40888. (Contributed by NM, 9-Apr-2015.) |
β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & ⒠⨣ = (+gβπ ) & β’ πΏ = (-gβπ ) & β’ π = (0gβπ ) & β’ πΌ = (invgβπ ) β β’ (π β (πβ{(π β π)}) = (((πβ{π}) β (πβ{π})) β© ((πβ{(π β π)}) β (πβ{(π β π)})))) | ||
Theorem | baerlem5alem2 40886 | Lemma for baerlem5a 40889. (Contributed by NM, 9-Apr-2015.) |
β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & ⒠⨣ = (+gβπ ) & β’ πΏ = (-gβπ ) & β’ π = (0gβπ ) & β’ πΌ = (invgβπ ) β β’ (π β (πβ{(π β (π + π))}) = (((πβ{(π β π)}) β (πβ{π})) β© ((πβ{(π β π)}) β (πβ{π})))) | ||
Theorem | baerlem5blem2 40887 | Lemma for baerlem5b 40890. (Contributed by NM, 13-Apr-2015.) |
β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (Scalarβπ) & β’ π΅ = (Baseβπ ) & ⒠⨣ = (+gβπ ) & β’ πΏ = (-gβπ ) & β’ π = (0gβπ ) & β’ πΌ = (invgβπ ) β β’ (π β (πβ{(π + π)}) = (((πβ{π}) β (πβ{π})) β© ((πβ{(π β (π + π))}) β (πβ{π})))) | ||
Theorem | baerlem3 40888 | 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 40889 | 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 40890 | 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 40891 | 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 40893 is used. (Contributed by NM, 24-May-2015.) (New usage is discouraged.) |
β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) β β’ (π β (πβ{(π β (π β π))}) = (((πβ{(π β π)}) β (πβ{π})) β© ((πβ{(π + π)}) β (πβ{π})))) | ||
Theorem | baerlem5bmN 40892 | 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 40893 is used. (Contributed by NM, 24-May-2015.) (New usage is discouraged.) |
β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β Β¬ π β (πβ{π, π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ + = (+gβπ) β β’ (π β (πβ{(π β π)}) = (((πβ{π}) β (πβ{π})) β© ((πβ{(π β (π β π))}) β (πβ{π})))) | ||
Theorem | baerlem5abmN 40893 | 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 40894 | Vector independence lemma. (Contributed by NM, 29-Apr-2015.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π€ β (π β { 0 })) & β’ (π β (πβ{π}) = (πβ{π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β Β¬ π€ β (πβ{π, π})) & β’ (π β (π + π) β 0 ) β β’ (π β (πβ{(π + π)}) = (πβ{π})) | ||
Theorem | mapdindp1 40895 | Vector independence lemma. (Contributed by NM, 1-May-2015.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π€ β (π β { 0 })) & β’ (π β (πβ{π}) = (πβ{π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β Β¬ π€ β (πβ{π, π})) β β’ (π β (πβ{π}) β (πβ{(π + π)})) | ||
Theorem | mapdindp2 40896 | Vector independence lemma. (Contributed by NM, 1-May-2015.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π€ β (π β { 0 })) & β’ (π β (πβ{π}) = (πβ{π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β Β¬ π€ β (πβ{π, π})) β β’ (π β Β¬ π€ β (πβ{π, (π + π)})) | ||
Theorem | mapdindp3 40897 | Vector independence lemma. (Contributed by NM, 29-Apr-2015.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π€ β (π β { 0 })) & β’ (π β (πβ{π}) = (πβ{π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β Β¬ π€ β (πβ{π, π})) β β’ (π β (πβ{π}) β (πβ{(π€ + π)})) | ||
Theorem | mapdindp4 40898 | Vector independence lemma. (Contributed by NM, 29-Apr-2015.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ (π β π β LVec) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π β (π β { 0 })) & β’ (π β π€ β (π β { 0 })) & β’ (π β (πβ{π}) = (πβ{π})) & β’ (π β (πβ{π}) β (πβ{π})) & β’ (π β Β¬ π€ β (πβ{π, π})) β β’ (π β Β¬ π β (πβ{π, (π€ + π)})) | ||
Theorem | mapdhval 40899* | 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 40900* | Lemmma for ~? mapdh . (Contributed by NM, 3-Apr-2015.) |
β’ π = (0gβπΆ) & β’ πΌ = (π₯ β V β¦ if((2nd βπ₯) = 0 , π, (β©β β π· ((πβ(πβ{(2nd βπ₯)})) = (π½β{β}) β§ (πβ(πβ{((1st β(1st βπ₯)) β (2nd βπ₯))})) = (π½β{((2nd β(1st βπ₯))π β)}))))) & β’ 0 = (0gβπ) & β’ (π β π β π΄) & β’ (π β πΉ β π΅) β β’ (π β (πΌββ¨π, πΉ, 0 β©) = π) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |