Home | Metamath
Proof Explorer Theorem List (p. 171 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 | wunndx 17001 | Closure of the index extractor in an infinite weak universe. (Contributed by Mario Carneiro, 12-Jan-2017.) |
β’ (π β π β WUni) & β’ (π β Ο β π) β β’ (π β ndx β π) | ||
Theorem | ndxarg 17002 | Get the numeric argument from a defined structure component extractor such as df-base 17018. (Contributed by Mario Carneiro, 6-Oct-2013.) |
β’ πΈ = Slot π & β’ π β β β β’ (πΈβndx) = π | ||
Theorem | ndxid 17003 |
A structure component extractor is defined by its own index. This
theorem, together with strfv 17010 below, is useful for avoiding direct
reference to the hard-coded numeric index in component extractor
definitions, such as the 1 in df-base 17018 and the ;10 in
df-ple 17087, making it easier to change should the need
arise.
For example, we can refer to a specific poset with base set π΅ and order relation πΏ using {β¨(Baseβndx), π΅β©, β¨(leβndx), πΏβ©} rather than {β¨1, π΅β©, β¨;10, πΏβ©}. The latter, while shorter to state, requires revision if we later change ;10 to some other number, and it may also be harder to remember. (Contributed by NM, 19-Oct-2012.) (Revised by Mario Carneiro, 6-Oct-2013.) (Proof shortened by BJ, 27-Dec-2021.) |
β’ πΈ = Slot π & β’ π β β β β’ πΈ = Slot (πΈβndx) | ||
Theorem | strndxid 17004 | The value of a structure component extractor is the value of the corresponding slot of the structure. (Contributed by AV, 13-Mar-2020.) (New usage is discouraged.) Use strfvnd 16991 directly with π set to (πΈβndx) if possible. |
β’ (π β π β π) & β’ πΈ = Slot π & β’ π β β β β’ (π β (πβ(πΈβndx)) = (πΈβπ)) | ||
Theorem | setsidvald 17005 |
Value of the structure replacement function, deduction version.
Hint: Do not substitute π by a specific (positive) integer to be independent of a hard-coded index value. Often, (πΈβndx) can be used instead of π. (Contributed by AV, 14-Mar-2020.) (Revised by AV, 17-Oct-2024.) |
β’ πΈ = Slot π & β’ (π β π β π) & β’ (π β Fun π) & β’ (π β π β dom π) β β’ (π β π = (π sSet β¨π, (πΈβπ)β©)) | ||
Theorem | setsidvaldOLD 17006 | Obsolete version of setsidvald 17005 as of 17-Oct-2024. (Contributed by AV, 14-Mar-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ πΈ = Slot π & β’ π β β & β’ (π β π β π) & β’ (π β Fun π) & β’ (π β (πΈβndx) β dom π) β β’ (π β π = (π sSet β¨(πΈβndx), (πΈβπ)β©)) | ||
Theorem | strfvd 17007 | Deduction version of strfv 17010. (Contributed by Mario Carneiro, 15-Nov-2014.) |
β’ πΈ = Slot (πΈβndx) & β’ (π β π β π) & β’ (π β Fun π) & β’ (π β β¨(πΈβndx), πΆβ© β π) β β’ (π β πΆ = (πΈβπ)) | ||
Theorem | strfv2d 17008 | Deduction version of strfv2 17009. (Contributed by Mario Carneiro, 30-Apr-2015.) |
β’ πΈ = Slot (πΈβndx) & β’ (π β π β π) & β’ (π β Fun β‘β‘π) & β’ (π β β¨(πΈβndx), πΆβ© β π) & β’ (π β πΆ β π) β β’ (π β πΆ = (πΈβπ)) | ||
Theorem | strfv2 17009 | A variation on strfv 17010 to avoid asserting that π itself is a function, which involves sethood of all the ordered pair components of π. (Contributed by Mario Carneiro, 30-Apr-2015.) |
β’ π β V & β’ Fun β‘β‘π & β’ πΈ = Slot (πΈβndx) & β’ β¨(πΈβndx), πΆβ© β π β β’ (πΆ β π β πΆ = (πΈβπ)) | ||
Theorem | strfv 17010 | Extract a structure component πΆ (such as the base set) from a structure π (such as a member of Poset, df-poset 18136) with a component extractor πΈ (such as the base set extractor df-base 17018). By virtue of ndxid 17003, this can be done without having to refer to the hard-coded numeric index of πΈ. (Contributed by Mario Carneiro, 6-Oct-2013.) (Revised by Mario Carneiro, 29-Aug-2015.) |
β’ π Struct π & β’ πΈ = Slot (πΈβndx) & β’ {β¨(πΈβndx), πΆβ©} β π β β’ (πΆ β π β πΆ = (πΈβπ)) | ||
Theorem | strfv3 17011 | Variant on strfv 17010 for large structures. (Contributed by Mario Carneiro, 10-Jan-2017.) |
β’ (π β π = π) & β’ π Struct π & β’ πΈ = Slot (πΈβndx) & β’ {β¨(πΈβndx), πΆβ©} β π & β’ (π β πΆ β π) & β’ π΄ = (πΈβπ) β β’ (π β π΄ = πΆ) | ||
Theorem | strssd 17012 | Deduction version of strss 17013. (Contributed by Mario Carneiro, 15-Nov-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) |
β’ πΈ = Slot (πΈβndx) & β’ (π β π β π) & β’ (π β Fun π) & β’ (π β π β π) & β’ (π β β¨(πΈβndx), πΆβ© β π) β β’ (π β (πΈβπ) = (πΈβπ)) | ||
Theorem | strss 17013 | Propagate component extraction to a structure π from a subset structure π. (Contributed by Mario Carneiro, 11-Oct-2013.) (Revised by Mario Carneiro, 15-Jan-2014.) |
β’ π β V & β’ Fun π & β’ π β π & β’ πΈ = Slot (πΈβndx) & β’ β¨(πΈβndx), πΆβ© β π β β’ (πΈβπ) = (πΈβπ) | ||
Theorem | setsid 17014 | Value of the structure replacement function at a replaced index. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) |
β’ πΈ = Slot (πΈβndx) β β’ ((π β π΄ β§ πΆ β π) β πΆ = (πΈβ(π sSet β¨(πΈβndx), πΆβ©))) | ||
Theorem | setsnid 17015 | Value of the structure replacement function at an untouched index. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) (Proof shortened by AV, 7-Nov-2024.) |
β’ πΈ = Slot (πΈβndx) & β’ (πΈβndx) β π· β β’ (πΈβπ) = (πΈβ(π sSet β¨π·, πΆβ©)) | ||
Theorem | setsnidOLD 17016 | Obsolete proof of setsnid 17015 as of 7-Nov-2024. Value of the structure replacement function at an untouched index. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ πΈ = Slot (πΈβndx) & β’ (πΈβndx) β π· β β’ (πΈβπ) = (πΈβ(π sSet β¨π·, πΆβ©)) | ||
Syntax | cbs 17017 | Extend class notation with the class of all base set extractors. |
class Base | ||
Definition | df-base 17018 | Define the base set (also called underlying set, ground set, carrier set, or carrier) extractor for extensible structures. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) Use its index-independent form baseid 17020 instead. (New usage is discouraged.) |
β’ Base = Slot 1 | ||
Theorem | baseval 17019 | Value of the base set extractor. (Normally it is preferred to work with (Baseβndx) rather than the hard-coded 1 in order to make structure theorems portable. This is an example of how to obtain it when needed.) (New usage is discouraged.) (Contributed by NM, 4-Sep-2011.) |
β’ πΎ β V β β’ (BaseβπΎ) = (πΎβ1) | ||
Theorem | baseid 17020 | Utility theorem: index-independent form of df-base 17018. (Contributed by NM, 20-Oct-2012.) |
β’ Base = Slot (Baseβndx) | ||
Theorem | basfn 17021 | The base set extractor is a function on V. (Contributed by Stefan O'Rear, 8-Jul-2015.) |
β’ Base Fn V | ||
Theorem | base0 17022 | The base set of the empty structure. (Contributed by David A. Wheeler, 7-Jul-2016.) |
β’ β = (Baseββ ) | ||
Theorem | elbasfv 17023 | Utility theorem: reverse closure for any structure defined as a function. (Contributed by Stefan O'Rear, 24-Aug-2015.) |
β’ π = (πΉβπ) & β’ π΅ = (Baseβπ) β β’ (π β π΅ β π β V) | ||
Theorem | elbasov 17024 | Utility theorem: reverse closure for any structure defined as a two-argument function. (Contributed by Mario Carneiro, 3-Oct-2015.) |
β’ Rel dom π & β’ π = (πππ) & β’ π΅ = (Baseβπ) β β’ (π΄ β π΅ β (π β V β§ π β V)) | ||
Theorem | strov2rcl 17025 | Partial reverse closure for any structure defined as a two-argument function. (Contributed by Stefan O'Rear, 27-Mar-2015.) (Proof shortened by AV, 2-Dec-2019.) |
β’ π = (πΌπΉπ ) & β’ π΅ = (Baseβπ) & β’ Rel dom πΉ β β’ (π β π΅ β πΌ β V) | ||
Theorem | basendx 17026 | Index value of the base set extractor. (Contributed by Mario Carneiro, 2-Aug-2013.) Use of this theorem is discouraged since the particular value 1 for the index is an implementation detail, see section header comment mmtheorems.html#cnx for more information. (New usage is discouraged.) |
β’ (Baseβndx) = 1 | ||
Theorem | basendxnn 17027 | The index value of the base set extractor is a positive integer. This property should be ensured for every concrete coding because otherwise it could not be used in an extensible structure (slots must be positive integers). (Contributed by AV, 23-Sep-2020.) (Proof shortened by AV, 13-Oct-2024.) |
β’ (Baseβndx) β β | ||
Theorem | basendxnnOLD 17028 | Obsolete proof of basendxnn 17027 as of 13-Oct-2024. (Contributed by AV, 23-Sep-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (Baseβndx) β β | ||
Theorem | basndxelwund 17029 | The index of the base set is an element in a weak universe containing the natural numbers. Formerly part of proof for 1strwun 17037. (Contributed by AV, 27-Mar-2020.) (Revised by AV, 17-Oct-2024.) |
β’ (π β π β WUni) & β’ (π β Ο β π) β β’ (π β (Baseβndx) β π) | ||
Theorem | basprssdmsets 17030 | The pair of the base index and another index is a subset of the domain of the structure obtained by replacing/adding a slot at the other index in a structure having a base slot. (Contributed by AV, 7-Jun-2021.) (Revised by AV, 16-Nov-2021.) |
β’ (π β π Struct π) & β’ (π β πΌ β π) & β’ (π β πΈ β π) & β’ (π β (Baseβndx) β dom π) β β’ (π β {(Baseβndx), πΌ} β dom (π sSet β¨πΌ, πΈβ©)) | ||
Theorem | opelstrbas 17031 | The base set of a structure with a base set. (Contributed by AV, 10-Nov-2021.) |
β’ (π β π Struct π) & β’ (π β π β π) & β’ (π β β¨(Baseβndx), πβ© β π) β β’ (π β π = (Baseβπ)) | ||
Theorem | 1strstr 17032 | A constructed one-slot structure. Depending on hard-coded index. Use 1strstr1 17033 instead. (Contributed by AV, 27-Mar-2020.) (New usage is discouraged.) |
β’ πΊ = {β¨(Baseβndx), π΅β©} β β’ πΊ Struct β¨1, 1β© | ||
Theorem | 1strstr1 17033 | A constructed one-slot structure. (Contributed by AV, 15-Nov-2024.) |
β’ πΊ = {β¨(Baseβndx), π΅β©} β β’ πΊ Struct β¨(Baseβndx), (Baseβndx)β© | ||
Theorem | 1strbas 17034 | The base set of a constructed one-slot structure. (Contributed by AV, 27-Mar-2020.) (Proof shortened by AV, 15-Nov-2024.) |
β’ πΊ = {β¨(Baseβndx), π΅β©} β β’ (π΅ β π β π΅ = (BaseβπΊ)) | ||
Theorem | 1strbasOLD 17035 | Obsolete proof of 1strbas 17034 as of 15-Nov-2024. The base set of a constructed one-slot structure. (Contributed by AV, 27-Mar-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ πΊ = {β¨(Baseβndx), π΅β©} β β’ (π΅ β π β π΅ = (BaseβπΊ)) | ||
Theorem | 1strwunbndx 17036 | A constructed one-slot structure in a weak universe containing the index of the base set extractor. (Contributed by AV, 27-Mar-2020.) |
β’ πΊ = {β¨(Baseβndx), π΅β©} & β’ (π β π β WUni) & β’ (π β (Baseβndx) β π) β β’ ((π β§ π΅ β π) β πΊ β π) | ||
Theorem | 1strwun 17037 | A constructed one-slot structure in a weak universe. (Contributed by AV, 27-Mar-2020.) (Proof shortened by AV, 17-Oct-2024.) |
β’ πΊ = {β¨(Baseβndx), π΅β©} & β’ (π β π β WUni) & β’ (π β Ο β π) β β’ ((π β§ π΅ β π) β πΊ β π) | ||
Theorem | 1strwunOLD 17038 | Obsolete version of 1strwun 17037 as of 17-Oct-2024. A constructed one-slot structure in a weak universe. (Contributed by AV, 27-Mar-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ πΊ = {β¨(Baseβndx), π΅β©} & β’ (π β π β WUni) & β’ (π β Ο β π) β β’ ((π β§ π΅ β π) β πΊ β π) | ||
Theorem | 2strstr 17039 | A constructed two-slot structure. Depending on hard-coded indices. Use 2strstr1 17042 instead. (Contributed by Mario Carneiro, 29-Aug-2015.) (New usage is discouraged.) |
β’ πΊ = {β¨(Baseβndx), π΅β©, β¨(πΈβndx), + β©} & β’ πΈ = Slot π & β’ 1 < π & β’ π β β β β’ πΊ Struct β¨1, πβ© | ||
Theorem | 2strbas 17040 | The base set of a constructed two-slot structure. (Contributed by Mario Carneiro, 29-Aug-2015.) Use the index-independent version 2strbas1 17044 instead. (New usage is discouraged.) |
β’ πΊ = {β¨(Baseβndx), π΅β©, β¨(πΈβndx), + β©} & β’ πΈ = Slot π & β’ 1 < π & β’ π β β β β’ (π΅ β π β π΅ = (BaseβπΊ)) | ||
Theorem | 2strop 17041 | The other slot of a constructed two-slot structure. (Contributed by Mario Carneiro, 29-Aug-2015.) Use the index-independent version 2strop1 17045 instead. (New usage is discouraged.) |
β’ πΊ = {β¨(Baseβndx), π΅β©, β¨(πΈβndx), + β©} & β’ πΈ = Slot π & β’ 1 < π & β’ π β β β β’ ( + β π β + = (πΈβπΊ)) | ||
Theorem | 2strstr1 17042 | A constructed two-slot structure. Version of 2strstr 17039 not depending on the hard-coded index value of the base set. (Contributed by AV, 22-Sep-2020.) (Proof shortened by AV, 17-Oct-2024.) |
β’ πΊ = {β¨(Baseβndx), π΅β©, β¨π, + β©} & β’ (Baseβndx) < π & β’ π β β β β’ πΊ Struct β¨(Baseβndx), πβ© | ||
Theorem | 2strstr1OLD 17043 | Obsolete version of 2strstr1 17042 as of 27-Oct-2024. A constructed two-slot structure. Version of 2strstr 17039 not depending on the hard-coded index value of the base set. (Contributed by AV, 22-Sep-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ πΊ = {β¨(Baseβndx), π΅β©, β¨π, + β©} & β’ (Baseβndx) < π & β’ π β β β β’ πΊ Struct β¨(Baseβndx), πβ© | ||
Theorem | 2strbas1 17044 | The base set of a constructed two-slot structure. Version of 2strbas 17040 not depending on the hard-coded index value of the base set. (Contributed by AV, 22-Sep-2020.) |
β’ πΊ = {β¨(Baseβndx), π΅β©, β¨π, + β©} & β’ (Baseβndx) < π & β’ π β β β β’ (π΅ β π β π΅ = (BaseβπΊ)) | ||
Theorem | 2strop1 17045 | The other slot of a constructed two-slot structure. Version of 2strop 17041 not depending on the hard-coded index value of the base set. (Contributed by AV, 22-Sep-2020.) |
β’ πΊ = {β¨(Baseβndx), π΅β©, β¨π, + β©} & β’ (Baseβndx) < π & β’ π β β & β’ πΈ = Slot π β β’ ( + β π β + = (πΈβπΊ)) | ||
Syntax | cress 17046 | Extend class notation with the extensible structure builder restriction operator. |
class βΎs | ||
Definition | df-ress 17047* |
Define a multifunction restriction operator for extensible structures,
which can be used to turn statements about rings into statements about
subrings, modules into submodules, etc. This definition knows nothing
about individual structures and merely truncates the Base set while
leaving operators alone; individual kinds of structures will need to
handle this behavior, by ignoring operators' values outside the range
(like Ring), defining a function using the base
set and applying
that (like TopGrp), or explicitly truncating the
slot before use
(like MetSp).
(Credit for this operator goes to Mario Carneiro.) See ressbas 17052 for the altered base set, and resseqnbas 17056 (subrg0 20152, ressplusg 17105, subrg1 20155, ressmulr 17122) for the (un)altered other operations. (Contributed by Stefan O'Rear, 29-Nov-2014.) |
β’ βΎs = (π€ β V, π₯ β V β¦ if((Baseβπ€) β π₯, π€, (π€ sSet β¨(Baseβndx), (π₯ β© (Baseβπ€))β©))) | ||
Theorem | reldmress 17048 | The structure restriction is a proper operator, so it can be used with ovprc1 7388. (Contributed by Stefan O'Rear, 29-Nov-2014.) |
β’ Rel dom βΎs | ||
Theorem | ressval 17049 | Value of structure restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.) |
β’ π = (π βΎs π΄) & β’ π΅ = (Baseβπ) β β’ ((π β π β§ π΄ β π) β π = if(π΅ β π΄, π, (π sSet β¨(Baseβndx), (π΄ β© π΅)β©))) | ||
Theorem | ressid2 17050 | General behavior of trivial restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.) |
β’ π = (π βΎs π΄) & β’ π΅ = (Baseβπ) β β’ ((π΅ β π΄ β§ π β π β§ π΄ β π) β π = π) | ||
Theorem | ressval2 17051 | Value of nontrivial structure restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.) |
β’ π = (π βΎs π΄) & β’ π΅ = (Baseβπ) β β’ ((Β¬ π΅ β π΄ β§ π β π β§ π΄ β π) β π = (π sSet β¨(Baseβndx), (π΄ β© π΅)β©)) | ||
Theorem | ressbas 17052 | Base set of a structure restriction. (Contributed by Stefan O'Rear, 26-Nov-2014.) (Proof shortened by AV, 7-Nov-2024.) |
β’ π = (π βΎs π΄) & β’ π΅ = (Baseβπ) β β’ (π΄ β π β (π΄ β© π΅) = (Baseβπ )) | ||
Theorem | ressbasOLD 17053 | Obsolete proof of ressbas 17052 as of 7-Nov-2024. Base set of a structure restriction. (Contributed by Stefan O'Rear, 26-Nov-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = (π βΎs π΄) & β’ π΅ = (Baseβπ) β β’ (π΄ β π β (π΄ β© π΅) = (Baseβπ )) | ||
Theorem | ressbas2 17054 | Base set of a structure restriction. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ π = (π βΎs π΄) & β’ π΅ = (Baseβπ) β β’ (π΄ β π΅ β π΄ = (Baseβπ )) | ||
Theorem | ressbasss 17055 | The base set of a restriction is a subset of the base set of the original structure. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) |
β’ π = (π βΎs π΄) & β’ π΅ = (Baseβπ) β β’ (Baseβπ ) β π΅ | ||
Theorem | resseqnbas 17056 | The components of an extensible structure except the base set remain unchanged on a structure restriction. (Contributed by Mario Carneiro, 26-Nov-2014.) (Revised by Mario Carneiro, 2-Dec-2014.) (Revised by AV, 19-Oct-2024.) |
β’ π = (π βΎs π΄) & β’ πΆ = (πΈβπ) & β’ πΈ = Slot (πΈβndx) & β’ (πΈβndx) β (Baseβndx) β β’ (π΄ β π β πΆ = (πΈβπ )) | ||
Theorem | resslemOLD 17057 | Obsolete version of resseqnbas 17056 as of 21-Oct-2024. (Contributed by Mario Carneiro, 26-Nov-2014.) (Revised by Mario Carneiro, 2-Dec-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π = (π βΎs π΄) & β’ πΆ = (πΈβπ) & β’ πΈ = Slot π & β’ π β β & β’ 1 < π β β’ (π΄ β π β πΆ = (πΈβπ )) | ||
Theorem | ress0 17058 | All restrictions of the null set are trivial. (Contributed by Stefan O'Rear, 29-Nov-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) |
β’ (β βΎs π΄) = β | ||
Theorem | ressid 17059 | Behavior of trivial restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.) |
β’ π΅ = (Baseβπ) β β’ (π β π β (π βΎs π΅) = π) | ||
Theorem | ressinbas 17060 | Restriction only cares about the part of the second set which intersects the base of the first. (Contributed by Stefan O'Rear, 29-Nov-2014.) |
β’ π΅ = (Baseβπ) β β’ (π΄ β π β (π βΎs π΄) = (π βΎs (π΄ β© π΅))) | ||
Theorem | ressval3d 17061 | Value of structure restriction, deduction version. (Contributed by AV, 14-Mar-2020.) (Revised by AV, 3-Jul-2022.) (Proof shortened by AV, 17-Oct-2024.) |
β’ π = (π βΎs π΄) & β’ π΅ = (Baseβπ) & β’ πΈ = (Baseβndx) & β’ (π β π β π) & β’ (π β Fun π) & β’ (π β πΈ β dom π) & β’ (π β π΄ β π΅) β β’ (π β π = (π sSet β¨πΈ, π΄β©)) | ||
Theorem | ressval3dOLD 17062 | Obsolete version of ressval3d 17061 as of 17-Oct-2024. Value of structure restriction, deduction version. (Contributed by AV, 14-Mar-2020.) (Revised by AV, 3-Jul-2022.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = (π βΎs π΄) & β’ π΅ = (Baseβπ) & β’ πΈ = (Baseβndx) & β’ (π β π β π) & β’ (π β Fun π) & β’ (π β πΈ β dom π) & β’ (π β π΄ β π΅) β β’ (π β π = (π sSet β¨πΈ, π΄β©)) | ||
Theorem | ressress 17063 | Restriction composition law. (Contributed by Stefan O'Rear, 29-Nov-2014.) (Proof shortened by Mario Carneiro, 2-Dec-2014.) |
β’ ((π΄ β π β§ π΅ β π) β ((π βΎs π΄) βΎs π΅) = (π βΎs (π΄ β© π΅))) | ||
Theorem | ressabs 17064 | Restriction absorption law. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ ((π΄ β π β§ π΅ β π΄) β ((π βΎs π΄) βΎs π΅) = (π βΎs π΅)) | ||
Theorem | wunress 17065 | Closure of structure restriction in a weak universe. (Contributed by Mario Carneiro, 12-Jan-2017.) (Proof shortened by AV, 28-Oct-2024.) |
β’ (π β π β WUni) & β’ (π β Ο β π) & β’ (π β π β π) β β’ (π β (π βΎs π΄) β π) | ||
Theorem | wunressOLD 17066 | Obsolete proof of wunress 17065 as of 28-Oct-2024. Closure of structure restriction in a weak universe. (Contributed by Mario Carneiro, 12-Jan-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π β π β WUni) & β’ (π β Ο β π) & β’ (π β π β π) β β’ (π β (π βΎs π΄) β π) | ||
Syntax | cplusg 17067 | Extend class notation with group (addition) operation. |
class +g | ||
Syntax | cmulr 17068 | Extend class notation with ring multiplication. |
class .r | ||
Syntax | cstv 17069 | Extend class notation with involution. |
class *π | ||
Syntax | csca 17070 | Extend class notation with scalar field. |
class Scalar | ||
Syntax | cvsca 17071 | Extend class notation with scalar product. |
class Β·π | ||
Syntax | cip 17072 | Extend class notation with Hermitian form (inner product). |
class Β·π | ||
Syntax | cts 17073 | Extend class notation with the topology component of a topological space. |
class TopSet | ||
Syntax | cple 17074 | Extend class notation with "less than or equal to" for posets. |
class le | ||
Syntax | coc 17075 | Extend class notation with the class of orthocomplementation extractors. |
class oc | ||
Syntax | cds 17076 | Extend class notation with the metric space distance function. |
class dist | ||
Syntax | cunif 17077 | Extend class notation with the uniform structure. |
class UnifSet | ||
Syntax | chom 17078 | Extend class notation with the hom-set structure. |
class Hom | ||
Syntax | cco 17079 | Extend class notation with the composition operation. |
class comp | ||
Definition | df-plusg 17080 | Define group operation. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) Use its index-independent form plusgid 17094 instead. (New usage is discouraged.) |
β’ +g = Slot 2 | ||
Definition | df-mulr 17081 | Define ring multiplication. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) Use its index-independent form mulrid 17109 instead. (New usage is discouraged.) |
β’ .r = Slot 3 | ||
Definition | df-starv 17082 | Define the involution function of a *-ring. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) Use its index-independent form starvid 17118 instead. (New usage is discouraged.) |
β’ *π = Slot 4 | ||
Definition | df-sca 17083 | Define scalar field component of a vector space π£. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) Use its index-independent form scaid 17130 instead. (New usage is discouraged.) |
β’ Scalar = Slot 5 | ||
Definition | df-vsca 17084 | Define scalar product. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) Use its index-independent form vscaid 17135 instead. (New usage is discouraged.) |
β’ Β·π = Slot 6 | ||
Definition | df-ip 17085 | Define Hermitian form (inner product). (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) Use its index-independent form ipid 17146 instead. (New usage is discouraged.) |
β’ Β·π = Slot 8 | ||
Definition | df-tset 17086 | Define the topology component of a topological space (structure). (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) Use its index-independent form tsetid 17168 instead. (New usage is discouraged.) |
β’ TopSet = Slot 9 | ||
Definition | df-ple 17087 | Define "less than or equal to" ordering extractor for posets and related structures. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) (Revised by AV, 9-Sep-2021.) Use its index-independent form pleid 17182 instead. (New usage is discouraged.) |
β’ le = Slot ;10 | ||
Definition | df-ocomp 17088 | Define the orthocomplementation extractor for posets and related structures. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) Use its index-independent form ocid 17197 instead. (New usage is discouraged.) |
β’ oc = Slot ;11 | ||
Definition | df-ds 17089 | Define the distance function component of a metric space (structure). (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) Use its index-independent form dsid 17201 instead. (New usage is discouraged.) |
β’ dist = Slot ;12 | ||
Definition | df-unif 17090 | Define the uniform structure component of a uniform space. (Contributed by Mario Carneiro, 14-Aug-2015.) Use its index-independent form unifid 17211 instead. (New usage is discouraged.) |
β’ UnifSet = Slot ;13 | ||
Definition | df-hom 17091 | Define the hom-set component of a category. (Contributed by Mario Carneiro, 2-Jan-2017.) Use its index-independent form homid 17227 instead. (New usage is discouraged.) |
β’ Hom = Slot ;14 | ||
Definition | df-cco 17092 | Define the composition operation of a category. (Contributed by Mario Carneiro, 2-Jan-2017.) Use its index-independent form ccoid 17229 instead. (New usage is discouraged.) |
β’ comp = Slot ;15 | ||
Theorem | plusgndx 17093 | Index value of the df-plusg 17080 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (New usage is discouraged.) |
β’ (+gβndx) = 2 | ||
Theorem | plusgid 17094 | Utility theorem: index-independent form of df-plusg 17080. (Contributed by NM, 20-Oct-2012.) |
β’ +g = Slot (+gβndx) | ||
Theorem | plusgndxnn 17095 | The index of the slot for the group operation in an extensible structure is a positive integer. (Contributed by AV, 17-Oct-2024.) |
β’ (+gβndx) β β | ||
Theorem | basendxltplusgndx 17096 | The index of the slot for the base set is less then the index of the slot for the group operation in an extensible structure. (Contributed by AV, 17-Oct-2024.) |
β’ (Baseβndx) < (+gβndx) | ||
Theorem | basendxnplusgndx 17097 | The slot for the base set is not the slot for the group operation in an extensible structure. (Contributed by AV, 14-Nov-2021.) (Proof shortened by AV, 17-Oct-2024.) |
β’ (Baseβndx) β (+gβndx) | ||
Theorem | basendxnplusgndxOLD 17098 | Obsolete version of basendxnplusgndx 17097 as of 17-Oct-2024. The slot for the base set is not the slot for the group operation in an extensible structure. (Contributed by AV, 14-Nov-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (Baseβndx) β (+gβndx) | ||
Theorem | grpstr 17099 | A constructed group is a structure on 1...2. Depending on hard-coded index values. Use grpstrndx 17100 instead. (Contributed by Mario Carneiro, 28-Sep-2013.) (Revised by Mario Carneiro, 30-Apr-2015.) (New usage is discouraged.) |
β’ πΊ = {β¨(Baseβndx), π΅β©, β¨(+gβndx), + β©} β β’ πΊ Struct β¨1, 2β© | ||
Theorem | grpstrndx 17100 | A constructed group is a structure. Version not depending on the implementation of the indices. (Contributed by AV, 27-Oct-2024.) |
β’ πΊ = {β¨(Baseβndx), π΅β©, β¨(+gβndx), + β©} β β’ πΊ Struct β¨(Baseβndx), (+gβndx)β© |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |