![]() |
Metamath
Proof Explorer Theorem List (p. 384 of 481) | < 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-30640) |
![]() (30641-32163) |
![]() (32164-48040) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ax12eq 38301 | Basis step for constructing a substitution instance of ax-c15 38249 without using ax-c15 38249. Atomic formula for equality predicate. (Contributed by NM, 22-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (Β¬ βπ₯ π₯ = π¦ β (π₯ = π¦ β (π§ = π€ β βπ₯(π₯ = π¦ β π§ = π€)))) | ||
Theorem | ax12el 38302 | Basis step for constructing a substitution instance of ax-c15 38249 without using ax-c15 38249. Atomic formula for membership predicate. (Contributed by NM, 22-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (Β¬ βπ₯ π₯ = π¦ β (π₯ = π¦ β (π§ β π€ β βπ₯(π₯ = π¦ β π§ β π€)))) | ||
Theorem | ax12indn 38303 | Induction step for constructing a substitution instance of ax-c15 38249 without using ax-c15 38249. Negation case. (Contributed by NM, 21-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (Β¬ βπ₯ π₯ = π¦ β (π₯ = π¦ β (π β βπ₯(π₯ = π¦ β π)))) β β’ (Β¬ βπ₯ π₯ = π¦ β (π₯ = π¦ β (Β¬ π β βπ₯(π₯ = π¦ β Β¬ π)))) | ||
Theorem | ax12indi 38304 | Induction step for constructing a substitution instance of ax-c15 38249 without using ax-c15 38249. Implication case. (Contributed by NM, 21-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (Β¬ βπ₯ π₯ = π¦ β (π₯ = π¦ β (π β βπ₯(π₯ = π¦ β π)))) & β’ (Β¬ βπ₯ π₯ = π¦ β (π₯ = π¦ β (π β βπ₯(π₯ = π¦ β π)))) β β’ (Β¬ βπ₯ π₯ = π¦ β (π₯ = π¦ β ((π β π) β βπ₯(π₯ = π¦ β (π β π))))) | ||
Theorem | ax12indalem 38305 | Lemma for ax12inda2 38307 and ax12inda 38308. (Contributed by NM, 24-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (Β¬ βπ₯ π₯ = π¦ β (π₯ = π¦ β (π β βπ₯(π₯ = π¦ β π)))) β β’ (Β¬ βπ¦ π¦ = π§ β (Β¬ βπ₯ π₯ = π¦ β (π₯ = π¦ β (βπ§π β βπ₯(π₯ = π¦ β βπ§π))))) | ||
Theorem | ax12inda2ALT 38306* | Alternate proof of ax12inda2 38307, slightly more direct and not requiring ax-c16 38252. (Contributed by NM, 4-May-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (Β¬ βπ₯ π₯ = π¦ β (π₯ = π¦ β (π β βπ₯(π₯ = π¦ β π)))) β β’ (Β¬ βπ₯ π₯ = π¦ β (π₯ = π¦ β (βπ§π β βπ₯(π₯ = π¦ β βπ§π)))) | ||
Theorem | ax12inda2 38307* | Induction step for constructing a substitution instance of ax-c15 38249 without using ax-c15 38249. Quantification case. When π§ and π¦ are distinct, this theorem avoids the dummy variables needed by the more general ax12inda 38308. (Contributed by NM, 24-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (Β¬ βπ₯ π₯ = π¦ β (π₯ = π¦ β (π β βπ₯(π₯ = π¦ β π)))) β β’ (Β¬ βπ₯ π₯ = π¦ β (π₯ = π¦ β (βπ§π β βπ₯(π₯ = π¦ β βπ§π)))) | ||
Theorem | ax12inda 38308* | Induction step for constructing a substitution instance of ax-c15 38249 without using ax-c15 38249. Quantification case. (When π§ and π¦ are distinct, ax12inda2 38307 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 38309* | Rederivation of ax-c15 38249 from ax12v 2164 (without using ax-c15 38249 or the full ax-12 2163). Thus, the hypothesis (ax12v 2164) provides an alternate axiom that can be used in place of ax-c15 38249. See also axc15 2413. (Contributed by NM, 2-Feb-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π₯ = π§ β (π β βπ₯(π₯ = π§ β π))) β β’ (Β¬ βπ₯ π₯ = π¦ β (π₯ = π¦ β (π β βπ₯(π₯ = π¦ β π)))) | ||
Theorem | ax12a2-o 38310* | Derive ax-c15 38249 from a hypothesis in the form of ax-12 2163, without using ax-12 2163 or ax-c15 38249. The hypothesis is weaker than ax-12 2163, with π§ both distinct from π₯ and not occurring in π. Thus, the hypothesis provides an alternate axiom that can be used in place of ax-12 2163, if we also have ax-c11 38247, which this proof uses. As Theorem ax12 2414 shows, the distinct variable conditions are optional. An open problem is whether we can derive this with ax-c11n 38248 instead of ax-c11 38247. (Contributed by NM, 2-Feb-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π₯ = π§ β (βπ§π β βπ₯(π₯ = π§ β π))) β β’ (Β¬ βπ₯ π₯ = π¦ β (π₯ = π¦ β (π β βπ₯(π₯ = π¦ β π)))) | ||
Theorem | axc11-o 38311 |
Show that ax-c11 38247 can be derived from ax-c11n 38248 and ax-12 2163. An open
problem is whether this theorem can be derived from ax-c11n 38248 and the
others when ax-12 2163 is replaced with ax-c15 38249 or ax12v 2164. See Theorems
axc11nfromc11 38286 for the rederivation of ax-c11n 38248 from axc11 2421.
Normally, axc11 2421 should be used rather than ax-c11 38247 or axc11-o 38311, 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 38312* | Index shift of a finite sum with a weaker "implicit substitution" hypothesis than fsumshft 15723. The proof demonstrates how this can be derived starting from from fsumshft 15723. (Contributed by NM, 1-Nov-2019.) |
β’ (π β πΎ β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ ((π β§ π β (π...π)) β π΄ β β) & β’ ((π β§ π = (π β πΎ)) β π΄ = π΅) β β’ (π β Ξ£π β (π...π)π΄ = Ξ£π β ((π + πΎ)...(π + πΎ))π΅) | ||
Axiom | ax-riotaBAD 38313 | 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 6485. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) WARNING: THIS "AXIOM", WHICH IS THE OLD df-riota 7357, CONFLICTS WITH (THE NEW) df-riota 7357 AND MAKES THE SYSTEM IN set.mm INCONSISTENT. IT IS TEMPORARY AND WILL BE DELETED AFTER ALL USES ARE ELIMINATED. |
β’ (β©π₯ β π΄ π) = if(β!π₯ β π΄ π, (β©π₯(π₯ β π΄ β§ π)), (Undefβ{π₯ β£ π₯ β π΄})) | ||
Theorem | riotaclbgBAD 38314* | Closure of restricted iota. (Contributed by NM, 28-Feb-2013.) (Revised by Mario Carneiro, 24-Dec-2016.) |
β’ (π΄ β π β (β!π₯ β π΄ π β (β©π₯ β π΄ π) β π΄)) | ||
Theorem | riotaclbBAD 38315* | Closure of restricted iota. (Contributed by NM, 15-Sep-2011.) |
β’ π΄ β V β β’ (β!π₯ β π΄ π β (β©π₯ β π΄ π) β π΄) | ||
Theorem | riotasvd 38316* | Deduction version of riotasv 38319. (Contributed by NM, 4-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
β’ (π β π· = (β©π₯ β π΄ βπ¦ β π΅ (π β π₯ = πΆ))) & β’ (π β π· β π΄) β β’ ((π β§ π΄ β π) β ((π¦ β π΅ β§ π) β π· = πΆ)) | ||
Theorem | riotasv2d 38317* | Value of description binder π· for a single-valued class expression πΆ(π¦) (as in e.g. reusv2 5391). Special case of riota2f 7382. (Contributed by NM, 2-Mar-2013.) |
β’ β²π¦π & β’ (π β β²π¦πΉ) & β’ (π β β²π¦π) & β’ (π β π· = (β©π₯ β π΄ βπ¦ β π΅ (π β π₯ = πΆ))) & β’ ((π β§ π¦ = πΈ) β (π β π)) & β’ ((π β§ π¦ = πΈ) β πΆ = πΉ) & β’ (π β π· β π΄) & β’ (π β πΈ β π΅) & β’ (π β π) β β’ ((π β§ π΄ β π) β π· = πΉ) | ||
Theorem | riotasv2s 38318* | The value of description binder π· for a single-valued class expression πΆ(π¦) (as in e.g. reusv2 5391) in the form of a substitution instance. Special case of riota2f 7382. (Contributed by NM, 3-Mar-2013.) (Proof shortened by Mario Carneiro, 6-Dec-2016.) |
β’ π· = (β©π₯ β π΄ βπ¦ β π΅ (π β π₯ = πΆ)) β β’ ((π΄ β π β§ π· β π΄ β§ (πΈ β π΅ β§ [πΈ / π¦]π)) β π· = β¦πΈ / π¦β¦πΆ) | ||
Theorem | riotasv 38319* | Value of description binder π· for a single-valued class expression πΆ(π¦) (as in e.g. reusv2 5391). Special case of riota2f 7382. (Contributed by NM, 26-Jan-2013.) (Proof shortened by Mario Carneiro, 6-Dec-2016.) |
β’ π΄ β V & β’ π· = (β©π₯ β π΄ βπ¦ β π΅ (π β π₯ = πΆ)) β β’ ((π· β π΄ β§ π¦ β π΅ β§ π) β π· = πΆ) | ||
Theorem | riotasv3d 38320* | A property π holding for a representative of a single-valued class expression πΆ(π¦) (see e.g. reusv2 5391) 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 38321 | A version of elimhyp 4585 using explicit substitution. (Contributed by NM, 15-Jun-2019.) |
β’ [π΅ / π₯]π β β’ [if(π, π₯, π΅) / π₯]π | ||
Theorem | dedths 38322 | A version of weak deduction theorem dedth 4578 using explicit substitution. (Contributed by NM, 15-Jun-2019.) |
β’ [if(π, π₯, π΅) / π₯]π β β’ (π β π) | ||
Theorem | renegclALT 38323 | Closure law for negative of reals. Demonstrates use of weak deduction theorem with explicit substitution. The proof is much longer than that of renegcl 11520. (Contributed by NM, 15-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π΄ β β β -π΄ β β) | ||
Theorem | elimhyps2 38324 | Generalization of elimhyps 38321 that is not useful unless we can separately prove β’ π΄ β V. (Contributed by NM, 13-Jun-2019.) |
β’ [π΅ / π₯]π β β’ [if([π΄ / π₯]π, π΄, π΅) / π₯]π | ||
Theorem | dedths2 38325 | Generalization of dedths 38322 that is not useful unless we can separately prove β’ π΄ β V. (Contributed by NM, 13-Jun-2019.) |
β’ [if([π΄ / π₯]π, π΄, π΅) / π₯]π β β’ ([π΄ / π₯]π β [π΄ / π₯]π) | ||
Theorem | nfcxfrdf 38326 | A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by NM, 19-Nov-2020.) |
β’ β²π₯π & β’ (π β π΄ = π΅) & β’ (π β β²π₯π΅) β β’ (π β β²π₯π΄) | ||
Theorem | nfded 38327 | 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 3690. The last is assigned to the inference form (e.g., β²π₯βͺ {π¦ β£ βπ₯π¦ β π΄}) whose hypothesis is satisfied using nfaba1 2903. (Contributed by NM, 19-Nov-2020.) |
β’ (π β β²π₯π΄) & β’ (β²π₯π΄ β π΅ = πΆ) & β’ β²π₯π΅ β β’ (π β β²π₯πΆ) | ||
Theorem | nfded2 38328 | 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 4882) that starts from abidnf 3690. The last is assigned to the inference form (e.g., β²π₯β¨{π¦ β£ βπ₯π¦ β π΄}, {π¦ β£ βπ₯π¦ β π΅}β© for nfop 4881) whose hypotheses are satisfied using nfaba1 2903. (Contributed by NM, 19-Nov-2020.) |
β’ (π β β²π₯π΄) & β’ (π β β²π₯π΅) & β’ ((β²π₯π΄ β§ β²π₯π΅) β πΆ = π·) & β’ β²π₯πΆ β β’ (π β β²π₯π·) | ||
Theorem | nfunidALT2 38329 | Deduction version of nfuni 4906. (Contributed by NM, 19-Nov-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π β β²π₯π΄) β β’ (π β β²π₯βͺ π΄) | ||
Theorem | nfunidALT 38330 | Deduction version of nfuni 4906. (Contributed by NM, 19-Nov-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π β β²π₯π΄) β β’ (π β β²π₯βͺ π΄) | ||
Theorem | nfopdALT 38331 | Deduction version of bound-variable hypothesis builder nfop 4881. This shows how the deduction version of a not-free theorem such as nfop 4881 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 38332 | 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 38333* | 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 38334 | Extend class notation with all 1-dim subspaces (atoms) of a left module or left vector space. |
class LSAtoms | ||
Syntax | clsh 38335 | Extend class notation with all subspaces of a left module or left vector space that are hyperplanes. |
class LSHyp | ||
Definition | df-lsatoms 38336* | 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 38337* | 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 38338* | 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 38339* | 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 38340* | Hyperplane properties expressed with subspace sum. (Contributed by NM, 3-Jul-2014.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π» = (LSHypβπ) & β’ (π β π β LMod) β β’ (π β (π β π» β (π β π β§ π β π β§ βπ£ β π (π β (πβ{π£})) = π))) | ||
Theorem | lshplss 38341 | A hyperplane is a subspace. (Contributed by NM, 3-Jul-2014.) |
β’ π = (LSubSpβπ) & β’ π» = (LSHypβπ) & β’ (π β π β LMod) & β’ (π β π β π») β β’ (π β π β π) | ||
Theorem | lshpne 38342 | A hyperplane is not equal to the vector space. (Contributed by NM, 4-Jul-2014.) |
β’ π = (Baseβπ) & β’ π» = (LSHypβπ) & β’ (π β π β LMod) & β’ (π β π β π») β β’ (π β π β π) | ||
Theorem | lshpnel 38343 | A hyperplane's generating vector does not belong to the hyperplane. (Contributed by NM, 3-Jul-2014.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ β = (LSSumβπ) & β’ π» = (LSHypβπ) & β’ (π β π β LMod) & β’ (π β π β π») & β’ (π β π β π) & β’ (π β (π β (πβ{π})) = π) β β’ (π β Β¬ π β π) | ||
Theorem | lshpnelb 38344 | 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 38345 | Condition that determines a hyperplane. (Contributed by NM, 3-Oct-2014.) (New usage is discouraged.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) & β’ β = (LSSumβπ) & β’ π» = (LSHypβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β Β¬ π β π) β β’ (π β (π β π» β (π β (πβ{π})) = π)) | ||
Theorem | lshpne0 38346 | 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 38347 | 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 38348 | If two hyperplanes are comparable, they are equal. (Contributed by NM, 9-Oct-2014.) |
β’ π» = (LSHypβπ) & β’ (π β π β LVec) & β’ (π β π β π») & β’ (π β π β π») β β’ (π β (π β π β π = π)) | ||
Theorem | lshpinN 38349 | The intersection of two different hyperplanes is not a hyperplane. (Contributed by NM, 29-Oct-2014.) (New usage is discouraged.) |
β’ π» = (LSHypβπ) & β’ (π β π β LVec) & β’ (π β π β π») & β’ (π β π β π») β β’ (π β ((π β© π) β π» β π = π)) | ||
Theorem | lsatset 38350* | 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 38351* | 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 38352 | The span of a nonzero singleton is an atom. TODO: make this obsolete and use lsatlspsn 38353 instead? (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 24-Jun-2014.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) β β’ ((π β LMod β§ π β π β§ π β 0 ) β (πβ{π}) β π΄) | ||
Theorem | lsatlspsn 38353 | The span of a nonzero singleton is an atom. (Contributed by NM, 16-Jan-2015.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β (π β { 0 })) β β’ (π β (πβ{π}) β π΄) | ||
Theorem | islsati 38354* | 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 38355* | 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 38356 | 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 38357 | An atom is a subspace. (Contributed by NM, 25-Aug-2014.) |
β’ π = (LSubSpβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β π΄) β β’ (π β π β π) | ||
Theorem | lsatssv 38358 | An atom is a set of vectors. (Contributed by NM, 27-Feb-2015.) |
β’ π = (Baseβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β π΄) β β’ (π β π β π) | ||
Theorem | lsatn0 38359 | A 1-dim subspace (atom) of a left module or left vector space is nonzero. (atne0 32067 analog.) (Contributed by NM, 25-Aug-2014.) |
β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β π΄) β β’ (π β π β { 0 }) | ||
Theorem | lsatspn0 38360 | 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 38361 | 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 38362 | A subspace (or any class) including an atom is nonzero. (Contributed by NM, 3-Feb-2015.) |
β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β π΄) & β’ (π β π β π) β β’ (π β π β { 0 }) | ||
Theorem | lsatcmp 38363 | If two atoms are comparable, they are equal. (atsseq 32069 analog.) TODO: can lspsncmp 20957 shorten this? (Contributed by NM, 25-Aug-2014.) |
β’ π΄ = (LSAtomsβπ) & β’ (π β π β LVec) & β’ (π β π β π΄) & β’ (π β π β π΄) β β’ (π β (π β π β π = π)) | ||
Theorem | lsatcmp2 38364 | If an atom is included in at-most an atom, they are equal. More general version of lsatcmp 38363. TODO: can lspsncmp 20957 shorten this? (Contributed by NM, 3-Feb-2015.) |
β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LVec) & β’ (π β π β π΄) & β’ (π β (π β π΄ β¨ π = { 0 })) β β’ (π β (π β π β π = π)) | ||
Theorem | lsatel 38365 | A nonzero vector in an atom determines the atom. (Contributed by NM, 25-Aug-2014.) |
β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LVec) & β’ (π β π β π΄) & β’ (π β π β π) & β’ (π β π β 0 ) β β’ (π β π = (πβ{π})) | ||
Theorem | lsatelbN 38366 | 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 38367 | Two atoms sharing a nonzero vector are equal. (Contributed by NM, 8-Mar-2015.) |
β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LVec) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β π β 0 ) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β π = π) | ||
Theorem | lsmsat 38368* | Convert comparison of atom with sum of subspaces to a comparison to sum with atom. (elpaddatiN 39166 analog.) TODO: any way to shorten this? (Contributed by NM, 15-Jan-2015.) |
β’ 0 = (0gβπ) & β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π΄) & β’ (π β π β { 0 }) & β’ (π β π β (π β π)) β β’ (π β βπ β π΄ (π β π β§ π β (π β π))) | ||
Theorem | lsatfixedN 38369* | Show equality with the span of the sum of two vectors, one of which (π) is fixed in advance. Compare lspfixed 20969. (Contributed by NM, 29-May-2015.) (New usage is discouraged.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LVec) & β’ (π β π β π΄) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β (πβ{π})) & β’ (π β π β (πβ{π})) & β’ (π β π β (πβ{π, π})) β β’ (π β βπ§ β ((πβ{π}) β { 0 })π = (πβ{(π + π§)})) | ||
Theorem | lsmsatcv 38370 | Subspace sum has the covering property (using spans of singletons to represent atoms). Similar to Exercise 5 of [Kalmbach] p. 153. (spansncvi 31374 analog.) Explicit atom version of lsmcv 20982. (Contributed by NM, 29-Oct-2014.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π΄) β β’ ((π β§ π β π β§ π β (π β π)) β π = (π β π)) | ||
Theorem | lssatomic 38371* | The lattice of subspaces is atomic, i.e. any nonzero element is greater than or equal to some atom. (shatomici 32080 analog.) (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β { 0 }) β β’ (π β βπ β π΄ π β π) | ||
Theorem | lssats 38372* | 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 32083 analog.) (Contributed by NM, 9-Apr-2014.) |
β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) & β’ π΄ = (LSAtomsβπ) β β’ ((π β LMod β§ π β π) β π = (πββͺ {π₯ β π΄ β£ π₯ β π})) | ||
Theorem | lpssat 38373* | Two subspaces in a proper subset relationship imply the existence of an atom less than or equal to one but not the other. (chpssati 32085 analog.) (Contributed by NM, 11-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β βπ β π΄ (π β π β§ Β¬ π β π)) | ||
Theorem | lrelat 38374* | Subspaces are relatively atomic. Remark 2 of [Kalmbach] p. 149. (chrelati 32086 analog.) (Contributed by NM, 11-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β βπ β π΄ (π β (π β π) β§ (π β π) β π)) | ||
Theorem | lssatle 38375* | The ordering of two subspaces is determined by the atoms under them. (chrelat3 32093 analog.) (Contributed by NM, 29-Oct-2014.) |
β’ π = (LSubSpβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (π β π β βπ β π΄ (π β π β π β π))) | ||
Theorem | lssat 38376* | 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 32085 analog.) (Contributed by NM, 9-Apr-2014.) |
β’ π = (LSubSpβπ) & β’ π΄ = (LSAtomsβπ) β β’ (((π β LMod β§ π β π β§ π β π) β§ π β π) β βπ β π΄ (π β π β§ Β¬ π β π)) | ||
Theorem | islshpat 38377* | Hyperplane properties expressed with subspace sum and an atom. TODO: can proof be shortened? Seems long for a simple variation of islshpsm 38340. (Contributed by NM, 11-Jan-2015.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π» = (LSHypβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) β β’ (π β (π β π» β (π β π β§ π β π β§ βπ β π΄ (π β π) = π))) | ||
Syntax | clcv 38378 | Extend class notation with the covering relation for a left module or left vector space. |
class βL | ||
Definition | df-lcv 38379* | 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 38381 for binary relation. (df-cv 32001 analog.) (Contributed by NM, 7-Jan-2015.) |
β’ βL = (π€ β V β¦ {β¨π‘, π’β© β£ ((π‘ β (LSubSpβπ€) β§ π’ β (LSubSpβπ€)) β§ (π‘ β π’ β§ Β¬ βπ β (LSubSpβπ€)(π‘ β π β§ π β π’)))}) | ||
Theorem | lcvfbr 38380* | The covers relation for a left vector space (or a left module). (Contributed by NM, 7-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β π) β β’ (π β πΆ = {β¨π‘, π’β© β£ ((π‘ β π β§ π’ β π) β§ (π‘ β π’ β§ Β¬ βπ β π (π‘ β π β§ π β π’)))}) | ||
Theorem | lcvbr 38381* | The covers relation for a left vector space (or a left module). (cvbr 32004 analog.) (Contributed by NM, 9-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (ππΆπ β (π β π β§ Β¬ βπ β π (π β π β§ π β π)))) | ||
Theorem | lcvbr2 38382* | The covers relation for a left vector space (or a left module). (cvbr2 32005 analog.) (Contributed by NM, 9-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (ππΆπ β (π β π β§ βπ β π ((π β π β§ π β π) β π = π)))) | ||
Theorem | lcvbr3 38383* | The covers relation for a left vector space (or a left module). (Contributed by NM, 9-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (ππΆπ β (π β π β§ βπ β π ((π β π β§ π β π) β (π = π β¨ π = π))))) | ||
Theorem | lcvpss 38384 | The covers relation implies proper subset. (cvpss 32007 analog.) (Contributed by NM, 7-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β ππΆπ) β β’ (π β π β π) | ||
Theorem | lcvnbtwn 38385 | The covers relation implies no in-betweenness. (cvnbtwn 32008 analog.) (Contributed by NM, 7-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π πΆπ) β β’ (π β Β¬ (π β π β§ π β π)) | ||
Theorem | lcvntr 38386 | The covers relation is not transitive. (cvntr 32014 analog.) (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π πΆπ) & β’ (π β ππΆπ) β β’ (π β Β¬ π πΆπ) | ||
Theorem | lcvnbtwn2 38387 | The covers relation implies no in-betweenness. (cvnbtwn2 32009 analog.) (Contributed by NM, 7-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π πΆπ) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β π = π) | ||
Theorem | lcvnbtwn3 38388 | The covers relation implies no in-betweenness. (cvnbtwn3 32010 analog.) (Contributed by NM, 7-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π πΆπ) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β π = π ) | ||
Theorem | lsmcv2 38389 | Subspace sum has the covering property (using spans of singletons to represent atoms). Proposition 1(ii) of [Kalmbach] p. 153. (spansncv2 32015 analog.) (Contributed by NM, 10-Jan-2015.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) & β’ β = (LSSumβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β Β¬ (πβ{π}) β π) β β’ (π β ππΆ(π β (πβ{π}))) | ||
Theorem | lcvat 38390* | If a subspace covers another, it equals the other joined with some atom. This is a consequence of relative atomicity. (cvati 32088 analog.) (Contributed by NM, 11-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π΄ = (LSAtomsβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β ππΆπ) β β’ (π β βπ β π΄ (π β π) = π) | ||
Theorem | lsatcv0 38391 | An atom covers the zero subspace. (atcv0 32064 analog.) (Contributed by NM, 7-Jan-2015.) |
β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LVec) & β’ (π β π β π΄) β β’ (π β { 0 }πΆπ) | ||
Theorem | lsatcveq0 38392 | A subspace covered by an atom must be the zero subspace. (atcveq0 32070 analog.) (Contributed by NM, 7-Jan-2015.) |
β’ 0 = (0gβπ) & β’ π = (LSubSpβπ) & β’ π΄ = (LSAtomsβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β π΄) β β’ (π β (ππΆπ β π = { 0 })) | ||
Theorem | lsat0cv 38393 | 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 38394 | Lemma for lcvexch 38399. (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (π β (π β π) β (π β© π) β π)) | ||
Theorem | lcvexchlem2 38395 | Lemma for lcvexch 38399. (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β (π β© π) β π ) & β’ (π β π β π) β β’ (π β ((π β π) β© π) = π ) | ||
Theorem | lcvexchlem3 38396 | Lemma for lcvexch 38399. (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π ) & β’ (π β π β (π β π)) β β’ (π β ((π β© π) β π) = π ) | ||
Theorem | lcvexchlem4 38397 | Lemma for lcvexch 38399. (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β ππΆ(π β π)) β β’ (π β (π β© π)πΆπ) | ||
Theorem | lcvexchlem5 38398 | Lemma for lcvexch 38399. (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β (π β© π)πΆπ) β β’ (π β ππΆ(π β π)) | ||
Theorem | lcvexch 38399 | Subspaces satisfy the exchange axiom. Lemma 7.5 of [MaedaMaeda] p. 31. (cvexchi 32091 analog.) TODO: combine some lemmas. (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β ((π β© π)πΆπ β ππΆ(π β π))) | ||
Theorem | lcvp 38400 | Covering property of Definition 7.4 of [MaedaMaeda] p. 31 and its converse. (cvp 32097 analog.) (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β π΄) β β’ (π β ((π β© π) = { 0 } β ππΆ(π β π))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |