Sketchy looking proof shortening

[Kyle Wyonch]

Hello all,

I was practicing some proof shortening skills and I came across this proof for cnfex that accomplishes it in 2 steps rather than the original 20,

Original: 

$d f y J $.  $d f y K $.

cnfex $p |- ( ( J e. Top /\ K e. Top ) -> ( J Cn K ) e. _V ) $=

      ( vf vy ctop wcel wa co cuni cvv ctopon cfv wceq eqid jctr istopon sylibr

      cv syl2an uniexg ccn ccnv cima wral cmap crab cnfval wf cab mapvalg mapex

      syl2anr eqeltrd rabexg syl ) AEFZBEFZGZABUAHZCRZUBDRUCAFDBUDZCBIZAIZUEHZUFZJUPAVCKLFZBVBKLFZUSVEMUQUPUPVCVCMZGVFUPVHVCNOVCAPQUQUQVBVBMZGVGUQVIVBNOVBBPQDCABVCVBUGSURVDJFVEJFURVDVCVBUTUHCUIZJUQVBJFZVCJFZVDVJMUPBETZAETZVBVCJJCUJULUPVLVKVJJFUQVNVMVCVBJJCUKSUMVACVDJUNUOUM $.

Shortened:

cnfex $p |- ( ( J e. Top /\ K e. Top ) -> ( J Cn K ) e. _V ) $=

    ( ccn co cvv wcel ctop wa ovex a1i ) ABCDEFAGFBGFHABCIJ $.

I was wondering if this shortening was valid, as it gets rid of the two dummy variables originally used, and just seems too good to be true for an originally, fairly large proof.

Can anyone comment on whether this shortening is valid?  At least Metamath seems to think so.

Thanks,

[andrew sauer]

It is certainly valid as long as ovex is valid. In Metamath the result of any function evaluated on a class is a set, as shown by fvex, so this extends to operations as well, no matter how complicated. It seems the original proof unnecessarily expanded on the meaning of Cn, when its use as an operation was sufficient to complete the proof.

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/f756107b-2a48-47a3-a0e6-9a590f4ed0cdn%40googlegroups.com.

[Jim Kingdon]

On 4/21/21 5:37 PM, Kyle Wyonch wrote:

> I was wondering if this shortening [of cnfex] was valid

Short answer is, yes it is valid.

The longer answer is that set.mm defines a function evaluated outside
its domain to be the empty set which is why
http://us.metamath.org/mpeuni/fvex.html does not have any conditions.

By contrast, iset.mm does not have the ability to do quite this, so
instead cnfex would need to use
http://us.metamath.org/ileuni/funfvex.html or one of the other
alternatives under fvex at http://us.metamath.org/ileuni/mmil.html#setmm

There is some discussion of this in the "undefined results" section of
http://us.metamath.org/mpeuni/conventions.html and
http://us.metamath.org/ileuni/conventions.html

[Mario Carneiro]

It is a bit of a strange theorem. I see that it is in Glauco's mathbox (and referenced a few times), and both the proof and the uses can be simplified using ovex, but perhaps there is something that they were trying to avoid (not axioms, the axiom list is a strict subset with the new proof). Perhaps they can chime in here.

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/c36661f8-ac06-7264-2dd8-d95a1cb1b41f%40panix.com.

[Glauco]

Did I really write it? :-)

It looks like I wrote it when I was proving the Stone Weierstrass theorem, and that's been my first theorem in mm.

Back then, the whole framework was new to me, and I guess that the (sad) simple explanation is that I didn't know I was just one a1i away from ovex.

Thanks for the post, added to the refactor/cleanup mathbox to-do list.

Glauco

[Kyle Wyonch]

Thanks everyone!

Glauco, if you are interested, I was able to shorten 3 other proofs in your mathbox, they are: n0p (339 to 330 bytes), unima (412 to 79 bytes), and nelrnresa (87 to 58 bytes), all of them rely on the same, or a subset of the axioms originally used.  Let me know if you want to see them and I will post them here!

[Glauco]

Sure, please.

As a side note, I (as everybody else, in this forum) keep adding small theorems that could be used to shorten proofs I wrote before.

When I find myself writing three times the same 5 line proof, then I decide to extract a theorem, and almost certainly it could be used to shorten a dozen of my previous theorems, but it's hard to go back and find/rewrite them all.

But cnfex is simply useless :-)

[Kyle Wyonch]

The three shortened proofs are as follows,

n0p:

n0p $p |- ( ( P e. ( Poly ` ZZ ) /\ N e. NN0 /\ ( ( coeff ` P ) ` N ) =/= 0 ) -> P =/= 0p ) $=

    ( cz cply cfv wcel cn0 ccoe cc0 wne w3a c0p wceq wn neneq 3ad2ant3 wa eqtrd

    csn cxp fveq2 coe0 a1i fveq1d adantlr c0ex fvconst2 ad2antlr 3adantl3 mtand

    adantl neqned ) ACDEFZBGFZBAHEZEZIJZKZALURALMZUPIMZUQUMUTNUNUPIOPUMUNUSUTUQ

    UMUNQUSQUPBGISTZEZIUMUSUPVBMZUNUSVCUMUSBUOVAUSUOLHEZVAALHUAVDVAMUSUBUCRUDUK

    UEUNVBIMUMUSGIBUFUGUHRUIUJUL $.

unima:

unima $p |- ( ( F Fn A /\ B C_ A /\ C C_ A ) -> ( F " ( B u. C ) ) = 

    ( ( F " B ) u. ( F " C ) ) ) $=

    ( wfn wss w3a cun cima imaundi eqidd syl5eq ) DAEBAFCAFGZDBCHIDBIDCIHZNDB

      CJMNKL $.

(oops I meant nelrnres, not nelrnresa):

nelrnres $p |- ( -. A e. ran B -> -. A e. ran ( B |` C ) ) $=

     ( cres crn wcel rnresss sseli con3i ) ABCDEZFABEZFJKABCGHI $.

You will notice that n0p, nelrnres have the same axioms, and the unima isn't dependent on axiom-9, or df-eu anymore.

Thanks,

[Benoit]

When I find myself writing three times the same 5 line proof, then I decide to extract a theorem, and almost certainly it could be used to shorten a dozen of my previous theorems, but it's hard to go back and find/rewrite them all.

It's not that hard: place your new theorem as early as possible in set.mm, and then run the script in the github repository "scripts/min.cmd". The file itself contains a comment explaining how to use it.

Benoît

[Norman Megill]

There are several possibilities for defining out-of-domain behavior of function values. We chose the empty set in large part because it is very convenient to have function values exist unconditionally (fvex and consequently ovex).
Another possibility is to define out-of-domain function value to be the universe _V, which has the advantage of providing us with a simple test (sethood) to determine whether we are using the function outside of its domain. Alexander van der Vekens studied an alternate function value definition with this property; see df-afv and associated theorems in his mathbox.

There is a certain philosophical elegance to the df-afv approach that I can appreciate, but from a practical point of view the drawback is that proofs that a function value exists would be significantly longer. The long proof of cnfex (whose author had presumably overlooked ovex) actually illustrates this point nicely - this is the kind of thing we would have to do frequently if we used a function value definition whose out-of-domain behavior evaluated to _V. The unconditional fvex and ovex are used 2783 and 1913 times respectively in set.mm. With df-afv, the size of set.mm would grow considerably and would make function value existence a major part of many otherwise short proofs, obscuring the more important parts of the proof.

There was a discussion of df-afv in this thread:
https://groups.google.com/g/metamath/c/cteNUppB6A4/m/1qv4j6wyAgAJ

Norm