Home | Metamath
Proof Explorer Theorem List (p. 374 of 470) | < 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: | Metamath Proof Explorer
(1-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ax12indi 37301 | Induction step for constructing a substitution instance of ax-c15 37246 without using ax-c15 37246. Implication case. (Contributed by NM, 21-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (Β¬ βπ₯ π₯ = π¦ β (π₯ = π¦ β (π β βπ₯(π₯ = π¦ β π)))) & β’ (Β¬ βπ₯ π₯ = π¦ β (π₯ = π¦ β (π β βπ₯(π₯ = π¦ β π)))) β β’ (Β¬ βπ₯ π₯ = π¦ β (π₯ = π¦ β ((π β π) β βπ₯(π₯ = π¦ β (π β π))))) | ||
Theorem | ax12indalem 37302 | Lemma for ax12inda2 37304 and ax12inda 37305. (Contributed by NM, 24-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (Β¬ βπ₯ π₯ = π¦ β (π₯ = π¦ β (π β βπ₯(π₯ = π¦ β π)))) β β’ (Β¬ βπ¦ π¦ = π§ β (Β¬ βπ₯ π₯ = π¦ β (π₯ = π¦ β (βπ§π β βπ₯(π₯ = π¦ β βπ§π))))) | ||
Theorem | ax12inda2ALT 37303* | Alternate proof of ax12inda2 37304, slightly more direct and not requiring ax-c16 37249. (Contributed by NM, 4-May-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (Β¬ βπ₯ π₯ = π¦ β (π₯ = π¦ β (π β βπ₯(π₯ = π¦ β π)))) β β’ (Β¬ βπ₯ π₯ = π¦ β (π₯ = π¦ β (βπ§π β βπ₯(π₯ = π¦ β βπ§π)))) | ||
Theorem | ax12inda2 37304* | Induction step for constructing a substitution instance of ax-c15 37246 without using ax-c15 37246. Quantification case. When π§ and π¦ are distinct, this theorem avoids the dummy variables needed by the more general ax12inda 37305. (Contributed by NM, 24-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (Β¬ βπ₯ π₯ = π¦ β (π₯ = π¦ β (π β βπ₯(π₯ = π¦ β π)))) β β’ (Β¬ βπ₯ π₯ = π¦ β (π₯ = π¦ β (βπ§π β βπ₯(π₯ = π¦ β βπ§π)))) | ||
Theorem | ax12inda 37305* | Induction step for constructing a substitution instance of ax-c15 37246 without using ax-c15 37246. Quantification case. (When π§ and π¦ are distinct, ax12inda2 37304 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 37306* | Rederivation of ax-c15 37246 from ax12v 2172 (without using ax-c15 37246 or the full ax-12 2171). Thus, the hypothesis (ax12v 2172) provides an alternate axiom that can be used in place of ax-c15 37246. See also axc15 2421. (Contributed by NM, 2-Feb-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π₯ = π§ β (π β βπ₯(π₯ = π§ β π))) β β’ (Β¬ βπ₯ π₯ = π¦ β (π₯ = π¦ β (π β βπ₯(π₯ = π¦ β π)))) | ||
Theorem | ax12a2-o 37307* | Derive ax-c15 37246 from a hypothesis in the form of ax-12 2171, without using ax-12 2171 or ax-c15 37246. 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 37244, 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 37245 instead of ax-c11 37244. (Contributed by NM, 2-Feb-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π₯ = π§ β (βπ§π β βπ₯(π₯ = π§ β π))) β β’ (Β¬ βπ₯ π₯ = π¦ β (π₯ = π¦ β (π β βπ₯(π₯ = π¦ β π)))) | ||
Theorem | axc11-o 37308 |
Show that ax-c11 37244 can be derived from ax-c11n 37245 and ax-12 2171. An open
problem is whether this theorem can be derived from ax-c11n 37245 and the
others when ax-12 2171 is replaced with ax-c15 37246 or ax12v 2172. See Theorems
axc11nfromc11 37283 for the rederivation of ax-c11n 37245 from axc11 2429.
Normally, axc11 2429 should be used rather than ax-c11 37244 or axc11-o 37308, 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 37309* | Index shift of a finite sum with a weaker "implicit substitution" hypothesis than fsumshft 15599. The proof demonstrates how this can be derived starting from from fsumshft 15599. (Contributed by NM, 1-Nov-2019.) |
β’ (π β πΎ β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ ((π β§ π β (π...π)) β π΄ β β) & β’ ((π β§ π = (π β πΎ)) β π΄ = π΅) β β’ (π β Ξ£π β (π...π)π΄ = Ξ£π β ((π + πΎ)...(π + πΎ))π΅) | ||
Axiom | ax-riotaBAD 37310 | 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 6443. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) WARNING: THIS "AXIOM", WHICH IS THE OLD df-riota 7305, CONFLICTS WITH (THE NEW) df-riota 7305 AND MAKES THE SYSTEM IN set.mm INCONSISTENT. IT IS TEMPORARY AND WILL BE DELETED AFTER ALL USES ARE ELIMINATED. |
β’ (β©π₯ β π΄ π) = if(β!π₯ β π΄ π, (β©π₯(π₯ β π΄ β§ π)), (Undefβ{π₯ β£ π₯ β π΄})) | ||
Theorem | riotaclbgBAD 37311* | Closure of restricted iota. (Contributed by NM, 28-Feb-2013.) (Revised by Mario Carneiro, 24-Dec-2016.) |
β’ (π΄ β π β (β!π₯ β π΄ π β (β©π₯ β π΄ π) β π΄)) | ||
Theorem | riotaclbBAD 37312* | Closure of restricted iota. (Contributed by NM, 15-Sep-2011.) |
β’ π΄ β V β β’ (β!π₯ β π΄ π β (β©π₯ β π΄ π) β π΄) | ||
Theorem | riotasvd 37313* | Deduction version of riotasv 37316. (Contributed by NM, 4-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
β’ (π β π· = (β©π₯ β π΄ βπ¦ β π΅ (π β π₯ = πΆ))) & β’ (π β π· β π΄) β β’ ((π β§ π΄ β π) β ((π¦ β π΅ β§ π) β π· = πΆ)) | ||
Theorem | riotasv2d 37314* | Value of description binder π· for a single-valued class expression πΆ(π¦) (as in e.g. reusv2 5356). Special case of riota2f 7330. (Contributed by NM, 2-Mar-2013.) |
β’ β²π¦π & β’ (π β β²π¦πΉ) & β’ (π β β²π¦π) & β’ (π β π· = (β©π₯ β π΄ βπ¦ β π΅ (π β π₯ = πΆ))) & β’ ((π β§ π¦ = πΈ) β (π β π)) & β’ ((π β§ π¦ = πΈ) β πΆ = πΉ) & β’ (π β π· β π΄) & β’ (π β πΈ β π΅) & β’ (π β π) β β’ ((π β§ π΄ β π) β π· = πΉ) | ||
Theorem | riotasv2s 37315* | The value of description binder π· for a single-valued class expression πΆ(π¦) (as in e.g. reusv2 5356) in the form of a substitution instance. Special case of riota2f 7330. (Contributed by NM, 3-Mar-2013.) (Proof shortened by Mario Carneiro, 6-Dec-2016.) |
β’ π· = (β©π₯ β π΄ βπ¦ β π΅ (π β π₯ = πΆ)) β β’ ((π΄ β π β§ π· β π΄ β§ (πΈ β π΅ β§ [πΈ / π¦]π)) β π· = β¦πΈ / π¦β¦πΆ) | ||
Theorem | riotasv 37316* | Value of description binder π· for a single-valued class expression πΆ(π¦) (as in e.g. reusv2 5356). Special case of riota2f 7330. (Contributed by NM, 26-Jan-2013.) (Proof shortened by Mario Carneiro, 6-Dec-2016.) |
β’ π΄ β V & β’ π· = (β©π₯ β π΄ βπ¦ β π΅ (π β π₯ = πΆ)) β β’ ((π· β π΄ β§ π¦ β π΅ β§ π) β π· = πΆ) | ||
Theorem | riotasv3d 37317* | A property π holding for a representative of a single-valued class expression πΆ(π¦) (see e.g. reusv2 5356) 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 37318 | A version of elimhyp 4549 using explicit substitution. (Contributed by NM, 15-Jun-2019.) |
β’ [π΅ / π₯]π β β’ [if(π, π₯, π΅) / π₯]π | ||
Theorem | dedths 37319 | A version of weak deduction theorem dedth 4542 using explicit substitution. (Contributed by NM, 15-Jun-2019.) |
β’ [if(π, π₯, π΅) / π₯]π β β’ (π β π) | ||
Theorem | renegclALT 37320 | Closure law for negative of reals. Demonstrates use of weak deduction theorem with explicit substitution. The proof is much longer than that of renegcl 11397. (Contributed by NM, 15-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π΄ β β β -π΄ β β) | ||
Theorem | elimhyps2 37321 | Generalization of elimhyps 37318 that is not useful unless we can separately prove β’ π΄ β V. (Contributed by NM, 13-Jun-2019.) |
β’ [π΅ / π₯]π β β’ [if([π΄ / π₯]π, π΄, π΅) / π₯]π | ||
Theorem | dedths2 37322 | Generalization of dedths 37319 that is not useful unless we can separately prove β’ π΄ β V. (Contributed by NM, 13-Jun-2019.) |
β’ [if([π΄ / π₯]π, π΄, π΅) / π₯]π β β’ ([π΄ / π₯]π β [π΄ / π₯]π) | ||
Theorem | nfcxfrdf 37323 | A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by NM, 19-Nov-2020.) |
β’ β²π₯π & β’ (π β π΄ = π΅) & β’ (π β β²π₯π΅) β β’ (π β β²π₯π΄) | ||
Theorem | nfded 37324 | 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 3658. The last is assigned to the inference form (e.g., β²π₯βͺ {π¦ β£ βπ₯π¦ β π΄}) whose hypothesis is satisfied using nfaba1 2913. (Contributed by NM, 19-Nov-2020.) |
β’ (π β β²π₯π΄) & β’ (β²π₯π΄ β π΅ = πΆ) & β’ β²π₯π΅ β β’ (π β β²π₯πΆ) | ||
Theorem | nfded2 37325 | 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 4845) that starts from abidnf 3658. The last is assigned to the inference form (e.g., β²π₯β¨{π¦ β£ βπ₯π¦ β π΄}, {π¦ β£ βπ₯π¦ β π΅}β© for nfop 4844) whose hypotheses are satisfied using nfaba1 2913. (Contributed by NM, 19-Nov-2020.) |
β’ (π β β²π₯π΄) & β’ (π β β²π₯π΅) & β’ ((β²π₯π΄ β§ β²π₯π΅) β πΆ = π·) & β’ β²π₯πΆ β β’ (π β β²π₯π·) | ||
Theorem | nfunidALT2 37326 | Deduction version of nfuni 4870. (Contributed by NM, 19-Nov-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π β β²π₯π΄) β β’ (π β β²π₯βͺ π΄) | ||
Theorem | nfunidALT 37327 | Deduction version of nfuni 4870. (Contributed by NM, 19-Nov-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π β β²π₯π΄) β β’ (π β β²π₯βͺ π΄) | ||
Theorem | nfopdALT 37328 | Deduction version of bound-variable hypothesis builder nfop 4844. This shows how the deduction version of a not-free theorem such as nfop 4844 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 37329 | 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 37330* | 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 37331 | Extend class notation with all 1-dim subspaces (atoms) of a left module or left vector space. |
class LSAtoms | ||
Syntax | clsh 37332 | Extend class notation with all subspaces of a left module or left vector space that are hyperplanes. |
class LSHyp | ||
Definition | df-lsatoms 37333* | 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 37334* | 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 37335* | 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 37336* | 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 37337* | Hyperplane properties expressed with subspace sum. (Contributed by NM, 3-Jul-2014.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π» = (LSHypβπ) & β’ (π β π β LMod) β β’ (π β (π β π» β (π β π β§ π β π β§ βπ£ β π (π β (πβ{π£})) = π))) | ||
Theorem | lshplss 37338 | A hyperplane is a subspace. (Contributed by NM, 3-Jul-2014.) |
β’ π = (LSubSpβπ) & β’ π» = (LSHypβπ) & β’ (π β π β LMod) & β’ (π β π β π») β β’ (π β π β π) | ||
Theorem | lshpne 37339 | A hyperplane is not equal to the vector space. (Contributed by NM, 4-Jul-2014.) |
β’ π = (Baseβπ) & β’ π» = (LSHypβπ) & β’ (π β π β LMod) & β’ (π β π β π») β β’ (π β π β π) | ||
Theorem | lshpnel 37340 | A hyperplane's generating vector does not belong to the hyperplane. (Contributed by NM, 3-Jul-2014.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ β = (LSSumβπ) & β’ π» = (LSHypβπ) & β’ (π β π β LMod) & β’ (π β π β π») & β’ (π β π β π) & β’ (π β (π β (πβ{π})) = π) β β’ (π β Β¬ π β π) | ||
Theorem | lshpnelb 37341 | 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 37342 | Condition that determines a hyperplane. (Contributed by NM, 3-Oct-2014.) (New usage is discouraged.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) & β’ β = (LSSumβπ) & β’ π» = (LSHypβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β Β¬ π β π) β β’ (π β (π β π» β (π β (πβ{π})) = π)) | ||
Theorem | lshpne0 37343 | 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 37344 | 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 37345 | If two hyperplanes are comparable, they are equal. (Contributed by NM, 9-Oct-2014.) |
β’ π» = (LSHypβπ) & β’ (π β π β LVec) & β’ (π β π β π») & β’ (π β π β π») β β’ (π β (π β π β π = π)) | ||
Theorem | lshpinN 37346 | The intersection of two different hyperplanes is not a hyperplane. (Contributed by NM, 29-Oct-2014.) (New usage is discouraged.) |
β’ π» = (LSHypβπ) & β’ (π β π β LVec) & β’ (π β π β π») & β’ (π β π β π») β β’ (π β ((π β© π) β π» β π = π)) | ||
Theorem | lsatset 37347* | 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 37348* | 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 37349 | The span of a nonzero singleton is an atom. TODO: make this obsolete and use lsatlspsn 37350 instead? (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 24-Jun-2014.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) β β’ ((π β LMod β§ π β π β§ π β 0 ) β (πβ{π}) β π΄) | ||
Theorem | lsatlspsn 37350 | The span of a nonzero singleton is an atom. (Contributed by NM, 16-Jan-2015.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β (π β { 0 })) β β’ (π β (πβ{π}) β π΄) | ||
Theorem | islsati 37351* | 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 37352* | 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 37353 | 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 37354 | An atom is a subspace. (Contributed by NM, 25-Aug-2014.) |
β’ π = (LSubSpβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β π΄) β β’ (π β π β π) | ||
Theorem | lsatssv 37355 | An atom is a set of vectors. (Contributed by NM, 27-Feb-2015.) |
β’ π = (Baseβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β π΄) β β’ (π β π β π) | ||
Theorem | lsatn0 37356 | A 1-dim subspace (atom) of a left module or left vector space is nonzero. (atne0 31085 analog.) (Contributed by NM, 25-Aug-2014.) |
β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β π΄) β β’ (π β π β { 0 }) | ||
Theorem | lsatspn0 37357 | 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 37358 | 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 37359 | A subspace (or any class) including an atom is nonzero. (Contributed by NM, 3-Feb-2015.) |
β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β π΄) & β’ (π β π β π) β β’ (π β π β { 0 }) | ||
Theorem | lsatcmp 37360 | If two atoms are comparable, they are equal. (atsseq 31087 analog.) TODO: can lspsncmp 20500 shorten this? (Contributed by NM, 25-Aug-2014.) |
β’ π΄ = (LSAtomsβπ) & β’ (π β π β LVec) & β’ (π β π β π΄) & β’ (π β π β π΄) β β’ (π β (π β π β π = π)) | ||
Theorem | lsatcmp2 37361 | If an atom is included in at-most an atom, they are equal. More general version of lsatcmp 37360. TODO: can lspsncmp 20500 shorten this? (Contributed by NM, 3-Feb-2015.) |
β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LVec) & β’ (π β π β π΄) & β’ (π β (π β π΄ β¨ π = { 0 })) β β’ (π β (π β π β π = π)) | ||
Theorem | lsatel 37362 | A nonzero vector in an atom determines the atom. (Contributed by NM, 25-Aug-2014.) |
β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LVec) & β’ (π β π β π΄) & β’ (π β π β π) & β’ (π β π β 0 ) β β’ (π β π = (πβ{π})) | ||
Theorem | lsatelbN 37363 | 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 37364 | Two atoms sharing a nonzero vector are equal. (Contributed by NM, 8-Mar-2015.) |
β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LVec) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β π β 0 ) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β π = π) | ||
Theorem | lsmsat 37365* | Convert comparison of atom with sum of subspaces to a comparison to sum with atom. (elpaddatiN 38163 analog.) TODO: any way to shorten this? (Contributed by NM, 15-Jan-2015.) |
β’ 0 = (0gβπ) & β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π΄) & β’ (π β π β { 0 }) & β’ (π β π β (π β π)) β β’ (π β βπ β π΄ (π β π β§ π β (π β π))) | ||
Theorem | lsatfixedN 37366* | Show equality with the span of the sum of two vectors, one of which (π) is fixed in advance. Compare lspfixed 20512. (Contributed by NM, 29-May-2015.) (New usage is discouraged.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LVec) & β’ (π β π β π΄) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β (πβ{π})) & β’ (π β π β (πβ{π})) & β’ (π β π β (πβ{π, π})) β β’ (π β βπ§ β ((πβ{π}) β { 0 })π = (πβ{(π + π§)})) | ||
Theorem | lsmsatcv 37367 | Subspace sum has the covering property (using spans of singletons to represent atoms). Similar to Exercise 5 of [Kalmbach] p. 153. (spansncvi 30392 analog.) Explicit atom version of lsmcv 20525. (Contributed by NM, 29-Oct-2014.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π΄) β β’ ((π β§ π β π β§ π β (π β π)) β π = (π β π)) | ||
Theorem | lssatomic 37368* | The lattice of subspaces is atomic, i.e. any nonzero element is greater than or equal to some atom. (shatomici 31098 analog.) (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β { 0 }) β β’ (π β βπ β π΄ π β π) | ||
Theorem | lssats 37369* | 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 31101 analog.) (Contributed by NM, 9-Apr-2014.) |
β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) & β’ π΄ = (LSAtomsβπ) β β’ ((π β LMod β§ π β π) β π = (πββͺ {π₯ β π΄ β£ π₯ β π})) | ||
Theorem | lpssat 37370* | Two subspaces in a proper subset relationship imply the existence of an atom less than or equal to one but not the other. (chpssati 31103 analog.) (Contributed by NM, 11-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β βπ β π΄ (π β π β§ Β¬ π β π)) | ||
Theorem | lrelat 37371* | Subspaces are relatively atomic. Remark 2 of [Kalmbach] p. 149. (chrelati 31104 analog.) (Contributed by NM, 11-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β βπ β π΄ (π β (π β π) β§ (π β π) β π)) | ||
Theorem | lssatle 37372* | The ordering of two subspaces is determined by the atoms under them. (chrelat3 31111 analog.) (Contributed by NM, 29-Oct-2014.) |
β’ π = (LSubSpβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (π β π β βπ β π΄ (π β π β π β π))) | ||
Theorem | lssat 37373* | 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 31103 analog.) (Contributed by NM, 9-Apr-2014.) |
β’ π = (LSubSpβπ) & β’ π΄ = (LSAtomsβπ) β β’ (((π β LMod β§ π β π β§ π β π) β§ π β π) β βπ β π΄ (π β π β§ Β¬ π β π)) | ||
Theorem | islshpat 37374* | Hyperplane properties expressed with subspace sum and an atom. TODO: can proof be shortened? Seems long for a simple variation of islshpsm 37337. (Contributed by NM, 11-Jan-2015.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π» = (LSHypβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) β β’ (π β (π β π» β (π β π β§ π β π β§ βπ β π΄ (π β π) = π))) | ||
Syntax | clcv 37375 | Extend class notation with the covering relation for a left module or left vector space. |
class βL | ||
Definition | df-lcv 37376* | 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 37378 for binary relation. (df-cv 31019 analog.) (Contributed by NM, 7-Jan-2015.) |
β’ βL = (π€ β V β¦ {β¨π‘, π’β© β£ ((π‘ β (LSubSpβπ€) β§ π’ β (LSubSpβπ€)) β§ (π‘ β π’ β§ Β¬ βπ β (LSubSpβπ€)(π‘ β π β§ π β π’)))}) | ||
Theorem | lcvfbr 37377* | The covers relation for a left vector space (or a left module). (Contributed by NM, 7-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β π) β β’ (π β πΆ = {β¨π‘, π’β© β£ ((π‘ β π β§ π’ β π) β§ (π‘ β π’ β§ Β¬ βπ β π (π‘ β π β§ π β π’)))}) | ||
Theorem | lcvbr 37378* | The covers relation for a left vector space (or a left module). (cvbr 31022 analog.) (Contributed by NM, 9-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (ππΆπ β (π β π β§ Β¬ βπ β π (π β π β§ π β π)))) | ||
Theorem | lcvbr2 37379* | The covers relation for a left vector space (or a left module). (cvbr2 31023 analog.) (Contributed by NM, 9-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (ππΆπ β (π β π β§ βπ β π ((π β π β§ π β π) β π = π)))) | ||
Theorem | lcvbr3 37380* | The covers relation for a left vector space (or a left module). (Contributed by NM, 9-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (ππΆπ β (π β π β§ βπ β π ((π β π β§ π β π) β (π = π β¨ π = π))))) | ||
Theorem | lcvpss 37381 | The covers relation implies proper subset. (cvpss 31025 analog.) (Contributed by NM, 7-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β ππΆπ) β β’ (π β π β π) | ||
Theorem | lcvnbtwn 37382 | The covers relation implies no in-betweenness. (cvnbtwn 31026 analog.) (Contributed by NM, 7-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π πΆπ) β β’ (π β Β¬ (π β π β§ π β π)) | ||
Theorem | lcvntr 37383 | The covers relation is not transitive. (cvntr 31032 analog.) (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π πΆπ) & β’ (π β ππΆπ) β β’ (π β Β¬ π πΆπ) | ||
Theorem | lcvnbtwn2 37384 | The covers relation implies no in-betweenness. (cvnbtwn2 31027 analog.) (Contributed by NM, 7-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π πΆπ) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β π = π) | ||
Theorem | lcvnbtwn3 37385 | The covers relation implies no in-betweenness. (cvnbtwn3 31028 analog.) (Contributed by NM, 7-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π πΆπ) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β π = π ) | ||
Theorem | lsmcv2 37386 | Subspace sum has the covering property (using spans of singletons to represent atoms). Proposition 1(ii) of [Kalmbach] p. 153. (spansncv2 31033 analog.) (Contributed by NM, 10-Jan-2015.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) & β’ β = (LSSumβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β Β¬ (πβ{π}) β π) β β’ (π β ππΆ(π β (πβ{π}))) | ||
Theorem | lcvat 37387* | If a subspace covers another, it equals the other joined with some atom. This is a consequence of relative atomicity. (cvati 31106 analog.) (Contributed by NM, 11-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π΄ = (LSAtomsβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β ππΆπ) β β’ (π β βπ β π΄ (π β π) = π) | ||
Theorem | lsatcv0 37388 | An atom covers the zero subspace. (atcv0 31082 analog.) (Contributed by NM, 7-Jan-2015.) |
β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LVec) & β’ (π β π β π΄) β β’ (π β { 0 }πΆπ) | ||
Theorem | lsatcveq0 37389 | A subspace covered by an atom must be the zero subspace. (atcveq0 31088 analog.) (Contributed by NM, 7-Jan-2015.) |
β’ 0 = (0gβπ) & β’ π = (LSubSpβπ) & β’ π΄ = (LSAtomsβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β π΄) β β’ (π β (ππΆπ β π = { 0 })) | ||
Theorem | lsat0cv 37390 | 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 37391 | Lemma for lcvexch 37396. (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (π β (π β π) β (π β© π) β π)) | ||
Theorem | lcvexchlem2 37392 | Lemma for lcvexch 37396. (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β (π β© π) β π ) & β’ (π β π β π) β β’ (π β ((π β π) β© π) = π ) | ||
Theorem | lcvexchlem3 37393 | Lemma for lcvexch 37396. (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π ) & β’ (π β π β (π β π)) β β’ (π β ((π β© π) β π) = π ) | ||
Theorem | lcvexchlem4 37394 | Lemma for lcvexch 37396. (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β ππΆ(π β π)) β β’ (π β (π β© π)πΆπ) | ||
Theorem | lcvexchlem5 37395 | Lemma for lcvexch 37396. (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β (π β© π)πΆπ) β β’ (π β ππΆ(π β π)) | ||
Theorem | lcvexch 37396 | Subspaces satisfy the exchange axiom. Lemma 7.5 of [MaedaMaeda] p. 31. (cvexchi 31109 analog.) TODO: combine some lemmas. (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β ((π β© π)πΆπ β ππΆ(π β π))) | ||
Theorem | lcvp 37397 | Covering property of Definition 7.4 of [MaedaMaeda] p. 31 and its converse. (cvp 31115 analog.) (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β π΄) β β’ (π β ((π β© π) = { 0 } β ππΆ(π β π))) | ||
Theorem | lcv1 37398 | Covering property of a subspace plus an atom. (chcv1 31095 analog.) (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π΄ = (LSAtomsβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β π΄) β β’ (π β (Β¬ π β π β ππΆ(π β π))) | ||
Theorem | lcv2 37399 | Covering property of a subspace plus an atom. (chcv2 31096 analog.) (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π΄ = (LSAtomsβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β π΄) β β’ (π β (π β (π β π) β ππΆ(π β π))) | ||
Theorem | lsatexch 37400 | The atom exchange property. Proposition 1(i) of [Kalmbach] p. 140. A version of this theorem was originally proved by Hermann Grassmann in 1862. (atexch 31121 analog.) (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β π β (π β π )) & β’ (π β (π β© π) = { 0 }) β β’ (π β π β (π β π)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |