Home | Intuitionistic Logic Explorer Theorem List (p. 125 of 141) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | csts 12401 | Set components of a structure. |
class sSet | ||
Syntax | cslot 12402 | Extend class notation with the slot function. |
class Slot 𝐴 | ||
Syntax | cbs 12403 | Extend class notation with the class of all base set extractors. |
class Base | ||
Syntax | cress 12404 | Extend class notation with the extensible structure builder restriction operator. |
class ↾s | ||
Definition | df-struct 12405* |
Define a structure with components in 𝑀...𝑁. This is not a
requirement for groups, posets, etc., but it is a useful assumption for
component extraction theorems.
As mentioned in the section header, an "extensible structure should be implemented as a function (a set of ordered pairs)". The current definition, however, is less restrictive: it allows for classes which contain the empty set ∅ to be extensible structures. Because of 0nelfun 5214, such classes cannot be functions. Without the empty set, however, a structure must be a function, see structn0fun 12416: 𝐹 Struct 𝑋 → Fun (𝐹 ∖ {∅}). Allowing an extensible structure to contain the empty set ensures that expressions like {〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} are structures without asserting or implying that 𝐴, 𝐵, 𝐶 and 𝐷 are sets (if 𝐴 or 𝐵 is a proper class, then 〈𝐴, 𝐵〉 = ∅, see opprc 3784). (Contributed by Mario Carneiro, 29-Aug-2015.) |
⊢ Struct = {〈𝑓, 𝑥〉 ∣ (𝑥 ∈ ( ≤ ∩ (ℕ × ℕ)) ∧ Fun (𝑓 ∖ {∅}) ∧ dom 𝑓 ⊆ (...‘𝑥))} | ||
Definition | df-ndx 12406 | Define the structure component index extractor. See Theorem ndxarg 12426 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 12409) another set such as the set of finite ordinals ω (df-iom 4573). (Contributed by NM, 4-Sep-2011.) |
⊢ ndx = ( I ↾ ℕ) | ||
Definition | df-slot 12407* |
Define the slot extractor for extensible structures. The class
Slot 𝐴 is a function whose argument can be
any set, although it is
meaningful only if that set is a member of an extensible structure (such
as a partially ordered set or a group).
Note that Slot 𝐴 is implemented as "evaluation at 𝐴". That is, (Slot 𝐴‘𝑆) is defined to be (𝑆‘𝐴), where 𝐴 will typically be a small nonzero natural number. Each extensible structure 𝑆 is a function defined on specific natural number "slots", and this function extracts the value at a particular slot. The special "structure" ndx, defined as the identity function restricted to ℕ, can be used to extract the number 𝐴 from a slot, since (Slot 𝐴‘ndx) = 𝐴 (see ndxarg 12426). This is typically used to refer to the number of a slot when defining structures without having to expose the detail of what that number is (for instance, we use the expression (Base‘ndx) in theorems and proofs instead of its value 1). The class Slot cannot be defined as (𝑥 ∈ V ↦ (𝑓 ∈ V ↦ (𝑓‘𝑥))) because each Slot 𝐴 is a function on the proper class V so is itself a proper class, and the values of functions are sets (fvex 5514). It is necessary to allow proper classes as values of Slot 𝐴 since for instance the class of all (base sets of) groups is proper. (Contributed by Mario Carneiro, 22-Sep-2015.) |
⊢ Slot 𝐴 = (𝑥 ∈ V ↦ (𝑥‘𝐴)) | ||
Theorem | sloteq 12408 | Equality theorem for the Slot construction. The converse holds if 𝐴 (or 𝐵) is a set. (Contributed by BJ, 27-Dec-2021.) |
⊢ (𝐴 = 𝐵 → Slot 𝐴 = Slot 𝐵) | ||
Definition | df-base 12409 | 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.) |
⊢ Base = Slot 1 | ||
Definition | df-sets 12410* | Set a component of an extensible structure. This function is useful for taking an existing structure and "overriding" one of its components. For example, df-ress 12411 adjusts the base set to match its second argument, which has the effect of making subgroups, subspaces, subrings etc. from the original structures. (Contributed by Mario Carneiro, 1-Dec-2014.) |
⊢ sSet = (𝑠 ∈ V, 𝑒 ∈ V ↦ ((𝑠 ↾ (V ∖ dom {𝑒})) ∪ {𝑒})) | ||
Definition | df-ress 12411* |
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,
defining a function using the base set and applying that, or explicitly
truncating the slot before use.
(Credit for this operator goes to Mario Carneiro.) (Contributed by Stefan O'Rear, 29-Nov-2014.) |
⊢ ↾s = (𝑤 ∈ V, 𝑥 ∈ V ↦ if((Base‘𝑤) ⊆ 𝑥, 𝑤, (𝑤 sSet 〈(Base‘ndx), (𝑥 ∩ (Base‘𝑤))〉))) | ||
Theorem | brstruct 12412 | The structure relation is a relation. (Contributed by Mario Carneiro, 29-Aug-2015.) |
⊢ Rel Struct | ||
Theorem | isstruct2im 12413 | The property of being a structure with components in (1st ‘𝑋)...(2nd ‘𝑋). (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.) |
⊢ (𝐹 Struct 𝑋 → (𝑋 ∈ ( ≤ ∩ (ℕ × ℕ)) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (...‘𝑋))) | ||
Theorem | isstruct2r 12414 | The property of being a structure with components in (1st ‘𝑋)...(2nd ‘𝑋). (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.) |
⊢ (((𝑋 ∈ ( ≤ ∩ (ℕ × ℕ)) ∧ Fun (𝐹 ∖ {∅})) ∧ (𝐹 ∈ 𝑉 ∧ dom 𝐹 ⊆ (...‘𝑋))) → 𝐹 Struct 𝑋) | ||
Theorem | structex 12415 | A structure is a set. (Contributed by AV, 10-Nov-2021.) |
⊢ (𝐺 Struct 𝑋 → 𝐺 ∈ V) | ||
Theorem | structn0fun 12416 | A structure without the empty set is a function. (Contributed by AV, 13-Nov-2021.) |
⊢ (𝐹 Struct 𝑋 → Fun (𝐹 ∖ {∅})) | ||
Theorem | isstructim 12417 | The property of being a structure with components in 𝑀...𝑁. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.) |
⊢ (𝐹 Struct 〈𝑀, 𝑁〉 → ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) ∧ Fun (𝐹 ∖ {∅}) ∧ dom 𝐹 ⊆ (𝑀...𝑁))) | ||
Theorem | isstructr 12418 | The property of being a structure with components in 𝑀...𝑁. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.) |
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁) ∧ (Fun (𝐹 ∖ {∅}) ∧ 𝐹 ∈ 𝑉 ∧ dom 𝐹 ⊆ (𝑀...𝑁))) → 𝐹 Struct 〈𝑀, 𝑁〉) | ||
Theorem | structcnvcnv 12419 | Two ways to express the relational part of a structure. (Contributed by Mario Carneiro, 29-Aug-2015.) |
⊢ (𝐹 Struct 𝑋 → ◡◡𝐹 = (𝐹 ∖ {∅})) | ||
Theorem | structfung 12420 | The converse of the converse of a structure is a function. Closed form of structfun 12421. (Contributed by AV, 12-Nov-2021.) |
⊢ (𝐹 Struct 𝑋 → Fun ◡◡𝐹) | ||
Theorem | structfun 12421 | Convert between two kinds of structure closure. (Contributed by Mario Carneiro, 29-Aug-2015.) (Proof shortened by AV, 12-Nov-2021.) |
⊢ 𝐹 Struct 𝑋 ⇒ ⊢ Fun ◡◡𝐹 | ||
Theorem | structfn 12422 | Convert between two kinds of structure closure. (Contributed by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝐹 Struct 〈𝑀, 𝑁〉 ⇒ ⊢ (Fun ◡◡𝐹 ∧ dom 𝐹 ⊆ (1...𝑁)) | ||
Theorem | strnfvnd 12423 | Deduction version of strnfvn 12424. (Contributed by Mario Carneiro, 15-Nov-2014.) (Revised by Jim Kingdon, 19-Jan-2023.) |
⊢ 𝐸 = Slot 𝑁 & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝐸‘𝑆) = (𝑆‘𝑁)) | ||
Theorem | strnfvn 12424 |
Value of a structure component extractor 𝐸. Normally, 𝐸 is a
defined constant symbol such as Base (df-base 12409) and 𝑁 is a
fixed integer such as 1. 𝑆 is a structure, i.e. a
specific
member of a class of structures.
Note: Normally, this theorem shouldn't be used outside of this section, because it requires hard-coded index values. Instead, use strslfv 12447. (Contributed by NM, 9-Sep-2011.) (Revised by Jim Kingdon, 19-Jan-2023.) (New usage is discouraged.) |
⊢ 𝑆 ∈ V & ⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ (𝐸‘𝑆) = (𝑆‘𝑁) | ||
Theorem | strfvssn 12425 | A structure component extractor produces a value which is contained in a set dependent on 𝑆, but not 𝐸. This is sometimes useful for showing sethood. (Contributed by Mario Carneiro, 15-Aug-2015.) (Revised by Jim Kingdon, 19-Jan-2023.) |
⊢ 𝐸 = Slot 𝑁 & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝐸‘𝑆) ⊆ ∪ ran 𝑆) | ||
Theorem | ndxarg 12426 | Get the numeric argument from a defined structure component extractor such as df-base 12409. (Contributed by Mario Carneiro, 6-Oct-2013.) |
⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ (𝐸‘ndx) = 𝑁 | ||
Theorem | ndxid 12427 |
A structure component extractor is defined by its own index. This
theorem, together with strslfv 12447 below, is useful for avoiding direct
reference to the hard-coded numeric index in component extractor
definitions, such as the 1 in df-base 12409, making it easier to change
should the need arise.
(Contributed by NM, 19-Oct-2012.) (Revised by Mario Carneiro, 6-Oct-2013.) (Proof shortened by BJ, 27-Dec-2021.) |
⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ 𝐸 = Slot (𝐸‘ndx) | ||
Theorem | ndxslid 12428 | A structure component extractor is defined by its own index. That the index is a natural number will also be needed in quite a few contexts so it is included in the conclusion of this theorem which can be used as a hypothesis of theorems like strslfv 12447. (Contributed by Jim Kingdon, 29-Jan-2023.) |
⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ) | ||
Theorem | slotslfn 12429 | A slot is a function on sets, treated as structures. (Contributed by Mario Carneiro, 22-Sep-2015.) (Revised by Jim Kingdon, 10-Feb-2023.) |
⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ) ⇒ ⊢ 𝐸 Fn V | ||
Theorem | slotex 12430 | Existence of slot value. A corollary of slotslfn 12429. (Contributed by Jim Kingdon, 12-Feb-2023.) |
⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝐸‘𝐴) ∈ V) | ||
Theorem | strndxid 12431 | The value of a structure component extractor is the value of the corresponding slot of the structure. (Contributed by AV, 13-Mar-2020.) |
⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ (𝜑 → (𝑆‘(𝐸‘ndx)) = (𝐸‘𝑆)) | ||
Theorem | reldmsets 12432 | The structure override operator is a proper operator. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
⊢ Rel dom sSet | ||
Theorem | setsvalg 12433 | Value of the structure replacement function. (Contributed by Mario Carneiro, 30-Apr-2015.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑆 sSet 𝐴) = ((𝑆 ↾ (V ∖ dom {𝐴})) ∪ {𝐴})) | ||
Theorem | setsvala 12434 | Value of the structure replacement function. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon, 20-Jan-2023.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑊) → (𝑆 sSet 〈𝐴, 𝐵〉) = ((𝑆 ↾ (V ∖ {𝐴})) ∪ {〈𝐴, 𝐵〉})) | ||
Theorem | setsex 12435 | Applying the structure replacement function yields a set. (Contributed by Jim Kingdon, 22-Jan-2023.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑊) → (𝑆 sSet 〈𝐴, 𝐵〉) ∈ V) | ||
Theorem | strsetsid 12436 | Value of the structure replacement function. (Contributed by AV, 14-Mar-2020.) (Revised by Jim Kingdon, 30-Jan-2023.) |
⊢ 𝐸 = Slot (𝐸‘ndx) & ⊢ (𝜑 → 𝑆 Struct 〈𝑀, 𝑁〉) & ⊢ (𝜑 → Fun 𝑆) & ⊢ (𝜑 → (𝐸‘ndx) ∈ dom 𝑆) ⇒ ⊢ (𝜑 → 𝑆 = (𝑆 sSet 〈(𝐸‘ndx), (𝐸‘𝑆)〉)) | ||
Theorem | fvsetsid 12437 | The value of the structure replacement function for its first argument is its second argument. (Contributed by SO, 12-Jul-2018.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ∧ 𝑌 ∈ 𝑈) → ((𝐹 sSet 〈𝑋, 𝑌〉)‘𝑋) = 𝑌) | ||
Theorem | setsfun 12438 | A structure with replacement is a function if the original structure is a function. (Contributed by AV, 7-Jun-2021.) |
⊢ (((𝐺 ∈ 𝑉 ∧ Fun 𝐺) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → Fun (𝐺 sSet 〈𝐼, 𝐸〉)) | ||
Theorem | setsfun0 12439 | A structure with replacement without the empty set is a function if the original structure without the empty set is a function. This variant of setsfun 12438 is useful for proofs based on isstruct2r 12414 which requires Fun (𝐹 ∖ {∅}) for 𝐹 to be an extensible structure. (Contributed by AV, 7-Jun-2021.) |
⊢ (((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅})) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → Fun ((𝐺 sSet 〈𝐼, 𝐸〉) ∖ {∅})) | ||
Theorem | setsn0fun 12440 | The value of the structure replacement function (without the empty set) is a function if the structure (without the empty set) is a function. (Contributed by AV, 7-Jun-2021.) (Revised by AV, 16-Nov-2021.) |
⊢ (𝜑 → 𝑆 Struct 𝑋) & ⊢ (𝜑 → 𝐼 ∈ 𝑈) & ⊢ (𝜑 → 𝐸 ∈ 𝑊) ⇒ ⊢ (𝜑 → Fun ((𝑆 sSet 〈𝐼, 𝐸〉) ∖ {∅})) | ||
Theorem | setsresg 12441 | The structure replacement function does not affect the value of 𝑆 away from 𝐴. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon, 22-Jan-2023.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋) → ((𝑆 sSet 〈𝐴, 𝐵〉) ↾ (V ∖ {𝐴})) = (𝑆 ↾ (V ∖ {𝐴}))) | ||
Theorem | setsabsd 12442 | Replacing the same components twice yields the same as the second setting only. (Contributed by Mario Carneiro, 2-Dec-2014.) (Revised by Jim Kingdon, 22-Jan-2023.) |
⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝑊) & ⊢ (𝜑 → 𝐵 ∈ 𝑋) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) ⇒ ⊢ (𝜑 → ((𝑆 sSet 〈𝐴, 𝐵〉) sSet 〈𝐴, 𝐶〉) = (𝑆 sSet 〈𝐴, 𝐶〉)) | ||
Theorem | setscom 12443 | Component-setting is commutative when the x-values are different. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋)) → ((𝑆 sSet 〈𝐴, 𝐶〉) sSet 〈𝐵, 𝐷〉) = ((𝑆 sSet 〈𝐵, 𝐷〉) sSet 〈𝐴, 𝐶〉)) | ||
Theorem | strslfvd 12444 | Deduction version of strslfv 12447. (Contributed by Mario Carneiro, 15-Nov-2014.) (Revised by Jim Kingdon, 30-Jan-2023.) |
⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → Fun 𝑆) & ⊢ (𝜑 → 〈(𝐸‘ndx), 𝐶〉 ∈ 𝑆) ⇒ ⊢ (𝜑 → 𝐶 = (𝐸‘𝑆)) | ||
Theorem | strslfv2d 12445 | Deduction version of strslfv 12447. (Contributed by Mario Carneiro, 30-Apr-2015.) (Revised by Jim Kingdon, 30-Jan-2023.) |
⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → Fun ◡◡𝑆) & ⊢ (𝜑 → 〈(𝐸‘ndx), 𝐶〉 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝐶 = (𝐸‘𝑆)) | ||
Theorem | strslfv2 12446 | A variation on strslfv 12447 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.) (Revised by Jim Kingdon, 30-Jan-2023.) |
⊢ 𝑆 ∈ V & ⊢ Fun ◡◡𝑆 & ⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ) & ⊢ 〈(𝐸‘ndx), 𝐶〉 ∈ 𝑆 ⇒ ⊢ (𝐶 ∈ 𝑉 → 𝐶 = (𝐸‘𝑆)) | ||
Theorem | strslfv 12447 | Extract a structure component 𝐶 (such as the base set) from a structure 𝑆 with a component extractor 𝐸 (such as the base set extractor df-base 12409). By virtue of ndxslid 12428, this can be done without having to refer to the hard-coded numeric index of 𝐸. (Contributed by Mario Carneiro, 6-Oct-2013.) (Revised by Jim Kingdon, 30-Jan-2023.) |
⊢ 𝑆 Struct 𝑋 & ⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ) & ⊢ {〈(𝐸‘ndx), 𝐶〉} ⊆ 𝑆 ⇒ ⊢ (𝐶 ∈ 𝑉 → 𝐶 = (𝐸‘𝑆)) | ||
Theorem | strslfv3 12448 | Variant on strslfv 12447 for large structures. (Contributed by Mario Carneiro, 10-Jan-2017.) (Revised by Jim Kingdon, 30-Jan-2023.) |
⊢ (𝜑 → 𝑈 = 𝑆) & ⊢ 𝑆 Struct 𝑋 & ⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ) & ⊢ {〈(𝐸‘ndx), 𝐶〉} ⊆ 𝑆 & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ 𝐴 = (𝐸‘𝑈) ⇒ ⊢ (𝜑 → 𝐴 = 𝐶) | ||
Theorem | strslssd 12449 | Deduction version of strslss 12450. (Contributed by Mario Carneiro, 15-Nov-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) (Revised by Jim Kingdon, 31-Jan-2023.) |
⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ) & ⊢ (𝜑 → 𝑇 ∈ 𝑉) & ⊢ (𝜑 → Fun 𝑇) & ⊢ (𝜑 → 𝑆 ⊆ 𝑇) & ⊢ (𝜑 → 〈(𝐸‘ndx), 𝐶〉 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝐸‘𝑇) = (𝐸‘𝑆)) | ||
Theorem | strslss 12450 | Propagate component extraction to a structure 𝑇 from a subset structure 𝑆. (Contributed by Mario Carneiro, 11-Oct-2013.) (Revised by Jim Kingdon, 31-Jan-2023.) |
⊢ 𝑇 ∈ V & ⊢ Fun 𝑇 & ⊢ 𝑆 ⊆ 𝑇 & ⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ) & ⊢ 〈(𝐸‘ndx), 𝐶〉 ∈ 𝑆 ⇒ ⊢ (𝐸‘𝑇) = (𝐸‘𝑆) | ||
Theorem | strsl0 12451 | All components of the empty set are empty sets. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 31-Jan-2023.) |
⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ) ⇒ ⊢ ∅ = (𝐸‘∅) | ||
Theorem | base0 12452 | The base set of the empty structure. (Contributed by David A. Wheeler, 7-Jul-2016.) |
⊢ ∅ = (Base‘∅) | ||
Theorem | setsslid 12453 | Value of the structure replacement function at a replaced index. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon, 24-Jan-2023.) |
⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ) ⇒ ⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → 𝐶 = (𝐸‘(𝑊 sSet 〈(𝐸‘ndx), 𝐶〉))) | ||
Theorem | setsslnid 12454 | Value of the structure replacement function at an untouched index. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon, 24-Jan-2023.) |
⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ) & ⊢ (𝐸‘ndx) ≠ 𝐷 & ⊢ 𝐷 ∈ ℕ ⇒ ⊢ ((𝑊 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉) → (𝐸‘𝑊) = (𝐸‘(𝑊 sSet 〈𝐷, 𝐶〉))) | ||
Theorem | baseval 12455 | 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 12456 | Utility theorem: index-independent form of df-base 12409. (Contributed by NM, 20-Oct-2012.) |
⊢ Base = Slot (Base‘ndx) | ||
Theorem | basendx 12457 |
Index value of the base set extractor.
Use of this theorem is discouraged since the particular value 1 for the index is an implementation detail. It is generally sufficient to work with (Base‘ndx) and use theorems such as baseid 12456 and basendxnn 12458. The main circumstance in which it is necessary to look at indices directly is when showing that a set of indices are disjoint, in proofs such as lmodstrd 12538. Although we have a few theorems such as basendxnplusgndx 12511, we do not intend to add such theorems for every pair of indices (which would be quadradically many in the number of indices). (New usage is discouraged.) (Contributed by Mario Carneiro, 2-Aug-2013.) |
⊢ (Base‘ndx) = 1 | ||
Theorem | basendxnn 12458 | 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.) |
⊢ (Base‘ndx) ∈ ℕ | ||
Theorem | baseslid 12459 | The base set extractor is a slot. (Contributed by Jim Kingdon, 31-Jan-2023.) |
⊢ (Base = Slot (Base‘ndx) ∧ (Base‘ndx) ∈ ℕ) | ||
Theorem | basfn 12460 | The base set extractor is a function on V. (Contributed by Stefan O'Rear, 8-Jul-2015.) |
⊢ Base Fn V | ||
Theorem | basmex 12461 | A structure whose base is inhabited is a set. (Contributed by Jim Kingdon, 18-Nov-2024.) |
⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝐵 → 𝐺 ∈ V) | ||
Theorem | basmexd 12462 | A structure whose base is inhabited is a set. (Contributed by Jim Kingdon, 28-Nov-2024.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐺)) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝐺 ∈ V) | ||
Theorem | reldmress 12463 | The structure restriction is a proper operator, so it can be used with ovprc1 5886. (Contributed by Stefan O'Rear, 29-Nov-2014.) |
⊢ Rel dom ↾s | ||
Theorem | ressid2 12464 | General behavior of trivial restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.) (Revised by Jim Kingdon, 26-Jan-2023.) |
⊢ 𝑅 = (𝑊 ↾s 𝐴) & ⊢ 𝐵 = (Base‘𝑊) ⇒ ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = 𝑊) | ||
Theorem | ressval2 12465 | Value of nontrivial structure restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.) |
⊢ 𝑅 = (𝑊 ↾s 𝐴) & ⊢ 𝐵 = (Base‘𝑊) ⇒ ⊢ ((¬ 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = (𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ 𝐵)〉)) | ||
Theorem | ressid 12466 | Behavior of trivial restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.) |
⊢ 𝐵 = (Base‘𝑊) ⇒ ⊢ (𝑊 ∈ 𝑋 → (𝑊 ↾s 𝐵) = 𝑊) | ||
Syntax | cplusg 12467 | Extend class notation with group (addition) operation. |
class +g | ||
Syntax | cmulr 12468 | Extend class notation with ring multiplication. |
class .r | ||
Syntax | cstv 12469 | Extend class notation with involution. |
class *𝑟 | ||
Syntax | csca 12470 | Extend class notation with scalar field. |
class Scalar | ||
Syntax | cvsca 12471 | Extend class notation with scalar product. |
class ·𝑠 | ||
Syntax | cip 12472 | Extend class notation with Hermitian form (inner product). |
class ·𝑖 | ||
Syntax | cts 12473 | Extend class notation with the topology component of a topological space. |
class TopSet | ||
Syntax | cple 12474 | Extend class notation with "less than or equal to" for posets. |
class le | ||
Syntax | coc 12475 | Extend class notation with the class of orthocomplementation extractors. |
class oc | ||
Syntax | cds 12476 | Extend class notation with the metric space distance function. |
class dist | ||
Syntax | cunif 12477 | Extend class notation with the uniform structure. |
class UnifSet | ||
Syntax | chom 12478 | Extend class notation with the hom-set structure. |
class Hom | ||
Syntax | cco 12479 | Extend class notation with the composition operation. |
class comp | ||
Definition | df-plusg 12480 | Define group operation. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) |
⊢ +g = Slot 2 | ||
Definition | df-mulr 12481 | Define ring multiplication. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) |
⊢ .r = Slot 3 | ||
Definition | df-starv 12482 | Define the involution function of a *-ring. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) |
⊢ *𝑟 = Slot 4 | ||
Definition | df-sca 12483 | Define scalar field component of a vector space 𝑣. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) |
⊢ Scalar = Slot 5 | ||
Definition | df-vsca 12484 | Define scalar product. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) |
⊢ ·𝑠 = Slot 6 | ||
Definition | df-ip 12485 | Define Hermitian form (inner product). (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) |
⊢ ·𝑖 = Slot 8 | ||
Definition | df-tset 12486 | Define the topology component of a topological space (structure). (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) |
⊢ TopSet = Slot 9 | ||
Definition | df-ple 12487 | Define "less than or equal to" ordering extractor for posets and related structures. We use ;10 for the index to avoid conflict with 1 through 9 used for other purposes. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) (Revised by AV, 9-Sep-2021.) |
⊢ le = Slot ;10 | ||
Definition | df-ocomp 12488 | Define the orthocomplementation extractor for posets and related structures. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) |
⊢ oc = Slot ;11 | ||
Definition | df-ds 12489 | Define the distance function component of a metric space (structure). (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) |
⊢ dist = Slot ;12 | ||
Definition | df-unif 12490 | Define the uniform structure component of a uniform space. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ UnifSet = Slot ;13 | ||
Definition | df-hom 12491 | Define the hom-set component of a category. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ Hom = Slot ;14 | ||
Definition | df-cco 12492 | Define the composition operation of a category. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ comp = Slot ;15 | ||
Theorem | strleund 12493 | Combine two structures into one. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 27-Jan-2023.) |
⊢ (𝜑 → 𝐹 Struct 〈𝐴, 𝐵〉) & ⊢ (𝜑 → 𝐺 Struct 〈𝐶, 𝐷〉) & ⊢ (𝜑 → 𝐵 < 𝐶) ⇒ ⊢ (𝜑 → (𝐹 ∪ 𝐺) Struct 〈𝐴, 𝐷〉) | ||
Theorem | strleun 12494 | Combine two structures into one. (Contributed by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝐹 Struct 〈𝐴, 𝐵〉 & ⊢ 𝐺 Struct 〈𝐶, 𝐷〉 & ⊢ 𝐵 < 𝐶 ⇒ ⊢ (𝐹 ∪ 𝐺) Struct 〈𝐴, 𝐷〉 | ||
Theorem | strle1g 12495 | Make a structure from a singleton. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 27-Jan-2023.) |
⊢ 𝐼 ∈ ℕ & ⊢ 𝐴 = 𝐼 ⇒ ⊢ (𝑋 ∈ 𝑉 → {〈𝐴, 𝑋〉} Struct 〈𝐼, 𝐼〉) | ||
Theorem | strle2g 12496 | Make a structure from a pair. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 27-Jan-2023.) |
⊢ 𝐼 ∈ ℕ & ⊢ 𝐴 = 𝐼 & ⊢ 𝐼 < 𝐽 & ⊢ 𝐽 ∈ ℕ & ⊢ 𝐵 = 𝐽 ⇒ ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → {〈𝐴, 𝑋〉, 〈𝐵, 𝑌〉} Struct 〈𝐼, 𝐽〉) | ||
Theorem | strle3g 12497 | Make a structure from a triple. (Contributed by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝐼 ∈ ℕ & ⊢ 𝐴 = 𝐼 & ⊢ 𝐼 < 𝐽 & ⊢ 𝐽 ∈ ℕ & ⊢ 𝐵 = 𝐽 & ⊢ 𝐽 < 𝐾 & ⊢ 𝐾 ∈ ℕ & ⊢ 𝐶 = 𝐾 ⇒ ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑃) → {〈𝐴, 𝑋〉, 〈𝐵, 𝑌〉, 〈𝐶, 𝑍〉} Struct 〈𝐼, 𝐾〉) | ||
Theorem | plusgndx 12498 | Index value of the df-plusg 12480 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ (+g‘ndx) = 2 | ||
Theorem | plusgid 12499 | Utility theorem: index-independent form of df-plusg 12480. (Contributed by NM, 20-Oct-2012.) |
⊢ +g = Slot (+g‘ndx) | ||
Theorem | plusgslid 12500 | Slot property of +g. (Contributed by Jim Kingdon, 3-Feb-2023.) |
⊢ (+g = Slot (+g‘ndx) ∧ (+g‘ndx) ∈ ℕ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |