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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-ndx 17001 | Define the structure component index extractor. See Theorem ndxarg 17003 to understand its purpose. The restriction to ℕ ensures that ndx is a set. The restriction to some set is necessary since I is a proper class. In principle, we could have chosen ℂ or (if we revise all structure component definitions such as df-base 17019) another set such as the set of finite ordinals ω (df-om 7794). (Contributed by NM, 4-Sep-2011.) |
⊢ ndx = ( I ↾ ℕ) | ||
Theorem | wunndx 17002 | Closure of the index extractor in an infinite weak universe. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → ω ∈ 𝑈) ⇒ ⊢ (𝜑 → ndx ∈ 𝑈) | ||
Theorem | ndxarg 17003 | Get the numeric argument from a defined structure component extractor such as df-base 17019. (Contributed by Mario Carneiro, 6-Oct-2013.) |
⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ (𝐸‘ndx) = 𝑁 | ||
Theorem | ndxid 17004 |
A structure component extractor is defined by its own index. This
theorem, together with strfv 17011 below, is useful for avoiding direct
reference to the hard-coded numeric index in component extractor
definitions, such as the 1 in df-base 17019 and the ;10 in
df-ple 17088, 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 17005 | 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 16992 directly with 𝑁 set to (𝐸‘ndx) if possible. |
⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ (𝜑 → (𝑆‘(𝐸‘ndx)) = (𝐸‘𝑆)) | ||
Theorem | setsidvald 17006 |
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 17007 | Obsolete version of setsidvald 17006 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 17008 | Deduction version of strfv 17011. (Contributed by Mario Carneiro, 15-Nov-2014.) |
⊢ 𝐸 = Slot (𝐸‘ndx) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → Fun 𝑆) & ⊢ (𝜑 → ⟨(𝐸‘ndx), 𝐶⟩ ∈ 𝑆) ⇒ ⊢ (𝜑 → 𝐶 = (𝐸‘𝑆)) | ||
Theorem | strfv2d 17009 | Deduction version of strfv2 17010. (Contributed by Mario Carneiro, 30-Apr-2015.) |
⊢ 𝐸 = Slot (𝐸‘ndx) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → Fun ◡◡𝑆) & ⊢ (𝜑 → ⟨(𝐸‘ndx), 𝐶⟩ ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝐶 = (𝐸‘𝑆)) | ||
Theorem | strfv2 17010 | A variation on strfv 17011 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 17011 | Extract a structure component 𝐶 (such as the base set) from a structure 𝑆 (such as a member of Poset, df-poset 18137) with a component extractor 𝐸 (such as the base set extractor df-base 17019). By virtue of ndxid 17004, 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 17012 | Variant on strfv 17011 for large structures. (Contributed by Mario Carneiro, 10-Jan-2017.) |
⊢ (𝜑 → 𝑈 = 𝑆) & ⊢ 𝑆 Struct 𝑋 & ⊢ 𝐸 = Slot (𝐸‘ndx) & ⊢ {⟨(𝐸‘ndx), 𝐶⟩} ⊆ 𝑆 & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ 𝐴 = (𝐸‘𝑈) ⇒ ⊢ (𝜑 → 𝐴 = 𝐶) | ||
Theorem | strssd 17013 | Deduction version of strss 17014. (Contributed by Mario Carneiro, 15-Nov-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) |
⊢ 𝐸 = Slot (𝐸‘ndx) & ⊢ (𝜑 → 𝑇 ∈ 𝑉) & ⊢ (𝜑 → Fun 𝑇) & ⊢ (𝜑 → 𝑆 ⊆ 𝑇) & ⊢ (𝜑 → ⟨(𝐸‘ndx), 𝐶⟩ ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐸‘𝑇) = (𝐸‘𝑆)) | ||
Theorem | strss 17014 | 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 17015 | 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 17016 | 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 17017 | Obsolete proof of setsnid 17016 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 17018 | Extend class notation with the class of all base set extractors. |
class Base | ||
Definition | df-base 17019 | 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 17021 instead. (New usage is discouraged.) |
⊢ Base = Slot 1 | ||
Theorem | baseval 17020 | 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 17021 | Utility theorem: index-independent form of df-base 17019. (Contributed by NM, 20-Oct-2012.) |
⊢ Base = Slot (Base‘ndx) | ||
Theorem | basfn 17022 | The base set extractor is a function on V. (Contributed by Stefan O'Rear, 8-Jul-2015.) |
⊢ Base Fn V | ||
Theorem | base0 17023 | The base set of the empty structure. (Contributed by David A. Wheeler, 7-Jul-2016.) |
⊢ ∅ = (Base‘∅) | ||
Theorem | elbasfv 17024 | Utility theorem: reverse closure for any structure defined as a function. (Contributed by Stefan O'Rear, 24-Aug-2015.) |
⊢ 𝑆 = (𝐹‘𝑍) & ⊢ 𝐵 = (Base‘𝑆) ⇒ ⊢ (𝑋 ∈ 𝐵 → 𝑍 ∈ V) | ||
Theorem | elbasov 17025 | 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 17026 | 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 17027 | 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 17028 | 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 17029 | Obsolete proof of basendxnn 17028 as of 13-Oct-2024. (Contributed by AV, 23-Sep-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (Base‘ndx) ∈ ℕ | ||
Theorem | basndxelwund 17030 | The index of the base set is an element in a weak universe containing the natural numbers. Formerly part of proof for 1strwun 17038. (Contributed by AV, 27-Mar-2020.) (Revised by AV, 17-Oct-2024.) |
⊢ (𝜑 → 𝑈 ∈ WUni) & ⊢ (𝜑 → ω ∈ 𝑈) ⇒ ⊢ (𝜑 → (Base‘ndx) ∈ 𝑈) | ||
Theorem | basprssdmsets 17031 | 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 17032 | The base set of a structure with a base set. (Contributed by AV, 10-Nov-2021.) |
⊢ (𝜑 → 𝑆 Struct 𝑋) & ⊢ (𝜑 → 𝑉 ∈ 𝑌) & ⊢ (𝜑 → ⟨(Base‘ndx), 𝑉⟩ ∈ 𝑆) ⇒ ⊢ (𝜑 → 𝑉 = (Base‘𝑆)) | ||
Theorem | 1strstr 17033 | A constructed one-slot structure. Depending on hard-coded index. Use 1strstr1 17034 instead. (Contributed by AV, 27-Mar-2020.) (New usage is discouraged.) |
⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩} ⇒ ⊢ 𝐺 Struct ⟨1, 1⟩ | ||
Theorem | 1strstr1 17034 | A constructed one-slot structure. (Contributed by AV, 15-Nov-2024.) |
⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩} ⇒ ⊢ 𝐺 Struct ⟨(Base‘ndx), (Base‘ndx)⟩ | ||
Theorem | 1strbas 17035 | 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 17036 | Obsolete proof of 1strbas 17035 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 17037 | 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 17038 | 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 17039 | Obsolete version of 1strwun 17038 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 17040 | A constructed two-slot structure. Depending on hard-coded indices. Use 2strstr1 17043 instead. (Contributed by Mario Carneiro, 29-Aug-2015.) (New usage is discouraged.) |
⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨(𝐸‘ndx), + ⟩} & ⊢ 𝐸 = Slot 𝑁 & ⊢ 1 < 𝑁 & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ 𝐺 Struct ⟨1, 𝑁⟩ | ||
Theorem | 2strbas 17041 | The base set of a constructed two-slot structure. (Contributed by Mario Carneiro, 29-Aug-2015.) Use the index-independent version 2strbas1 17045 instead. (New usage is discouraged.) |
⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨(𝐸‘ndx), + ⟩} & ⊢ 𝐸 = Slot 𝑁 & ⊢ 1 < 𝑁 & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ (𝐵 ∈ 𝑉 → 𝐵 = (Base‘𝐺)) | ||
Theorem | 2strop 17042 | The other slot of a constructed two-slot structure. (Contributed by Mario Carneiro, 29-Aug-2015.) Use the index-independent version 2strop1 17046 instead. (New usage is discouraged.) |
⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨(𝐸‘ndx), + ⟩} & ⊢ 𝐸 = Slot 𝑁 & ⊢ 1 < 𝑁 & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ ( + ∈ 𝑉 → + = (𝐸‘𝐺)) | ||
Theorem | 2strstr1 17043 | A constructed two-slot structure. Version of 2strstr 17040 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 17044 | Obsolete version of 2strstr1 17043 as of 27-Oct-2024. A constructed two-slot structure. Version of 2strstr 17040 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 17045 | The base set of a constructed two-slot structure. Version of 2strbas 17041 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 17046 | The other slot of a constructed two-slot structure. Version of 2strop 17042 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 17047 | Extend class notation with the extensible structure builder restriction operator. |
class ↾s | ||
Definition | df-ress 17048* |
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 17053 for the altered base set, and resseqnbas 17057 (subrg0 20152, ressplusg 17106, subrg1 20155, ressmulr 17123) 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 17049 | The structure restriction is a proper operator, so it can be used with ovprc1 7389. (Contributed by Stefan O'Rear, 29-Nov-2014.) |
⊢ Rel dom ↾s | ||
Theorem | ressval 17050 | Value of structure restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.) |
⊢ 𝑅 = (𝑊 ↾s 𝐴) & ⊢ 𝐵 = (Base‘𝑊) ⇒ ⊢ ((𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = if(𝐵 ⊆ 𝐴, 𝑊, (𝑊 sSet ⟨(Base‘ndx), (𝐴 ∩ 𝐵)⟩))) | ||
Theorem | ressid2 17051 | General behavior of trivial restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.) |
⊢ 𝑅 = (𝑊 ↾s 𝐴) & ⊢ 𝐵 = (Base‘𝑊) ⇒ ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = 𝑊) | ||
Theorem | ressval2 17052 | Value of nontrivial structure restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.) |
⊢ 𝑅 = (𝑊 ↾s 𝐴) & ⊢ 𝐵 = (Base‘𝑊) ⇒ ⊢ ((¬ 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = (𝑊 sSet ⟨(Base‘ndx), (𝐴 ∩ 𝐵)⟩)) | ||
Theorem | ressbas 17053 | 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 17054 | Obsolete proof of ressbas 17053 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 17055 | Base set of a structure restriction. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ 𝑅 = (𝑊 ↾s 𝐴) & ⊢ 𝐵 = (Base‘𝑊) ⇒ ⊢ (𝐴 ⊆ 𝐵 → 𝐴 = (Base‘𝑅)) | ||
Theorem | ressbasss 17056 | 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 17057 | 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 17058 | Obsolete version of resseqnbas 17057 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 17059 | 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 17060 | Behavior of trivial restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.) |
⊢ 𝐵 = (Base‘𝑊) ⇒ ⊢ (𝑊 ∈ 𝑋 → (𝑊 ↾s 𝐵) = 𝑊) | ||
Theorem | ressinbas 17061 | 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 17062 | 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 17063 | Obsolete version of ressval3d 17062 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 17064 | Restriction composition law. (Contributed by Stefan O'Rear, 29-Nov-2014.) (Proof shortened by Mario Carneiro, 2-Dec-2014.) |
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵))) | ||
Theorem | ressabs 17065 | Restriction absorption law. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ⊆ 𝐴) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s 𝐵)) | ||
Theorem | wunress 17066 | 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 17067 | Obsolete proof of wunress 17066 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 17068 | Extend class notation with group (addition) operation. |
class +g | ||
Syntax | cmulr 17069 | Extend class notation with ring multiplication. |
class .r | ||
Syntax | cstv 17070 | Extend class notation with involution. |
class *𝑟 | ||
Syntax | csca 17071 | Extend class notation with scalar field. |
class Scalar | ||
Syntax | cvsca 17072 | Extend class notation with scalar product. |
class ·𝑠 | ||
Syntax | cip 17073 | Extend class notation with Hermitian form (inner product). |
class ·𝑖 | ||
Syntax | cts 17074 | Extend class notation with the topology component of a topological space. |
class TopSet | ||
Syntax | cple 17075 | Extend class notation with "less than or equal to" for posets. |
class le | ||
Syntax | coc 17076 | Extend class notation with the class of orthocomplementation extractors. |
class oc | ||
Syntax | cds 17077 | Extend class notation with the metric space distance function. |
class dist | ||
Syntax | cunif 17078 | Extend class notation with the uniform structure. |
class UnifSet | ||
Syntax | chom 17079 | Extend class notation with the hom-set structure. |
class Hom | ||
Syntax | cco 17080 | Extend class notation with the composition operation. |
class comp | ||
Definition | df-plusg 17081 | Define group operation. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) Use its index-independent form plusgid 17095 instead. (New usage is discouraged.) |
⊢ +g = Slot 2 | ||
Definition | df-mulr 17082 | Define ring multiplication. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) Use its index-independent form mulrid 17110 instead. (New usage is discouraged.) |
⊢ .r = Slot 3 | ||
Definition | df-starv 17083 | 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 17119 instead. (New usage is discouraged.) |
⊢ *𝑟 = Slot 4 | ||
Definition | df-sca 17084 | 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 17131 instead. (New usage is discouraged.) |
⊢ Scalar = Slot 5 | ||
Definition | df-vsca 17085 | Define scalar product. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) Use its index-independent form vscaid 17136 instead. (New usage is discouraged.) |
⊢ ·𝑠 = Slot 6 | ||
Definition | df-ip 17086 | Define Hermitian form (inner product). (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) Use its index-independent form ipid 17147 instead. (New usage is discouraged.) |
⊢ ·𝑖 = Slot 8 | ||
Definition | df-tset 17087 | 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 17169 instead. (New usage is discouraged.) |
⊢ TopSet = Slot 9 | ||
Definition | df-ple 17088 | 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 17183 instead. (New usage is discouraged.) |
⊢ le = Slot ;10 | ||
Definition | df-ocomp 17089 | 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 17198 instead. (New usage is discouraged.) |
⊢ oc = Slot ;11 | ||
Definition | df-ds 17090 | 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 17202 instead. (New usage is discouraged.) |
⊢ dist = Slot ;12 | ||
Definition | df-unif 17091 | Define the uniform structure component of a uniform space. (Contributed by Mario Carneiro, 14-Aug-2015.) Use its index-independent form unifid 17212 instead. (New usage is discouraged.) |
⊢ UnifSet = Slot ;13 | ||
Definition | df-hom 17092 | Define the hom-set component of a category. (Contributed by Mario Carneiro, 2-Jan-2017.) Use its index-independent form homid 17228 instead. (New usage is discouraged.) |
⊢ Hom = Slot ;14 | ||
Definition | df-cco 17093 | Define the composition operation of a category. (Contributed by Mario Carneiro, 2-Jan-2017.) Use its index-independent form ccoid 17230 instead. (New usage is discouraged.) |
⊢ comp = Slot ;15 | ||
Theorem | plusgndx 17094 | Index value of the df-plusg 17081 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) (New usage is discouraged.) |
⊢ (+g‘ndx) = 2 | ||
Theorem | plusgid 17095 | Utility theorem: index-independent form of df-plusg 17081. (Contributed by NM, 20-Oct-2012.) |
⊢ +g = Slot (+g‘ndx) | ||
Theorem | plusgndxnn 17096 | 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 17097 | 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 17098 | 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 17099 | Obsolete version of basendxnplusgndx 17098 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 17100 | A constructed group is a structure on 1...2. Depending on hard-coded index values. Use grpstrndx 17101 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⟩ |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |