![]() |
Intuitionistic Logic Explorer Theorem List (p. 126 of 152) | < 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 | ||
Theorem | ndxslid 12501 | 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 12521. (Contributed by Jim Kingdon, 29-Jan-2023.) |
⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ) | ||
Theorem | slotslfn 12502 | 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 12503 | Existence of slot value. A corollary of slotslfn 12502. (Contributed by Jim Kingdon, 12-Feb-2023.) |
⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝐸‘𝐴) ∈ V) | ||
Theorem | strndxid 12504 | 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 12505 | The structure override operator is a proper operator. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
⊢ Rel dom sSet | ||
Theorem | setsvalg 12506 | Value of the structure replacement function. (Contributed by Mario Carneiro, 30-Apr-2015.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑆 sSet 𝐴) = ((𝑆 ↾ (V ∖ dom {𝐴})) ∪ {𝐴})) | ||
Theorem | setsvala 12507 | Value of the structure replacement function. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon, 20-Jan-2023.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑊) → (𝑆 sSet 〈𝐴, 𝐵〉) = ((𝑆 ↾ (V ∖ {𝐴})) ∪ {〈𝐴, 𝐵〉})) | ||
Theorem | setsex 12508 | Applying the structure replacement function yields a set. (Contributed by Jim Kingdon, 22-Jan-2023.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑊) → (𝑆 sSet 〈𝐴, 𝐵〉) ∈ V) | ||
Theorem | strsetsid 12509 | 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 12510 | The value of the structure replacement function for its first argument is its second argument. (Contributed by SO, 12-Jul-2018.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ∧ 𝑌 ∈ 𝑈) → ((𝐹 sSet 〈𝑋, 𝑌〉)‘𝑋) = 𝑌) | ||
Theorem | setsfun 12511 | 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 12512 | 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 12511 is useful for proofs based on isstruct2r 12487 which requires Fun (𝐹 ∖ {∅}) for 𝐹 to be an extensible structure. (Contributed by AV, 7-Jun-2021.) |
⊢ (((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅})) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → Fun ((𝐺 sSet 〈𝐼, 𝐸〉) ∖ {∅})) | ||
Theorem | setsn0fun 12513 | 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 12514 | 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 12515 | 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 12516 | Different components can be set in any order. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋)) → ((𝑆 sSet 〈𝐴, 𝐶〉) sSet 〈𝐵, 𝐷〉) = ((𝑆 sSet 〈𝐵, 𝐷〉) sSet 〈𝐴, 𝐶〉)) | ||
Theorem | setscomd 12517 | Different components can be set in any order. (Contributed by Jim Kingdon, 20-Feb-2025.) |
⊢ (𝜑 → 𝐴 ∈ 𝑌) & ⊢ (𝜑 → 𝐵 ∈ 𝑍) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) & ⊢ (𝜑 → 𝐷 ∈ 𝑋) ⇒ ⊢ (𝜑 → ((𝑆 sSet 〈𝐴, 𝐶〉) sSet 〈𝐵, 𝐷〉) = ((𝑆 sSet 〈𝐵, 𝐷〉) sSet 〈𝐴, 𝐶〉)) | ||
Theorem | strslfvd 12518 | Deduction version of strslfv 12521. (Contributed by Mario Carneiro, 15-Nov-2014.) (Revised by Jim Kingdon, 30-Jan-2023.) |
⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → Fun 𝑆) & ⊢ (𝜑 → 〈(𝐸‘ndx), 𝐶〉 ∈ 𝑆) ⇒ ⊢ (𝜑 → 𝐶 = (𝐸‘𝑆)) | ||
Theorem | strslfv2d 12519 | Deduction version of strslfv 12521. (Contributed by Mario Carneiro, 30-Apr-2015.) (Revised by Jim Kingdon, 30-Jan-2023.) |
⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → Fun ◡◡𝑆) & ⊢ (𝜑 → 〈(𝐸‘ndx), 𝐶〉 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝐶 = (𝐸‘𝑆)) | ||
Theorem | strslfv2 12520 | A variation on strslfv 12521 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 12521 | Extract a structure component 𝐶 (such as the base set) from a structure 𝑆 with a component extractor 𝐸 (such as the base set extractor df-base 12482). By virtue of ndxslid 12501, 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 12522 | Variant on strslfv 12521 for large structures. (Contributed by Mario Carneiro, 10-Jan-2017.) (Revised by Jim Kingdon, 30-Jan-2023.) |
⊢ (𝜑 → 𝑈 = 𝑆) & ⊢ 𝑆 Struct 𝑋 & ⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ) & ⊢ {〈(𝐸‘ndx), 𝐶〉} ⊆ 𝑆 & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ 𝐴 = (𝐸‘𝑈) ⇒ ⊢ (𝜑 → 𝐴 = 𝐶) | ||
Theorem | strslssd 12523 | Deduction version of strslss 12524. (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 12524 | 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 12525 | 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 12526 | The base set of the empty structure. (Contributed by David A. Wheeler, 7-Jul-2016.) |
⊢ ∅ = (Base‘∅) | ||
Theorem | setsslid 12527 | 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 12528 | 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 12529 | 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 12530 | Utility theorem: index-independent form of df-base 12482. (Contributed by NM, 20-Oct-2012.) |
⊢ Base = Slot (Base‘ndx) | ||
Theorem | basendx 12531 |
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 12530 and basendxnn 12532. 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 12637. Although we have a few theorems such as basendxnplusgndx 12598, 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 12532 | 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 12533 | The base set extractor is a slot. (Contributed by Jim Kingdon, 31-Jan-2023.) |
⊢ (Base = Slot (Base‘ndx) ∧ (Base‘ndx) ∈ ℕ) | ||
Theorem | basfn 12534 | The base set extractor is a function on V. (Contributed by Stefan O'Rear, 8-Jul-2015.) |
⊢ Base Fn V | ||
Theorem | basmex 12535 | A structure whose base is inhabited is a set. (Contributed by Jim Kingdon, 18-Nov-2024.) |
⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝐵 → 𝐺 ∈ V) | ||
Theorem | basmexd 12536 | A structure whose base is inhabited is a set. (Contributed by Jim Kingdon, 28-Nov-2024.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐺)) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝐺 ∈ V) | ||
Theorem | reldmress 12537 | The structure restriction is a proper operator, so it can be used with ovprc1 5924. (Contributed by Stefan O'Rear, 29-Nov-2014.) |
⊢ Rel dom ↾s | ||
Theorem | ressvalsets 12538 | Value of structure restriction. (Contributed by Jim Kingdon, 16-Jan-2025.) |
⊢ ((𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → (𝑊 ↾s 𝐴) = (𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ (Base‘𝑊))〉)) | ||
Theorem | ressex 12539 | Existence of structure restriction. (Contributed by Jim Kingdon, 16-Jan-2025.) |
⊢ ((𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → (𝑊 ↾s 𝐴) ∈ V) | ||
Theorem | ressval2 12540 | Value of nontrivial structure restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.) |
⊢ 𝑅 = (𝑊 ↾s 𝐴) & ⊢ 𝐵 = (Base‘𝑊) ⇒ ⊢ ((¬ 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌) → 𝑅 = (𝑊 sSet 〈(Base‘ndx), (𝐴 ∩ 𝐵)〉)) | ||
Theorem | ressbasd 12541 | 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 | ressbas2d 12542 | Base set of a structure restriction. (Contributed by Mario Carneiro, 2-Dec-2014.) |
⊢ (𝜑 → 𝑅 = (𝑊 ↾s 𝐴)) & ⊢ (𝜑 → 𝐵 = (Base‘𝑊)) & ⊢ (𝜑 → 𝑊 ∈ 𝑋) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → 𝐴 = (Base‘𝑅)) | ||
Theorem | ressbasssd 12543 | 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 | ressbasid 12544 | The trivial structure restriction leaves the base set unchanged. (Contributed by Jim Kingdon, 29-Apr-2025.) |
⊢ 𝐵 = (Base‘𝑊) ⇒ ⊢ (𝑊 ∈ 𝑉 → (Base‘(𝑊 ↾s 𝐵)) = 𝐵) | ||
Theorem | strressid 12545 | Behavior of trivial restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.) (Revised by Jim Kingdon, 17-Jan-2025.) |
⊢ (𝜑 → 𝐵 = (Base‘𝑊)) & ⊢ (𝜑 → 𝑊 Struct 〈𝑀, 𝑁〉) & ⊢ (𝜑 → Fun 𝑊) & ⊢ (𝜑 → (Base‘ndx) ∈ dom 𝑊) ⇒ ⊢ (𝜑 → (𝑊 ↾s 𝐵) = 𝑊) | ||
Theorem | ressval3d 12546 | Value of structure restriction, deduction version. (Contributed by AV, 14-Mar-2020.) (Revised by Jim Kingdon, 17-Jan-2025.) |
⊢ 𝑅 = (𝑆 ↾s 𝐴) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝐸 = (Base‘ndx) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → Fun 𝑆) & ⊢ (𝜑 → 𝐸 ∈ dom 𝑆) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → 𝑅 = (𝑆 sSet 〈𝐸, 𝐴〉)) | ||
Theorem | resseqnbasd 12547 | 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) ∈ ℕ) & ⊢ (𝐸‘ndx) ≠ (Base‘ndx) & ⊢ (𝜑 → 𝑊 ∈ 𝑋) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐶 = (𝐸‘𝑅)) | ||
Theorem | ressinbasd 12548 | 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 | ressressg 12549 | Restriction composition law. (Contributed by Stefan O'Rear, 29-Nov-2014.) (Proof shortened by Mario Carneiro, 2-Dec-2014.) |
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑊 ∈ 𝑍) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s (𝐴 ∩ 𝐵))) | ||
Theorem | ressabsg 12550 | Restriction absorption law. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ 𝑌) → ((𝑊 ↾s 𝐴) ↾s 𝐵) = (𝑊 ↾s 𝐵)) | ||
Syntax | cplusg 12551 | Extend class notation with group (addition) operation. |
class +g | ||
Syntax | cmulr 12552 | Extend class notation with ring multiplication. |
class .r | ||
Syntax | cstv 12553 | Extend class notation with involution. |
class *𝑟 | ||
Syntax | csca 12554 | Extend class notation with scalar field. |
class Scalar | ||
Syntax | cvsca 12555 | Extend class notation with scalar product. |
class ·𝑠 | ||
Syntax | cip 12556 | Extend class notation with Hermitian form (inner product). |
class ·𝑖 | ||
Syntax | cts 12557 | Extend class notation with the topology component of a topological space. |
class TopSet | ||
Syntax | cple 12558 | Extend class notation with "less than or equal to" for posets. |
class le | ||
Syntax | coc 12559 | Extend class notation with the class of orthocomplementation extractors. |
class oc | ||
Syntax | cds 12560 | Extend class notation with the metric space distance function. |
class dist | ||
Syntax | cunif 12561 | Extend class notation with the uniform structure. |
class UnifSet | ||
Syntax | chom 12562 | Extend class notation with the hom-set structure. |
class Hom | ||
Syntax | cco 12563 | Extend class notation with the composition operation. |
class comp | ||
Definition | df-plusg 12564 | Define group operation. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) |
⊢ +g = Slot 2 | ||
Definition | df-mulr 12565 | Define ring multiplication. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) |
⊢ .r = Slot 3 | ||
Definition | df-starv 12566 | 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 12567 | 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 12568 | Define scalar product. (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) |
⊢ ·𝑠 = Slot 6 | ||
Definition | df-ip 12569 | Define Hermitian form (inner product). (Contributed by NM, 4-Sep-2011.) (Revised by Mario Carneiro, 14-Aug-2015.) |
⊢ ·𝑖 = Slot 8 | ||
Definition | df-tset 12570 | 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 12571 | 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 12572 | 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 12573 | 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 12574 | Define the uniform structure component of a uniform space. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ UnifSet = Slot ;13 | ||
Definition | df-hom 12575 | Define the hom-set component of a category. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ Hom = Slot ;14 | ||
Definition | df-cco 12576 | Define the composition operation of a category. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ comp = Slot ;15 | ||
Theorem | strleund 12577 | Combine two structures into one. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 27-Jan-2023.) |
⊢ (𝜑 → 𝐹 Struct 〈𝐴, 𝐵〉) & ⊢ (𝜑 → 𝐺 Struct 〈𝐶, 𝐷〉) & ⊢ (𝜑 → 𝐵 < 𝐶) ⇒ ⊢ (𝜑 → (𝐹 ∪ 𝐺) Struct 〈𝐴, 𝐷〉) | ||
Theorem | strleun 12578 | Combine two structures into one. (Contributed by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝐹 Struct 〈𝐴, 𝐵〉 & ⊢ 𝐺 Struct 〈𝐶, 𝐷〉 & ⊢ 𝐵 < 𝐶 ⇒ ⊢ (𝐹 ∪ 𝐺) Struct 〈𝐴, 𝐷〉 | ||
Theorem | strext 12579 | Extending the upper range of a structure. This works because when we say that a structure has components in 𝐴...𝐶 we are not saying that every slot in that range is present, just that all the slots that are present are within that range. (Contributed by Jim Kingdon, 26-Feb-2025.) |
⊢ (𝜑 → 𝐹 Struct 〈𝐴, 𝐵〉) & ⊢ (𝜑 → 𝐶 ∈ (ℤ≥‘𝐵)) ⇒ ⊢ (𝜑 → 𝐹 Struct 〈𝐴, 𝐶〉) | ||
Theorem | strle1g 12580 | Make a structure from a singleton. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 27-Jan-2023.) |
⊢ 𝐼 ∈ ℕ & ⊢ 𝐴 = 𝐼 ⇒ ⊢ (𝑋 ∈ 𝑉 → {〈𝐴, 𝑋〉} Struct 〈𝐼, 𝐼〉) | ||
Theorem | strle2g 12581 | Make a structure from a pair. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 27-Jan-2023.) |
⊢ 𝐼 ∈ ℕ & ⊢ 𝐴 = 𝐼 & ⊢ 𝐼 < 𝐽 & ⊢ 𝐽 ∈ ℕ & ⊢ 𝐵 = 𝐽 ⇒ ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → {〈𝐴, 𝑋〉, 〈𝐵, 𝑌〉} Struct 〈𝐼, 𝐽〉) | ||
Theorem | strle3g 12582 | Make a structure from a triple. (Contributed by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝐼 ∈ ℕ & ⊢ 𝐴 = 𝐼 & ⊢ 𝐼 < 𝐽 & ⊢ 𝐽 ∈ ℕ & ⊢ 𝐵 = 𝐽 & ⊢ 𝐽 < 𝐾 & ⊢ 𝐾 ∈ ℕ & ⊢ 𝐶 = 𝐾 ⇒ ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑃) → {〈𝐴, 𝑋〉, 〈𝐵, 𝑌〉, 〈𝐶, 𝑍〉} Struct 〈𝐼, 𝐾〉) | ||
Theorem | plusgndx 12583 | Index value of the df-plusg 12564 slot. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ (+g‘ndx) = 2 | ||
Theorem | plusgid 12584 | Utility theorem: index-independent form of df-plusg 12564. (Contributed by NM, 20-Oct-2012.) |
⊢ +g = Slot (+g‘ndx) | ||
Theorem | plusgndxnn 12585 | 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 | plusgslid 12586 | Slot property of +g. (Contributed by Jim Kingdon, 3-Feb-2023.) |
⊢ (+g = Slot (+g‘ndx) ∧ (+g‘ndx) ∈ ℕ) | ||
Theorem | basendxltplusgndx 12587 | 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 | opelstrsl 12588 | The slot of a structure which contains an ordered pair for that slot. (Contributed by Jim Kingdon, 5-Feb-2023.) |
⊢ (𝐸 = Slot (𝐸‘ndx) ∧ (𝐸‘ndx) ∈ ℕ) & ⊢ (𝜑 → 𝑆 Struct 𝑋) & ⊢ (𝜑 → 𝑉 ∈ 𝑌) & ⊢ (𝜑 → 〈(𝐸‘ndx), 𝑉〉 ∈ 𝑆) ⇒ ⊢ (𝜑 → 𝑉 = (𝐸‘𝑆)) | ||
Theorem | opelstrbas 12589 | The base set of a structure with a base set. (Contributed by AV, 10-Nov-2021.) |
⊢ (𝜑 → 𝑆 Struct 𝑋) & ⊢ (𝜑 → 𝑉 ∈ 𝑌) & ⊢ (𝜑 → 〈(Base‘ndx), 𝑉〉 ∈ 𝑆) ⇒ ⊢ (𝜑 → 𝑉 = (Base‘𝑆)) | ||
Theorem | 1strstrg 12590 | A constructed one-slot structure. (Contributed by AV, 27-Mar-2020.) (Revised by Jim Kingdon, 28-Jan-2023.) |
⊢ 𝐺 = {〈(Base‘ndx), 𝐵〉} ⇒ ⊢ (𝐵 ∈ 𝑉 → 𝐺 Struct 〈1, 1〉) | ||
Theorem | 1strbas 12591 | The base set of a constructed one-slot structure. (Contributed by AV, 27-Mar-2020.) |
⊢ 𝐺 = {〈(Base‘ndx), 𝐵〉} ⇒ ⊢ (𝐵 ∈ 𝑉 → 𝐵 = (Base‘𝐺)) | ||
Theorem | 2strstrg 12592 | A constructed two-slot structure. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 28-Jan-2023.) |
⊢ 𝐺 = {〈(Base‘ndx), 𝐵〉, 〈(𝐸‘ndx), + 〉} & ⊢ 𝐸 = Slot 𝑁 & ⊢ 1 < 𝑁 & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → 𝐺 Struct 〈1, 𝑁〉) | ||
Theorem | 2strbasg 12593 | The base set of a constructed two-slot structure. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 28-Jan-2023.) |
⊢ 𝐺 = {〈(Base‘ndx), 𝐵〉, 〈(𝐸‘ndx), + 〉} & ⊢ 𝐸 = Slot 𝑁 & ⊢ 1 < 𝑁 & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → 𝐵 = (Base‘𝐺)) | ||
Theorem | 2stropg 12594 | The other slot of a constructed two-slot structure. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 28-Jan-2023.) |
⊢ 𝐺 = {〈(Base‘ndx), 𝐵〉, 〈(𝐸‘ndx), + 〉} & ⊢ 𝐸 = Slot 𝑁 & ⊢ 1 < 𝑁 & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → + = (𝐸‘𝐺)) | ||
Theorem | 2strstr1g 12595 | A constructed two-slot structure. Version of 2strstrg 12592 not depending on the hard-coded index value of the base set. (Contributed by AV, 22-Sep-2020.) (Revised by Jim Kingdon, 2-Feb-2023.) |
⊢ 𝐺 = {〈(Base‘ndx), 𝐵〉, 〈𝑁, + 〉} & ⊢ (Base‘ndx) < 𝑁 & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → 𝐺 Struct 〈(Base‘ndx), 𝑁〉) | ||
Theorem | 2strbas1g 12596 | The base set of a constructed two-slot structure. Version of 2strbasg 12593 not depending on the hard-coded index value of the base set. (Contributed by AV, 22-Sep-2020.) (Revised by Jim Kingdon, 2-Feb-2023.) |
⊢ 𝐺 = {〈(Base‘ndx), 𝐵〉, 〈𝑁, + 〉} & ⊢ (Base‘ndx) < 𝑁 & ⊢ 𝑁 ∈ ℕ ⇒ ⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → 𝐵 = (Base‘𝐺)) | ||
Theorem | 2strop1g 12597 | The other slot of a constructed two-slot structure. Version of 2stropg 12594 not depending on the hard-coded index value of the base set. (Contributed by AV, 22-Sep-2020.) (Revised by Jim Kingdon, 2-Feb-2023.) |
⊢ 𝐺 = {〈(Base‘ndx), 𝐵〉, 〈𝑁, + 〉} & ⊢ (Base‘ndx) < 𝑁 & ⊢ 𝑁 ∈ ℕ & ⊢ 𝐸 = Slot 𝑁 ⇒ ⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → + = (𝐸‘𝐺)) | ||
Theorem | basendxnplusgndx 12598 | The slot for the base set is not the slot for the group operation in an extensible structure. (Contributed by AV, 14-Nov-2021.) |
⊢ (Base‘ndx) ≠ (+g‘ndx) | ||
Theorem | grpstrg 12599 | A constructed group is a structure on 1...2. (Contributed by Mario Carneiro, 28-Sep-2013.) (Revised by Mario Carneiro, 30-Apr-2015.) |
⊢ 𝐺 = {〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉} ⇒ ⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → 𝐺 Struct 〈1, 2〉) | ||
Theorem | grpbaseg 12600 | The base set of a constructed group. (Contributed by Mario Carneiro, 2-Aug-2013.) (Revised by Mario Carneiro, 30-Apr-2015.) |
⊢ 𝐺 = {〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉} ⇒ ⊢ ((𝐵 ∈ 𝑉 ∧ + ∈ 𝑊) → 𝐵 = (Base‘𝐺)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |