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,
On Thursday, April 22, 2021 at 3:00:40 PM UTC-4 Glauco wrote:
> 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 :-)
>
> Il giorno giovedì 22 aprile 2021 alle 20:16:37 UTC+2 [email protected]
> ha scritto:
>
>> 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!
>>
>> On Thursday, April 22, 2021 at 1:43:51 PM UTC-4 Glauco wrote:
>>
>>> 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
>>>
>>> Il giorno giovedì 22 aprile 2021 alle 04:15:04 UTC+2 [email protected]
>>> ha scritto:
>>>
>>>> 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.
>>>>
>>>> On Wed, Apr 21, 2021 at 9:48 PM Jim Kingdon <[email protected]> wrote:
>>>>
>>>>> 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
>>>>>
>>>>> --
>>>>> 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 [email protected].
>>>>>
>>>> To view this discussion on the web visit
>>>>> https://groups.google.com/d/msgid/metamath/c36661f8-ac06-7264-2dd8-d95a1cb1b41f%40panix.com
>>>>> .
>>>>>
>>>>
--
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 [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/384f98c4-1f40-45fb-89c1-d57edcada2b9n%40googlegroups.com.
