Permresults

[metakunt]

God this was such a pain to prove.....

[metakunt]

Whew, proving that B is a union of three disjoint functions by hand, congrats brainstorming how to make proving this easier

It seems like Metamath is particularly unsuited for "unsophisticated" "brute force" proofs where there are multiple disjoint subparts. Now that I think about it in this meta way, Metamath proofs that use some kind of "builder" theorems are much easier... I tried to think of a way to "build" the if, but I don't see a way that's faster than what you did, other than straight out using https://us.metamath.org/mpeuni/mmtheorems139.html#mm13862b, proving permbuilders for each relevant function, and a final domain hack that makes the function go from 1 to M instead of 0 to M

Not sure how my advice here would've applied to fsuppind though.

Honestly, that wasn't even the hardest part. What really, really made me desperate was proving that

( ( \{ 1,\dots,i-1\} \cup \{i,\dots,m-1\})\cup\{m\}) = \{1,\dots,m\}

I thought that would be one of the easier theorems, but it was actually the hardest. Honestly I've tried two approaches, one with A https://us.metamath.org/mpeuni/metakunt14.html , where I've used https://us.metamath.org/mpeuni/2fvidf1od.html , and a different one with B. Safe to say, they broke me both in different ways.

I suspect I might be doing something horribly wrong, but I don't know what it is yet.

[metakunt]

Whew, proving that B is a union of three disjoint functions by hand, congrats brainstorming how to make proving this easier

It seems like Metamath is particularly unsuited for "unsophisticated" "brute force" proofs where there are multiple disjoint subparts. Now that I think about it in this meta way, Metamath proofs that use some kind of "builder" theorems are much easier... I tried to think of a way to "build" the if, but I don't see a way that's faster than what you did, other than straight out using https://us.metamath.org/mpeuni/mmtheorems139.html#mm13862b, proving permbuilders for each relevant function, and a final domain hack that makes the function go from 1 to M instead of 0 to M

Not sure how my advice here would've applied to fsuppind though.

Ah just wait until I get to the point where I have to do distinction by 22 cases.

[icecream17]

fzsplit ($k := i - 1$) and fzsuc ($n := m - 1$) would seem to neatly fit here

---

If distinction by 22 cases is actually necessary please explain it first so that we may find a better solution 😅

[metakunt]

Ah crap, well I've missed that one.

To be fair, there is no other easier way. You need to split the set into 3 sets, each of those you need to split 3 more times, 2 of those sets you need to split twice again. That gives you 11 sets. That calculation you then need to do twice. You also need existence of three different values to make the calculation, as in

( ph -> A e. NN )
( ph -> B e. NN )
( ph -> C e. NN )
( ph -> A =/= B )
( ph -> B =/= C  )
( ph -> A =/= C  )

and you need to check whether a given condition holds on each of those sets.

[icecream17]

Incidentally, why does the calculation have to be done twice?

[metakunt]

You are constructing two sets based of three indices a,b,c where set 1 depends on index a and b and set 2 depends on index a and c. Then you split the base set up in 11 small parts that depend on all three. Now you need to argue whether the a property in the set holds or not. In general those are arbitrary maps but in my specific case there is some stucture. But you still need to verify that the property holds for each of these sets. There are 11 sets as they are chosen in a way such that most cancel out and the other are balanced in a delicate way that they cancel out by a different argument. So far I am not even close to even stating the theorem as I need to construct the final permutation first.

[tirix]

If what you have to prove is symmetric in a/b and b/c, you're probably better off making it a lemma and proving it only once, so I suppose it's not?

[metakunt]

Well the argument isn't that complex as for most of the sets the image is the same. For some of those the argument is equivalent, but some are the same by a different argument. And some are just plain different and have to be handled in a different way. But I am still far away from this theorem, I haven't even defined the main permutation yet, and that one is going to be doozy. I conjecture I am only at 20% of the progress and I will take a little bit of time off before I tackle it.