![]() |
Metamath
Proof Explorer Theorem List (p. 79 of 454) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | f1o2ndf1 7801 | The 2nd (second component of an ordered pair) function restricted to a one-to-one function 𝐹 is a one-to-one function from 𝐹 onto the range of 𝐹. (Contributed by Alexander van der Vekens, 4-Feb-2018.) |
⊢ (𝐹:𝐴–1-1→𝐵 → (2nd ↾ 𝐹):𝐹–1-1-onto→ran 𝐹) | ||
Theorem | algrflem 7802 | Lemma for algrf 15907 and related theorems. (Contributed by Mario Carneiro, 28-May-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) |
⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (𝐵(𝐹 ∘ 1st )𝐶) = (𝐹‘𝐵) | ||
Theorem | frxp 7803* | A lexicographical ordering of two well-founded classes. (Contributed by Scott Fenton, 17-Mar-2011.) (Revised by Mario Carneiro, 7-Mar-2013.) (Proof shortened by Wolf Lammen, 4-Oct-2014.) |
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥)𝑆(2nd ‘𝑦))))} ⇒ ⊢ ((𝑅 Fr 𝐴 ∧ 𝑆 Fr 𝐵) → 𝑇 Fr (𝐴 × 𝐵)) | ||
Theorem | xporderlem 7804* | Lemma for lexicographical ordering theorems. (Contributed by Scott Fenton, 16-Mar-2011.) |
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥)𝑆(2nd ‘𝑦))))} ⇒ ⊢ (〈𝑎, 𝑏〉𝑇〈𝑐, 𝑑〉 ↔ (((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)))) | ||
Theorem | poxp 7805* | A lexicographical ordering of two posets. (Contributed by Scott Fenton, 16-Mar-2011.) (Revised by Mario Carneiro, 7-Mar-2013.) |
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥)𝑆(2nd ‘𝑦))))} ⇒ ⊢ ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → 𝑇 Po (𝐴 × 𝐵)) | ||
Theorem | soxp 7806* | A lexicographical ordering of two strictly ordered classes. (Contributed by Scott Fenton, 17-Mar-2011.) (Revised by Mario Carneiro, 7-Mar-2013.) |
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥)𝑆(2nd ‘𝑦))))} ⇒ ⊢ ((𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵) → 𝑇 Or (𝐴 × 𝐵)) | ||
Theorem | wexp 7807* | A lexicographical ordering of two well-ordered classes. (Contributed by Scott Fenton, 17-Mar-2011.) (Revised by Mario Carneiro, 7-Mar-2013.) |
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥)𝑆(2nd ‘𝑦))))} ⇒ ⊢ ((𝑅 We 𝐴 ∧ 𝑆 We 𝐵) → 𝑇 We (𝐴 × 𝐵)) | ||
Theorem | fnwelem 7808* | Lemma for fnwe 7809. (Contributed by Mario Carneiro, 10-Mar-2013.) (Revised by Mario Carneiro, 18-Nov-2014.) |
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑆𝑦)))} & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝑅 We 𝐵) & ⊢ (𝜑 → 𝑆 We 𝐴) & ⊢ (𝜑 → (𝐹 “ 𝑤) ∈ V) & ⊢ 𝑄 = {〈𝑢, 𝑣〉 ∣ ((𝑢 ∈ (𝐵 × 𝐴) ∧ 𝑣 ∈ (𝐵 × 𝐴)) ∧ ((1st ‘𝑢)𝑅(1st ‘𝑣) ∨ ((1st ‘𝑢) = (1st ‘𝑣) ∧ (2nd ‘𝑢)𝑆(2nd ‘𝑣))))} & ⊢ 𝐺 = (𝑧 ∈ 𝐴 ↦ 〈(𝐹‘𝑧), 𝑧〉) ⇒ ⊢ (𝜑 → 𝑇 We 𝐴) | ||
Theorem | fnwe 7809* | A variant on lexicographic order, which sorts first by some function of the base set, and then by a "backup" well-ordering when the function value is equal on both elements. (Contributed by Mario Carneiro, 10-Mar-2013.) (Revised by Mario Carneiro, 18-Nov-2014.) |
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑆𝑦)))} & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝑅 We 𝐵) & ⊢ (𝜑 → 𝑆 We 𝐴) & ⊢ (𝜑 → (𝐹 “ 𝑤) ∈ V) ⇒ ⊢ (𝜑 → 𝑇 We 𝐴) | ||
Theorem | fnse 7810* | Condition for the well-order in fnwe 7809 to be set-like. (Contributed by Mario Carneiro, 25-Jun-2015.) |
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑆𝑦)))} & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝑅 Se 𝐵) & ⊢ (𝜑 → (◡𝐹 “ 𝑤) ∈ V) ⇒ ⊢ (𝜑 → 𝑇 Se 𝐴) | ||
Theorem | fvproj 7811* | Value of a function on ordered pairs with values expressed as ordered pairs. Note that 𝐹 and 𝐺 are the projections of 𝐻 to the first and second coordinate respectively. (Contributed by Thierry Arnoux, 30-Dec-2019.) |
⊢ 𝐻 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑦)〉) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐻‘〈𝑋, 𝑌〉) = 〈(𝐹‘𝑋), (𝐺‘𝑌)〉) | ||
Theorem | fimaproj 7812* | Image of a cartesian product for a function on ordered pairs with values expressed as ordered pairs. Note that 𝐹 and 𝐺 are the projections of 𝐻 to the first and second coordinate respectively. (Contributed by Thierry Arnoux, 30-Dec-2019.) |
⊢ 𝐻 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑦)〉) & ⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺 Fn 𝐵) & ⊢ (𝜑 → 𝑋 ⊆ 𝐴) & ⊢ (𝜑 → 𝑌 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐻 “ (𝑋 × 𝑌)) = ((𝐹 “ 𝑋) × (𝐺 “ 𝑌))) | ||
In this section, the support of functions is defined and corresponding theorems are provided. Since basic properties (see suppval 7815) are based on the Axiom of Union (usage of dmexg 7594), these definition and theorems cannot be provided earlier. Until April 2019, the support of a function was represented by the expression (◡𝑅 “ (V ∖ {𝑍})) (see suppimacnv 7824). The theorems which are based on this representation and which are provided in previous sections could be moved into this section to have all related theorems in one section, although they do not depend on the Axiom of Union. This was possible because they are not used before. The current theorems differ from the original ones by requiring that the classes representing the "function" (or its "domain") and the "zero element" are sets. Actually, this does not cause any problem (until now). | ||
Syntax | csupp 7813 | Extend class definition to include the support of functions. |
class supp | ||
Definition | df-supp 7814* | Define the support of a function against a "zero" value. According to Wikipedia ("Support (mathematics)", 31-Mar-2019, https://en.wikipedia.org/wiki/Support_(mathematics)) "In mathematics, the support of a real-valued function f is the subset of the domain containing those elements which are not mapped to zero." and "The notion of support also extends in a natural way to functions taking values in more general sets than R [the real numbers] and to other objects.". The following definition allows for such extensions, being applicable for any sets (which usually are functions) and any element (even not necessarily from the range of the function) regarded as "zero". (Contributed by AV, 31-Mar-2019.) (Revised by AV, 6-Apr-2019.) |
⊢ supp = (𝑥 ∈ V, 𝑧 ∈ V ↦ {𝑖 ∈ dom 𝑥 ∣ (𝑥 “ {𝑖}) ≠ {𝑧}}) | ||
Theorem | suppval 7815* | The value of the operation constructing the support of a function. (Contributed by AV, 31-Mar-2019.) (Revised by AV, 6-Apr-2019.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑋 supp 𝑍) = {𝑖 ∈ dom 𝑋 ∣ (𝑋 “ {𝑖}) ≠ {𝑍}}) | ||
Theorem | supp0prc 7816 | The support of a class is empty if either the class or the "zero" is a proper class. (Contributed by AV, 28-May-2019.) |
⊢ (¬ (𝑋 ∈ V ∧ 𝑍 ∈ V) → (𝑋 supp 𝑍) = ∅) | ||
Theorem | suppvalbr 7817* | The value of the operation constructing the support of a function expressed by binary relations. (Contributed by AV, 7-Apr-2019.) |
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑅 supp 𝑍) = {𝑥 ∣ (∃𝑦 𝑥𝑅𝑦 ∧ ∃𝑦(𝑥𝑅𝑦 ↔ 𝑦 ≠ 𝑍))}) | ||
Theorem | supp0 7818 | The support of the empty set is the empty set. (Contributed by AV, 12-Apr-2019.) |
⊢ (𝑍 ∈ 𝑊 → (∅ supp 𝑍) = ∅) | ||
Theorem | suppval1 7819* | The value of the operation constructing the support of a function. (Contributed by AV, 6-Apr-2019.) |
⊢ ((Fun 𝑋 ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑋 supp 𝑍) = {𝑖 ∈ dom 𝑋 ∣ (𝑋‘𝑖) ≠ 𝑍}) | ||
Theorem | suppvalfn 7820* | The value of the operation constructing the support of a function with a given domain. (Contributed by Stefan O'Rear, 1-Feb-2015.) (Revised by AV, 22-Apr-2019.) |
⊢ ((𝐹 Fn 𝑋 ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝐹 supp 𝑍) = {𝑖 ∈ 𝑋 ∣ (𝐹‘𝑖) ≠ 𝑍}) | ||
Theorem | elsuppfn 7821 | An element of the support of a function with a given domain. (Contributed by AV, 27-May-2019.) |
⊢ ((𝐹 Fn 𝑋 ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑆 ∈ (𝐹 supp 𝑍) ↔ (𝑆 ∈ 𝑋 ∧ (𝐹‘𝑆) ≠ 𝑍))) | ||
Theorem | cnvimadfsn 7822* | The support of functions "defined" by inverse images expressed by binary relations. (Contributed by AV, 7-Apr-2019.) |
⊢ (◡𝑅 “ (V ∖ {𝑍})) = {𝑥 ∣ ∃𝑦(𝑥𝑅𝑦 ∧ 𝑦 ≠ 𝑍)} | ||
Theorem | suppimacnvss 7823 | The support of functions "defined" by inverse images is a subset of the support defined by df-supp 7814. (Contributed by AV, 7-Apr-2019.) |
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (◡𝑅 “ (V ∖ {𝑍})) ⊆ (𝑅 supp 𝑍)) | ||
Theorem | suppimacnv 7824 | Support sets of functions expressed by inverse images. (Contributed by AV, 31-Mar-2019.) (Revised by AV, 7-Apr-2019.) |
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑅 supp 𝑍) = (◡𝑅 “ (V ∖ {𝑍}))) | ||
Theorem | frnsuppeq 7825 | Two ways of writing the support of a function with known codomain. (Contributed by Stefan O'Rear, 9-Jul-2015.) (Revised by AV, 7-Jul-2019.) |
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝐹:𝐼⟶𝑆 → (𝐹 supp 𝑍) = (◡𝐹 “ (𝑆 ∖ {𝑍})))) | ||
Theorem | suppssdm 7826 | The support of a function is a subset of the function's domain. (Contributed by AV, 30-May-2019.) |
⊢ (𝐹 supp 𝑍) ⊆ dom 𝐹 | ||
Theorem | suppsnop 7827 | The support of a singleton of an ordered pair. (Contributed by AV, 12-Apr-2019.) |
⊢ 𝐹 = {〈𝑋, 𝑌〉} ⇒ ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈) → (𝐹 supp 𝑍) = if(𝑌 = 𝑍, ∅, {𝑋})) | ||
Theorem | snopsuppss 7828 | The support of a singleton containing an ordered pair is a subset of the singleton containing the first element of the ordered pair, i.e. it is empty or the singleton itself. (Contributed by AV, 19-Jul-2019.) |
⊢ ({〈𝑋, 𝑌〉} supp 𝑍) ⊆ {𝑋} | ||
Theorem | fvn0elsupp 7829 | If the function value for a given argument is not empty, the argument belongs to the support of the function with the empty set as zero. (Contributed by AV, 2-Jul-2019.) (Revised by AV, 4-Apr-2020.) |
⊢ (((𝐵 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) ∧ (𝐺 Fn 𝐵 ∧ (𝐺‘𝑋) ≠ ∅)) → 𝑋 ∈ (𝐺 supp ∅)) | ||
Theorem | fvn0elsuppb 7830 | The function value for a given argument is not empty iff the argument belongs to the support of the function with the empty set as zero. (Contributed by AV, 4-Apr-2020.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 Fn 𝐵) → ((𝐺‘𝑋) ≠ ∅ ↔ 𝑋 ∈ (𝐺 supp ∅))) | ||
Theorem | rexsupp 7831* | Existential quantification restricted to a support. (Contributed by Stefan O'Rear, 23-Mar-2015.) (Revised by AV, 27-May-2019.) |
⊢ ((𝐹 Fn 𝑋 ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (∃𝑥 ∈ (𝐹 supp 𝑍)𝜑 ↔ ∃𝑥 ∈ 𝑋 ((𝐹‘𝑥) ≠ 𝑍 ∧ 𝜑))) | ||
Theorem | ressuppss 7832 | The support of the restriction of a function is a subset of the support of the function itself. (Contributed by AV, 22-Apr-2019.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → ((𝐹 ↾ 𝐵) supp 𝑍) ⊆ (𝐹 supp 𝑍)) | ||
Theorem | suppun 7833 | The support of a class/function is a subset of the support of the union of this class/function with another class/function. (Contributed by AV, 4-Jun-2019.) |
⊢ (𝜑 → 𝐺 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐹 supp 𝑍) ⊆ ((𝐹 ∪ 𝐺) supp 𝑍)) | ||
Theorem | ressuppssdif 7834 | The support of the restriction of a function is a subset of the support of the function itself. (Contributed by AV, 22-Apr-2019.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝐹 supp 𝑍) ⊆ (((𝐹 ↾ 𝐵) supp 𝑍) ∪ (dom 𝐹 ∖ 𝐵))) | ||
Theorem | mptsuppdifd 7835* | The support of a function in maps-to notation with a class difference. (Contributed by AV, 28-May-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐹 supp 𝑍) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ (V ∖ {𝑍})}) | ||
Theorem | mptsuppd 7836* | The support of a function in maps-to notation. (Contributed by AV, 10-Apr-2019.) (Revised by AV, 28-May-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝐹 supp 𝑍) = {𝑥 ∈ 𝐴 ∣ 𝐵 ≠ 𝑍}) | ||
Theorem | extmptsuppeq 7837* | The support of an extended function is the same as the original. (Contributed by Mario Carneiro, 25-May-2015.) (Revised by AV, 30-Jun-2019.) |
⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐵 ∖ 𝐴)) → 𝑋 = 𝑍) ⇒ ⊢ (𝜑 → ((𝑛 ∈ 𝐴 ↦ 𝑋) supp 𝑍) = ((𝑛 ∈ 𝐵 ↦ 𝑋) supp 𝑍)) | ||
Theorem | suppfnss 7838* | The support of a function which has the same zero values (in its domain) as another function is a subset of the support of this other function. (Contributed by AV, 30-Apr-2019.) (Proof shortened by AV, 6-Jun-2022.) |
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊)) → (∀𝑥 ∈ 𝐴 ((𝐺‘𝑥) = 𝑍 → (𝐹‘𝑥) = 𝑍) → (𝐹 supp 𝑍) ⊆ (𝐺 supp 𝑍))) | ||
Theorem | funsssuppss 7839 | The support of a function which is a subset of another function is a subset of the support of this other function. (Contributed by AV, 27-Jul-2019.) |
⊢ ((Fun 𝐺 ∧ 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉) → (𝐹 supp 𝑍) ⊆ (𝐺 supp 𝑍)) | ||
Theorem | fnsuppres 7840 | Two ways to express restriction of a support set. (Contributed by Stefan O'Rear, 5-Feb-2015.) (Revised by AV, 28-May-2019.) |
⊢ ((𝐹 Fn (𝐴 ∪ 𝐵) ∧ (𝐹 ∈ 𝑊 ∧ 𝑍 ∈ 𝑉) ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐹 supp 𝑍) ⊆ 𝐴 ↔ (𝐹 ↾ 𝐵) = (𝐵 × {𝑍}))) | ||
Theorem | fnsuppeq0 7841 | The support of a function is empty iff it is identically zero. (Contributed by Stefan O'Rear, 22-Mar-2015.) (Revised by AV, 28-May-2019.) |
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑊 ∧ 𝑍 ∈ 𝑉) → ((𝐹 supp 𝑍) = ∅ ↔ 𝐹 = (𝐴 × {𝑍}))) | ||
Theorem | fczsupp0 7842 | The support of a constant function with value zero is empty. (Contributed by AV, 30-Jun-2019.) |
⊢ ((𝐵 × {𝑍}) supp 𝑍) = ∅ | ||
Theorem | suppss 7843* | Show that the support of a function is contained in a set. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 28-May-2019.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝑊)) → (𝐹‘𝑘) = 𝑍) ⇒ ⊢ (𝜑 → (𝐹 supp 𝑍) ⊆ 𝑊) | ||
Theorem | suppssr 7844 | A function is zero outside its support. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 28-May-2019.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → (𝐹 supp 𝑍) ⊆ 𝑊) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑈) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ (𝐴 ∖ 𝑊)) → (𝐹‘𝑋) = 𝑍) | ||
Theorem | suppssov1 7845* | Formula building theorem for support restrictions: operator with left annihilator. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 28-May-2019.) |
⊢ (𝜑 → ((𝑥 ∈ 𝐷 ↦ 𝐴) supp 𝑌) ⊆ 𝐿) & ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑅) → (𝑌𝑂𝑣) = 𝑍) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐵 ∈ 𝑅) & ⊢ (𝜑 → 𝑌 ∈ 𝑊) ⇒ ⊢ (𝜑 → ((𝑥 ∈ 𝐷 ↦ (𝐴𝑂𝐵)) supp 𝑍) ⊆ 𝐿) | ||
Theorem | suppssof1 7846* | Formula building theorem for support restrictions: vector operation with left annihilator. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 28-May-2019.) |
⊢ (𝜑 → (𝐴 supp 𝑌) ⊆ 𝐿) & ⊢ ((𝜑 ∧ 𝑣 ∈ 𝑅) → (𝑌𝑂𝑣) = 𝑍) & ⊢ (𝜑 → 𝐴:𝐷⟶𝑉) & ⊢ (𝜑 → 𝐵:𝐷⟶𝑅) & ⊢ (𝜑 → 𝐷 ∈ 𝑊) & ⊢ (𝜑 → 𝑌 ∈ 𝑈) ⇒ ⊢ (𝜑 → ((𝐴 ∘f 𝑂𝐵) supp 𝑍) ⊆ 𝐿) | ||
Theorem | suppss2 7847* | Show that the support of a function is contained in a set. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Mario Carneiro, 22-Mar-2015.) (Revised by AV, 28-May-2019.) |
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝑊)) → 𝐵 = 𝑍) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝑘 ∈ 𝐴 ↦ 𝐵) supp 𝑍) ⊆ 𝑊) | ||
Theorem | suppsssn 7848* | Show that the support of a function is a subset of a singleton. (Contributed by AV, 21-Jul-2019.) |
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴 ∧ 𝑘 ≠ 𝑊) → 𝐵 = 𝑍) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝑘 ∈ 𝐴 ↦ 𝐵) supp 𝑍) ⊆ {𝑊}) | ||
Theorem | suppssfv 7849* | Formula building theorem for support restriction, on a function which preserves zero. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 28-May-2019.) |
⊢ (𝜑 → ((𝑥 ∈ 𝐷 ↦ 𝐴) supp 𝑌) ⊆ 𝐿) & ⊢ (𝜑 → (𝐹‘𝑌) = 𝑍) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑈) ⇒ ⊢ (𝜑 → ((𝑥 ∈ 𝐷 ↦ (𝐹‘𝐴)) supp 𝑍) ⊆ 𝐿) | ||
Theorem | suppofssd 7850 | Condition for the support of a function operation to be a subset of the union of the supports of the left and right function terms. (Contributed by Steven Nguyen, 28-Aug-2023.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐴⟶𝐵) & ⊢ (𝜑 → (𝑍𝑋𝑍) = 𝑍) ⇒ ⊢ (𝜑 → ((𝐹 ∘f 𝑋𝐺) supp 𝑍) ⊆ ((𝐹 supp 𝑍) ∪ (𝐺 supp 𝑍))) | ||
Theorem | suppofss1d 7851* | Condition for the support of a function operation to be a subset of the support of the left function term. (Contributed by Thierry Arnoux, 21-Jun-2019.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐴⟶𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑍𝑋𝑥) = 𝑍) ⇒ ⊢ (𝜑 → ((𝐹 ∘f 𝑋𝐺) supp 𝑍) ⊆ (𝐹 supp 𝑍)) | ||
Theorem | suppofss2d 7852* | Condition for the support of a function operation to be a subset of the support of the right function term. (Contributed by Thierry Arnoux, 21-Jun-2019.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐴⟶𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥𝑋𝑍) = 𝑍) ⇒ ⊢ (𝜑 → ((𝐹 ∘f 𝑋𝐺) supp 𝑍) ⊆ (𝐺 supp 𝑍)) | ||
Theorem | suppco 7853 | The support of the composition of two functions is the inverse image by the inner function of the support of the outer function. (Contributed by AV, 30-May-2019.) Extract this statement from the proof of supp0cosupp0 7855. (Revised by SN, 15-Sep-2023.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → ((𝐹 ∘ 𝐺) supp 𝑍) = (◡𝐺 “ (𝐹 supp 𝑍))) | ||
Theorem | suppcoss 7854 | The support of the composition of two functions is a subset of the support of the inner function if the outer function preserves zero. Compare suppssfv 7849, which has a sethood condition on 𝐴 instead of 𝐵. (Contributed by SN, 25-May-2024.) |
⊢ (𝜑 → 𝐹 Fn 𝐴) & ⊢ (𝜑 → 𝐺:𝐵⟶𝐴) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → (𝐹‘𝑌) = 𝑍) ⇒ ⊢ (𝜑 → ((𝐹 ∘ 𝐺) supp 𝑍) ⊆ (𝐺 supp 𝑌)) | ||
Theorem | supp0cosupp0 7855 | The support of the composition of two functions is empty if the support of the outer function is empty. (Contributed by AV, 30-May-2019.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → ((𝐹 supp 𝑍) = ∅ → ((𝐹 ∘ 𝐺) supp 𝑍) = ∅)) | ||
Theorem | supp0cosupp0OLD 7856 | Obsolete version of supp0cosupp0 7855 as of 15-Sep-2023. The support of the composition of two functions is empty if the support of the outer function is empty. (Contributed by AV, 30-May-2019.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → ((𝐹 supp 𝑍) = ∅ → ((𝐹 ∘ 𝐺) supp 𝑍) = ∅)) | ||
Theorem | imacosupp 7857 | The image of the support of the composition of two functions is the support of the outer function. (Contributed by AV, 30-May-2019.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → ((Fun 𝐺 ∧ (𝐹 supp 𝑍) ⊆ ran 𝐺) → (𝐺 “ ((𝐹 ∘ 𝐺) supp 𝑍)) = (𝐹 supp 𝑍))) | ||
Theorem | imacosuppOLD 7858 | Obsolete version of imacosupp 7857 as of 15-Sep-2023. The image of the support of the composition of two functions is the support of the outer function. (Contributed by AV, 30-May-2019.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → ((Fun 𝐺 ∧ (𝐹 supp 𝑍) ⊆ ran 𝐺) → (𝐺 “ ((𝐹 ∘ 𝐺) supp 𝑍)) = (𝐹 supp 𝑍))) | ||
The following theorems are about maps-to operations (see df-mpo 7140) where the domain of the second argument depends on the domain of the first argument, especially when the first argument is a pair and the base set of the second argument is the first component of the first argument, in short "x-maps-to operations". For labels, the abbreviations "mpox" are used (since "x" usually denotes the first argument). This is in line with the currently used conventions for such cases (see cbvmpox 7226, ovmpox 7282 and fmpox 7747). If the first argument is an ordered pair, as in the following, the abbreviation is extended to "mpoxop", and the maps-to operations are called "x-op maps-to operations" for short. | ||
Theorem | opeliunxp2f 7859* | Membership in a union of Cartesian products, using bound-variable hypothesis for 𝐸 instead of distinct variable conditions as in opeliunxp2 5673. (Contributed by AV, 25-Oct-2020.) |
⊢ Ⅎ𝑥𝐸 & ⊢ (𝑥 = 𝐶 → 𝐵 = 𝐸) ⇒ ⊢ (〈𝐶, 𝐷〉 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸)) | ||
Theorem | mpoxeldm 7860* | If there is an element of the value of an operation given by a maps-to rule, then the first argument is an element of the first component of the domain and the second argument is an element of the second component of the domain depending on the first argument. (Contributed by AV, 25-Oct-2020.) |
⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) ⇒ ⊢ (𝑁 ∈ (𝑋𝐹𝑌) → (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ ⦋𝑋 / 𝑥⦌𝐷)) | ||
Theorem | mpoxneldm 7861* | If the first argument of an operation given by a maps-to rule is not an element of the first component of the domain or the second argument is not an element of the second component of the domain depending on the first argument, then the value of the operation is the empty set. (Contributed by AV, 25-Oct-2020.) |
⊢ 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅) ⇒ ⊢ ((𝑋 ∉ 𝐶 ∨ 𝑌 ∉ ⦋𝑋 / 𝑥⦌𝐷) → (𝑋𝐹𝑌) = ∅) | ||
Theorem | mpoxopn0yelv 7862* | If there is an element of the value of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument, then the second argument is an element of the first component of the first argument. (Contributed by Alexander van der Vekens, 10-Oct-2017.) |
⊢ 𝐹 = (𝑥 ∈ V, 𝑦 ∈ (1st ‘𝑥) ↦ 𝐶) ⇒ ⊢ ((𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) → (𝑁 ∈ (〈𝑉, 𝑊〉𝐹𝐾) → 𝐾 ∈ 𝑉)) | ||
Theorem | mpoxopynvov0g 7863* | If the second argument of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument is not element of the first component of the first argument, then the value of the operation is the empty set. (Contributed by Alexander van der Vekens, 10-Oct-2017.) |
⊢ 𝐹 = (𝑥 ∈ V, 𝑦 ∈ (1st ‘𝑥) ↦ 𝐶) ⇒ ⊢ (((𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) ∧ 𝐾 ∉ 𝑉) → (〈𝑉, 𝑊〉𝐹𝐾) = ∅) | ||
Theorem | mpoxopxnop0 7864* | If the first argument of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument, is not an ordered pair, then the value of the operation is the empty set. (Contributed by Alexander van der Vekens, 10-Oct-2017.) |
⊢ 𝐹 = (𝑥 ∈ V, 𝑦 ∈ (1st ‘𝑥) ↦ 𝐶) ⇒ ⊢ (¬ 𝑉 ∈ (V × V) → (𝑉𝐹𝐾) = ∅) | ||
Theorem | mpoxopx0ov0 7865* | If the first argument of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument, is the empty set, then the value of the operation is the empty set. (Contributed by Alexander van der Vekens, 10-Oct-2017.) |
⊢ 𝐹 = (𝑥 ∈ V, 𝑦 ∈ (1st ‘𝑥) ↦ 𝐶) ⇒ ⊢ (∅𝐹𝐾) = ∅ | ||
Theorem | mpoxopxprcov0 7866* | If the components of the first argument of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument, are not sets, then the value of the operation is the empty set. (Contributed by Alexander van der Vekens, 10-Oct-2017.) |
⊢ 𝐹 = (𝑥 ∈ V, 𝑦 ∈ (1st ‘𝑥) ↦ 𝐶) ⇒ ⊢ (¬ (𝑉 ∈ V ∧ 𝑊 ∈ V) → (〈𝑉, 𝑊〉𝐹𝐾) = ∅) | ||
Theorem | mpoxopynvov0 7867* | If the second argument of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument is not element of the first component of the first argument, then the value of the operation is the empty set. (Contributed by Alexander van der Vekens, 10-Oct-2017.) |
⊢ 𝐹 = (𝑥 ∈ V, 𝑦 ∈ (1st ‘𝑥) ↦ 𝐶) ⇒ ⊢ (𝐾 ∉ 𝑉 → (〈𝑉, 𝑊〉𝐹𝐾) = ∅) | ||
Theorem | mpoxopoveq 7868* | Value of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument. (Contributed by Alexander van der Vekens, 11-Oct-2017.) |
⊢ 𝐹 = (𝑥 ∈ V, 𝑦 ∈ (1st ‘𝑥) ↦ {𝑛 ∈ (1st ‘𝑥) ∣ 𝜑}) ⇒ ⊢ (((𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) ∧ 𝐾 ∈ 𝑉) → (〈𝑉, 𝑊〉𝐹𝐾) = {𝑛 ∈ 𝑉 ∣ [〈𝑉, 𝑊〉 / 𝑥][𝐾 / 𝑦]𝜑}) | ||
Theorem | mpoxopovel 7869* | Element of the value of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument. (Contributed by Alexander van der Vekens and Mario Carneiro, 10-Oct-2017.) |
⊢ 𝐹 = (𝑥 ∈ V, 𝑦 ∈ (1st ‘𝑥) ↦ {𝑛 ∈ (1st ‘𝑥) ∣ 𝜑}) ⇒ ⊢ ((𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) → (𝑁 ∈ (〈𝑉, 𝑊〉𝐹𝐾) ↔ (𝐾 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ∧ [〈𝑉, 𝑊〉 / 𝑥][𝐾 / 𝑦][𝑁 / 𝑛]𝜑))) | ||
Theorem | mpoxopoveqd 7870* | Value of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument, deduction version. (Contributed by Alexander van der Vekens, 11-Oct-2017.) |
⊢ 𝐹 = (𝑥 ∈ V, 𝑦 ∈ (1st ‘𝑥) ↦ {𝑛 ∈ (1st ‘𝑥) ∣ 𝜑}) & ⊢ (𝜓 → (𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌)) & ⊢ ((𝜓 ∧ ¬ 𝐾 ∈ 𝑉) → {𝑛 ∈ 𝑉 ∣ [〈𝑉, 𝑊〉 / 𝑥][𝐾 / 𝑦]𝜑} = ∅) ⇒ ⊢ (𝜓 → (〈𝑉, 𝑊〉𝐹𝐾) = {𝑛 ∈ 𝑉 ∣ [〈𝑉, 𝑊〉 / 𝑥][𝐾 / 𝑦]𝜑}) | ||
Theorem | brovex 7871* | A binary relation of the value of an operation given by the maps-to notation. (Contributed by Alexander van der Vekens, 21-Oct-2017.) |
⊢ 𝑂 = (𝑥 ∈ V, 𝑦 ∈ V ↦ 𝐶) & ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → Rel (𝑉𝑂𝐸)) ⇒ ⊢ (𝐹(𝑉𝑂𝐸)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) | ||
Theorem | brovmpoex 7872* | A binary relation of the value of an operation given by the maps-to notation. (Contributed by Alexander van der Vekens, 21-Oct-2017.) |
⊢ 𝑂 = (𝑥 ∈ V, 𝑦 ∈ V ↦ {〈𝑧, 𝑤〉 ∣ 𝜑}) ⇒ ⊢ (𝐹(𝑉𝑂𝐸)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) | ||
Theorem | sprmpod 7873* | The extension of a binary relation which is the value of an operation given in maps-to notation. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 20-Jun-2019.) |
⊢ 𝑀 = (𝑣 ∈ V, 𝑒 ∈ V ↦ {〈𝑥, 𝑦〉 ∣ (𝑥(𝑣𝑅𝑒)𝑦 ∧ 𝜒)}) & ⊢ ((𝜑 ∧ 𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝜒 ↔ 𝜓)) & ⊢ (𝜑 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) & ⊢ (𝜑 → ∀𝑥∀𝑦(𝑥(𝑉𝑅𝐸)𝑦 → 𝜃)) & ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝜃} ∈ V) ⇒ ⊢ (𝜑 → (𝑉𝑀𝐸) = {〈𝑥, 𝑦〉 ∣ (𝑥(𝑉𝑅𝐸)𝑦 ∧ 𝜓)}) | ||
Syntax | ctpos 7874 | The transposition of a function. |
class tpos 𝐹 | ||
Definition | df-tpos 7875* | Define the transposition of a function, which is a function 𝐺 = tpos 𝐹 satisfying 𝐺(𝑥, 𝑦) = 𝐹(𝑦, 𝑥). (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ tpos 𝐹 = (𝐹 ∘ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})) | ||
Theorem | tposss 7876 | Subset theorem for transposition. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (𝐹 ⊆ 𝐺 → tpos 𝐹 ⊆ tpos 𝐺) | ||
Theorem | tposeq 7877 | Equality theorem for transposition. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (𝐹 = 𝐺 → tpos 𝐹 = tpos 𝐺) | ||
Theorem | tposeqd 7878 | Equality theorem for transposition. (Contributed by Mario Carneiro, 7-Jan-2017.) |
⊢ (𝜑 → 𝐹 = 𝐺) ⇒ ⊢ (𝜑 → tpos 𝐹 = tpos 𝐺) | ||
Theorem | tposssxp 7879 | The transposition is a subset of a Cartesian product. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ tpos 𝐹 ⊆ ((◡dom 𝐹 ∪ {∅}) × ran 𝐹) | ||
Theorem | reltpos 7880 | The transposition is a relation. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ Rel tpos 𝐹 | ||
Theorem | brtpos2 7881 | Value of the transposition at a pair 〈𝐴, 𝐵〉. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴tpos 𝐹𝐵 ↔ (𝐴 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{𝐴}𝐹𝐵))) | ||
Theorem | brtpos0 7882 | The behavior of tpos when the left argument is the empty set (which is not an ordered pair but is the "default" value of an ordered pair when the arguments are proper classes). This allows us to eliminate sethood hypotheses on 𝐴, 𝐵 in brtpos 7884. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (𝐴 ∈ 𝑉 → (∅tpos 𝐹𝐴 ↔ ∅𝐹𝐴)) | ||
Theorem | reldmtpos 7883 | Necessary and sufficient condition for dom tpos 𝐹 to be a relation. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (Rel dom tpos 𝐹 ↔ ¬ ∅ ∈ dom 𝐹) | ||
Theorem | brtpos 7884 | The transposition swaps arguments of a three-parameter relation. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (𝐶 ∈ 𝑉 → (〈𝐴, 𝐵〉tpos 𝐹𝐶 ↔ 〈𝐵, 𝐴〉𝐹𝐶)) | ||
Theorem | ottpos 7885 | The transposition swaps the first two elements in a collection of ordered triples. (Contributed by Mario Carneiro, 1-Dec-2014.) |
⊢ (𝐶 ∈ 𝑉 → (〈𝐴, 𝐵, 𝐶〉 ∈ tpos 𝐹 ↔ 〈𝐵, 𝐴, 𝐶〉 ∈ 𝐹)) | ||
Theorem | relbrtpos 7886 | The transposition swaps arguments of a three-parameter relation. (Contributed by Mario Carneiro, 3-Nov-2015.) |
⊢ (Rel 𝐹 → (〈𝐴, 𝐵〉tpos 𝐹𝐶 ↔ 〈𝐵, 𝐴〉𝐹𝐶)) | ||
Theorem | dmtpos 7887 | The domain of tpos 𝐹 when dom 𝐹 is a relation. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (Rel dom 𝐹 → dom tpos 𝐹 = ◡dom 𝐹) | ||
Theorem | rntpos 7888 | The range of tpos 𝐹 when dom 𝐹 is a relation. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (Rel dom 𝐹 → ran tpos 𝐹 = ran 𝐹) | ||
Theorem | tposexg 7889 | The transposition of a set is a set. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (𝐹 ∈ 𝑉 → tpos 𝐹 ∈ V) | ||
Theorem | ovtpos 7890 | The transposition swaps the arguments in a two-argument function. When 𝐹 is a matrix, which is to say a function from (1...𝑚) × (1...𝑛) to ℝ or some ring, tpos 𝐹 is the transposition of 𝐹, which is where the name comes from. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (𝐴tpos 𝐹𝐵) = (𝐵𝐹𝐴) | ||
Theorem | tposfun 7891 | The transposition of a function is a function. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (Fun 𝐹 → Fun tpos 𝐹) | ||
Theorem | dftpos2 7892* | Alternate definition of tpos when 𝐹 has relational domain. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (Rel dom 𝐹 → tpos 𝐹 = (𝐹 ∘ (𝑥 ∈ ◡dom 𝐹 ↦ ∪ ◡{𝑥}))) | ||
Theorem | dftpos3 7893* | Alternate definition of tpos when 𝐹 has relational domain. Compare df-cnv 5527. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (Rel dom 𝐹 → tpos 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 〈𝑦, 𝑥〉𝐹𝑧}) | ||
Theorem | dftpos4 7894* | Alternate definition of tpos. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ tpos 𝐹 = (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})) | ||
Theorem | tpostpos 7895 | Value of the double transposition for a general class 𝐹. (Contributed by Mario Carneiro, 16-Sep-2015.) |
⊢ tpos tpos 𝐹 = (𝐹 ∩ (((V × V) ∪ {∅}) × V)) | ||
Theorem | tpostpos2 7896 | Value of the double transposition for a relation on triples. (Contributed by Mario Carneiro, 16-Sep-2015.) |
⊢ ((Rel 𝐹 ∧ Rel dom 𝐹) → tpos tpos 𝐹 = 𝐹) | ||
Theorem | tposfn2 7897 | The domain of a transposition. (Contributed by NM, 10-Sep-2015.) |
⊢ (Rel 𝐴 → (𝐹 Fn 𝐴 → tpos 𝐹 Fn ◡𝐴)) | ||
Theorem | tposfo2 7898 | Condition for a surjective transposition. (Contributed by NM, 10-Sep-2015.) |
⊢ (Rel 𝐴 → (𝐹:𝐴–onto→𝐵 → tpos 𝐹:◡𝐴–onto→𝐵)) | ||
Theorem | tposf2 7899 | The domain and range of a transposition. (Contributed by NM, 10-Sep-2015.) |
⊢ (Rel 𝐴 → (𝐹:𝐴⟶𝐵 → tpos 𝐹:◡𝐴⟶𝐵)) | ||
Theorem | tposf12 7900 | Condition for an injective transposition. (Contributed by NM, 10-Sep-2015.) |
⊢ (Rel 𝐴 → (𝐹:𝐴–1-1→𝐵 → tpos 𝐹:◡𝐴–1-1→𝐵)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |