![]() |
Metamath
Proof Explorer Theorem List (p. 380 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-30209) |
![]() (30210-31732) |
![]() (31733-47936) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dveel2ALT 37901* | Alternate proof of dveel2 2461 using ax-c16 37854 instead of ax-5 1913. (Contributed by NM, 10-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (Β¬ βπ₯ π₯ = π¦ β (π§ β π¦ β βπ₯ π§ β π¦)) | ||
Theorem | ax12f 37902 | Basis step for constructing a substitution instance of ax-c15 37851 without using ax-c15 37851. We can start with any formula π in which π₯ is not free. (Contributed by NM, 21-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π β βπ₯π) β β’ (Β¬ βπ₯ π₯ = π¦ β (π₯ = π¦ β (π β βπ₯(π₯ = π¦ β π)))) | ||
Theorem | ax12eq 37903 | Basis step for constructing a substitution instance of ax-c15 37851 without using ax-c15 37851. Atomic formula for equality predicate. (Contributed by NM, 22-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (Β¬ βπ₯ π₯ = π¦ β (π₯ = π¦ β (π§ = π€ β βπ₯(π₯ = π¦ β π§ = π€)))) | ||
Theorem | ax12el 37904 | Basis step for constructing a substitution instance of ax-c15 37851 without using ax-c15 37851. Atomic formula for membership predicate. (Contributed by NM, 22-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (Β¬ βπ₯ π₯ = π¦ β (π₯ = π¦ β (π§ β π€ β βπ₯(π₯ = π¦ β π§ β π€)))) | ||
Theorem | ax12indn 37905 | Induction step for constructing a substitution instance of ax-c15 37851 without using ax-c15 37851. Negation case. (Contributed by NM, 21-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (Β¬ βπ₯ π₯ = π¦ β (π₯ = π¦ β (π β βπ₯(π₯ = π¦ β π)))) β β’ (Β¬ βπ₯ π₯ = π¦ β (π₯ = π¦ β (Β¬ π β βπ₯(π₯ = π¦ β Β¬ π)))) | ||
Theorem | ax12indi 37906 | Induction step for constructing a substitution instance of ax-c15 37851 without using ax-c15 37851. Implication case. (Contributed by NM, 21-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (Β¬ βπ₯ π₯ = π¦ β (π₯ = π¦ β (π β βπ₯(π₯ = π¦ β π)))) & β’ (Β¬ βπ₯ π₯ = π¦ β (π₯ = π¦ β (π β βπ₯(π₯ = π¦ β π)))) β β’ (Β¬ βπ₯ π₯ = π¦ β (π₯ = π¦ β ((π β π) β βπ₯(π₯ = π¦ β (π β π))))) | ||
Theorem | ax12indalem 37907 | Lemma for ax12inda2 37909 and ax12inda 37910. (Contributed by NM, 24-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (Β¬ βπ₯ π₯ = π¦ β (π₯ = π¦ β (π β βπ₯(π₯ = π¦ β π)))) β β’ (Β¬ βπ¦ π¦ = π§ β (Β¬ βπ₯ π₯ = π¦ β (π₯ = π¦ β (βπ§π β βπ₯(π₯ = π¦ β βπ§π))))) | ||
Theorem | ax12inda2ALT 37908* | Alternate proof of ax12inda2 37909, slightly more direct and not requiring ax-c16 37854. (Contributed by NM, 4-May-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (Β¬ βπ₯ π₯ = π¦ β (π₯ = π¦ β (π β βπ₯(π₯ = π¦ β π)))) β β’ (Β¬ βπ₯ π₯ = π¦ β (π₯ = π¦ β (βπ§π β βπ₯(π₯ = π¦ β βπ§π)))) | ||
Theorem | ax12inda2 37909* | Induction step for constructing a substitution instance of ax-c15 37851 without using ax-c15 37851. Quantification case. When π§ and π¦ are distinct, this theorem avoids the dummy variables needed by the more general ax12inda 37910. (Contributed by NM, 24-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (Β¬ βπ₯ π₯ = π¦ β (π₯ = π¦ β (π β βπ₯(π₯ = π¦ β π)))) β β’ (Β¬ βπ₯ π₯ = π¦ β (π₯ = π¦ β (βπ§π β βπ₯(π₯ = π¦ β βπ§π)))) | ||
Theorem | ax12inda 37910* | Induction step for constructing a substitution instance of ax-c15 37851 without using ax-c15 37851. Quantification case. (When π§ and π¦ are distinct, ax12inda2 37909 may be used instead to avoid the dummy variable π€ in the proof.) (Contributed by NM, 24-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (Β¬ βπ₯ π₯ = π€ β (π₯ = π€ β (π β βπ₯(π₯ = π€ β π)))) β β’ (Β¬ βπ₯ π₯ = π¦ β (π₯ = π¦ β (βπ§π β βπ₯(π₯ = π¦ β βπ§π)))) | ||
Theorem | ax12v2-o 37911* | Rederivation of ax-c15 37851 from ax12v 2172 (without using ax-c15 37851 or the full ax-12 2171). Thus, the hypothesis (ax12v 2172) provides an alternate axiom that can be used in place of ax-c15 37851. See also axc15 2421. (Contributed by NM, 2-Feb-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π₯ = π§ β (π β βπ₯(π₯ = π§ β π))) β β’ (Β¬ βπ₯ π₯ = π¦ β (π₯ = π¦ β (π β βπ₯(π₯ = π¦ β π)))) | ||
Theorem | ax12a2-o 37912* | Derive ax-c15 37851 from a hypothesis in the form of ax-12 2171, without using ax-12 2171 or ax-c15 37851. The hypothesis is weaker than ax-12 2171, with π§ both distinct from π₯ and not occurring in π. Thus, the hypothesis provides an alternate axiom that can be used in place of ax-12 2171, if we also have ax-c11 37849, which this proof uses. As Theorem ax12 2422 shows, the distinct variable conditions are optional. An open problem is whether we can derive this with ax-c11n 37850 instead of ax-c11 37849. (Contributed by NM, 2-Feb-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π₯ = π§ β (βπ§π β βπ₯(π₯ = π§ β π))) β β’ (Β¬ βπ₯ π₯ = π¦ β (π₯ = π¦ β (π β βπ₯(π₯ = π¦ β π)))) | ||
Theorem | axc11-o 37913 |
Show that ax-c11 37849 can be derived from ax-c11n 37850 and ax-12 2171. An open
problem is whether this theorem can be derived from ax-c11n 37850 and the
others when ax-12 2171 is replaced with ax-c15 37851 or ax12v 2172. See Theorems
axc11nfromc11 37888 for the rederivation of ax-c11n 37850 from axc11 2429.
Normally, axc11 2429 should be used rather than ax-c11 37849 or axc11-o 37913, except by theorems specifically studying the latter's properties. (Contributed by NM, 16-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (βπ₯ π₯ = π¦ β (βπ₯π β βπ¦π)) | ||
Theorem | fsumshftd 37914* | Index shift of a finite sum with a weaker "implicit substitution" hypothesis than fsumshft 15728. The proof demonstrates how this can be derived starting from from fsumshft 15728. (Contributed by NM, 1-Nov-2019.) |
β’ (π β πΎ β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ ((π β§ π β (π...π)) β π΄ β β) & β’ ((π β§ π = (π β πΎ)) β π΄ = π΅) β β’ (π β Ξ£π β (π...π)π΄ = Ξ£π β ((π + πΎ)...(π + πΎ))π΅) | ||
Axiom | ax-riotaBAD 37915 | Define restricted description binder. In case it doesn't exist, we return a set which is not a member of the domain of discourse π΄. See also comments for df-iota 6495. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) WARNING: THIS "AXIOM", WHICH IS THE OLD df-riota 7367, CONFLICTS WITH (THE NEW) df-riota 7367 AND MAKES THE SYSTEM IN set.mm INCONSISTENT. IT IS TEMPORARY AND WILL BE DELETED AFTER ALL USES ARE ELIMINATED. |
β’ (β©π₯ β π΄ π) = if(β!π₯ β π΄ π, (β©π₯(π₯ β π΄ β§ π)), (Undefβ{π₯ β£ π₯ β π΄})) | ||
Theorem | riotaclbgBAD 37916* | Closure of restricted iota. (Contributed by NM, 28-Feb-2013.) (Revised by Mario Carneiro, 24-Dec-2016.) |
β’ (π΄ β π β (β!π₯ β π΄ π β (β©π₯ β π΄ π) β π΄)) | ||
Theorem | riotaclbBAD 37917* | Closure of restricted iota. (Contributed by NM, 15-Sep-2011.) |
β’ π΄ β V β β’ (β!π₯ β π΄ π β (β©π₯ β π΄ π) β π΄) | ||
Theorem | riotasvd 37918* | Deduction version of riotasv 37921. (Contributed by NM, 4-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
β’ (π β π· = (β©π₯ β π΄ βπ¦ β π΅ (π β π₯ = πΆ))) & β’ (π β π· β π΄) β β’ ((π β§ π΄ β π) β ((π¦ β π΅ β§ π) β π· = πΆ)) | ||
Theorem | riotasv2d 37919* | Value of description binder π· for a single-valued class expression πΆ(π¦) (as in e.g. reusv2 5401). Special case of riota2f 7392. (Contributed by NM, 2-Mar-2013.) |
β’ β²π¦π & β’ (π β β²π¦πΉ) & β’ (π β β²π¦π) & β’ (π β π· = (β©π₯ β π΄ βπ¦ β π΅ (π β π₯ = πΆ))) & β’ ((π β§ π¦ = πΈ) β (π β π)) & β’ ((π β§ π¦ = πΈ) β πΆ = πΉ) & β’ (π β π· β π΄) & β’ (π β πΈ β π΅) & β’ (π β π) β β’ ((π β§ π΄ β π) β π· = πΉ) | ||
Theorem | riotasv2s 37920* | The value of description binder π· for a single-valued class expression πΆ(π¦) (as in e.g. reusv2 5401) in the form of a substitution instance. Special case of riota2f 7392. (Contributed by NM, 3-Mar-2013.) (Proof shortened by Mario Carneiro, 6-Dec-2016.) |
β’ π· = (β©π₯ β π΄ βπ¦ β π΅ (π β π₯ = πΆ)) β β’ ((π΄ β π β§ π· β π΄ β§ (πΈ β π΅ β§ [πΈ / π¦]π)) β π· = β¦πΈ / π¦β¦πΆ) | ||
Theorem | riotasv 37921* | Value of description binder π· for a single-valued class expression πΆ(π¦) (as in e.g. reusv2 5401). Special case of riota2f 7392. (Contributed by NM, 26-Jan-2013.) (Proof shortened by Mario Carneiro, 6-Dec-2016.) |
β’ π΄ β V & β’ π· = (β©π₯ β π΄ βπ¦ β π΅ (π β π₯ = πΆ)) β β’ ((π· β π΄ β§ π¦ β π΅ β§ π) β π· = πΆ) | ||
Theorem | riotasv3d 37922* | A property π holding for a representative of a single-valued class expression πΆ(π¦) (see e.g. reusv2 5401) also holds for its description binder π· (in the form of property π). (Contributed by NM, 5-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
β’ β²π¦π & β’ (π β β²π¦π) & β’ (π β π· = (β©π₯ β π΄ βπ¦ β π΅ (π β π₯ = πΆ))) & β’ ((π β§ πΆ = π·) β (π β π)) & β’ (π β ((π¦ β π΅ β§ π) β π)) & β’ (π β π· β π΄) & β’ (π β βπ¦ β π΅ π) β β’ ((π β§ π΄ β π) β π) | ||
Theorem | elimhyps 37923 | A version of elimhyp 4593 using explicit substitution. (Contributed by NM, 15-Jun-2019.) |
β’ [π΅ / π₯]π β β’ [if(π, π₯, π΅) / π₯]π | ||
Theorem | dedths 37924 | A version of weak deduction theorem dedth 4586 using explicit substitution. (Contributed by NM, 15-Jun-2019.) |
β’ [if(π, π₯, π΅) / π₯]π β β’ (π β π) | ||
Theorem | renegclALT 37925 | Closure law for negative of reals. Demonstrates use of weak deduction theorem with explicit substitution. The proof is much longer than that of renegcl 11525. (Contributed by NM, 15-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π΄ β β β -π΄ β β) | ||
Theorem | elimhyps2 37926 | Generalization of elimhyps 37923 that is not useful unless we can separately prove β’ π΄ β V. (Contributed by NM, 13-Jun-2019.) |
β’ [π΅ / π₯]π β β’ [if([π΄ / π₯]π, π΄, π΅) / π₯]π | ||
Theorem | dedths2 37927 | Generalization of dedths 37924 that is not useful unless we can separately prove β’ π΄ β V. (Contributed by NM, 13-Jun-2019.) |
β’ [if([π΄ / π₯]π, π΄, π΅) / π₯]π β β’ ([π΄ / π₯]π β [π΄ / π₯]π) | ||
Theorem | nfcxfrdf 37928 | A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by NM, 19-Nov-2020.) |
β’ β²π₯π & β’ (π β π΄ = π΅) & β’ (π β β²π₯π΅) β β’ (π β β²π₯π΄) | ||
Theorem | nfded 37929 | A deduction theorem that converts a not-free inference directly to deduction form. The first hypothesis is the hypothesis of the deduction form. The second is an equality deduction (e.g., (β²π₯π΄ β βͺ {π¦ β£ βπ₯π¦ β π΄} = βͺ π΄)) that starts from abidnf 3698. The last is assigned to the inference form (e.g., β²π₯βͺ {π¦ β£ βπ₯π¦ β π΄}) whose hypothesis is satisfied using nfaba1 2911. (Contributed by NM, 19-Nov-2020.) |
β’ (π β β²π₯π΄) & β’ (β²π₯π΄ β π΅ = πΆ) & β’ β²π₯π΅ β β’ (π β β²π₯πΆ) | ||
Theorem | nfded2 37930 | A deduction theorem that converts a not-free inference directly to deduction form. The first 2 hypotheses are the hypotheses of the deduction form. The third is an equality deduction (e.g., ((β²π₯π΄ β§ β²π₯π΅) β β¨{π¦ β£ βπ₯π¦ β π΄}, {π¦ β£ βπ₯π¦ β π΅}β© = β¨π΄, π΅β©) for nfopd 4890) that starts from abidnf 3698. The last is assigned to the inference form (e.g., β²π₯β¨{π¦ β£ βπ₯π¦ β π΄}, {π¦ β£ βπ₯π¦ β π΅}β© for nfop 4889) whose hypotheses are satisfied using nfaba1 2911. (Contributed by NM, 19-Nov-2020.) |
β’ (π β β²π₯π΄) & β’ (π β β²π₯π΅) & β’ ((β²π₯π΄ β§ β²π₯π΅) β πΆ = π·) & β’ β²π₯πΆ β β’ (π β β²π₯π·) | ||
Theorem | nfunidALT2 37931 | Deduction version of nfuni 4915. (Contributed by NM, 19-Nov-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π β β²π₯π΄) β β’ (π β β²π₯βͺ π΄) | ||
Theorem | nfunidALT 37932 | Deduction version of nfuni 4915. (Contributed by NM, 19-Nov-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π β β²π₯π΄) β β’ (π β β²π₯βͺ π΄) | ||
Theorem | nfopdALT 37933 | Deduction version of bound-variable hypothesis builder nfop 4889. This shows how the deduction version of a not-free theorem such as nfop 4889 can be created from the corresponding not-free inference theorem. (Contributed by NM, 19-Nov-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π β β²π₯π΄) & β’ (π β β²π₯π΅) β β’ (π β β²π₯β¨π΄, π΅β©) | ||
Theorem | cnaddcom 37934 | Recover the commutative law of addition for complex numbers from the Abelian group structure. (Contributed by NM, 17-Mar-2013.) (Proof modification is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ + π΅) = (π΅ + π΄)) | ||
Theorem | toycom 37935* | Show the commutative law for an operation π on a toy structure class πΆ of commuatitive operations on β. This illustrates how a structure class can be partially specialized. In practice, we would ordinarily define a new constant such as "CAbel" in place of πΆ. (Contributed by NM, 17-Mar-2013.) (Proof modification is discouraged.) |
β’ πΆ = {π β Abel β£ (Baseβπ) = β} & β’ + = (+gβπΎ) β β’ ((πΎ β πΆ β§ π΄ β β β§ π΅ β β) β (π΄ + π΅) = (π΅ + π΄)) | ||
Syntax | clsa 37936 | Extend class notation with all 1-dim subspaces (atoms) of a left module or left vector space. |
class LSAtoms | ||
Syntax | clsh 37937 | Extend class notation with all subspaces of a left module or left vector space that are hyperplanes. |
class LSHyp | ||
Definition | df-lsatoms 37938* | Define the set of all 1-dim subspaces (atoms) of a left module or left vector space. (Contributed by NM, 9-Apr-2014.) |
β’ LSAtoms = (π€ β V β¦ ran (π£ β ((Baseβπ€) β {(0gβπ€)}) β¦ ((LSpanβπ€)β{π£}))) | ||
Definition | df-lshyp 37939* | Define the set of all hyperplanes of a left module or left vector space. Also called co-atoms, these are subspaces that are one dimension less than the full space. (Contributed by NM, 29-Jun-2014.) |
β’ LSHyp = (π€ β V β¦ {π β (LSubSpβπ€) β£ (π β (Baseβπ€) β§ βπ£ β (Baseβπ€)((LSpanβπ€)β(π βͺ {π£})) = (Baseβπ€))}) | ||
Theorem | lshpset 37940* | The set of all hyperplanes of a left module or left vector space. The vector π£ is called a generating vector for the hyperplane. (Contributed by NM, 29-Jun-2014.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ π = (LSubSpβπ) & β’ π» = (LSHypβπ) β β’ (π β π β π» = {π β π β£ (π β π β§ βπ£ β π (πβ(π βͺ {π£})) = π)}) | ||
Theorem | islshp 37941* | The predicate "is a hyperplane" (of a left module or left vector space). (Contributed by NM, 29-Jun-2014.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ π = (LSubSpβπ) & β’ π» = (LSHypβπ) β β’ (π β π β (π β π» β (π β π β§ π β π β§ βπ£ β π (πβ(π βͺ {π£})) = π))) | ||
Theorem | islshpsm 37942* | Hyperplane properties expressed with subspace sum. (Contributed by NM, 3-Jul-2014.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π» = (LSHypβπ) & β’ (π β π β LMod) β β’ (π β (π β π» β (π β π β§ π β π β§ βπ£ β π (π β (πβ{π£})) = π))) | ||
Theorem | lshplss 37943 | A hyperplane is a subspace. (Contributed by NM, 3-Jul-2014.) |
β’ π = (LSubSpβπ) & β’ π» = (LSHypβπ) & β’ (π β π β LMod) & β’ (π β π β π») β β’ (π β π β π) | ||
Theorem | lshpne 37944 | A hyperplane is not equal to the vector space. (Contributed by NM, 4-Jul-2014.) |
β’ π = (Baseβπ) & β’ π» = (LSHypβπ) & β’ (π β π β LMod) & β’ (π β π β π») β β’ (π β π β π) | ||
Theorem | lshpnel 37945 | A hyperplane's generating vector does not belong to the hyperplane. (Contributed by NM, 3-Jul-2014.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ β = (LSSumβπ) & β’ π» = (LSHypβπ) & β’ (π β π β LMod) & β’ (π β π β π») & β’ (π β π β π) & β’ (π β (π β (πβ{π})) = π) β β’ (π β Β¬ π β π) | ||
Theorem | lshpnelb 37946 | The subspace sum of a hyperplane and the span of an element equals the vector space iff the element is not in the hyperplane. (Contributed by NM, 2-Oct-2014.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ β = (LSSumβπ) & β’ π» = (LSHypβπ) & β’ (π β π β LVec) & β’ (π β π β π») & β’ (π β π β π) β β’ (π β (Β¬ π β π β (π β (πβ{π})) = π)) | ||
Theorem | lshpnel2N 37947 | Condition that determines a hyperplane. (Contributed by NM, 3-Oct-2014.) (New usage is discouraged.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) & β’ β = (LSSumβπ) & β’ π» = (LSHypβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β Β¬ π β π) β β’ (π β (π β π» β (π β (πβ{π})) = π)) | ||
Theorem | lshpne0 37948 | The member of the span in the hyperplane definition does not belong to the hyperplane. (Contributed by NM, 14-Jul-2014.) (Proof shortened by AV, 19-Jul-2022.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ β = (LSSumβπ) & β’ π» = (LSHypβπ) & β’ 0 = (0gβπ) & β’ (π β π β LMod) & β’ (π β π β π») & β’ (π β π β π) & β’ (π β (π β (πβ{π})) = π) β β’ (π β π β 0 ) | ||
Theorem | lshpdisj 37949 | A hyperplane and the span in the hyperplane definition are disjoint. (Contributed by NM, 3-Jul-2014.) |
β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ β = (LSSumβπ) & β’ π» = (LSHypβπ) & β’ (π β π β LVec) & β’ (π β π β π») & β’ (π β π β π) & β’ (π β (π β (πβ{π})) = π) β β’ (π β (π β© (πβ{π})) = { 0 }) | ||
Theorem | lshpcmp 37950 | If two hyperplanes are comparable, they are equal. (Contributed by NM, 9-Oct-2014.) |
β’ π» = (LSHypβπ) & β’ (π β π β LVec) & β’ (π β π β π») & β’ (π β π β π») β β’ (π β (π β π β π = π)) | ||
Theorem | lshpinN 37951 | The intersection of two different hyperplanes is not a hyperplane. (Contributed by NM, 29-Oct-2014.) (New usage is discouraged.) |
β’ π» = (LSHypβπ) & β’ (π β π β LVec) & β’ (π β π β π») & β’ (π β π β π») β β’ (π β ((π β© π) β π» β π = π)) | ||
Theorem | lsatset 37952* | The set of all 1-dim subspaces (atoms) of a left module or left vector space. (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 22-Sep-2015.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) β β’ (π β π β π΄ = ran (π£ β (π β { 0 }) β¦ (πβ{π£}))) | ||
Theorem | islsat 37953* | The predicate "is a 1-dim subspace (atom)" (of a left module or left vector space). (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 24-Jun-2014.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) β β’ (π β π β (π β π΄ β βπ₯ β (π β { 0 })π = (πβ{π₯}))) | ||
Theorem | lsatlspsn2 37954 | The span of a nonzero singleton is an atom. TODO: make this obsolete and use lsatlspsn 37955 instead? (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 24-Jun-2014.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) β β’ ((π β LMod β§ π β π β§ π β 0 ) β (πβ{π}) β π΄) | ||
Theorem | lsatlspsn 37955 | The span of a nonzero singleton is an atom. (Contributed by NM, 16-Jan-2015.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β (π β { 0 })) β β’ (π β (πβ{π}) β π΄) | ||
Theorem | islsati 37956* | A 1-dim subspace (atom) (of a left module or left vector space) equals the span of some vector. (Contributed by NM, 1-Oct-2014.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ π΄ = (LSAtomsβπ) β β’ ((π β π β§ π β π΄) β βπ£ β π π = (πβ{π£})) | ||
Theorem | lsateln0 37957* | A 1-dim subspace (atom) (of a left module or left vector space) contains a nonzero vector. (Contributed by NM, 2-Jan-2015.) |
β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β π΄) β β’ (π β βπ£ β π π£ β 0 ) | ||
Theorem | lsatlss 37958 | The set of 1-dim subspaces is a set of subspaces. (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 24-Jun-2014.) |
β’ π = (LSubSpβπ) & β’ π΄ = (LSAtomsβπ) β β’ (π β LMod β π΄ β π) | ||
Theorem | lsatlssel 37959 | An atom is a subspace. (Contributed by NM, 25-Aug-2014.) |
β’ π = (LSubSpβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β π΄) β β’ (π β π β π) | ||
Theorem | lsatssv 37960 | An atom is a set of vectors. (Contributed by NM, 27-Feb-2015.) |
β’ π = (Baseβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β π΄) β β’ (π β π β π) | ||
Theorem | lsatn0 37961 | A 1-dim subspace (atom) of a left module or left vector space is nonzero. (atne0 31636 analog.) (Contributed by NM, 25-Aug-2014.) |
β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β π΄) β β’ (π β π β { 0 }) | ||
Theorem | lsatspn0 37962 | The span of a vector is an atom iff the vector is nonzero. (Contributed by NM, 4-Feb-2015.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β π) β β’ (π β ((πβ{π}) β π΄ β π β 0 )) | ||
Theorem | lsator0sp 37963 | The span of a vector is either an atom or the zero subspace. (Contributed by NM, 15-Mar-2015.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β π) β β’ (π β ((πβ{π}) β π΄ β¨ (πβ{π}) = { 0 })) | ||
Theorem | lsatssn0 37964 | A subspace (or any class) including an atom is nonzero. (Contributed by NM, 3-Feb-2015.) |
β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β π΄) & β’ (π β π β π) β β’ (π β π β { 0 }) | ||
Theorem | lsatcmp 37965 | If two atoms are comparable, they are equal. (atsseq 31638 analog.) TODO: can lspsncmp 20735 shorten this? (Contributed by NM, 25-Aug-2014.) |
β’ π΄ = (LSAtomsβπ) & β’ (π β π β LVec) & β’ (π β π β π΄) & β’ (π β π β π΄) β β’ (π β (π β π β π = π)) | ||
Theorem | lsatcmp2 37966 | If an atom is included in at-most an atom, they are equal. More general version of lsatcmp 37965. TODO: can lspsncmp 20735 shorten this? (Contributed by NM, 3-Feb-2015.) |
β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LVec) & β’ (π β π β π΄) & β’ (π β (π β π΄ β¨ π = { 0 })) β β’ (π β (π β π β π = π)) | ||
Theorem | lsatel 37967 | A nonzero vector in an atom determines the atom. (Contributed by NM, 25-Aug-2014.) |
β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LVec) & β’ (π β π β π΄) & β’ (π β π β π) & β’ (π β π β 0 ) β β’ (π β π = (πβ{π})) | ||
Theorem | lsatelbN 37968 | A nonzero vector in an atom determines the atom. (Contributed by NM, 3-Feb-2015.) (New usage is discouraged.) |
β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LVec) & β’ (π β π β (π β { 0 })) & β’ (π β π β π΄) β β’ (π β (π β π β π = (πβ{π}))) | ||
Theorem | lsat2el 37969 | Two atoms sharing a nonzero vector are equal. (Contributed by NM, 8-Mar-2015.) |
β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LVec) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β π β 0 ) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β π = π) | ||
Theorem | lsmsat 37970* | Convert comparison of atom with sum of subspaces to a comparison to sum with atom. (elpaddatiN 38768 analog.) TODO: any way to shorten this? (Contributed by NM, 15-Jan-2015.) |
β’ 0 = (0gβπ) & β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π΄) & β’ (π β π β { 0 }) & β’ (π β π β (π β π)) β β’ (π β βπ β π΄ (π β π β§ π β (π β π))) | ||
Theorem | lsatfixedN 37971* | Show equality with the span of the sum of two vectors, one of which (π) is fixed in advance. Compare lspfixed 20747. (Contributed by NM, 29-May-2015.) (New usage is discouraged.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LVec) & β’ (π β π β π΄) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β (πβ{π})) & β’ (π β π β (πβ{π})) & β’ (π β π β (πβ{π, π})) β β’ (π β βπ§ β ((πβ{π}) β { 0 })π = (πβ{(π + π§)})) | ||
Theorem | lsmsatcv 37972 | Subspace sum has the covering property (using spans of singletons to represent atoms). Similar to Exercise 5 of [Kalmbach] p. 153. (spansncvi 30943 analog.) Explicit atom version of lsmcv 20760. (Contributed by NM, 29-Oct-2014.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π΄) β β’ ((π β§ π β π β§ π β (π β π)) β π = (π β π)) | ||
Theorem | lssatomic 37973* | The lattice of subspaces is atomic, i.e. any nonzero element is greater than or equal to some atom. (shatomici 31649 analog.) (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β { 0 }) β β’ (π β βπ β π΄ π β π) | ||
Theorem | lssats 37974* | The lattice of subspaces is atomistic, i.e. any element is the supremum of its atoms. Part of proof of Theorem 16.9 of [MaedaMaeda] p. 70. Hypothesis (shatomistici 31652 analog.) (Contributed by NM, 9-Apr-2014.) |
β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) & β’ π΄ = (LSAtomsβπ) β β’ ((π β LMod β§ π β π) β π = (πββͺ {π₯ β π΄ β£ π₯ β π})) | ||
Theorem | lpssat 37975* | Two subspaces in a proper subset relationship imply the existence of an atom less than or equal to one but not the other. (chpssati 31654 analog.) (Contributed by NM, 11-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β βπ β π΄ (π β π β§ Β¬ π β π)) | ||
Theorem | lrelat 37976* | Subspaces are relatively atomic. Remark 2 of [Kalmbach] p. 149. (chrelati 31655 analog.) (Contributed by NM, 11-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β βπ β π΄ (π β (π β π) β§ (π β π) β π)) | ||
Theorem | lssatle 37977* | The ordering of two subspaces is determined by the atoms under them. (chrelat3 31662 analog.) (Contributed by NM, 29-Oct-2014.) |
β’ π = (LSubSpβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (π β π β βπ β π΄ (π β π β π β π))) | ||
Theorem | lssat 37978* | Two subspaces in a proper subset relationship imply the existence of a 1-dim subspace less than or equal to one but not the other. (chpssati 31654 analog.) (Contributed by NM, 9-Apr-2014.) |
β’ π = (LSubSpβπ) & β’ π΄ = (LSAtomsβπ) β β’ (((π β LMod β§ π β π β§ π β π) β§ π β π) β βπ β π΄ (π β π β§ Β¬ π β π)) | ||
Theorem | islshpat 37979* | Hyperplane properties expressed with subspace sum and an atom. TODO: can proof be shortened? Seems long for a simple variation of islshpsm 37942. (Contributed by NM, 11-Jan-2015.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π» = (LSHypβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) β β’ (π β (π β π» β (π β π β§ π β π β§ βπ β π΄ (π β π) = π))) | ||
Syntax | clcv 37980 | Extend class notation with the covering relation for a left module or left vector space. |
class βL | ||
Definition | df-lcv 37981* | Define the covering relation for subspaces of a left vector space. Similar to Definition 3.2.18 of [PtakPulmannova] p. 68. Ptak/Pulmannova's notation π΄( βL βπ)π΅ is read "π΅ covers π΄ " or "π΄ is covered by π΅ " , and it means that π΅ is larger than π΄ and there is nothing in between. See lcvbr 37983 for binary relation. (df-cv 31570 analog.) (Contributed by NM, 7-Jan-2015.) |
β’ βL = (π€ β V β¦ {β¨π‘, π’β© β£ ((π‘ β (LSubSpβπ€) β§ π’ β (LSubSpβπ€)) β§ (π‘ β π’ β§ Β¬ βπ β (LSubSpβπ€)(π‘ β π β§ π β π’)))}) | ||
Theorem | lcvfbr 37982* | The covers relation for a left vector space (or a left module). (Contributed by NM, 7-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β π) β β’ (π β πΆ = {β¨π‘, π’β© β£ ((π‘ β π β§ π’ β π) β§ (π‘ β π’ β§ Β¬ βπ β π (π‘ β π β§ π β π’)))}) | ||
Theorem | lcvbr 37983* | The covers relation for a left vector space (or a left module). (cvbr 31573 analog.) (Contributed by NM, 9-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (ππΆπ β (π β π β§ Β¬ βπ β π (π β π β§ π β π)))) | ||
Theorem | lcvbr2 37984* | The covers relation for a left vector space (or a left module). (cvbr2 31574 analog.) (Contributed by NM, 9-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (ππΆπ β (π β π β§ βπ β π ((π β π β§ π β π) β π = π)))) | ||
Theorem | lcvbr3 37985* | The covers relation for a left vector space (or a left module). (Contributed by NM, 9-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (ππΆπ β (π β π β§ βπ β π ((π β π β§ π β π) β (π = π β¨ π = π))))) | ||
Theorem | lcvpss 37986 | The covers relation implies proper subset. (cvpss 31576 analog.) (Contributed by NM, 7-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β ππΆπ) β β’ (π β π β π) | ||
Theorem | lcvnbtwn 37987 | The covers relation implies no in-betweenness. (cvnbtwn 31577 analog.) (Contributed by NM, 7-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π πΆπ) β β’ (π β Β¬ (π β π β§ π β π)) | ||
Theorem | lcvntr 37988 | The covers relation is not transitive. (cvntr 31583 analog.) (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π πΆπ) & β’ (π β ππΆπ) β β’ (π β Β¬ π πΆπ) | ||
Theorem | lcvnbtwn2 37989 | The covers relation implies no in-betweenness. (cvnbtwn2 31578 analog.) (Contributed by NM, 7-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π πΆπ) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β π = π) | ||
Theorem | lcvnbtwn3 37990 | The covers relation implies no in-betweenness. (cvnbtwn3 31579 analog.) (Contributed by NM, 7-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π πΆπ) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β π = π ) | ||
Theorem | lsmcv2 37991 | Subspace sum has the covering property (using spans of singletons to represent atoms). Proposition 1(ii) of [Kalmbach] p. 153. (spansncv2 31584 analog.) (Contributed by NM, 10-Jan-2015.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) & β’ β = (LSSumβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β Β¬ (πβ{π}) β π) β β’ (π β ππΆ(π β (πβ{π}))) | ||
Theorem | lcvat 37992* | If a subspace covers another, it equals the other joined with some atom. This is a consequence of relative atomicity. (cvati 31657 analog.) (Contributed by NM, 11-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π΄ = (LSAtomsβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β ππΆπ) β β’ (π β βπ β π΄ (π β π) = π) | ||
Theorem | lsatcv0 37993 | An atom covers the zero subspace. (atcv0 31633 analog.) (Contributed by NM, 7-Jan-2015.) |
β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LVec) & β’ (π β π β π΄) β β’ (π β { 0 }πΆπ) | ||
Theorem | lsatcveq0 37994 | A subspace covered by an atom must be the zero subspace. (atcveq0 31639 analog.) (Contributed by NM, 7-Jan-2015.) |
β’ 0 = (0gβπ) & β’ π = (LSubSpβπ) & β’ π΄ = (LSAtomsβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β π΄) β β’ (π β (ππΆπ β π = { 0 })) | ||
Theorem | lsat0cv 37995 | A subspace is an atom iff it covers the zero subspace. This could serve as an alternate definition of an atom. TODO: this is a quick-and-dirty proof that could probably be more efficient. (Contributed by NM, 14-Mar-2015.) |
β’ 0 = (0gβπ) & β’ π = (LSubSpβπ) & β’ π΄ = (LSAtomsβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LVec) & β’ (π β π β π) β β’ (π β (π β π΄ β { 0 }πΆπ)) | ||
Theorem | lcvexchlem1 37996 | Lemma for lcvexch 38001. (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (π β (π β π) β (π β© π) β π)) | ||
Theorem | lcvexchlem2 37997 | Lemma for lcvexch 38001. (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β (π β© π) β π ) & β’ (π β π β π) β β’ (π β ((π β π) β© π) = π ) | ||
Theorem | lcvexchlem3 37998 | Lemma for lcvexch 38001. (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π ) & β’ (π β π β (π β π)) β β’ (π β ((π β© π) β π) = π ) | ||
Theorem | lcvexchlem4 37999 | Lemma for lcvexch 38001. (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β ππΆ(π β π)) β β’ (π β (π β© π)πΆπ) | ||
Theorem | lcvexchlem5 38000 | Lemma for lcvexch 38001. (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β (π β© π)πΆπ) β β’ (π β ππΆ(π β π)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |