![]() |
Metamath
Proof Explorer Theorem List (p. 385 of 482) | < 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-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lsatlspsn2 38401 | The span of a nonzero singleton is an atom. TODO: make this obsolete and use lsatlspsn 38402 instead? (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 24-Jun-2014.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) β β’ ((π β LMod β§ π β π β§ π β 0 ) β (πβ{π}) β π΄) | ||
Theorem | lsatlspsn 38402 | The span of a nonzero singleton is an atom. (Contributed by NM, 16-Jan-2015.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β (π β { 0 })) β β’ (π β (πβ{π}) β π΄) | ||
Theorem | islsati 38403* | 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 38404* | 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 38405 | 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 38406 | An atom is a subspace. (Contributed by NM, 25-Aug-2014.) |
β’ π = (LSubSpβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β π΄) β β’ (π β π β π) | ||
Theorem | lsatssv 38407 | An atom is a set of vectors. (Contributed by NM, 27-Feb-2015.) |
β’ π = (Baseβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β π΄) β β’ (π β π β π) | ||
Theorem | lsatn0 38408 | A 1-dim subspace (atom) of a left module or left vector space is nonzero. (atne0 32142 analog.) (Contributed by NM, 25-Aug-2014.) |
β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β π΄) β β’ (π β π β { 0 }) | ||
Theorem | lsatspn0 38409 | 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 38410 | 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 38411 | A subspace (or any class) including an atom is nonzero. (Contributed by NM, 3-Feb-2015.) |
β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β π΄) & β’ (π β π β π) β β’ (π β π β { 0 }) | ||
Theorem | lsatcmp 38412 | If two atoms are comparable, they are equal. (atsseq 32144 analog.) TODO: can lspsncmp 20993 shorten this? (Contributed by NM, 25-Aug-2014.) |
β’ π΄ = (LSAtomsβπ) & β’ (π β π β LVec) & β’ (π β π β π΄) & β’ (π β π β π΄) β β’ (π β (π β π β π = π)) | ||
Theorem | lsatcmp2 38413 | If an atom is included in at-most an atom, they are equal. More general version of lsatcmp 38412. TODO: can lspsncmp 20993 shorten this? (Contributed by NM, 3-Feb-2015.) |
β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LVec) & β’ (π β π β π΄) & β’ (π β (π β π΄ β¨ π = { 0 })) β β’ (π β (π β π β π = π)) | ||
Theorem | lsatel 38414 | A nonzero vector in an atom determines the atom. (Contributed by NM, 25-Aug-2014.) |
β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LVec) & β’ (π β π β π΄) & β’ (π β π β π) & β’ (π β π β 0 ) β β’ (π β π = (πβ{π})) | ||
Theorem | lsatelbN 38415 | 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 38416 | Two atoms sharing a nonzero vector are equal. (Contributed by NM, 8-Mar-2015.) |
β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LVec) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β π β 0 ) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β π = π) | ||
Theorem | lsmsat 38417* | Convert comparison of atom with sum of subspaces to a comparison to sum with atom. (elpaddatiN 39215 analog.) TODO: any way to shorten this? (Contributed by NM, 15-Jan-2015.) |
β’ 0 = (0gβπ) & β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π΄) & β’ (π β π β { 0 }) & β’ (π β π β (π β π)) β β’ (π β βπ β π΄ (π β π β§ π β (π β π))) | ||
Theorem | lsatfixedN 38418* | Show equality with the span of the sum of two vectors, one of which (π) is fixed in advance. Compare lspfixed 21005. (Contributed by NM, 29-May-2015.) (New usage is discouraged.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LVec) & β’ (π β π β π΄) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β (πβ{π})) & β’ (π β π β (πβ{π})) & β’ (π β π β (πβ{π, π})) β β’ (π β βπ§ β ((πβ{π}) β { 0 })π = (πβ{(π + π§)})) | ||
Theorem | lsmsatcv 38419 | Subspace sum has the covering property (using spans of singletons to represent atoms). Similar to Exercise 5 of [Kalmbach] p. 153. (spansncvi 31449 analog.) Explicit atom version of lsmcv 21018. (Contributed by NM, 29-Oct-2014.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π΄) β β’ ((π β§ π β π β§ π β (π β π)) β π = (π β π)) | ||
Theorem | lssatomic 38420* | The lattice of subspaces is atomic, i.e. any nonzero element is greater than or equal to some atom. (shatomici 32155 analog.) (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β { 0 }) β β’ (π β βπ β π΄ π β π) | ||
Theorem | lssats 38421* | 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 32158 analog.) (Contributed by NM, 9-Apr-2014.) |
β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) & β’ π΄ = (LSAtomsβπ) β β’ ((π β LMod β§ π β π) β π = (πββͺ {π₯ β π΄ β£ π₯ β π})) | ||
Theorem | lpssat 38422* | Two subspaces in a proper subset relationship imply the existence of an atom less than or equal to one but not the other. (chpssati 32160 analog.) (Contributed by NM, 11-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β βπ β π΄ (π β π β§ Β¬ π β π)) | ||
Theorem | lrelat 38423* | Subspaces are relatively atomic. Remark 2 of [Kalmbach] p. 149. (chrelati 32161 analog.) (Contributed by NM, 11-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β βπ β π΄ (π β (π β π) β§ (π β π) β π)) | ||
Theorem | lssatle 38424* | The ordering of two subspaces is determined by the atoms under them. (chrelat3 32168 analog.) (Contributed by NM, 29-Oct-2014.) |
β’ π = (LSubSpβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (π β π β βπ β π΄ (π β π β π β π))) | ||
Theorem | lssat 38425* | 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 32160 analog.) (Contributed by NM, 9-Apr-2014.) |
β’ π = (LSubSpβπ) & β’ π΄ = (LSAtomsβπ) β β’ (((π β LMod β§ π β π β§ π β π) β§ π β π) β βπ β π΄ (π β π β§ Β¬ π β π)) | ||
Theorem | islshpat 38426* | Hyperplane properties expressed with subspace sum and an atom. TODO: can proof be shortened? Seems long for a simple variation of islshpsm 38389. (Contributed by NM, 11-Jan-2015.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π» = (LSHypβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LMod) β β’ (π β (π β π» β (π β π β§ π β π β§ βπ β π΄ (π β π) = π))) | ||
Syntax | clcv 38427 | Extend class notation with the covering relation for a left module or left vector space. |
class βL | ||
Definition | df-lcv 38428* | 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 38430 for binary relation. (df-cv 32076 analog.) (Contributed by NM, 7-Jan-2015.) |
β’ βL = (π€ β V β¦ {β¨π‘, π’β© β£ ((π‘ β (LSubSpβπ€) β§ π’ β (LSubSpβπ€)) β§ (π‘ β π’ β§ Β¬ βπ β (LSubSpβπ€)(π‘ β π β§ π β π’)))}) | ||
Theorem | lcvfbr 38429* | The covers relation for a left vector space (or a left module). (Contributed by NM, 7-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β π) β β’ (π β πΆ = {β¨π‘, π’β© β£ ((π‘ β π β§ π’ β π) β§ (π‘ β π’ β§ Β¬ βπ β π (π‘ β π β§ π β π’)))}) | ||
Theorem | lcvbr 38430* | The covers relation for a left vector space (or a left module). (cvbr 32079 analog.) (Contributed by NM, 9-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (ππΆπ β (π β π β§ Β¬ βπ β π (π β π β§ π β π)))) | ||
Theorem | lcvbr2 38431* | The covers relation for a left vector space (or a left module). (cvbr2 32080 analog.) (Contributed by NM, 9-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (ππΆπ β (π β π β§ βπ β π ((π β π β§ π β π) β π = π)))) | ||
Theorem | lcvbr3 38432* | The covers relation for a left vector space (or a left module). (Contributed by NM, 9-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (ππΆπ β (π β π β§ βπ β π ((π β π β§ π β π) β (π = π β¨ π = π))))) | ||
Theorem | lcvpss 38433 | The covers relation implies proper subset. (cvpss 32082 analog.) (Contributed by NM, 7-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β ππΆπ) β β’ (π β π β π) | ||
Theorem | lcvnbtwn 38434 | The covers relation implies no in-betweenness. (cvnbtwn 32083 analog.) (Contributed by NM, 7-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π πΆπ) β β’ (π β Β¬ (π β π β§ π β π)) | ||
Theorem | lcvntr 38435 | The covers relation is not transitive. (cvntr 32089 analog.) (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π πΆπ) & β’ (π β ππΆπ) β β’ (π β Β¬ π πΆπ) | ||
Theorem | lcvnbtwn2 38436 | The covers relation implies no in-betweenness. (cvnbtwn2 32084 analog.) (Contributed by NM, 7-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π πΆπ) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β π = π) | ||
Theorem | lcvnbtwn3 38437 | The covers relation implies no in-betweenness. (cvnbtwn3 32085 analog.) (Contributed by NM, 7-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π πΆπ) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β π = π ) | ||
Theorem | lsmcv2 38438 | Subspace sum has the covering property (using spans of singletons to represent atoms). Proposition 1(ii) of [Kalmbach] p. 153. (spansncv2 32090 analog.) (Contributed by NM, 10-Jan-2015.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) & β’ β = (LSSumβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β Β¬ (πβ{π}) β π) β β’ (π β ππΆ(π β (πβ{π}))) | ||
Theorem | lcvat 38439* | If a subspace covers another, it equals the other joined with some atom. This is a consequence of relative atomicity. (cvati 32163 analog.) (Contributed by NM, 11-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π΄ = (LSAtomsβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β ππΆπ) β β’ (π β βπ β π΄ (π β π) = π) | ||
Theorem | lsatcv0 38440 | An atom covers the zero subspace. (atcv0 32139 analog.) (Contributed by NM, 7-Jan-2015.) |
β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LVec) & β’ (π β π β π΄) β β’ (π β { 0 }πΆπ) | ||
Theorem | lsatcveq0 38441 | A subspace covered by an atom must be the zero subspace. (atcveq0 32145 analog.) (Contributed by NM, 7-Jan-2015.) |
β’ 0 = (0gβπ) & β’ π = (LSubSpβπ) & β’ π΄ = (LSAtomsβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β π΄) β β’ (π β (ππΆπ β π = { 0 })) | ||
Theorem | lsat0cv 38442 | 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 38443 | Lemma for lcvexch 38448. (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (π β (π β π) β (π β© π) β π)) | ||
Theorem | lcvexchlem2 38444 | Lemma for lcvexch 38448. (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β (π β© π) β π ) & β’ (π β π β π) β β’ (π β ((π β π) β© π) = π ) | ||
Theorem | lcvexchlem3 38445 | Lemma for lcvexch 38448. (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π ) & β’ (π β π β (π β π)) β β’ (π β ((π β© π) β π) = π ) | ||
Theorem | lcvexchlem4 38446 | Lemma for lcvexch 38448. (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β ππΆ(π β π)) β β’ (π β (π β© π)πΆπ) | ||
Theorem | lcvexchlem5 38447 | Lemma for lcvexch 38448. (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β (π β© π)πΆπ) β β’ (π β ππΆ(π β π)) | ||
Theorem | lcvexch 38448 | Subspaces satisfy the exchange axiom. Lemma 7.5 of [MaedaMaeda] p. 31. (cvexchi 32166 analog.) TODO: combine some lemmas. (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LMod) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β ((π β© π)πΆπ β ππΆ(π β π))) | ||
Theorem | lcvp 38449 | Covering property of Definition 7.4 of [MaedaMaeda] p. 31 and its converse. (cvp 32172 analog.) (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β π΄) β β’ (π β ((π β© π) = { 0 } β ππΆ(π β π))) | ||
Theorem | lcv1 38450 | Covering property of a subspace plus an atom. (chcv1 32152 analog.) (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π΄ = (LSAtomsβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β π΄) β β’ (π β (Β¬ π β π β ππΆ(π β π))) | ||
Theorem | lcv2 38451 | Covering property of a subspace plus an atom. (chcv2 32153 analog.) (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π΄ = (LSAtomsβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β π΄) β β’ (π β (π β (π β π) β ππΆ(π β π))) | ||
Theorem | lsatexch 38452 | 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 32178 analog.) (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β π β (π β π )) & β’ (π β (π β© π) = { 0 }) β β’ (π β π β (π β π)) | ||
Theorem | lsatnle 38453 | The meet of a subspace and an incomparable atom is the zero subspace. (atnssm0 32173 analog.) (Contributed by NM, 10-Jan-2015.) |
β’ 0 = (0gβπ) & β’ π = (LSubSpβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β π΄) β β’ (π β (Β¬ π β π β (π β© π) = { 0 })) | ||
Theorem | lsatnem0 38454 | The meet of distinct atoms is the zero subspace. (atnemeq0 32174 analog.) (Contributed by NM, 10-Jan-2015.) |
β’ 0 = (0gβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LVec) & β’ (π β π β π΄) & β’ (π β π β π΄) β β’ (π β (π β π β (π β© π ) = { 0 })) | ||
Theorem | lsatexch1 38455 | The atom exch1ange property. (hlatexch1 38805 analog.) (Contributed by NM, 14-Jan-2015.) |
β’ β = (LSSumβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LVec) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β π β (π β π )) & β’ (π β π β π) β β’ (π β π β (π β π)) | ||
Theorem | lsatcv0eq 38456 | If the sum of two atoms cover the zero subspace, they are equal. (atcv0eq 32176 analog.) (Contributed by NM, 10-Jan-2015.) |
β’ 0 = (0gβπ) & β’ β = (LSSumβπ) & β’ π΄ = (LSAtomsβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LVec) & β’ (π β π β π΄) & β’ (π β π β π΄) β β’ (π β ({ 0 }πΆ(π β π ) β π = π )) | ||
Theorem | lsatcv1 38457 | Two atoms covering the zero subspace are equal. (atcv1 32177 analog.) (Contributed by NM, 10-Jan-2015.) |
β’ 0 = (0gβπ) & β’ β = (LSSumβπ) & β’ π = (LSubSpβπ) & β’ π΄ = (LSAtomsβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β ππΆ(π β π )) β β’ (π β (π = { 0 } β π = π )) | ||
Theorem | lsatcvatlem 38458 | Lemma for lsatcvat 38459. (Contributed by NM, 10-Jan-2015.) |
β’ 0 = (0gβπ) & β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β π β { 0 }) & β’ (π β π β (π β π )) & β’ (π β Β¬ π β π) β β’ (π β π β π΄) | ||
Theorem | lsatcvat 38459 | A nonzero subspace less than the sum of two atoms is an atom. (atcvati 32183 analog.) (Contributed by NM, 10-Jan-2015.) |
β’ 0 = (0gβπ) & β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β π β { 0 }) & β’ (π β π β (π β π )) β β’ (π β π β π΄) | ||
Theorem | lsatcvat2 38460 | A subspace covered by the sum of two distinct atoms is an atom. (atcvat2i 32184 analog.) (Contributed by NM, 10-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π΄ = (LSAtomsβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β π β π ) & β’ (π β ππΆ(π β π )) β β’ (π β π β π΄) | ||
Theorem | lsatcvat3 38461 | A condition implying that a certain subspace is an atom. Part of Lemma 3.2.20 of [PtakPulmannova] p. 68. (atcvat3i 32193 analog.) (Contributed by NM, 11-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β π β π ) & β’ (π β Β¬ π β π) & β’ (π β π β (π β π )) β β’ (π β (π β© (π β π )) β π΄) | ||
Theorem | islshpcv 38462 | Hyperplane properties expressed with covers relation. (Contributed by NM, 11-Jan-2015.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) & β’ π» = (LSHypβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LVec) β β’ (π β (π β π» β (π β π β§ ππΆπ))) | ||
Theorem | l1cvpat 38463 | A subspace covered by the set of all vectors, when summed with an atom not under it, equals the set of all vectors. (1cvrjat 38885 analog.) (Contributed by NM, 11-Jan-2015.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π΄ = (LSAtomsβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β π΄) & β’ (π β ππΆπ) & β’ (π β Β¬ π β π) β β’ (π β (π β π) = π) | ||
Theorem | l1cvat 38464 | Create an atom under an element covered by the lattice unity. Part of proof of Lemma B in [Crawley] p. 112. (1cvrat 38886 analog.) (Contributed by NM, 11-Jan-2015.) |
β’ π = (Baseβπ) & β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π΄ = (LSAtomsβπ) & β’ πΆ = ( βL βπ) & β’ (π β π β LVec) & β’ (π β π β π) & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β π β π ) & β’ (π β ππΆπ) & β’ (π β Β¬ π β π) β β’ (π β ((π β π ) β© π) β π΄) | ||
Theorem | lshpat 38465 | Create an atom under a hyperplane. Part of proof of Lemma B in [Crawley] p. 112. (lhpat 39453 analog.) TODO: This changes ππΆπ in l1cvpat 38463 and l1cvat 38464 to π β π», which in turn change π β π» in islshpcv 38462 to ππΆπ, with a couple of conversions of span to atom. Seems convoluted. Would a direct proof be better? (Contributed by NM, 11-Jan-2015.) |
β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π» = (LSHypβπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β π β LVec) & β’ (π β π β π») & β’ (π β π β π΄) & β’ (π β π β π΄) & β’ (π β π β π ) & β’ (π β Β¬ π β π) β β’ (π β ((π β π ) β© π) β π΄) | ||
Syntax | clfn 38466 | Extend class notation with all linear functionals of a left module or left vector space. |
class LFnl | ||
Definition | df-lfl 38467* | Define the set of all linear functionals (maps from vectors to the ring) of a left module or left vector space. (Contributed by NM, 15-Apr-2014.) |
β’ LFnl = (π€ β V β¦ {π β ((Baseβ(Scalarβπ€)) βm (Baseβπ€)) β£ βπ β (Baseβ(Scalarβπ€))βπ₯ β (Baseβπ€)βπ¦ β (Baseβπ€)(πβ((π( Β·π βπ€)π₯)(+gβπ€)π¦)) = ((π(.rβ(Scalarβπ€))(πβπ₯))(+gβ(Scalarβπ€))(πβπ¦))}) | ||
Theorem | lflset 38468* | The set of linear functionals in a left module or left vector space. (Contributed by NM, 15-Apr-2014.) (Revised by Mario Carneiro, 24-Jun-2014.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ π· = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (Baseβπ·) & ⒠⨣ = (+gβπ·) & β’ Γ = (.rβπ·) & β’ πΉ = (LFnlβπ) β β’ (π β π β πΉ = {π β (πΎ βm π) β£ βπ β πΎ βπ₯ β π βπ¦ β π (πβ((π Β· π₯) + π¦)) = ((π Γ (πβπ₯)) ⨣ (πβπ¦))}) | ||
Theorem | islfl 38469* | The predicate "is a linear functional". (Contributed by NM, 15-Apr-2014.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ π· = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (Baseβπ·) & ⒠⨣ = (+gβπ·) & β’ Γ = (.rβπ·) & β’ πΉ = (LFnlβπ) β β’ (π β π β (πΊ β πΉ β (πΊ:πβΆπΎ β§ βπ β πΎ βπ₯ β π βπ¦ β π (πΊβ((π Β· π₯) + π¦)) = ((π Γ (πΊβπ₯)) ⨣ (πΊβπ¦))))) | ||
Theorem | lfli 38470 | Property of a linear functional. (lnfnli 31837 analog.) (Contributed by NM, 16-Apr-2014.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ π· = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (Baseβπ·) & ⒠⨣ = (+gβπ·) & β’ Γ = (.rβπ·) & β’ πΉ = (LFnlβπ) β β’ ((π β π β§ πΊ β πΉ β§ (π β πΎ β§ π β π β§ π β π)) β (πΊβ((π Β· π) + π)) = ((π Γ (πΊβπ)) ⨣ (πΊβπ))) | ||
Theorem | islfld 38471* | Properties that determine a linear functional. TODO: use this in place of islfl 38469 when it shortens the proof. (Contributed by NM, 19-Oct-2014.) |
β’ (π β π = (Baseβπ)) & β’ (π β + = (+gβπ)) & β’ (π β π· = (Scalarβπ)) & β’ (π β Β· = ( Β·π βπ)) & β’ (π β πΎ = (Baseβπ·)) & β’ (π β ⨣ = (+gβπ·)) & β’ (π β Γ = (.rβπ·)) & β’ (π β πΉ = (LFnlβπ)) & β’ (π β πΊ:πβΆπΎ) & β’ ((π β§ (π β πΎ β§ π₯ β π β§ π¦ β π)) β (πΊβ((π Β· π₯) + π¦)) = ((π Γ (πΊβπ₯)) ⨣ (πΊβπ¦))) & β’ (π β π β π) β β’ (π β πΊ β πΉ) | ||
Theorem | lflf 38472 | A linear functional is a function from vectors to scalars. (lnfnfi 31838 analog.) (Contributed by NM, 15-Apr-2014.) |
β’ π· = (Scalarβπ) & β’ πΎ = (Baseβπ·) & β’ π = (Baseβπ) & β’ πΉ = (LFnlβπ) β β’ ((π β π β§ πΊ β πΉ) β πΊ:πβΆπΎ) | ||
Theorem | lflcl 38473 | A linear functional value is a scalar. (Contributed by NM, 15-Apr-2014.) |
β’ π· = (Scalarβπ) & β’ πΎ = (Baseβπ·) & β’ π = (Baseβπ) & β’ πΉ = (LFnlβπ) β β’ ((π β π β§ πΊ β πΉ β§ π β π) β (πΊβπ) β πΎ) | ||
Theorem | lfl0 38474 | A linear functional is zero at the zero vector. (lnfn0i 31839 analog.) (Contributed by NM, 16-Apr-2014.) (Revised by Mario Carneiro, 24-Jun-2014.) |
β’ π· = (Scalarβπ) & β’ 0 = (0gβπ·) & β’ π = (0gβπ) & β’ πΉ = (LFnlβπ) β β’ ((π β LMod β§ πΊ β πΉ) β (πΊβπ) = 0 ) | ||
Theorem | lfladd 38475 | Property of a linear functional. (lnfnaddi 31840 analog.) (Contributed by NM, 18-Apr-2014.) |
β’ π· = (Scalarβπ) & ⒠⨣ = (+gβπ·) & β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ πΉ = (LFnlβπ) β β’ ((π β LMod β§ πΊ β πΉ β§ (π β π β§ π β π)) β (πΊβ(π + π)) = ((πΊβπ) ⨣ (πΊβπ))) | ||
Theorem | lflsub 38476 | Property of a linear functional. (lnfnaddi 31840 analog.) (Contributed by NM, 18-Apr-2014.) |
β’ π· = (Scalarβπ) & β’ π = (-gβπ·) & β’ π = (Baseβπ) & β’ β = (-gβπ) & β’ πΉ = (LFnlβπ) β β’ ((π β LMod β§ πΊ β πΉ β§ (π β π β§ π β π)) β (πΊβ(π β π)) = ((πΊβπ)π(πΊβπ))) | ||
Theorem | lflmul 38477 | Property of a linear functional. (lnfnmuli 31841 analog.) (Contributed by NM, 16-Apr-2014.) |
β’ π· = (Scalarβπ) & β’ πΎ = (Baseβπ·) & β’ Γ = (.rβπ·) & β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΉ = (LFnlβπ) β β’ ((π β LMod β§ πΊ β πΉ β§ (π β πΎ β§ π β π)) β (πΊβ(π Β· π)) = (π Γ (πΊβπ))) | ||
Theorem | lfl0f 38478 | The zero function is a functional. (Contributed by NM, 16-Apr-2014.) |
β’ π· = (Scalarβπ) & β’ 0 = (0gβπ·) & β’ π = (Baseβπ) & β’ πΉ = (LFnlβπ) β β’ (π β LMod β (π Γ { 0 }) β πΉ) | ||
Theorem | lfl1 38479* | A nonzero functional has a value of 1 at some argument. (Contributed by NM, 16-Apr-2014.) |
β’ π· = (Scalarβπ) & β’ 0 = (0gβπ·) & β’ 1 = (1rβπ·) & β’ π = (Baseβπ) & β’ πΉ = (LFnlβπ) β β’ ((π β LVec β§ πΊ β πΉ β§ πΊ β (π Γ { 0 })) β βπ₯ β π (πΊβπ₯) = 1 ) | ||
Theorem | lfladdcl 38480 | Closure of addition of two functionals. (Contributed by NM, 19-Oct-2014.) |
β’ π = (Scalarβπ) & β’ + = (+gβπ ) & β’ πΉ = (LFnlβπ) & β’ (π β π β LMod) & β’ (π β πΊ β πΉ) & β’ (π β π» β πΉ) β β’ (π β (πΊ βf + π») β πΉ) | ||
Theorem | lfladdcom 38481 | Commutativity of functional addition. (Contributed by NM, 19-Oct-2014.) |
β’ π = (Scalarβπ) & β’ + = (+gβπ ) & β’ πΉ = (LFnlβπ) & β’ (π β π β LMod) & β’ (π β πΊ β πΉ) & β’ (π β π» β πΉ) β β’ (π β (πΊ βf + π») = (π» βf + πΊ)) | ||
Theorem | lfladdass 38482 | Associativity of functional addition. (Contributed by NM, 19-Oct-2014.) |
β’ π = (Scalarβπ) & β’ + = (+gβπ ) & β’ πΉ = (LFnlβπ) & β’ (π β π β LMod) & β’ (π β πΊ β πΉ) & β’ (π β π» β πΉ) & β’ (π β πΌ β πΉ) β β’ (π β ((πΊ βf + π») βf + πΌ) = (πΊ βf + (π» βf + πΌ))) | ||
Theorem | lfladd0l 38483 | Functional addition with the zero functional. (Contributed by NM, 21-Oct-2014.) |
β’ π = (Baseβπ) & β’ π = (Scalarβπ) & β’ + = (+gβπ ) & β’ 0 = (0gβπ ) & β’ πΉ = (LFnlβπ) & β’ (π β π β LMod) & β’ (π β πΊ β πΉ) β β’ (π β ((π Γ { 0 }) βf + πΊ) = πΊ) | ||
Theorem | lflnegcl 38484* | Closure of the negative of a functional. (This is specialized for the purpose of proving ldualgrp 38555, and we do not define a general operation here.) (Contributed by NM, 22-Oct-2014.) |
β’ π = (Baseβπ) & β’ π = (Scalarβπ) & β’ πΌ = (invgβπ ) & β’ π = (π₯ β π β¦ (πΌβ(πΊβπ₯))) & β’ πΉ = (LFnlβπ) & β’ (π β π β LMod) & β’ (π β πΊ β πΉ) β β’ (π β π β πΉ) | ||
Theorem | lflnegl 38485* | A functional plus its negative is the zero functional. (This is specialized for the purpose of proving ldualgrp 38555, and we do not define a general operation here.) (Contributed by NM, 22-Oct-2014.) |
β’ π = (Baseβπ) & β’ π = (Scalarβπ) & β’ πΌ = (invgβπ ) & β’ π = (π₯ β π β¦ (πΌβ(πΊβπ₯))) & β’ πΉ = (LFnlβπ) & β’ (π β π β LMod) & β’ (π β πΊ β πΉ) & β’ + = (+gβπ ) & β’ 0 = (0gβπ ) β β’ (π β (π βf + πΊ) = (π Γ { 0 })) | ||
Theorem | lflvscl 38486 | Closure of a scalar product with a functional. Note that this is the scalar product for a right vector space with the scalar after the vector; reversing these fails closure. (Contributed by NM, 9-Oct-2014.) (Revised by Mario Carneiro, 22-Apr-2015.) |
β’ π = (Baseβπ) & β’ π· = (Scalarβπ) & β’ πΎ = (Baseβπ·) & β’ Β· = (.rβπ·) & β’ πΉ = (LFnlβπ) & β’ (π β π β LMod) & β’ (π β πΊ β πΉ) & β’ (π β π β πΎ) β β’ (π β (πΊ βf Β· (π Γ {π })) β πΉ) | ||
Theorem | lflvsdi1 38487 | Distributive law for (right vector space) scalar product of functionals. (Contributed by NM, 19-Oct-2014.) |
β’ π = (Baseβπ) & β’ π = (Scalarβπ) & β’ πΎ = (Baseβπ ) & β’ + = (+gβπ ) & β’ Β· = (.rβπ ) & β’ πΉ = (LFnlβπ) & β’ (π β π β LMod) & β’ (π β π β πΎ) & β’ (π β πΊ β πΉ) & β’ (π β π» β πΉ) β β’ (π β ((πΊ βf + π») βf Β· (π Γ {π})) = ((πΊ βf Β· (π Γ {π})) βf + (π» βf Β· (π Γ {π})))) | ||
Theorem | lflvsdi2 38488 | Reverse distributive law for (right vector space) scalar product of functionals. (Contributed by NM, 19-Oct-2014.) |
β’ π = (Baseβπ) & β’ π = (Scalarβπ) & β’ πΎ = (Baseβπ ) & β’ + = (+gβπ ) & β’ Β· = (.rβπ ) & β’ πΉ = (LFnlβπ) & β’ (π β π β LMod) & β’ (π β π β πΎ) & β’ (π β π β πΎ) & β’ (π β πΊ β πΉ) β β’ (π β (πΊ βf Β· ((π Γ {π}) βf + (π Γ {π}))) = ((πΊ βf Β· (π Γ {π})) βf + (πΊ βf Β· (π Γ {π})))) | ||
Theorem | lflvsdi2a 38489 | Reverse distributive law for (right vector space) scalar product of functionals. (Contributed by NM, 21-Oct-2014.) |
β’ π = (Baseβπ) & β’ π = (Scalarβπ) & β’ πΎ = (Baseβπ ) & β’ + = (+gβπ ) & β’ Β· = (.rβπ ) & β’ πΉ = (LFnlβπ) & β’ (π β π β LMod) & β’ (π β π β πΎ) & β’ (π β π β πΎ) & β’ (π β πΊ β πΉ) β β’ (π β (πΊ βf Β· (π Γ {(π + π)})) = ((πΊ βf Β· (π Γ {π})) βf + (πΊ βf Β· (π Γ {π})))) | ||
Theorem | lflvsass 38490 | Associative law for (right vector space) scalar product of functionals. (Contributed by NM, 19-Oct-2014.) |
β’ π = (Baseβπ) & β’ π = (Scalarβπ) & β’ πΎ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ πΉ = (LFnlβπ) & β’ (π β π β LMod) & β’ (π β π β πΎ) & β’ (π β π β πΎ) & β’ (π β πΊ β πΉ) β β’ (π β (πΊ βf Β· (π Γ {(π Β· π)})) = ((πΊ βf Β· (π Γ {π})) βf Β· (π Γ {π}))) | ||
Theorem | lfl0sc 38491 | The (right vector space) scalar product of a functional with zero is the zero functional. Note that the first occurrence of (π Γ { 0 }) represents the zero scalar, and the second is the zero functional. (Contributed by NM, 7-Oct-2014.) |
β’ π = (Baseβπ) & β’ π· = (Scalarβπ) & β’ πΉ = (LFnlβπ) & β’ πΎ = (Baseβπ·) & β’ Β· = (.rβπ·) & β’ 0 = (0gβπ·) & β’ (π β π β LMod) & β’ (π β πΊ β πΉ) β β’ (π β (πΊ βf Β· (π Γ { 0 })) = (π Γ { 0 })) | ||
Theorem | lflsc0N 38492 | The scalar product with the zero functional is the zero functional. (Contributed by NM, 7-Oct-2014.) (New usage is discouraged.) |
β’ π = (Baseβπ) & β’ π· = (Scalarβπ) & β’ πΎ = (Baseβπ·) & β’ Β· = (.rβπ·) & β’ 0 = (0gβπ·) & β’ (π β π β LMod) & β’ (π β π β πΎ) β β’ (π β ((π Γ { 0 }) βf Β· (π Γ {π})) = (π Γ { 0 })) | ||
Theorem | lfl1sc 38493 | The (right vector space) scalar product of a functional with one is the functional. (Contributed by NM, 21-Oct-2014.) |
β’ π = (Baseβπ) & β’ π· = (Scalarβπ) & β’ πΉ = (LFnlβπ) & β’ πΎ = (Baseβπ·) & β’ Β· = (.rβπ·) & β’ 1 = (1rβπ·) & β’ (π β π β LMod) & β’ (π β πΊ β πΉ) β β’ (π β (πΊ βf Β· (π Γ { 1 })) = πΊ) | ||
Syntax | clk 38494 | Extend class notation with the kernel of a functional (set of vectors whose functional value is zero) on a left module or left vector space. |
class LKer | ||
Definition | df-lkr 38495* | Define the kernel of a functional (set of vectors whose functional value is zero) on a left module or left vector space. (Contributed by NM, 15-Apr-2014.) |
β’ LKer = (π€ β V β¦ (π β (LFnlβπ€) β¦ (β‘π β {(0gβ(Scalarβπ€))}))) | ||
Theorem | lkrfval 38496* | The kernel of a functional. (Contributed by NM, 15-Apr-2014.) (Revised by Mario Carneiro, 24-Jun-2014.) |
β’ π· = (Scalarβπ) & β’ 0 = (0gβπ·) & β’ πΉ = (LFnlβπ) & β’ πΎ = (LKerβπ) β β’ (π β π β πΎ = (π β πΉ β¦ (β‘π β { 0 }))) | ||
Theorem | lkrval 38497 | Value of the kernel of a functional. (Contributed by NM, 15-Apr-2014.) |
β’ π· = (Scalarβπ) & β’ 0 = (0gβπ·) & β’ πΉ = (LFnlβπ) & β’ πΎ = (LKerβπ) β β’ ((π β π β§ πΊ β πΉ) β (πΎβπΊ) = (β‘πΊ β { 0 })) | ||
Theorem | ellkr 38498 | Membership in the kernel of a functional. (elnlfn 31725 analog.) (Contributed by NM, 16-Apr-2014.) |
β’ π = (Baseβπ) & β’ π· = (Scalarβπ) & β’ 0 = (0gβπ·) & β’ πΉ = (LFnlβπ) & β’ πΎ = (LKerβπ) β β’ ((π β π β§ πΊ β πΉ) β (π β (πΎβπΊ) β (π β π β§ (πΊβπ) = 0 ))) | ||
Theorem | lkrval2 38499* | Value of the kernel of a functional. (Contributed by NM, 15-Apr-2014.) |
β’ π = (Baseβπ) & β’ π· = (Scalarβπ) & β’ 0 = (0gβπ·) & β’ πΉ = (LFnlβπ) & β’ πΎ = (LKerβπ) β β’ ((π β π β§ πΊ β πΉ) β (πΎβπΊ) = {π₯ β π β£ (πΊβπ₯) = 0 }) | ||
Theorem | ellkr2 38500 | Membership in the kernel of a functional. (Contributed by NM, 12-Jan-2015.) |
β’ π = (Baseβπ) & β’ π· = (Scalarβπ) & β’ 0 = (0gβπ·) & β’ πΉ = (LFnlβπ) & β’ πΎ = (LKerβπ) & β’ (π β π β π) & β’ (π β πΊ β πΉ) & β’ (π β π β π) β β’ (π β (π β (πΎβπΊ) β (πΊβπ) = 0 )) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |