Add part of sticks and stones (need help with dv condition #4254

metakunt · 2024-09-27T18:22:28Z

I am trying to prove the sticks and stones formula.
However sadly there seems to be a distinct variable condition that I can't get rid of sadly.

Could someone guide me which part of my proof is messed up? I would be very thankful for that.

metakunt · 2024-09-27T18:30:40Z

In particular, there seems to be a unliked dv condition on both the A and the I. This way I can't even do eqid to satisfy both.
I'd like to get rid of the dv conditions: A f and I z, since otherwise I can't use eqid to satisfy them.

All other dv appear to be fine.

icecream17 · 2024-09-27T18:33:10Z

You can just have this be a lemma, and another lemma use cbv* theorems instead of eqid

For example, https://us.metamath.org/mpeuni/etransc.html works even with $d I i n $. in https://us.metamath.org/mpeuni/etransclem48.html

metakunt · 2024-09-27T18:47:24Z

So is this proof fine as is or is there a grave mistake that still needs fixing?

icecream17 · 2024-09-28T01:33:30Z

I wouldn't say there's a grave mistake since it's perfectly usable... but I took a look at the actual proof to try to find a more definitive answer about whether the dvs can be removed.

First I minimized the proof

Then it looks like the dv on f, A can be removed using elab2 on step 68

...
67:66:ralrimiva                   |- ( ph -> A. f e. A ( f : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) )
68:63,67,53:rspcdva              |- ( ph -> ( X : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( X ` x ) < ( X ` y ) ) ) )

becomes

d8:63,52:elab2g                    |- ( X e. A -> ( X e. A <-> ( X : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( X ` x ) < ( X ` y ) ) ) ) )
d4:53,d8:syl                      |- ( ph -> ( X e. A <-> ( X : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( X ` x ) < ( X ` y ) ) ) ) )
68:53,d4:mpbid         |- ( ph -> ( X : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( X ` x ) < ( X ` y ) ) ) )

For $d I z the only thing I can think of is to add a cbv* within the proof, which ofc makes it longer...

175:56,105:eqeltrid   |- ( ph -> I e. { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } )

d18::fveq2         |- ( z = w -> ( X ` z ) = ( X ` w ) )
d19::fveq2         |- ( z = w -> ( Y ` z ) = ( Y ` w ) )
d17:d18,d19:neeq12d |- ( z = w -> ( ( X ` z ) =/= ( Y ` z ) <-> ( X ` w ) =/= ( Y ` w ) ) )
n1:d17:cbvrabv |- { z e. ( 1 ... K ) | ( X ` z ) =/= ( Y ` z ) } = { w e. ( 1 ... K ) | ( X ` w ) =/= ( Y ` w ) }

n2:175,n1:eleqtrdi |- ( ph -> I e. { w e. ( 1 ... K ) | ( X ` w ) =/= ( Y ` w ) } )

d14::fveq2         |- ( w = I -> ( X ` w ) = ( X ` I ) )
d15::fveq2         |- ( w = I -> ( Y ` w ) = ( Y ` I ) )
d13:d14,d15:neeq12d |- ( w = I -> ( ( X ` w ) =/= ( Y ` w ) <-> ( X ` I ) =/= ( Y ` I ) ) )
179:d13:elrab3      |- ( I e. ( 1 ... K ) -> ( I e. { w e. ( 1 ... K ) | ( X ` w ) =/= ( Y ` w ) } <-> ( X ` I ) =/= ( Y ` I ) ) )

So the result is (edit: second minimize):

    $d I j w x y $.  $d K f j w x y $.  $d K z $.  $d N a f $.  $d X f j x y $.
    $d X w z $.  $d Y f x y $.  $d Y j w z $.  $d ph a j $.
    sticksstones1.1 $e |- ( ph -> N e. NN ) $.
    sticksstones1.2 $e |- ( ph -> K e. NN0 ) $.
    sticksstones1.3 $e |- A = { f | ( f : ( 1 ... K ) --> ( 1 ... N ) /\ A. x
    e. ( 1 ... K ) A. y e. ( 1 ... K )
    ( x < y -> ( f ` x ) < ( f ` y ) ) ) } $.
    sticksstones1.4 $e |- ( ph -> X e. A ) $.
    sticksstones1.5 $e |- ( ph -> Y e. A ) $.
    sticksstones1.6 $e |- ( ph -> X =/= Y ) $.
    sticksstones1.7 $e |- I = inf ( { z e. ( 1 ... K ) |
     ( X ` z ) =/= ( Y ` z ) } , RR , < ) $.
    $( Different strictly monotone functions have different ranges.
       (Contributed by metakunt, 27-Sep-2024.) $)
    sticksstones1 $p  |- ( ph -> ran X =/= ran Y ) $=
      ( clt wcel vj vw cfv wbr crn wne wa wnel wfun cdm c1 cfz co wf cv wi wral
      wb wceq feq1 fveq1 breq12d imbi2d 2ralbidv anbi12d elab2g syl mpbid ffund
      simpld crab cr cinf ssrab2 wor cfn c0 wss ltso a1i wn nne wfn ffnd adantr
      syl2an2r syldbl2 fz1ssnn nnssre sstri sseldi eqeltrid eleqtrrd fvelrn w3a
      cn fdmd 3ad2ant1 simp3 ffvelrnd elfznn nnred wo cle syl2anc fveq2 neeq12d
      imp sylib 3expa 3adantl2 simprd simpl3 breq1 breq1d imbi12d breq2d rspc2v
      breq2 mpd ltned necomd neeq1d adantl mpbird simpl2 lttrd 3ad2ant3 lttri4d
      gtned mpjao3dan neneqd ralrimiva wrex ralnex nnel fvelrnb syl5bb elnelne1
      con1bid fzfid rabeq0 ralbii eqfnfv biimprd sylan2b mteqand sstrid fiinfcl
      ssfid bitri syl13anc simp2 3ad2ant2 ltnled infrefilb eqbrtrid mtand ianor
      3expia elrab xchnxbir imor sylibr mpdan eqbrtrrd cbvrabv eleqtrdi eqbrtrd
      elrab3 lttri2d mpjaodan ) AGJUCZGKUCZSUDZJUEZKUEZUFZUVNUVMSUDZAUVOUGZUVMU
      VPTZUVMUVQUHZUVRAJUIUVOGJUJZTZUWAAUKHULUMZUKIULUMZJAUWEUWFJUNZBUOZCUOZSUD
      ZUWHJUCZUWIJUCZSUDZUPZCUWEUQBUWEUQZAJETZUWGUWOUGZOAUWPUWPUWQUROUWEUWFFUOZ
      UNZUWJUWHUWRUCZUWIUWRUCZSUDZUPZCUWEUQBUWEUQZUGZUWQFJEEUWRJUSZUWSUWGUXDUWO
      UWEUWFUWRJUTUXFUXCUWNBCUWEUWEUXFUXBUWMUWJUXFUWTUWKUXAUWLSUWHUWRJVAUWIUWRJ
      VAVBVCVDVENVFVGVHZVJZVIAUWDUVOAGUWEUWCAGDUOZJUCZUXIKUCZUFZDUWEVKZVLSVMZUW
      ERAUXMUWEUXNUXLDUWEVNZAVLSVOZUXMVPTZUXMVQUFUXMVLVRZUXNUXMTUXPAVSVTAUWEUXM
      AUKHUUAUXMUWEVRAUXOVTUUJZAUXMVQJKQUXMVQUSZAUXJUXKUSZDUWEUQZJKUSZUXTUXLWAZ
      DUWEUQUYBUXLDUWEUUBUYDUYADUWEUXJUXKWBUUCUUKAUYBUYCAUYBUGUYCUYBAJUWEWCZUYB
      KUWEWCZUYCUYBURAUWEUWFJUXHWDZAUYFUYBAUWEUWFKAUWEUWFKUNZUWJUWHKUCZUWIKUCZS
      UDZUPZCUWEUQBUWEUQZAKETZUYHUYMUGZPAUYNUYNUYOURPUXEUYOFKEEUWRKUSZUWSUYHUXD
      UYMUWEUWFUWRKUTUYPUXCUYLBCUWEUWEUYPUXBUYKUWJUYPUWTUYIUXAUYJSUWHUWRKVAUWIU
      WRKVAVBVCVDVENVFVGVHZVJZWDZWEDUWEJKUUDWFUUEWGUUFUUGAUXMUWEVLUXOUWEVLVRAUW
      EWPVLHWHWIWJZVTUUHZVLUXMSUUIUULZWKWLZAUWEUWFJUXHWQWMWEGJWNWFUVTUAUOZKUCZU
      VMUSZWAZUAUWEUQZUWBUVTVUGUAUWEUVTVUDUWETZUGVUEUVMAUVOVUIVUEUVMUFZAUVOVUIW
      OZVUDGSUDZVUJVUDGUSZGVUDSUDZVUKVULUGZVUEUVMVUKVUEVLTZVULVUKVUEUWFTZVUPVUK
      UWEUWFVUDKAUVOUYHVUIUYRWRAUVOVUIWSWTVUQVUEVUEIXAXBVGZWEVUOVUDJUCZVUEUVMSA
      VUIVULVUSVUEUSZUVOAVUIVULVUTAVUIVULWOZVUIVUTAVUIVULUUMVVAVUIUGVUSVUEUFZWA
      ZVUTVVAVUIVVCVVAVUIWAVVCXCZVUIVVCUPVVAVUDUXMTZWAVVDVVAVVEGVUDXDUDZVVAVULV
      VFWAAVUIVULWSVVAVUDGVVAVUDVUIAVUDWPTZVULVUDHXAZUUNXBAVUIGVLTZVULAUWEVLGUY
      TVUCWKZWRUUOVHVVAVVEUGGUXNVUDXDRVVAVVEUXNVUDXDUDZVVAUXRUXQVVEVVKUPAVUIUXR
      VULVUAWRAVUIUXQVULUXSWRUXRUXQVVEVVKVUDUXMUUPUUTXEXHUUQUURVUIVVBUGVVDVVEVU
      IVVBUUSUXLVVBDVUDUWEUXIVUDUSUXJVUSUXKVUEUXIVUDJXFUXIVUDKXFXGUVAUVBXIVUIVV
      CUVCUVDXHVUSVUEWBXIUVEXJZXKVUKVULVUSUVMSUDZVUOUWOVULVVMUPZVUKUWOVULAUVOUW
      OVUIAUWGUWOUXGXLZWRWEVUOVUIGUWETZUWOVVNUPAUVOVUIVULXMVUKVVPVULAUVOVVPVUIV
      UCWRZWEUWNVVNVUDUWISUDZVUSUWLSUDZUPBCVUDGUWEUWEUWHVUDUSZUWJVVRUWMVVSUWHVU
      DUWISXNZVVTUWKVUSUWLSUWHVUDJXFXOXPUWIGUSZVVRVULVVSVVMUWIGVUDSXSZVWBUWLUVM
      VUSSUWIGJXFXQXPXRXEXTWGUVFYAVUKVUMUGZVUJUVNUVMUFZVWDUVMUVNVUKUVMUVNUFZVUM
      AUVOVWFVUIAGUBUOZJUCZVWGKUCZUFZUBUWEVKZTZVWFAGUXMVWKAGUXNUXMRVUBWLUXLVWJD
      UBUWEUXIVWGUSUXJVWHUXKVWIUXIVWGJXFUXIVWGKXFXGUVGUVHAVVPVWLVWFURVUCVWJVWFU
      BGUWEVWGGUSVWHUVMVWIUVNVWGGJXFVWGGKXFXGUVJVGVHZWRWEYBVUMVUJVWEURVUKVUMVUE
      UVNUVMVUDGKXFYCYDYEVUKVUNUGZUVMVUEVUKUVMVLTZVUNAUVOVWOVUIAUWFVLUVMUWFWPVL
      IWHWIWJZAUWEUWFGJUXHVUCWTWKZWRWEZVWNUVMUVNVUEVWRVUKUVNVLTZVUNAUVOVWSVUIAU
      WFVLUVNVWPAUWEUWFGKUYRVUCWTWKZWRWEVUKVUPVUNVURWEAUVOVUIVUNYFVUKVUNUVNVUES
      UDZVWNUYMVUNVXAUPZVUKUYMVUNAUVOUYMVUIAUYHUYMUYQXLZWRWEVUKVVPVUNVUIUYMVXBU
      PVVQAUVOVUIVUNXMUYLVXBGUWISUDZUVNUYJSUDZUPBCGVUDUWEUWEUWHGUSZUWJVXDUYKVXE
      UWHGUWISXNZVXFUYIUVNUYJSUWHGKXFXOXPUWIVUDUSZVXDVUNVXEVXAUWIVUDGSXSZVXHUYJ
      VUEUVNSUWIVUDKXFXQXPXRWFXTWGYGYJVUKVUDGVUKVUDVUIAVVGUVOVVHYHXBAUVOVVIVUIV
      VJWRYIYKXJYLYMAVUHUWBURUVOVUHVUFUAUWEYNZWAAUWBVUFUAUWEYOAUWBVXJUWBWAUVMUV
      QTZAVXJUVMUVQYPAUYFVXKVXJURUYSUAUWEUVMKYQVGYRYTYRWEVHUVMUVPUVQYSXEAUVSUGZ
      UVNUVQTZUVNUVPUHZUVRAKUIUVSGKUJZTZVXMAUWEUWFKUYRVIAVXPUVSAGUWEVXOVUCAUWEU
      WFKUYRWQWMWEGKWNWFVXLVUSUVNUSZWAZUAUWEUQZVXNVXLVXRUAUWEVXLVUIUGVUSUVNAUVS
      VUIVUSUVNUFZAUVSVUIWOZVULVXTVUMVUNVYAVULUGZVUSUVNVYAVUSVLTZVULVYAVUSVYAVU
      SUWFTVUSWPTVYAUWEUWFVUDJAUVSUWGVUIUXHWRAUVSVUIWSWTVUSIXAVGXBZWEVYBVUSVUEU
      VNSAVUIVULVUTUVSVVLXKVYAVULVUEUVNSUDZVYBUYMVULVYEUPZVYAUYMVULAUVSUYMVUIVX
      CWRWEVYBVUIVVPUYMVYFUPAUVSVUIVULXMVYAVVPVULAUVSVVPVUIVUCWRZWEUYLVYFVVRVUE
      UYJSUDZUPBCVUDGUWEUWEVVTUWJVVRUYKVYHVWAVVTUYIVUEUYJSUWHVUDKXFXOXPVWBVVRVU
      LVYHVYEVWCVWBUYJUVNVUESUWIGKXFXQXPXRXEXTWGUVIYAVYAVUMUGZVXTVWFVYIUVNUVMVY
      AVWSVUMAUVSVWSVUIVWTWRZWEAUVSVUIVUMYFYJVUMVXTVWFURVYAVUMVUSUVMUVNVUDGJXFY
      CYDYEVYAVUNUGZUVNVUSVYAVWSVUNVYJWEZVYKUVNUVMVUSVYLVYAVWOVUNAUVSVWOVUIVWQW
      RWEVYAVYCVUNVYDWEAUVSVUIVUNYFVYAVUNUVMVUSSUDZVYKUWOVUNVYMUPZVYAUWOVUNAUVS
      UWOVUIVVOWRWEVYAVVPVUNVUIUWOVYNUPVYGAUVSVUIVUNXMUWNVYNVXDUVMUWLSUDZUPBCGV
      UDUWEUWEVXFUWJVXDUWMVYOVXGVXFUWKUVMUWLSUWHGJXFXOXPVXHVXDVUNVYOVYMVXIVXHUW
      LVUSUVMSUWIVUDJXFXQXPXRWFXTWGYGYJVYAVUDGVYAVUDVUIAVVGUVSVVHYHXBAUVSVVIVUI
      VVJWRYIYKXJYLYMAVXSVXNURUVSVXSVXQUAUWEYNZWAAVXNVXQUAUWEYOAVXNVYPVXNWAUVNU
      VPTZAVYPUVNUVPYPAUYEVYQVYPURUYGUAUWEUVNJYQVGYRYTYRWEVHVXMVXNUGUVQUVPUVNUV
      QUVPYSYBXEAVWFUVOUVSXCVWMAUVMUVNVWQVWTUVKVHUVL $.

Sidenote: It seems like the mmj2 error gives the diff while the metamath-knife error just gives The file './discouraged' needs to be regenerated.

I think the former looks nicer even though they're equivalent

glacode · 2024-09-28T09:27:45Z

You can just have this be a lemma, and another lemma use cbv* theorems instead of eqid

I agree.

To make it "more usable", the

$d A f
$d I z

constraints should be removed.

IMHO, in general, a good approach is to use the "true" proof as a lemma, and the last theorem to be just an external "wrapper" that minimizes the $d condition (it would play a role similar to a FOL metatheorem that proofs which are the non-free variables)

metakunt · 2024-09-28T10:20:07Z

Alright, that helps me much. That means I can keep dv conditions as long as I want to keep the proofs shorter and just remove them in the last step with cbv* theorems.

Did I understand that correctly?

metakunt · 2024-09-28T10:28:21Z

My first proof had

    sticksstones1.7 $e |- I = inf ( { x e. ( 1 ... K ) |
     ( X ` x ) =/= ( Y ` x ) } , RR , < ) $.

and I thought I had to rewrite the whole proof since in my opinion that's where the original dv conditions came from.
In my mind the issues were that I've used the x both in the definition of I and in the definition of A and that they leaked into each other.
Then I rewrote it and figured out that that didn't remove the dv conditions. By then my heart sunk a little bit since I've already spent like 10 hours writing this proof. But it's nice to know that definitional hypotheses like A = ... can be either satisfied with eqid or the corresponding cbv* + eq theorems.

You always learn something new.

icecream17 · 2024-09-28T17:06:29Z

set.mm

+ sticksstones4.4 $e |- A = { f | ( f : ( 1 ... K ) --> ( 1 ... N ) /\ A. x
+ e. ( 1 ... K ) A. y e. ( 1 ... K )
+ ( x < y -> ( f ` x ) < ( f ` y ) ) ) } $.
+ $( Equinumerosity lemma for sticks and stones .) (Contributed by metakunt,


Suggested change

$( Equinumerosity lemma for sticks and stones .) (Contributed by metakunt,

$( Equinumerosity lemma for sticks and stones. (Contributed by metakunt,

this is probably still a draft, but I'll note this typo

Should be fixed now

Actually the theorem I've wanted to prove is proven, it can be reviewed now

glacode · 2024-09-28T20:48:20Z

Alright, that helps me much. That means I can keep dv conditions as long as I want to keep the proofs shorter and just remove them in the last step with cbv* theorems.

Did I understand that correctly?

Yes, I like to keep theorems as "general" as possible, thus if $d statements are unnecessary I prefer to add one more final theorem, just to remove them.
It only takes another theorem using your theorem, to pay for it.
Otherwise, if two theorems will use your theorem, they would both have to do the same cbv* dance, instead of a simple eqid.

metakunt · 2024-09-28T21:58:04Z

Understood, the final theorem will have its dv's removed. For now there will be certainly more steps with dv's and I'd like to carry them so that each lemma does not have to do cbv* applications.

I'm also quite happy to hear that you can't mess up with distinct variables that much. I always was scared of them since they could impact future theorem use. But since you can change them that problem disappeared.

icecream17 · 2024-09-29T00:23:19Z

set.mm

+ ${
+ syldbl2.1 $e |- ( ( ph /\ ps ) -> ( ps -> th ) ) $.
+ $( Stacked hypotheseis implies goal. (Contributed by Stanislas Polu,
+ 9-Mar-2020.) $)
+ syldbl2 $p |- ( ( ph /\ ps ) -> th ) $=
+ ( wa com12 anabsi7 ) ABCABEBCDFG $.
+ $}
+


This theorem would be anabsi3, as anabsi* (5, 6, 7, 8) commuted is presumably (1, 2, 3, 4), but this is arguably not really an improvement. So just a comment, not a suggestion.

Yeah those renaming commits should be done in a separate pr. I've just moved the theorem because mmj2 autofilled it for me. This is actually how most theorems that I move are getting moved to main. MMJ2 autofills it and I get too lazy to find a different route because it is usually the shortest.

I think we should give theorems which are moved to main adequate and hopefully final names. That's why we have (besides other reasons) the column "New" in changes-set.txt. If we defer the renaming to future PRs, this will easily be forgotten.

metakunt · 2024-09-29T12:42:55Z

Minor generalisation from NN to NN0, surprisingly it was just 2 lines that I had to change. This allows me to have the hypotheses ( A e. Fin ) instead of ( A e. Fin /\ A =/= (/) ) once I move to monoid generators. I thought to do it in the next pr after this is merged, however the change is quite minimal and it's best to clean it up immediately.

Also do we have the fundamental theorem of arithmetic over a polynomial ring over a Field or UFD? I likely need it in the following form. Consider a set of irreducibles ( in our case linear factors) that are not associate to each other.
It will be something like S= ( x, x-1, x-2, ...) and show that for any mapping f: S -> NN0 the product of

$$\prod_{s\in S} s^{f(s)}$$

is distinct. Basically two different mappings $f$ and $g$ lead to different polynomials $R[X]$

icecream17 · 2024-09-30T12:13:23Z

It doesn't look like there's any addition there, so I'm confused on how it translates to polynomials, so I'm assuming you meant sum.

If I understand correctly, this is indirectly equivalent to showing the ring homomorphism https://us.metamath.org/mpeuni/evlrhm.html is one-to-one, which hasn't been proven yet.

The definitions are rather complicated so here's how polynomials work:
Multivariate polynomials are functions ((variables --> exponents) --> coefficients), the evaluation homomorphism maps this to a function ((variables --> assignments) --> evaluationOfPolynomial)

metakunt · 2024-09-30T16:31:46Z

No it is the product. Essentially S will be a finite set of irreducible nonassociated linear factors of $$K[X]$$ and n will be the sum of the degrees while k will be the size of S.

Essentially I want to show that two factorisations of polynomials are equal if the exponent of their irreducibles are equal.
This is true for any Polynomial ring over an UFD, but in the case of $$K$$ being a field this follows since $$K[X]$$ is euclidean.

Basically this is the fundamental theorem of arithmetic for polynomials.

You can interpret this for natural numbers as follows. S is a finite set of primes and $$a,b\in A$$ are two distinct such mappings. Then

$$\prod_{p\in S}p^{a(p)} \neq \prod_{p\in S}p^{b(p)}$$

https://en.wikipedia.org/wiki/Unique_factorization_domain I need this basically, for either $$K[X]$$ or $$R[X]$$.

icecream17 · 2024-09-30T20:31:39Z

Unfortunately, it seems like https://us.metamath.org/mpeuni/df-ufd.html is only used (recursively) by isufd, so we definitely haven't reached that far.

Actually, we have a division algorithm for singlevariable polynomials, but nothing about factors of multivariate polynomials, as far as I can tell.

avekens · 2024-09-30T20:33:35Z

set.mm

+ fvelrn lttri4d simp3 sseli simprd simpl3 breq1 breq1d breq2 breq2d rspc2v
+ 3ad2ant1 imbi12d mpd cle sylib 3expa 3adantl2 ltned necomd neeq1d 3jaodan
+ simpl2 lttrd neneqd wrex ralnex nnel fvelrnb bitrd con1bid elnelne1 fzfid
+ wor ltso ssrab2 ssfi rabeq0 ralbii cab wal abeq2 spi biimpi eqfnfv bicomd


Why is ~abeq used here? It's usage is discouraged. Why not use ~abeqw instead?

I needed a theorem to unfold the class abstraction. Not knowing which theorems to use I used the mmj2 search feature and searched on the website. This was surprisingly the only theorem I've found in mmj2.

I've conjectured that this is the only theorem that unfolds the definition and by the time I did the merge request I've figured that the theorem may not be that straightforward to change. Then I've looked at the axioms and pretty much concluded that I am using all of those axioms anyways.

Honestly I wouldn't mind refactoring it but it is very likely that my theorems are going to use the full suite of predicate calculus axioms anyways.
https://us.metamath.org/mpeuni/fvelrnb.html is used in the first theorem that uses all axioms that sticksstones1 uses and https://us.metamath.org/mpeuni/hashf1rn.html in sticksstones2.

So I don't even get any smaller axiom footprint in the final theorem.

To be fair most of my workflow comes from the point that MMJ2 autofills. I am not checking discouraged or mathbox theorems before opening a pr, so by the time it hits it is usually too late.

I guess for the future I will use elab2g, now that I know that alternatives exist to unfold the theorem.

If that's fine I'd like to keep things as is, as my workspace is currently dirty with other theorems.

@metakunt thank you for these explanations. It looks like the problem is not using this theorem, but the tag "(New usage is discouraged.)" within the comment of ~abeq2. The usage of this theorem should only be discouraged in proofs which become dependent on more axioms using ~abeq2 instead of ~abeq2w, but this does not seem to be the case here. Unfortunately, we cannot distinguish between a general discouragement and a specific discouragement for axiom usage.

Since ~abeq2 cannot simply be replaced by ~abeq2w in a proof (probably the bound variable has to be changed for that, and this blows up the proof unnecessarily). Therefore, I propose to remove the tag "(New usage is discouraged.)" from the comment of ~abeq2. It is absolutely correct to use this theorem in the proofs of high level theorems. @GinoGiotto, @benjub what's your opinion? Maybe other theorems of this kind are also concerned.

@GinoGiotto, @benjub what's your opinion? Maybe other theorems of this kind are also concerned.

Yes, I'd remove the tag. Proving theorems is already difficult enough. We don’t need to make it harder by restricting the use of axioms that are still common in the database. I think it's fine to let people prove theorems whatever way they want and optimize those proofs later.

I agree, remove the discouragement tag from ~abeq2. The reason to avoid ~abeq2 does exist but it is not strong enough to put the tag.

Note: a standard format for these tags is:

(* Blabla. (Contributed by XX, 11-Jan-2024.) [Brief explanation why proof modification is discouraged.] (Proof modification is discouraged). [Brief indication why new usage is discouraged.] Use ~ xxx instead. (New usage is discouraged.) $)

Mnemonic why tags are in that order (when both are present): you prove a result before you can use it.

I have removed the discouragement tag.

avekens · 2024-09-30T20:33:58Z

set.mm

+ sticksstones2 $p |- ( ph -> F : A -1-1-> B ) $=
+ ( cfv wceq wcel clt vi vj vb vs vr wf cv wi wral wa wf1 crn chash cfz cpw
+ c1 co crab fveqeq2 cfn fzfid wbr eleq1w feq1 fveq1 breq12d imbi2d ralbidv
+ wb anbi12d bibi12d cab wal abeq2 spi chvarvv biimpi adantl simpld sselpwd


PS: I think that MMJ2 only showed me abeq2 because it has no hypotheses, it tends to show me theorems in closed form.

metakunt added 2 commits September 27, 2024 20:20

Add part of sticks and stones

ab1bb78

Format

339f1bf

metakunt added 4 commits September 27, 2024 20:57

Regen discouraged

3cee380

Add injectivity

30f9d43

regen

4db18ed

typo

c030ed4

metakunt added 3 commits September 28, 2024 18:38

Add equinumerosity lemma

8cfed8c

Fix whitespace

d1cfe60

inc functions cardinality

33ac48f

icecream17 reviewed Sep 28, 2024

View reviewed changes

fix typo

41c0626

icecream17 reviewed Sep 29, 2024

View reviewed changes

icecream17 approved these changes Sep 29, 2024

View reviewed changes

Generalise proofs on nn0 instead of nn

dbe9e70

avekens reviewed Sep 30, 2024

View reviewed changes

Merge branch 'develop' into ststone

88cbe7f

metakunt added 3 commits October 1, 2024 22:33

remove discouraged frome abeq2

696a405

more closure properties

f674701

typo

957894b

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add part of sticks and stones (need help with dv condition #4254

Add part of sticks and stones (need help with dv condition #4254

metakunt commented Sep 27, 2024

metakunt commented Sep 27, 2024

icecream17 commented Sep 27, 2024 •

edited

Loading

metakunt commented Sep 27, 2024

icecream17 commented Sep 28, 2024 •

edited

Loading

glacode commented Sep 28, 2024

metakunt commented Sep 28, 2024

metakunt commented Sep 28, 2024

icecream17 Sep 28, 2024

metakunt Sep 28, 2024

metakunt Sep 28, 2024

glacode commented Sep 28, 2024 •

edited

Loading

metakunt commented Sep 28, 2024

icecream17 Sep 29, 2024

metakunt Sep 29, 2024

avekens Sep 30, 2024

metakunt commented Sep 29, 2024 •

edited

Loading

icecream17 commented Sep 30, 2024

metakunt commented Sep 30, 2024

icecream17 commented Sep 30, 2024 •

edited

Loading

avekens Sep 30, 2024

metakunt Sep 30, 2024

avekens Oct 1, 2024

GinoGiotto Oct 1, 2024

benjub Oct 1, 2024

metakunt Oct 1, 2024

avekens Sep 30, 2024

metakunt Sep 30, 2024

	$( Equinumerosity lemma for sticks and stones .) (Contributed by metakunt,
	$( Equinumerosity lemma for sticks and stones. (Contributed by metakunt,

Add part of sticks and stones (need help with dv condition #4254

Are you sure you want to change the base?

Add part of sticks and stones (need help with dv condition #4254

Conversation

metakunt commented Sep 27, 2024

metakunt commented Sep 27, 2024

icecream17 commented Sep 27, 2024 • edited Loading

metakunt commented Sep 27, 2024

icecream17 commented Sep 28, 2024 • edited Loading

glacode commented Sep 28, 2024

metakunt commented Sep 28, 2024

metakunt commented Sep 28, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

glacode commented Sep 28, 2024 • edited Loading

metakunt commented Sep 28, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

metakunt commented Sep 29, 2024 • edited Loading

icecream17 commented Sep 30, 2024

metakunt commented Sep 30, 2024

icecream17 commented Sep 30, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

icecream17 commented Sep 27, 2024 •

edited

Loading

icecream17 commented Sep 28, 2024 •

edited

Loading

glacode commented Sep 28, 2024 •

edited

Loading

metakunt commented Sep 29, 2024 •

edited

Loading

icecream17 commented Sep 30, 2024 •

edited

Loading