![]() |
Metamath
Proof Explorer Theorem List (p. 430 of 479) | < 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-30166) |
![]() (30167-31689) |
![]() (31690-47842) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | imadisjld 42901 | Natural dduction form of one side of imadisj 6079. (Contributed by Stanislas Polu, 9-Mar-2020.) |
β’ (π β (dom π΄ β© π΅) = β ) β β’ (π β (π΄ β π΅) = β ) | ||
Theorem | imadisjlnd 42902 | Natural deduction form of one negated side of imadisj 6079. (Contributed by Stanislas Polu, 9-Mar-2020.) |
β’ (π β (dom π΄ β© π΅) β β ) β β’ (π β (π΄ β π΅) β β ) | ||
Theorem | wnefimgd 42903 | The image of a mapping from A is nonempty if A is nonempty. (Contributed by Stanislas Polu, 9-Mar-2020.) |
β’ (π β π΄ β β ) & β’ (π β πΉ:π΄βΆπ΅) β β’ (π β (πΉ β π΄) β β ) | ||
Theorem | fco2d 42904 | Natural deduction form of fco2 6744. (Contributed by Stanislas Polu, 9-Mar-2020.) |
β’ (π β πΊ:π΄βΆπ΅) & β’ (π β (πΉ βΎ π΅):π΅βΆπΆ) β β’ (π β (πΉ β πΊ):π΄βΆπΆ) | ||
Theorem | wfximgfd 42905 | The value of a function on its domain is in the image of the function. (Contributed by Stanislas Polu, 9-Mar-2020.) |
β’ (π β πΆ β π΄) & β’ (π β πΉ:π΄βΆπ΅) β β’ (π β (πΉβπΆ) β (πΉ β π΄)) | ||
Theorem | extoimad 42906* | If |f(x)| <= C for all x then it applies to all x in the image of |f(x)| (Contributed by Stanislas Polu, 9-Mar-2020.) |
β’ (π β πΉ:ββΆβ) & β’ (π β βπ¦ β β (absβ(πΉβπ¦)) β€ πΆ) β β’ (π β βπ₯ β (abs β (πΉ β β))π₯ β€ πΆ) | ||
Theorem | imo72b2lem0 42907* | Lemma for imo72b2 42914. (Contributed by Stanislas Polu, 9-Mar-2020.) |
β’ (π β πΉ:ββΆβ) & β’ (π β πΊ:ββΆβ) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β ((πΉβ(π΄ + π΅)) + (πΉβ(π΄ β π΅))) = (2 Β· ((πΉβπ΄) Β· (πΊβπ΅)))) & β’ (π β βπ¦ β β (absβ(πΉβπ¦)) β€ 1) β β’ (π β ((absβ(πΉβπ΄)) Β· (absβ(πΊβπ΅))) β€ sup((abs β (πΉ β β)), β, < )) | ||
Theorem | suprleubrd 42908* | Natural deduction form of specialized suprleub 12179. (Contributed by Stanislas Polu, 9-Mar-2020.) |
β’ (π β π΄ β β) & β’ (π β π΄ β β ) & β’ (π β βπ₯ β β βπ¦ β π΄ π¦ β€ π₯) & β’ (π β π΅ β β) & β’ (π β βπ§ β π΄ π§ β€ π΅) β β’ (π β sup(π΄, β, < ) β€ π΅) | ||
Theorem | imo72b2lem2 42909* | Lemma for imo72b2 42914. (Contributed by Stanislas Polu, 9-Mar-2020.) |
β’ (π β πΉ:ββΆβ) & β’ (π β πΆ β β) & β’ (π β βπ§ β β (absβ(πΉβπ§)) β€ πΆ) β β’ (π β sup((abs β (πΉ β β)), β, < ) β€ πΆ) | ||
Theorem | suprlubrd 42910* | Natural deduction form of specialized suprlub 12177. (Contributed by Stanislas Polu, 9-Mar-2020.) |
β’ (π β π΄ β β) & β’ (π β π΄ β β ) & β’ (π β βπ₯ β β βπ¦ β π΄ π¦ β€ π₯) & β’ (π β π΅ β β) & β’ (π β βπ§ β π΄ π΅ < π§) β β’ (π β π΅ < sup(π΄, β, < )) | ||
Theorem | imo72b2lem1 42911* | Lemma for imo72b2 42914. (Contributed by Stanislas Polu, 9-Mar-2020.) |
β’ (π β πΉ:ββΆβ) & β’ (π β βπ₯ β β (πΉβπ₯) β 0) & β’ (π β βπ¦ β β (absβ(πΉβπ¦)) β€ 1) β β’ (π β 0 < sup((abs β (πΉ β β)), β, < )) | ||
Theorem | lemuldiv3d 42912 | 'Less than or equal to' relationship between division and multiplication. (Contributed by Stanislas Polu, 9-Mar-2020.) |
β’ (π β (π΅ Β· π΄) β€ πΆ) & β’ (π β 0 < π΄) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) β β’ (π β π΅ β€ (πΆ / π΄)) | ||
Theorem | lemuldiv4d 42913 | 'Less than or equal to' relationship between division and multiplication. (Contributed by Stanislas Polu, 9-Mar-2020.) |
β’ (π β π΅ β€ (πΆ / π΄)) & β’ (π β 0 < π΄) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) β β’ (π β (π΅ Β· π΄) β€ πΆ) | ||
Theorem | imo72b2 42914* | IMO 1972 B2. (14th International Mathematical Olympiad in Poland, problem B2). (Contributed by Stanislas Polu, 9-Mar-2020.) |
β’ (π β πΉ:ββΆβ) & β’ (π β πΊ:ββΆβ) & β’ (π β π΅ β β) & β’ (π β βπ’ β β βπ£ β β ((πΉβ(π’ + π£)) + (πΉβ(π’ β π£))) = (2 Β· ((πΉβπ’) Β· (πΊβπ£)))) & β’ (π β βπ¦ β β (absβ(πΉβπ¦)) β€ 1) & β’ (π β βπ₯ β β (πΉβπ₯) β 0) β β’ (π β (absβ(πΊβπ΅)) β€ 1) | ||
This section formalizes theorems necessary to reproduce the equality and inequality generator described in "Neural Theorem Proving on Inequality Problems" http://aitp-conference.org/2020/abstract/paper_18.pdf. Other theorems required: 0red 11216 1red 11214 readdcld 11242 remulcld 11243 eqcomd 2738. | ||
Theorem | int-addcomd 42915 | AdditionCommutativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π΄ = π΅) β β’ (π β (π΅ + πΆ) = (πΆ + π΄)) | ||
Theorem | int-addassocd 42916 | AdditionAssociativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
β’ (π β π΄ β β) & β’ (π β πΆ β β) & β’ (π β π· β β) & β’ (π β π΄ = π΅) β β’ (π β (π΅ + (πΆ + π·)) = ((π΄ + πΆ) + π·)) | ||
Theorem | int-addsimpd 42917 | AdditionSimplification generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
β’ (π β π΄ β β) & β’ (π β π΄ = π΅) β β’ (π β 0 = (π΄ β π΅)) | ||
Theorem | int-mulcomd 42918 | MultiplicationCommutativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π΄ = π΅) β β’ (π β (π΅ Β· πΆ) = (πΆ Β· π΄)) | ||
Theorem | int-mulassocd 42919 | MultiplicationAssociativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π· β β) & β’ (π β π΄ = π΅) β β’ (π β (π΅ Β· (πΆ Β· π·)) = ((π΄ Β· πΆ) Β· π·)) | ||
Theorem | int-mulsimpd 42920 | MultiplicationSimplification generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
β’ (π β π΅ β β) & β’ (π β π΄ = π΅) & β’ (π β π΅ β 0) β β’ (π β 1 = (π΄ / π΅)) | ||
Theorem | int-leftdistd 42921 | AdditionMultiplicationLeftDistribution generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π· β β) & β’ (π β π΄ = π΅) β β’ (π β ((πΆ + π·) Β· π΅) = ((πΆ Β· π΄) + (π· Β· π΄))) | ||
Theorem | int-rightdistd 42922 | AdditionMultiplicationRightDistribution generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π· β β) & β’ (π β π΄ = π΅) β β’ (π β (π΅ Β· (πΆ + π·)) = ((π΄ Β· πΆ) + (π΄ Β· π·))) | ||
Theorem | int-sqdefd 42923 | SquareDefinition generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
β’ (π β π΅ β β) & β’ (π β π΄ = π΅) β β’ (π β (π΄ Β· π΅) = (π΄β2)) | ||
Theorem | int-mul11d 42924 | First MultiplicationOne generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
β’ (π β π΄ β β) & β’ (π β π΄ = π΅) β β’ (π β (π΄ Β· 1) = π΅) | ||
Theorem | int-mul12d 42925 | Second MultiplicationOne generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
β’ (π β π΄ β β) & β’ (π β π΄ = π΅) β β’ (π β (1 Β· π΄) = π΅) | ||
Theorem | int-add01d 42926 | First AdditionZero generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
β’ (π β π΄ β β) & β’ (π β π΄ = π΅) β β’ (π β (π΄ + 0) = π΅) | ||
Theorem | int-add02d 42927 | Second AdditionZero generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
β’ (π β π΄ β β) & β’ (π β π΄ = π΅) β β’ (π β (0 + π΄) = π΅) | ||
Theorem | int-sqgeq0d 42928 | SquareGEQZero generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ = π΅) β β’ (π β 0 β€ (π΄ Β· π΅)) | ||
Theorem | int-eqprincd 42929 | PrincipleOfEquality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
β’ (π β π΄ = π΅) & β’ (π β πΆ = π·) β β’ (π β (π΄ + πΆ) = (π΅ + π·)) | ||
Theorem | int-eqtransd 42930 | EqualityTransitivity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
β’ (π β π΄ = π΅) & β’ (π β π΅ = πΆ) β β’ (π β π΄ = πΆ) | ||
Theorem | int-eqmvtd 42931 | EquMoveTerm generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
β’ (π β πΆ β β) & β’ (π β π· β β) & β’ (π β π΄ = π΅) & β’ (π β π΄ = (πΆ + π·)) β β’ (π β πΆ = (π΅ β π·)) | ||
Theorem | int-eqineqd 42932 | EquivalenceImpliesDoubleInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
β’ (π β π΅ β β) & β’ (π β π΄ = π΅) β β’ (π β π΅ β€ π΄) | ||
Theorem | int-ineqmvtd 42933 | IneqMoveTerm generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π· β β) & β’ (π β π΅ β€ π΄) & β’ (π β π΄ = (πΆ + π·)) β β’ (π β (π΅ β π·) β€ πΆ) | ||
Theorem | int-ineq1stprincd 42934 | FirstPrincipleOfInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π· β β) & β’ (π β π΅ β€ π΄) & β’ (π β π· β€ πΆ) β β’ (π β (π΅ + π·) β€ (π΄ + πΆ)) | ||
Theorem | int-ineq2ndprincd 42935 | SecondPrincipleOfInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π΅ β€ π΄) & β’ (π β 0 β€ πΆ) β β’ (π β (π΅ Β· πΆ) β€ (π΄ Β· πΆ)) | ||
Theorem | int-ineqtransd 42936 | InequalityTransitivity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π΅ β€ π΄) & β’ (π β πΆ β€ π΅) β β’ (π β πΆ β€ π΄) | ||
This section formalizes theorems used in an n-digit addition proof generator. Other theorems required: deccl 12691 addcomli 11405 00id 11388 addridi 11400 addlidi 11401 eqid 2732 dec0h 12698 decadd 12730 decaddc 12731. | ||
Theorem | unitadd 42937 | Theorem used in conjunction with decaddc 12731 to absorb carry when generating n-digit addition synthetic proofs. (Contributed by Stanislas Polu, 7-Apr-2020.) |
β’ (π΄ + π΅) = πΉ & β’ (πΆ + 1) = π΅ & β’ π΄ β β0 & β’ πΆ β β0 β β’ ((π΄ + πΆ) + 1) = πΉ | ||
Theorem | gsumws3 42938 | Valuation of a length 3 word in a monoid. (Contributed by Stanislas Polu, 9-Sep-2020.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ ((πΊ β Mnd β§ (π β π΅ β§ (π β π΅ β§ π β π΅))) β (πΊ Ξ£g β¨βπππββ©) = (π + (π + π))) | ||
Theorem | gsumws4 42939 | Valuation of a length 4 word in a monoid. (Contributed by Stanislas Polu, 10-Sep-2020.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ ((πΊ β Mnd β§ (π β π΅ β§ (π β π΅ β§ (π β π΅ β§ π β π΅)))) β (πΊ Ξ£g β¨βππππββ©) = (π + (π + (π + π)))) | ||
Theorem | amgm2d 42940 | Arithmetic-geometric mean inequality for π = 2, derived from amgmlem 26491. (Contributed by Stanislas Polu, 8-Sep-2020.) |
β’ (π β π΄ β β+) & β’ (π β π΅ β β+) β β’ (π β ((π΄ Β· π΅)βπ(1 / 2)) β€ ((π΄ + π΅) / 2)) | ||
Theorem | amgm3d 42941 | Arithmetic-geometric mean inequality for π = 3. (Contributed by Stanislas Polu, 11-Sep-2020.) |
β’ (π β π΄ β β+) & β’ (π β π΅ β β+) & β’ (π β πΆ β β+) β β’ (π β ((π΄ Β· (π΅ Β· πΆ))βπ(1 / 3)) β€ ((π΄ + (π΅ + πΆ)) / 3)) | ||
Theorem | amgm4d 42942 | Arithmetic-geometric mean inequality for π = 4. (Contributed by Stanislas Polu, 11-Sep-2020.) |
β’ (π β π΄ β β+) & β’ (π β π΅ β β+) & β’ (π β πΆ β β+) & β’ (π β π· β β+) β β’ (π β ((π΄ Β· (π΅ Β· (πΆ Β· π·)))βπ(1 / 4)) β€ ((π΄ + (π΅ + (πΆ + π·))) / 4)) | ||
Theorem | spALT 42943 | sp 2176 can be proven from the other classic axioms. (Contributed by Rohan Ridenour, 3-Nov-2023.) (Proof modification is discouraged.) Use sp 2176 instead. (New usage is discouraged.) |
β’ (βπ₯π β π) | ||
Theorem | elnelneqd 42944 | Two classes are not equal if there is an element of one which is not an element of the other. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ (π β πΆ β π΄) & β’ (π β Β¬ πΆ β π΅) β β’ (π β Β¬ π΄ = π΅) | ||
Theorem | elnelneq2d 42945 | Two classes are not equal if one but not the other is an element of a given class. (Contributed by Rohan Ridenour, 12-Aug-2023.) |
β’ (π β π΄ β πΆ) & β’ (π β Β¬ π΅ β πΆ) β β’ (π β Β¬ π΄ = π΅) | ||
Theorem | rr-spce 42946* | Prove an existential. (Contributed by Rohan Ridenour, 12-Aug-2023.) |
β’ ((π β§ π₯ = π΄) β π) & β’ (π β π΄ β π) β β’ (π β βπ₯π) | ||
Theorem | rexlimdvaacbv 42947* | Unpack a restricted existential antecedent while changing the variable with implicit substitution. The equivalent of this theorem without the bound variable change is rexlimdvaa 3156. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
β’ (π₯ = π¦ β (π β π)) & β’ ((π β§ (π¦ β π΄ β§ π)) β π) β β’ (π β (βπ₯ β π΄ π β π)) | ||
Theorem | rexlimddvcbvw 42948* | Unpack a restricted existential assumption while changing the variable with implicit substitution. Similar to rexlimdvaacbv 42947. The equivalent of this theorem without the bound variable change is rexlimddv 3161. Version of rexlimddvcbv 42949 with a disjoint variable condition, which does not require ax-13 2371. (Contributed by Rohan Ridenour, 3-Aug-2023.) (Revised by Gino Giotto, 2-Apr-2024.) |
β’ (π β βπ₯ β π΄ π) & β’ ((π β§ (π¦ β π΄ β§ π)) β π) & β’ (π₯ = π¦ β (π β π)) β β’ (π β π) | ||
Theorem | rexlimddvcbv 42949* | Unpack a restricted existential assumption while changing the variable with implicit substitution. Similar to rexlimdvaacbv 42947. The equivalent of this theorem without the bound variable change is rexlimddv 3161. Usage of this theorem is discouraged because it depends on ax-13 2371, see rexlimddvcbvw 42948 for a weaker version that does not require it. (Contributed by Rohan Ridenour, 3-Aug-2023.) (New usage is discouraged.) |
β’ (π β βπ₯ β π΄ π) & β’ ((π β§ (π¦ β π΄ β§ π)) β π) & β’ (π₯ = π¦ β (π β π)) β β’ (π β π) | ||
Theorem | rr-elrnmpt3d 42950* | Elementhood in an image set. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ πΉ = (π₯ β π΄ β¦ π΅) & β’ (π β πΆ β π΄) & β’ (π β π· β π) & β’ ((π β§ π₯ = πΆ) β π΅ = π·) β β’ (π β π· β ran πΉ) | ||
Theorem | finnzfsuppd 42951* | If a function is zero outside of a finite set, it has finite support. (Contributed by Rohan Ridenour, 13-May-2024.) |
β’ (π β πΉ β π) & β’ (π β πΉ Fn π·) & β’ (π β π β π) & β’ (π β π΄ β Fin) & β’ ((π β§ π₯ β π·) β (π₯ β π΄ β¨ (πΉβπ₯) = π)) β β’ (π β πΉ finSupp π) | ||
Theorem | rr-phpd 42952 | Equivalent of php 9209 without negation. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
β’ (π β π΄ β Ο) & β’ (π β π΅ β π΄) & β’ (π β π΄ β π΅) β β’ (π β π΄ = π΅) | ||
Theorem | suceqd 42953 | Deduction associated with suceq 6430. (Contributed by Rohan Ridenour, 8-Aug-2023.) |
β’ (π β π΄ = π΅) β β’ (π β suc π΄ = suc π΅) | ||
Theorem | tfindsd 42954* | Deduction associated with tfinds 7848. (Contributed by Rohan Ridenour, 8-Aug-2023.) |
β’ (π₯ = β β (π β π)) & β’ (π₯ = π¦ β (π β π)) & β’ (π₯ = suc π¦ β (π β π)) & β’ (π₯ = π΄ β (π β π)) & β’ (π β π) & β’ ((π β§ π¦ β On β§ π) β π) & β’ ((π β§ Lim π₯ β§ βπ¦ β π₯ π) β π) & β’ (π β π΄ β On) β β’ (π β π) | ||
Syntax | cmnring 42955 | Extend class notation with the monoid ring function. |
class MndRing | ||
Definition | df-mnring 42956* | Define the monoid ring function. This takes a monoid π and a ring π and produces a free left module over π with a product extending the monoid function on π. (Contributed by Rohan Ridenour, 13-May-2024.) |
β’ MndRing = (π β V, π β V β¦ β¦(π freeLMod (Baseβπ)) / π£β¦(π£ sSet β¨(.rβndx), (π₯ β (Baseβπ£), π¦ β (Baseβπ£) β¦ (π£ Ξ£g (π β (Baseβπ), π β (Baseβπ) β¦ (π β (Baseβπ) β¦ if(π = (π(+gβπ)π), ((π₯βπ)(.rβπ)(π¦βπ)), (0gβπ))))))β©)) | ||
Theorem | mnringvald 42957* | Value of the monoid ring function. (Contributed by Rohan Ridenour, 14-May-2024.) |
β’ πΉ = (π MndRing π) & β’ Β· = (.rβπ ) & β’ 0 = (0gβπ ) & β’ π΄ = (Baseβπ) & β’ + = (+gβπ) & β’ π = (π freeLMod π΄) & β’ π΅ = (Baseβπ) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β πΉ = (π sSet β¨(.rβndx), (π₯ β π΅, π¦ β π΅ β¦ (π Ξ£g (π β π΄, π β π΄ β¦ (π β π΄ β¦ if(π = (π + π), ((π₯βπ) Β· (π¦βπ)), 0 )))))β©)) | ||
Theorem | mnringnmulrd 42958 | Components of a monoid ring other than its ring product match its underlying free module. (Contributed by Rohan Ridenour, 14-May-2024.) (Revised by AV, 1-Nov-2024.) |
β’ πΉ = (π MndRing π) & β’ πΈ = Slot (πΈβndx) & β’ (πΈβndx) β (.rβndx) & β’ π΄ = (Baseβπ) & β’ π = (π freeLMod π΄) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (πΈβπ) = (πΈβπΉ)) | ||
Theorem | mnringnmulrdOLD 42959 | Obsolete version of mnringnmulrd 42958 as of 1-Nov-2024. Components of a monoid ring other than its ring product match its underlying free module. (Contributed by Rohan Ridenour, 14-May-2024.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ πΉ = (π MndRing π) & β’ πΈ = Slot π & β’ π β β & β’ π β (.rβndx) & β’ π΄ = (Baseβπ) & β’ π = (π freeLMod π΄) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (πΈβπ) = (πΈβπΉ)) | ||
Theorem | mnringbased 42960 | The base set of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) (Proof shortened by AV, 1-Nov-2024.) |
β’ πΉ = (π MndRing π) & β’ π΄ = (Baseβπ) & β’ π = (π freeLMod π΄) & β’ π΅ = (Baseβπ) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β π΅ = (BaseβπΉ)) | ||
Theorem | mnringbasedOLD 42961 | Obsolete version of mnringnmulrd 42958 as of 1-Nov-2024. The base set of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ πΉ = (π MndRing π) & β’ π΄ = (Baseβπ) & β’ π = (π freeLMod π΄) & β’ π΅ = (Baseβπ) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β π΅ = (BaseβπΉ)) | ||
Theorem | mnringbaserd 42962 | The base set of a monoid ring. Converse of mnringbased 42960. (Contributed by Rohan Ridenour, 14-May-2024.) |
β’ πΉ = (π MndRing π) & β’ π΅ = (BaseβπΉ) & β’ π΄ = (Baseβπ) & β’ π = (π freeLMod π΄) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β π΅ = (Baseβπ)) | ||
Theorem | mnringelbased 42963 | Membership in the base set of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) |
β’ πΉ = (π MndRing π) & β’ π΅ = (BaseβπΉ) & β’ π΄ = (Baseβπ) & β’ πΆ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (π β π΅ β (π β (πΆ βm π΄) β§ π finSupp 0 ))) | ||
Theorem | mnringbasefd 42964 | Elements of a monoid ring are functions. (Contributed by Rohan Ridenour, 14-May-2024.) |
β’ πΉ = (π MndRing π) & β’ π΅ = (BaseβπΉ) & β’ π΄ = (Baseβπ) & β’ πΆ = (Baseβπ ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π΅) β β’ (π β π:π΄βΆπΆ) | ||
Theorem | mnringbasefsuppd 42965 | Elements of a monoid ring are finitely supported. (Contributed by Rohan Ridenour, 14-May-2024.) |
β’ πΉ = (π MndRing π) & β’ π΅ = (BaseβπΉ) & β’ 0 = (0gβπ ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π΅) β β’ (π β π finSupp 0 ) | ||
Theorem | mnringaddgd 42966 | The additive operation of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) (Proof shortened by AV, 1-Nov-2024.) |
β’ πΉ = (π MndRing π) & β’ π΄ = (Baseβπ) & β’ π = (π freeLMod π΄) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (+gβπ) = (+gβπΉ)) | ||
Theorem | mnringaddgdOLD 42967 | Obsolete version of mnringaddgd 42966 as of 1-Nov-2024. The additive operation of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ πΉ = (π MndRing π) & β’ π΄ = (Baseβπ) & β’ π = (π freeLMod π΄) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (+gβπ) = (+gβπΉ)) | ||
Theorem | mnring0gd 42968 | The additive identity of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) |
β’ πΉ = (π MndRing π) & β’ π΄ = (Baseβπ) & β’ π = (π freeLMod π΄) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (0gβπ) = (0gβπΉ)) | ||
Theorem | mnring0g2d 42969 | The additive identity of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) |
β’ πΉ = (π MndRing π) & β’ 0 = (0gβπ ) & β’ π΄ = (Baseβπ) & β’ (π β π β Ring) & β’ (π β π β π) β β’ (π β (π΄ Γ { 0 }) = (0gβπΉ)) | ||
Theorem | mnringmulrd 42970* | The ring product of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) |
β’ πΉ = (π MndRing π) & β’ π΅ = (BaseβπΉ) & β’ Β· = (.rβπ ) & β’ 0 = (0gβπ ) & β’ π΄ = (Baseβπ) & β’ + = (+gβπ) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (π₯ β π΅, π¦ β π΅ β¦ (πΉ Ξ£g (π β π΄, π β π΄ β¦ (π β π΄ β¦ if(π = (π + π), ((π₯βπ) Β· (π¦βπ)), 0 ))))) = (.rβπΉ)) | ||
Theorem | mnringscad 42971 | The scalar ring of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) (Proof shortened by AV, 1-Nov-2024.) |
β’ πΉ = (π MndRing π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β π = (ScalarβπΉ)) | ||
Theorem | mnringscadOLD 42972 | Obsolete version of mnringscad 42971 as of 1-Nov-2024. The scalar ring of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ πΉ = (π MndRing π) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β π = (ScalarβπΉ)) | ||
Theorem | mnringvscad 42973 | The scalar product of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) (Proof shortened by AV, 1-Nov-2024.) |
β’ πΉ = (π MndRing π) & β’ π΅ = (Baseβπ) & β’ π = (π freeLMod π΅) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β ( Β·π βπ) = ( Β·π βπΉ)) | ||
Theorem | mnringvscadOLD 42974 | Obsolete version of mnringvscad 42973 as of 1-Nov-2024. The scalar product of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ πΉ = (π MndRing π) & β’ π΅ = (Baseβπ) & β’ π = (π freeLMod π΅) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β ( Β·π βπ) = ( Β·π βπΉ)) | ||
Theorem | mnringlmodd 42975 | Monoid rings are left modules. (Contributed by Rohan Ridenour, 14-May-2024.) |
β’ πΉ = (π MndRing π) & β’ (π β π β Ring) & β’ (π β π β π) β β’ (π β πΉ β LMod) | ||
Theorem | mnringmulrvald 42976* | Value of multiplication in a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) |
β’ πΉ = (π MndRing π) & β’ π΅ = (BaseβπΉ) & β’ β = (.rβπ ) & β’ π = (0gβπ ) & β’ π΄ = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = (.rβπΉ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π Β· π) = (πΉ Ξ£g (π β π΄, π β π΄ β¦ (π β π΄ β¦ if(π = (π + π), ((πβπ) β (πβπ)), π ))))) | ||
Theorem | mnringmulrcld 42977 | Monoid rings are closed under multiplication. (Contributed by Rohan Ridenour, 14-May-2024.) |
β’ πΉ = (π MndRing π) & β’ π΅ = (BaseβπΉ) & β’ π΄ = (Baseβπ) & β’ Β· = (.rβπΉ) & β’ (π β π β Ring) & β’ (π β π β π) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π Β· π) β π΅) | ||
Theorem | gru0eld 42978 | A nonempty Grothendieck universe contains the empty set. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ (π β πΊ β Univ) & β’ (π β π΄ β πΊ) β β’ (π β β β πΊ) | ||
Theorem | grusucd 42979 | Grothendieck universes are closed under ordinal successor. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
β’ (π β πΊ β Univ) & β’ (π β π΄ β πΊ) β β’ (π β suc π΄ β πΊ) | ||
Theorem | r1rankcld 42980 | Any rank of the cumulative hierarchy is closed under the rank function. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ (π β π΄ β (π 1βπ )) β β’ (π β (rankβπ΄) β (π 1βπ )) | ||
Theorem | grur1cld 42981 | Grothendieck universes are closed under the cumulative hierarchy function. (Contributed by Rohan Ridenour, 8-Aug-2023.) |
β’ (π β πΊ β Univ) & β’ (π β π΄ β πΊ) β β’ (π β (π 1βπ΄) β πΊ) | ||
Theorem | grurankcld 42982 | Grothendieck universes are closed under the rank function. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
β’ (π β πΊ β Univ) & β’ (π β π΄ β πΊ) β β’ (π β (rankβπ΄) β πΊ) | ||
Theorem | grurankrcld 42983 | If a Grothendieck universe contains a set's rank, it contains that set. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
β’ (π β πΊ β Univ) & β’ (π β (rankβπ΄) β πΊ) & β’ (π β π΄ β π) β β’ (π β π΄ β πΊ) | ||
Syntax | cscott 42984 | Extend class notation with the Scott's trick operation. |
class Scott π΄ | ||
Definition | df-scott 42985* | Define the Scott operation. This operation constructs a subset of the input class which is nonempty whenever its input is using Scott's trick. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
β’ Scott π΄ = {π₯ β π΄ β£ βπ¦ β π΄ (rankβπ₯) β (rankβπ¦)} | ||
Theorem | scotteqd 42986 | Equality theorem for the Scott operation. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
β’ (π β π΄ = π΅) β β’ (π β Scott π΄ = Scott π΅) | ||
Theorem | scotteq 42987 | Closed form of scotteqd 42986. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
β’ (π΄ = π΅ β Scott π΄ = Scott π΅) | ||
Theorem | nfscott 42988 | Bound-variable hypothesis builder for the Scott operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ β²π₯π΄ β β’ β²π₯Scott π΄ | ||
Theorem | scottabf 42989* | Value of the Scott operation at a class abstraction. Variant of scottab 42990 with a nonfreeness hypothesis instead of a disjoint variable condition. (Contributed by Rohan Ridenour, 14-Aug-2023.) |
β’ β²π₯π & β’ (π₯ = π¦ β (π β π)) β β’ Scott {π₯ β£ π} = {π₯ β£ (π β§ βπ¦(π β (rankβπ₯) β (rankβπ¦)))} | ||
Theorem | scottab 42990* | Value of the Scott operation at a class abstraction. (Contributed by Rohan Ridenour, 14-Aug-2023.) |
β’ (π₯ = π¦ β (π β π)) β β’ Scott {π₯ β£ π} = {π₯ β£ (π β§ βπ¦(π β (rankβπ₯) β (rankβπ¦)))} | ||
Theorem | scottabes 42991* | Value of the Scott operation at a class abstraction. Variant of scottab 42990 using explicit substitution. (Contributed by Rohan Ridenour, 14-Aug-2023.) |
β’ Scott {π₯ β£ π} = {π₯ β£ (π β§ βπ¦([π¦ / π₯]π β (rankβπ₯) β (rankβπ¦)))} | ||
Theorem | scottss 42992 | Scott's trick produces a subset of the input class. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ Scott π΄ β π΄ | ||
Theorem | elscottab 42993* | An element of the output of the Scott operation applied to a class abstraction satisfies the class abstraction's predicate. (Contributed by Rohan Ridenour, 14-Aug-2023.) |
β’ (π₯ = π¦ β (π β π)) β β’ (π¦ β Scott {π₯ β£ π} β π) | ||
Theorem | scottex2 42994 | scottex 9879 expressed using Scott. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
β’ Scott π΄ β V | ||
Theorem | scotteld 42995* | The Scott operation sends inhabited classes to inhabited sets. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ (π β βπ₯ π₯ β π΄) β β’ (π β βπ₯ π₯ β Scott π΄) | ||
Theorem | scottelrankd 42996 | Property of a Scott's trick set. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ (π β π΅ β Scott π΄) & β’ (π β πΆ β Scott π΄) β β’ (π β (rankβπ΅) β (rankβπΆ)) | ||
Theorem | scottrankd 42997 | Rank of a nonempty Scott's trick set. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ (π β π΅ β Scott π΄) β β’ (π β (rankβScott π΄) = suc (rankβπ΅)) | ||
Theorem | gruscottcld 42998 | If a Grothendieck universe contains an element of a Scott's trick set, it contains the Scott's trick set. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ (π β πΊ β Univ) & β’ (π β π΅ β πΊ) & β’ (π β π΅ β Scott π΄) β β’ (π β Scott π΄ β πΊ) | ||
Syntax | ccoll 42999 | Extend class notation with the collection operation. |
class (πΉ Coll π΄) | ||
Definition | df-coll 43000* | Define the collection operation. This is similar to the image set operation β, but it uses Scott's trick to ensure the output is always a set. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ (πΉ Coll π΄) = βͺ π₯ β π΄ Scott (πΉ β {π₯}) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |