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
>
> 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
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
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
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.
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
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
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
