Home | Metamath
Proof Explorer Theorem List (p. 423 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | extoimad 42201* | 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 42202* | Lemma for imo72b2 42209. (Contributed by Stanislas Polu, 9-Mar-2020.) |
β’ (π β πΉ:ββΆβ) & β’ (π β πΊ:ββΆβ) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β ((πΉβ(π΄ + π΅)) + (πΉβ(π΄ β π΅))) = (2 Β· ((πΉβπ΄) Β· (πΊβπ΅)))) & β’ (π β βπ¦ β β (absβ(πΉβπ¦)) β€ 1) β β’ (π β ((absβ(πΉβπ΄)) Β· (absβ(πΊβπ΅))) β€ sup((abs β (πΉ β β)), β, < )) | ||
Theorem | suprleubrd 42203* | Natural deduction form of specialized suprleub 12054. (Contributed by Stanislas Polu, 9-Mar-2020.) |
β’ (π β π΄ β β) & β’ (π β π΄ β β ) & β’ (π β βπ₯ β β βπ¦ β π΄ π¦ β€ π₯) & β’ (π β π΅ β β) & β’ (π β βπ§ β π΄ π§ β€ π΅) β β’ (π β sup(π΄, β, < ) β€ π΅) | ||
Theorem | imo72b2lem2 42204* | Lemma for imo72b2 42209. (Contributed by Stanislas Polu, 9-Mar-2020.) |
β’ (π β πΉ:ββΆβ) & β’ (π β πΆ β β) & β’ (π β βπ§ β β (absβ(πΉβπ§)) β€ πΆ) β β’ (π β sup((abs β (πΉ β β)), β, < ) β€ πΆ) | ||
Theorem | suprlubrd 42205* | Natural deduction form of specialized suprlub 12052. (Contributed by Stanislas Polu, 9-Mar-2020.) |
β’ (π β π΄ β β) & β’ (π β π΄ β β ) & β’ (π β βπ₯ β β βπ¦ β π΄ π¦ β€ π₯) & β’ (π β π΅ β β) & β’ (π β βπ§ β π΄ π΅ < π§) β β’ (π β π΅ < sup(π΄, β, < )) | ||
Theorem | imo72b2lem1 42206* | Lemma for imo72b2 42209. (Contributed by Stanislas Polu, 9-Mar-2020.) |
β’ (π β πΉ:ββΆβ) & β’ (π β βπ₯ β β (πΉβπ₯) β 0) & β’ (π β βπ¦ β β (absβ(πΉβπ¦)) β€ 1) β β’ (π β 0 < sup((abs β (πΉ β β)), β, < )) | ||
Theorem | lemuldiv3d 42207 | 'Less than or equal to' relationship between division and multiplication. (Contributed by Stanislas Polu, 9-Mar-2020.) |
β’ (π β (π΅ Β· π΄) β€ πΆ) & β’ (π β 0 < π΄) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) β β’ (π β π΅ β€ (πΆ / π΄)) | ||
Theorem | lemuldiv4d 42208 | 'Less than or equal to' relationship between division and multiplication. (Contributed by Stanislas Polu, 9-Mar-2020.) |
β’ (π β π΅ β€ (πΆ / π΄)) & β’ (π β 0 < π΄) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) β β’ (π β (π΅ Β· π΄) β€ πΆ) | ||
Theorem | imo72b2 42209* | 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 11091 1red 11089 readdcld 11117 remulcld 11118 eqcomd 2743. | ||
Theorem | int-addcomd 42210 | AdditionCommutativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π΄ = π΅) β β’ (π β (π΅ + πΆ) = (πΆ + π΄)) | ||
Theorem | int-addassocd 42211 | AdditionAssociativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
β’ (π β π΄ β β) & β’ (π β πΆ β β) & β’ (π β π· β β) & β’ (π β π΄ = π΅) β β’ (π β (π΅ + (πΆ + π·)) = ((π΄ + πΆ) + π·)) | ||
Theorem | int-addsimpd 42212 | AdditionSimplification generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
β’ (π β π΄ β β) & β’ (π β π΄ = π΅) β β’ (π β 0 = (π΄ β π΅)) | ||
Theorem | int-mulcomd 42213 | MultiplicationCommutativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π΄ = π΅) β β’ (π β (π΅ Β· πΆ) = (πΆ Β· π΄)) | ||
Theorem | int-mulassocd 42214 | MultiplicationAssociativity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π· β β) & β’ (π β π΄ = π΅) β β’ (π β (π΅ Β· (πΆ Β· π·)) = ((π΄ Β· πΆ) Β· π·)) | ||
Theorem | int-mulsimpd 42215 | MultiplicationSimplification generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
β’ (π β π΅ β β) & β’ (π β π΄ = π΅) & β’ (π β π΅ β 0) β β’ (π β 1 = (π΄ / π΅)) | ||
Theorem | int-leftdistd 42216 | AdditionMultiplicationLeftDistribution generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π· β β) & β’ (π β π΄ = π΅) β β’ (π β ((πΆ + π·) Β· π΅) = ((πΆ Β· π΄) + (π· Β· π΄))) | ||
Theorem | int-rightdistd 42217 | AdditionMultiplicationRightDistribution generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π· β β) & β’ (π β π΄ = π΅) β β’ (π β (π΅ Β· (πΆ + π·)) = ((π΄ Β· πΆ) + (π΄ Β· π·))) | ||
Theorem | int-sqdefd 42218 | SquareDefinition generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
β’ (π β π΅ β β) & β’ (π β π΄ = π΅) β β’ (π β (π΄ Β· π΅) = (π΄β2)) | ||
Theorem | int-mul11d 42219 | First MultiplicationOne generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
β’ (π β π΄ β β) & β’ (π β π΄ = π΅) β β’ (π β (π΄ Β· 1) = π΅) | ||
Theorem | int-mul12d 42220 | Second MultiplicationOne generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
β’ (π β π΄ β β) & β’ (π β π΄ = π΅) β β’ (π β (1 Β· π΄) = π΅) | ||
Theorem | int-add01d 42221 | First AdditionZero generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
β’ (π β π΄ β β) & β’ (π β π΄ = π΅) β β’ (π β (π΄ + 0) = π΅) | ||
Theorem | int-add02d 42222 | Second AdditionZero generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
β’ (π β π΄ β β) & β’ (π β π΄ = π΅) β β’ (π β (0 + π΄) = π΅) | ||
Theorem | int-sqgeq0d 42223 | SquareGEQZero generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π΄ = π΅) β β’ (π β 0 β€ (π΄ Β· π΅)) | ||
Theorem | int-eqprincd 42224 | PrincipleOfEquality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
β’ (π β π΄ = π΅) & β’ (π β πΆ = π·) β β’ (π β (π΄ + πΆ) = (π΅ + π·)) | ||
Theorem | int-eqtransd 42225 | EqualityTransitivity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
β’ (π β π΄ = π΅) & β’ (π β π΅ = πΆ) β β’ (π β π΄ = πΆ) | ||
Theorem | int-eqmvtd 42226 | EquMoveTerm generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
β’ (π β πΆ β β) & β’ (π β π· β β) & β’ (π β π΄ = π΅) & β’ (π β π΄ = (πΆ + π·)) β β’ (π β πΆ = (π΅ β π·)) | ||
Theorem | int-eqineqd 42227 | EquivalenceImpliesDoubleInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
β’ (π β π΅ β β) & β’ (π β π΄ = π΅) β β’ (π β π΅ β€ π΄) | ||
Theorem | int-ineqmvtd 42228 | IneqMoveTerm generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π· β β) & β’ (π β π΅ β€ π΄) & β’ (π β π΄ = (πΆ + π·)) β β’ (π β (π΅ β π·) β€ πΆ) | ||
Theorem | int-ineq1stprincd 42229 | FirstPrincipleOfInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π· β β) & β’ (π β π΅ β€ π΄) & β’ (π β π· β€ πΆ) β β’ (π β (π΅ + π·) β€ (π΄ + πΆ)) | ||
Theorem | int-ineq2ndprincd 42230 | SecondPrincipleOfInequality generator rule. (Contributed by Stanislas Polu, 7-Apr-2020.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β) & β’ (π β π΅ β€ π΄) & β’ (π β 0 β€ πΆ) β β’ (π β (π΅ Β· πΆ) β€ (π΄ Β· πΆ)) | ||
Theorem | int-ineqtransd 42231 | 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 12565 addcomli 11280 00id 11263 addid1i 11275 addid2i 11276 eqid 2737 dec0h 12572 decadd 12604 decaddc 12605. | ||
Theorem | unitadd 42232 | Theorem used in conjunction with decaddc 12605 to absorb carry when generating n-digit addition synthetic proofs. (Contributed by Stanislas Polu, 7-Apr-2020.) |
β’ (π΄ + π΅) = πΉ & β’ (πΆ + 1) = π΅ & β’ π΄ β β0 & β’ πΆ β β0 β β’ ((π΄ + πΆ) + 1) = πΉ | ||
Theorem | gsumws3 42233 | Valuation of a length 3 word in a monoid. (Contributed by Stanislas Polu, 9-Sep-2020.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ ((πΊ β Mnd β§ (π β π΅ β§ (π β π΅ β§ π β π΅))) β (πΊ Ξ£g β¨βπππββ©) = (π + (π + π))) | ||
Theorem | gsumws4 42234 | Valuation of a length 4 word in a monoid. (Contributed by Stanislas Polu, 10-Sep-2020.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ ((πΊ β Mnd β§ (π β π΅ β§ (π β π΅ β§ (π β π΅ β§ π β π΅)))) β (πΊ Ξ£g β¨βππππββ©) = (π + (π + (π + π)))) | ||
Theorem | amgm2d 42235 | Arithmetic-geometric mean inequality for π = 2, derived from amgmlem 26261. (Contributed by Stanislas Polu, 8-Sep-2020.) |
β’ (π β π΄ β β+) & β’ (π β π΅ β β+) β β’ (π β ((π΄ Β· π΅)βπ(1 / 2)) β€ ((π΄ + π΅) / 2)) | ||
Theorem | amgm3d 42236 | Arithmetic-geometric mean inequality for π = 3. (Contributed by Stanislas Polu, 11-Sep-2020.) |
β’ (π β π΄ β β+) & β’ (π β π΅ β β+) & β’ (π β πΆ β β+) β β’ (π β ((π΄ Β· (π΅ Β· πΆ))βπ(1 / 3)) β€ ((π΄ + (π΅ + πΆ)) / 3)) | ||
Theorem | amgm4d 42237 | Arithmetic-geometric mean inequality for π = 4. (Contributed by Stanislas Polu, 11-Sep-2020.) |
β’ (π β π΄ β β+) & β’ (π β π΅ β β+) & β’ (π β πΆ β β+) & β’ (π β π· β β+) β β’ (π β ((π΄ Β· (π΅ Β· (πΆ Β· π·)))βπ(1 / 4)) β€ ((π΄ + (π΅ + (πΆ + π·))) / 4)) | ||
Theorem | spALT 42238 | 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 42239 | 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 42240 | 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 42241* | Prove an existential. (Contributed by Rohan Ridenour, 12-Aug-2023.) |
β’ ((π β§ π₯ = π΄) β π) & β’ (π β π΄ β π) β β’ (π β βπ₯π) | ||
Theorem | rexlimdvaacbv 42242* | Unpack a restricted existential antecedent while changing the variable with implicit substitution. The equivalent of this theorem without the bound variable change is rexlimdvaa 3151. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
β’ (π₯ = π¦ β (π β π)) & β’ ((π β§ (π¦ β π΄ β§ π)) β π) β β’ (π β (βπ₯ β π΄ π β π)) | ||
Theorem | rexlimddvcbvw 42243* | Unpack a restricted existential assumption while changing the variable with implicit substitution. Similar to rexlimdvaacbv 42242. The equivalent of this theorem without the bound variable change is rexlimddv 3156. Version of rexlimddvcbv 42244 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 42244* | Unpack a restricted existential assumption while changing the variable with implicit substitution. Similar to rexlimdvaacbv 42242. The equivalent of this theorem without the bound variable change is rexlimddv 3156. Usage of this theorem is discouraged because it depends on ax-13 2371, see rexlimddvcbvw 42243 for a weaker version that does not require it. (Contributed by Rohan Ridenour, 3-Aug-2023.) (New usage is discouraged.) |
β’ (π β βπ₯ β π΄ π) & β’ ((π β§ (π¦ β π΄ β§ π)) β π) & β’ (π₯ = π¦ β (π β π)) β β’ (π β π) | ||
Theorem | rr-elrnmpt3d 42245* | Elementhood in an image set. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ πΉ = (π₯ β π΄ β¦ π΅) & β’ (π β πΆ β π΄) & β’ (π β π· β π) & β’ ((π β§ π₯ = πΆ) β π΅ = π·) β β’ (π β π· β ran πΉ) | ||
Theorem | finnzfsuppd 42246* | 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 42247 | Equivalent of php 9087 without negation. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
β’ (π β π΄ β Ο) & β’ (π β π΅ β π΄) & β’ (π β π΄ β π΅) β β’ (π β π΄ = π΅) | ||
Theorem | suceqd 42248 | Deduction associated with suceq 6379. (Contributed by Rohan Ridenour, 8-Aug-2023.) |
β’ (π β π΄ = π΅) β β’ (π β suc π΄ = suc π΅) | ||
Theorem | tfindsd 42249* | Deduction associated with tfinds 7786. (Contributed by Rohan Ridenour, 8-Aug-2023.) |
β’ (π₯ = β β (π β π)) & β’ (π₯ = π¦ β (π β π)) & β’ (π₯ = suc π¦ β (π β π)) & β’ (π₯ = π΄ β (π β π)) & β’ (π β π) & β’ ((π β§ π¦ β On β§ π) β π) & β’ ((π β§ Lim π₯ β§ βπ¦ β π₯ π) β π) & β’ (π β π΄ β On) β β’ (π β π) | ||
Syntax | cmnring 42250 | Extend class notation with the monoid ring function. |
class MndRing | ||
Definition | df-mnring 42251* | 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 42252* | 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 42253 | 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 42254 | Obsolete version of mnringnmulrd 42253 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 42255 | 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 42256 | Obsolete version of mnringnmulrd 42253 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 42257 | The base set of a monoid ring. Converse of mnringbased 42255. (Contributed by Rohan Ridenour, 14-May-2024.) |
β’ πΉ = (π MndRing π) & β’ π΅ = (BaseβπΉ) & β’ π΄ = (Baseβπ) & β’ π = (π freeLMod π΄) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β π΅ = (Baseβπ)) | ||
Theorem | mnringelbased 42258 | 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 42259 | Elements of a monoid ring are functions. (Contributed by Rohan Ridenour, 14-May-2024.) |
β’ πΉ = (π MndRing π) & β’ π΅ = (BaseβπΉ) & β’ π΄ = (Baseβπ) & β’ πΆ = (Baseβπ ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π΅) β β’ (π β π:π΄βΆπΆ) | ||
Theorem | mnringbasefsuppd 42260 | Elements of a monoid ring are finitely supported. (Contributed by Rohan Ridenour, 14-May-2024.) |
β’ πΉ = (π MndRing π) & β’ π΅ = (BaseβπΉ) & β’ 0 = (0gβπ ) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β π β π΅) β β’ (π β π finSupp 0 ) | ||
Theorem | mnringaddgd 42261 | 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 42262 | Obsolete version of mnringaddgd 42261 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 42263 | The additive identity of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) |
β’ πΉ = (π MndRing π) & β’ π΄ = (Baseβπ) & β’ π = (π freeLMod π΄) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (0gβπ) = (0gβπΉ)) | ||
Theorem | mnring0g2d 42264 | The additive identity of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.) |
β’ πΉ = (π MndRing π) & β’ 0 = (0gβπ ) & β’ π΄ = (Baseβπ) & β’ (π β π β Ring) & β’ (π β π β π) β β’ (π β (π΄ Γ { 0 }) = (0gβπΉ)) | ||
Theorem | mnringmulrd 42265* | 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 42266 | 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 42267 | Obsolete version of mnringscad 42266 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 42268 | 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 42269 | Obsolete version of mnringvscad 42268 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 42270 | Monoid rings are left modules. (Contributed by Rohan Ridenour, 14-May-2024.) |
β’ πΉ = (π MndRing π) & β’ (π β π β Ring) & β’ (π β π β π) β β’ (π β πΉ β LMod) | ||
Theorem | mnringmulrvald 42271* | 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 42272 | Monoid rings are closed under multiplication. (Contributed by Rohan Ridenour, 14-May-2024.) |
β’ πΉ = (π MndRing π) & β’ π΅ = (BaseβπΉ) & β’ π΄ = (Baseβπ) & β’ Β· = (.rβπΉ) & β’ (π β π β Ring) & β’ (π β π β π) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π Β· π) β π΅) | ||
Theorem | gru0eld 42273 | A nonempty Grothendieck universe contains the empty set. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ (π β πΊ β Univ) & β’ (π β π΄ β πΊ) β β’ (π β β β πΊ) | ||
Theorem | grusucd 42274 | Grothendieck universes are closed under ordinal successor. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
β’ (π β πΊ β Univ) & β’ (π β π΄ β πΊ) β β’ (π β suc π΄ β πΊ) | ||
Theorem | r1rankcld 42275 | Any rank of the cumulative hierarchy is closed under the rank function. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ (π β π΄ β (π 1βπ )) β β’ (π β (rankβπ΄) β (π 1βπ )) | ||
Theorem | grur1cld 42276 | Grothendieck universes are closed under the cumulative hierarchy function. (Contributed by Rohan Ridenour, 8-Aug-2023.) |
β’ (π β πΊ β Univ) & β’ (π β π΄ β πΊ) β β’ (π β (π 1βπ΄) β πΊ) | ||
Theorem | grurankcld 42277 | Grothendieck universes are closed under the rank function. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
β’ (π β πΊ β Univ) & β’ (π β π΄ β πΊ) β β’ (π β (rankβπ΄) β πΊ) | ||
Theorem | grurankrcld 42278 | If a Grothendieck universe contains a set's rank, it contains that set. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
β’ (π β πΊ β Univ) & β’ (π β (rankβπ΄) β πΊ) & β’ (π β π΄ β π) β β’ (π β π΄ β πΊ) | ||
Syntax | cscott 42279 | Extend class notation with the Scott's trick operation. |
class Scott π΄ | ||
Definition | df-scott 42280* | 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 42281 | Equality theorem for the Scott operation. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
β’ (π β π΄ = π΅) β β’ (π β Scott π΄ = Scott π΅) | ||
Theorem | scotteq 42282 | Closed form of scotteqd 42281. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
β’ (π΄ = π΅ β Scott π΄ = Scott π΅) | ||
Theorem | nfscott 42283 | Bound-variable hypothesis builder for the Scott operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ β²π₯π΄ β β’ β²π₯Scott π΄ | ||
Theorem | scottabf 42284* | Value of the Scott operation at a class abstraction. Variant of scottab 42285 with a nonfreeness hypothesis instead of a disjoint variable condition. (Contributed by Rohan Ridenour, 14-Aug-2023.) |
β’ β²π₯π & β’ (π₯ = π¦ β (π β π)) β β’ Scott {π₯ β£ π} = {π₯ β£ (π β§ βπ¦(π β (rankβπ₯) β (rankβπ¦)))} | ||
Theorem | scottab 42285* | Value of the Scott operation at a class abstraction. (Contributed by Rohan Ridenour, 14-Aug-2023.) |
β’ (π₯ = π¦ β (π β π)) β β’ Scott {π₯ β£ π} = {π₯ β£ (π β§ βπ¦(π β (rankβπ₯) β (rankβπ¦)))} | ||
Theorem | scottabes 42286* | Value of the Scott operation at a class abstraction. Variant of scottab 42285 using explicit substitution. (Contributed by Rohan Ridenour, 14-Aug-2023.) |
β’ Scott {π₯ β£ π} = {π₯ β£ (π β§ βπ¦([π¦ / π₯]π β (rankβπ₯) β (rankβπ¦)))} | ||
Theorem | scottss 42287 | Scott's trick produces a subset of the input class. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ Scott π΄ β π΄ | ||
Theorem | elscottab 42288* | 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 42289 | scottex 9754 expressed using Scott. (Contributed by Rohan Ridenour, 9-Aug-2023.) |
β’ Scott π΄ β V | ||
Theorem | scotteld 42290* | The Scott operation sends inhabited classes to inhabited sets. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ (π β βπ₯ π₯ β π΄) β β’ (π β βπ₯ π₯ β Scott π΄) | ||
Theorem | scottelrankd 42291 | Property of a Scott's trick set. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ (π β π΅ β Scott π΄) & β’ (π β πΆ β Scott π΄) β β’ (π β (rankβπ΅) β (rankβπΆ)) | ||
Theorem | scottrankd 42292 | Rank of a nonempty Scott's trick set. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ (π β π΅ β Scott π΄) β β’ (π β (rankβScott π΄) = suc (rankβπ΅)) | ||
Theorem | gruscottcld 42293 | 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 42294 | Extend class notation with the collection operation. |
class (πΉ Coll π΄) | ||
Definition | df-coll 42295* | 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 (πΉ β {π₯}) | ||
Theorem | dfcoll2 42296* | Alternate definition of the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ (πΉ Coll π΄) = βͺ π₯ β π΄ Scott {π¦ β£ π₯πΉπ¦} | ||
Theorem | colleq12d 42297 | Equality theorem for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ (π β πΉ = πΊ) & β’ (π β π΄ = π΅) β β’ (π β (πΉ Coll π΄) = (πΊ Coll π΅)) | ||
Theorem | colleq1 42298 | Equality theorem for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ (πΉ = πΊ β (πΉ Coll π΄) = (πΊ Coll π΄)) | ||
Theorem | colleq2 42299 | Equality theorem for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ (π΄ = π΅ β (πΉ Coll π΄) = (πΉ Coll π΅)) | ||
Theorem | nfcoll 42300 | Bound-variable hypothesis builder for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023.) |
β’ β²π₯πΉ & β’ β²π₯π΄ β β’ β²π₯(πΉ Coll π΄) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |