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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Axiom | ax-riotaBAD 37301 | 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 6444. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 15-Oct-2016.) WARNING: THIS "AXIOM", WHICH IS THE OLD df-riota 7306, CONFLICTS WITH (THE NEW) df-riota 7306 AND MAKES THE SYSTEM IN set.mm INCONSISTENT. IT IS TEMPORARY AND WILL BE DELETED AFTER ALL USES ARE ELIMINATED. |
β’ (β©π₯ β π΄ π) = if(β!π₯ β π΄ π, (β©π₯(π₯ β π΄ β§ π)), (Undefβ{π₯ β£ π₯ β π΄})) | ||
Theorem | riotaclbgBAD 37302* | Closure of restricted iota. (Contributed by NM, 28-Feb-2013.) (Revised by Mario Carneiro, 24-Dec-2016.) |
β’ (π΄ β π β (β!π₯ β π΄ π β (β©π₯ β π΄ π) β π΄)) | ||
Theorem | riotaclbBAD 37303* | Closure of restricted iota. (Contributed by NM, 15-Sep-2011.) |
β’ π΄ β V β β’ (β!π₯ β π΄ π β (β©π₯ β π΄ π) β π΄) | ||
Theorem | riotasvd 37304* | Deduction version of riotasv 37307. (Contributed by NM, 4-Mar-2013.) (Revised by Mario Carneiro, 15-Oct-2016.) |
β’ (π β π· = (β©π₯ β π΄ βπ¦ β π΅ (π β π₯ = πΆ))) & β’ (π β π· β π΄) β β’ ((π β§ π΄ β π) β ((π¦ β π΅ β§ π) β π· = πΆ)) | ||
Theorem | riotasv2d 37305* | Value of description binder π· for a single-valued class expression πΆ(π¦) (as in e.g. reusv2 5357). Special case of riota2f 7331. (Contributed by NM, 2-Mar-2013.) |
β’ β²π¦π & β’ (π β β²π¦πΉ) & β’ (π β β²π¦π) & β’ (π β π· = (β©π₯ β π΄ βπ¦ β π΅ (π β π₯ = πΆ))) & β’ ((π β§ π¦ = πΈ) β (π β π)) & β’ ((π β§ π¦ = πΈ) β πΆ = πΉ) & β’ (π β π· β π΄) & β’ (π β πΈ β π΅) & β’ (π β π) β β’ ((π β§ π΄ β π) β π· = πΉ) | ||
Theorem | riotasv2s 37306* | The value of description binder π· for a single-valued class expression πΆ(π¦) (as in e.g. reusv2 5357) in the form of a substitution instance. Special case of riota2f 7331. (Contributed by NM, 3-Mar-2013.) (Proof shortened by Mario Carneiro, 6-Dec-2016.) |
β’ π· = (β©π₯ β π΄ βπ¦ β π΅ (π β π₯ = πΆ)) β β’ ((π΄ β π β§ π· β π΄ β§ (πΈ β π΅ β§ [πΈ / π¦]π)) β π· = β¦πΈ / π¦β¦πΆ) | ||
Theorem | riotasv 37307* | Value of description binder π· for a single-valued class expression πΆ(π¦) (as in e.g. reusv2 5357). Special case of riota2f 7331. (Contributed by NM, 26-Jan-2013.) (Proof shortened by Mario Carneiro, 6-Dec-2016.) |
β’ π΄ β V & β’ π· = (β©π₯ β π΄ βπ¦ β π΅ (π β π₯ = πΆ)) β β’ ((π· β π΄ β§ π¦ β π΅ β§ π) β π· = πΆ) | ||
Theorem | riotasv3d 37308* | A property π holding for a representative of a single-valued class expression πΆ(π¦) (see e.g. reusv2 5357) 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 37309 | A version of elimhyp 4550 using explicit substitution. (Contributed by NM, 15-Jun-2019.) |
β’ [π΅ / π₯]π β β’ [if(π, π₯, π΅) / π₯]π | ||
Theorem | dedths 37310 | A version of weak deduction theorem dedth 4543 using explicit substitution. (Contributed by NM, 15-Jun-2019.) |
β’ [if(π, π₯, π΅) / π₯]π β β’ (π β π) | ||
Theorem | renegclALT 37311 | Closure law for negative of reals. Demonstrates use of weak deduction theorem with explicit substitution. The proof is much longer than that of renegcl 11398. (Contributed by NM, 15-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π΄ β β β -π΄ β β) | ||
Theorem | elimhyps2 37312 | Generalization of elimhyps 37309 that is not useful unless we can separately prove β’ π΄ β V. (Contributed by NM, 13-Jun-2019.) |
β’ [π΅ / π₯]π β β’ [if([π΄ / π₯]π, π΄, π΅) / π₯]π | ||
Theorem | dedths2 37313 | Generalization of dedths 37310 that is not useful unless we can separately prove β’ π΄ β V. (Contributed by NM, 13-Jun-2019.) |
β’ [if([π΄ / π₯]π, π΄, π΅) / π₯]π β β’ ([π΄ / π₯]π β [π΄ / π₯]π) | ||
Theorem | nfcxfrdf 37314 | A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by NM, 19-Nov-2020.) |
β’ β²π₯π & β’ (π β π΄ = π΅) & β’ (π β β²π₯π΅) β β’ (π β β²π₯π΄) | ||
Theorem | nfded 37315 | 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 3659. The last is assigned to the inference form (e.g., β²π₯βͺ {π¦ β£ βπ₯π¦ β π΄}) whose hypothesis is satisfied using nfaba1 2914. (Contributed by NM, 19-Nov-2020.) |
β’ (π β β²π₯π΄) & β’ (β²π₯π΄ β π΅ = πΆ) & β’ β²π₯π΅ β β’ (π β β²π₯πΆ) | ||
Theorem | nfded2 37316 | 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 4846) that starts from abidnf 3659. The last is assigned to the inference form (e.g., β²π₯β¨{π¦ β£ βπ₯π¦ β π΄}, {π¦ β£ βπ₯π¦ β π΅}β© for nfop 4845) whose hypotheses are satisfied using nfaba1 2914. (Contributed by NM, 19-Nov-2020.) |
β’ (π β β²π₯π΄) & β’ (π β β²π₯π΅) & β’ ((β²π₯π΄ β§ β²π₯π΅) β πΆ = π·) & β’ β²π₯πΆ β β’ (π β β²π₯π·) | ||
Theorem | nfunidALT2 37317 | Deduction version of nfuni 4871. (Contributed by NM, 19-Nov-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π β β²π₯π΄) β β’ (π β β²π₯βͺ π΄) | ||
Theorem | nfunidALT 37318 | Deduction version of nfuni 4871. (Contributed by NM, 19-Nov-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π β β²π₯π΄) β β’ (π β β²π₯βͺ π΄) | ||
Theorem | nfopdALT 37319 | Deduction version of bound-variable hypothesis builder nfop 4845. This shows how the deduction version of a not-free theorem such as nfop 4845 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 37320 | 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 37321* | 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 37322 | Extend class notation with all 1-dim subspaces (atoms) of a left module or left vector space. |
class LSAtoms | ||
Syntax | clsh 37323 | Extend class notation with all subspaces of a left module or left vector space that are hyperplanes. |
class LSHyp | ||
Definition | df-lsatoms 37324* | 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 37325* | 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 37326* | 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 37327* | 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 37328* | Hyperplane properties expressed with subspace sum. (Contributed by NM, 3-Jul-2014.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π» = (LSHypβπ) & β’ (π β π β LMod) β β’ (π β (π β π» β (π β π β§ π β π β§ βπ£ β π (π β (πβ{π£})) = π))) | ||
Theorem | lshplss 37329 | A hyperplane is a subspace. (Contributed by NM, 3-Jul-2014.) |
β’ π = (LSubSpβπ) & β’ π» = (LSHypβπ) & β’ (π β π β LMod) & β’ (π β π β π») β β’ (π β π β π) | ||
Theorem | lshpne 37330 | A hyperplane is not equal to the vector space. (Contributed by NM, 4-Jul-2014.) |
β’ π = (Baseβπ) & β’ π» = (LSHypβπ) & β’ (π β π β LMod) & β’ (π β π β π») β β’ (π β π β π) | ||
Theorem | lshpnel 37331 | A hyperplane's generating vector does not belong to the hyperplane. (Contributed by NM, 3-Jul-2014.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ β = (LSSumβπ) & β’ π» = (LSHypβπ) & β’ (π β π β LMod) & β’ (π β π β π») & β’ (π β π β π) & β’ (π β (π β (πβ{π})) = π) β β’ (π β Β¬ π β π) | ||
Theorem | lshpnelb 37332 | 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 37333 | Condition that determines a hyperplane. (Contributed by NM, 3-Oct-2014.) (New usage is discouraged.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) & β’ β = (LSSumβπ) & β’ π» = (LSHypβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β Β¬ π β π) β β’ (π β (π β π» β (π β (πβ{π})) = π)) | ||
Theorem | lshpne0 37334 | 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 37335 | 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 37336 | If two hyperplanes are comparable, they are equal. (Contributed by NM, 9-Oct-2014.) |
β’ π» = (LSHypβπ) & β’ (π β π β LVec) & β’ (π β π β π») & β’ (π β π β π») β β’ (π β (π β π β π = π)) | ||
Theorem | lshpinN 37337 | The intersection of two different hyperplanes is not a hyperplane. (Contributed by NM, 29-Oct-2014.) (New usage is discouraged.) |
β’ π» = (LSHypβπ) & β’ (π β π β LVec) & β’ (π β π β π») & β’ (π β π β π») β β’ (π β ((π β© π) β π» β π = π)) | ||
Theorem | lsatset 37338* | 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 37339* | 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 37340 | The span of a nonzero singleton is an atom. TODO: make this obsolete and use lsatlspsn 37341 instead? (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 24-Jun-2014.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) β β’ ((π β LMod β§ π β π β§ π β 0 ) β (πβ{π}) β π΄) | ||
Theorem | lsatlspsn 37341 | The span of a nonzero singleton is an atom. (Contributed by NM, 16-Jan-2015.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β (π β { 0 })) β β’ (π β (πβ{π}) β π΄) | ||
Theorem | islsati 37342* | 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 37343* | 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 37344 | 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 37345 | An atom is a subspace. (Contributed by NM, 25-Aug-2014.) |
β’ π = (LSubSpβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β π΄) β β’ (π β π β π) | ||
Theorem | lsatssv 37346 | An atom is a set of vectors. (Contributed by NM, 27-Feb-2015.) |
β’ π = (Baseβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β π΄) β β’ (π β π β π) | ||
Theorem | lsatn0 37347 | A 1-dim subspace (atom) of a left module or left vector space is nonzero. (atne0 31073 analog.) (Contributed by NM, 25-Aug-2014.) |
β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β π΄) β β’ (π β π β { 0 }) | ||
Theorem | lsatspn0 37348 | 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 37349 | 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 37350 | A subspace (or any class) including an atom is nonzero. (Contributed by NM, 3-Feb-2015.) |
β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β π΄) & β’ (π β π β π) β β’ (π β π β { 0 }) | ||
Theorem | lsatcmp 37351 | If two atoms are comparable, they are equal. (atsseq 31075 analog.) TODO: can lspsncmp 20500 shorten this? (Contributed by NM, 25-Aug-2014.) |
β’ π΄ = (LSAtomsβπ) & β’ (π β π β LVec) & β’ (π β π β π΄) & β’ (π β π β π΄) β β’ (π β (π β π β π = π)) | ||
Theorem | lsatcmp2 37352 | If an atom is included in at-most an atom, they are equal. More general version of lsatcmp 37351. TODO: can lspsncmp 20500 shorten this? (Contributed by NM, 3-Feb-2015.) |
β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LVec) & β’ (π β π β π΄) & β’ (π β (π β π΄ β¨ π = { 0 })) β β’ (π β (π β π β π = π)) | ||
Theorem | lsatel 37353 | A nonzero vector in an atom determines the atom. (Contributed by NM, 25-Aug-2014.) |
β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LVec) & β’ (π β π β π΄) & β’ (π β π β π) & β’ (π β π β 0 ) β β’ (π β π = (πβ{π})) | ||
Theorem | lsatelbN 37354 | 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 37355 | Two atoms sharing a nonzero vector are equal. (Contributed by NM, 8-Mar-2015.) |
β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LVec) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β π β 0 ) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β π = π) | ||
Theorem | lsmsat 37356* | Convert comparison of atom with sum of subspaces to a comparison to sum with atom. (elpaddatiN 38154 analog.) TODO: any way to shorten this? (Contributed by NM, 15-Jan-2015.) |
β’ 0 = (0gβπ) & β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π΄) & β’ (π β π β { 0 }) & β’ (π β π β (π β π)) β β’ (π β βπ β π΄ (π β π β§ π β (π β π))) | ||
Theorem | lsatfixedN 37357* | 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 37358 | Subspace sum has the covering property (using spans of singletons to represent atoms). Similar to Exercise 5 of [Kalmbach] p. 153. (spansncvi 30380 analog.) Explicit atom version of lsmcv 20525. (Contributed by NM, 29-Oct-2014.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π΄) β β’ ((π β§ π β π β§ π β (π β π)) β π = (π β π)) | ||
Theorem | lssatomic 37359* | The lattice of subspaces is atomic, i.e. any nonzero element is greater than or equal to some atom. (shatomici 31086 analog.) (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β { 0 }) β β’ (π β βπ β π΄ π β π) | ||
Theorem | lssats 37360* | 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 31089 analog.) (Contributed by NM, 9-Apr-2014.) |
β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) & β’ π΄ = (LSAtomsβπ) β β’ ((π β LMod β§ π β π) β π = (πββͺ {π₯ β π΄ β£ π₯ β π})) | ||
Theorem | lpssat 37361* | Two subspaces in a proper subset relationship imply the existence of an atom less than or equal to one but not the other. (chpssati 31091 analog.) (Contributed by NM, 11-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β βπ β π΄ (π β π β§ Β¬ π β π)) | ||
Theorem | lrelat 37362* | Subspaces are relatively atomic. Remark 2 of [Kalmbach] p. 149. (chrelati 31092 analog.) (Contributed by NM, 11-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β βπ β π΄ (π β (π β π) β§ (π β π) β π)) | ||
Theorem | lssatle 37363* | The ordering of two subspaces is determined by the atoms under them. (chrelat3 31099 analog.) (Contributed by NM, 29-Oct-2014.) |
β’ π = (LSubSpβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (π β π β βπ β π΄ (π β π β π β π))) | ||
Theorem | lssat 37364* | 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 31091 analog.) (Contributed by NM, 9-Apr-2014.) |
β’ π = (LSubSpβπ) & β’ π΄ = (LSAtomsβπ) β β’ (((π β LMod β§ π β π β§ π β π) β§ π β π) β βπ β π΄ (π β π β§ Β¬ π β π)) | ||
Theorem | islshpat 37365* | Hyperplane properties expressed with subspace sum and an atom. TODO: can proof be shortened? Seems long for a simple variation of islshpsm 37328. (Contributed by NM, 11-Jan-2015.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π» = (LSHypβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) β β’ (π β (π β π» β (π β π β§ π β π β§ βπ β π΄ (π β π) = π))) | ||
Syntax | clcv 37366 | Extend class notation with the covering relation for a left module or left vector space. |
class βL | ||
Definition | df-lcv 37367* | 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 37369 for binary relation. (df-cv 31007 analog.) (Contributed by NM, 7-Jan-2015.) |
β’ βL = (π€ β V β¦ {β¨π‘, π’β© β£ ((π‘ β (LSubSpβπ€) β§ π’ β (LSubSpβπ€)) β§ (π‘ β π’ β§ Β¬ βπ β (LSubSpβπ€)(π‘ β π β§ π β π’)))}) | ||
Theorem | lcvfbr 37368* | The covers relation for a left vector space (or a left module). (Contributed by NM, 7-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β π) β β’ (π β πΆ = {β¨π‘, π’β© β£ ((π‘ β π β§ π’ β π) β§ (π‘ β π’ β§ Β¬ βπ β π (π‘ β π β§ π β π’)))}) | ||
Theorem | lcvbr 37369* | The covers relation for a left vector space (or a left module). (cvbr 31010 analog.) (Contributed by NM, 9-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (ππΆπ β (π β π β§ Β¬ βπ β π (π β π β§ π β π)))) | ||
Theorem | lcvbr2 37370* | The covers relation for a left vector space (or a left module). (cvbr2 31011 analog.) (Contributed by NM, 9-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (ππΆπ β (π β π β§ βπ β π ((π β π β§ π β π) β π = π)))) | ||
Theorem | lcvbr3 37371* | The covers relation for a left vector space (or a left module). (Contributed by NM, 9-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (ππΆπ β (π β π β§ βπ β π ((π β π β§ π β π) β (π = π β¨ π = π))))) | ||
Theorem | lcvpss 37372 | The covers relation implies proper subset. (cvpss 31013 analog.) (Contributed by NM, 7-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β ππΆπ) β β’ (π β π β π) | ||
Theorem | lcvnbtwn 37373 | The covers relation implies no in-betweenness. (cvnbtwn 31014 analog.) (Contributed by NM, 7-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π πΆπ) β β’ (π β Β¬ (π β π β§ π β π)) | ||
Theorem | lcvntr 37374 | The covers relation is not transitive. (cvntr 31020 analog.) (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π πΆπ) & β’ (π β ππΆπ) β β’ (π β Β¬ π πΆπ) | ||
Theorem | lcvnbtwn2 37375 | The covers relation implies no in-betweenness. (cvnbtwn2 31015 analog.) (Contributed by NM, 7-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π πΆπ) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β π = π) | ||
Theorem | lcvnbtwn3 37376 | The covers relation implies no in-betweenness. (cvnbtwn3 31016 analog.) (Contributed by NM, 7-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π πΆπ) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β π = π ) | ||
Theorem | lsmcv2 37377 | Subspace sum has the covering property (using spans of singletons to represent atoms). Proposition 1(ii) of [Kalmbach] p. 153. (spansncv2 31021 analog.) (Contributed by NM, 10-Jan-2015.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) & β’ β = (LSSumβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β Β¬ (πβ{π}) β π) β β’ (π β ππΆ(π β (πβ{π}))) | ||
Theorem | lcvat 37378* | If a subspace covers another, it equals the other joined with some atom. This is a consequence of relative atomicity. (cvati 31094 analog.) (Contributed by NM, 11-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π΄ = (LSAtomsβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β ππΆπ) β β’ (π β βπ β π΄ (π β π) = π) | ||
Theorem | lsatcv0 37379 | An atom covers the zero subspace. (atcv0 31070 analog.) (Contributed by NM, 7-Jan-2015.) |
β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LVec) & β’ (π β π β π΄) β β’ (π β { 0 }πΆπ) | ||
Theorem | lsatcveq0 37380 | A subspace covered by an atom must be the zero subspace. (atcveq0 31076 analog.) (Contributed by NM, 7-Jan-2015.) |
β’ 0 = (0gβπ) & β’ π = (LSubSpβπ) & β’ π΄ = (LSAtomsβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β π΄) β β’ (π β (ππΆπ β π = { 0 })) | ||
Theorem | lsat0cv 37381 | 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 37382 | Lemma for lcvexch 37387. (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (π β (π β π) β (π β© π) β π)) | ||
Theorem | lcvexchlem2 37383 | Lemma for lcvexch 37387. (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β (π β© π) β π ) & β’ (π β π β π) β β’ (π β ((π β π) β© π) = π ) | ||
Theorem | lcvexchlem3 37384 | Lemma for lcvexch 37387. (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π ) & β’ (π β π β (π β π)) β β’ (π β ((π β© π) β π) = π ) | ||
Theorem | lcvexchlem4 37385 | Lemma for lcvexch 37387. (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β ππΆ(π β π)) β β’ (π β (π β© π)πΆπ) | ||
Theorem | lcvexchlem5 37386 | Lemma for lcvexch 37387. (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β (π β© π)πΆπ) β β’ (π β ππΆ(π β π)) | ||
Theorem | lcvexch 37387 | Subspaces satisfy the exchange axiom. Lemma 7.5 of [MaedaMaeda] p. 31. (cvexchi 31097 analog.) TODO: combine some lemmas. (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β ((π β© π)πΆπ β ππΆ(π β π))) | ||
Theorem | lcvp 37388 | Covering property of Definition 7.4 of [MaedaMaeda] p. 31 and its converse. (cvp 31103 analog.) (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β π΄) β β’ (π β ((π β© π) = { 0 } β ππΆ(π β π))) | ||
Theorem | lcv1 37389 | Covering property of a subspace plus an atom. (chcv1 31083 analog.) (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π΄ = (LSAtomsβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β π΄) β β’ (π β (Β¬ π β π β ππΆ(π β π))) | ||
Theorem | lcv2 37390 | Covering property of a subspace plus an atom. (chcv2 31084 analog.) (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π΄ = (LSAtomsβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β π΄) β β’ (π β (π β (π β π) β ππΆ(π β π))) | ||
Theorem | lsatexch 37391 | 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 31109 analog.) (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β π β (π β π )) & β’ (π β (π β© π) = { 0 }) β β’ (π β π β (π β π)) | ||
Theorem | lsatnle 37392 | The meet of a subspace and an incomparable atom is the zero subspace. (atnssm0 31104 analog.) (Contributed by NM, 10-Jan-2015.) |
β’ 0 = (0gβπ) & β’ π = (LSubSpβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β π΄) β β’ (π β (Β¬ π β π β (π β© π) = { 0 })) | ||
Theorem | lsatnem0 37393 | The meet of distinct atoms is the zero subspace. (atnemeq0 31105 analog.) (Contributed by NM, 10-Jan-2015.) |
β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LVec) & β’ (π β π β π΄) & β’ (π β π β π΄) β β’ (π β (π β π β (π β© π ) = { 0 })) | ||
Theorem | lsatexch1 37394 | The atom exch1ange property. (hlatexch1 37744 analog.) (Contributed by NM, 14-Jan-2015.) |
β’ β = (LSSumβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LVec) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β π β (π β π )) & β’ (π β π β π) β β’ (π β π β (π β π)) | ||
Theorem | lsatcv0eq 37395 | If the sum of two atoms cover the zero subspace, they are equal. (atcv0eq 31107 analog.) (Contributed by NM, 10-Jan-2015.) |
β’ 0 = (0gβπ) & β’ β = (LSSumβπ) & β’ π΄ = (LSAtomsβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LVec) & β’ (π β π β π΄) & β’ (π β π β π΄) β β’ (π β ({ 0 }πΆ(π β π ) β π = π )) | ||
Theorem | lsatcv1 37396 | Two atoms covering the zero subspace are equal. (atcv1 31108 analog.) (Contributed by NM, 10-Jan-2015.) |
β’ 0 = (0gβπ) & β’ β = (LSSumβπ) & β’ π = (LSubSpβπ) & β’ π΄ = (LSAtomsβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β ππΆ(π β π )) β β’ (π β (π = { 0 } β π = π )) | ||
Theorem | lsatcvatlem 37397 | Lemma for lsatcvat 37398. (Contributed by NM, 10-Jan-2015.) |
β’ 0 = (0gβπ) & β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β π β { 0 }) & β’ (π β π β (π β π )) & β’ (π β Β¬ π β π) β β’ (π β π β π΄) | ||
Theorem | lsatcvat 37398 | A nonzero subspace less than the sum of two atoms is an atom. (atcvati 31114 analog.) (Contributed by NM, 10-Jan-2015.) |
β’ 0 = (0gβπ) & β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β π β { 0 }) & β’ (π β π β (π β π )) β β’ (π β π β π΄) | ||
Theorem | lsatcvat2 37399 | A subspace covered by the sum of two distinct atoms is an atom. (atcvat2i 31115 analog.) (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π΄ = (LSAtomsβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β π β π ) & β’ (π β ππΆ(π β π )) β β’ (π β π β π΄) | ||
Theorem | lsatcvat3 37400 | A condition implying that a certain subspace is an atom. Part of Lemma 3.2.20 of [PtakPulmannova] p. 68. (atcvat3i 31124 analog.) (Contributed by NM, 11-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β π β π ) & β’ (π β Β¬ π β π) & β’ (π β π β (π β π )) β β’ (π β (π β© (π β π )) β π΄) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |