[tirix]

As proposed in #5416 , this changes the definition of EEhil (df-ehl) to use 0-based indices, and converts theorems depending on that definition. The index set is changed from ( 1 ... N ) to ( 0 ..^ N ).

This is only part one of two, the next step would be to do the same for EE (df-ee).

One theorem is moved to main from my mathbox, f1od2.
Theorems in @avekens's mathbox related to line-sphere intersections have been updated.
Theorem eenglngeehlnm unfortunately needed to be temporarily commented out, since it refers both to EEHil and EEG, and the former has been converted, but not yet the latter. That theorem should be available again once the conversion is complete.

---

This is D0 on the DALIA scale: No AI was used.

[benjub]

Thanks for this work !

I see that you chose the idiom ( 0 ..^ 2 ) instead of { 0 , 1 }. Both have their pros and cons but I haven't looked into details and I rely on your judgment for that choice.

[tirix]

Some additional nodes on design choices, especially regarding @avekens's sections about the plane:

• the original theorems used the pair { 1 , 2 } as the index set. I chose to keep ( 0 ..^ 2 ) rather than { 0 , 1 } because it clearly makes the dimension 2 appear and keeps the general format ( 0 ..^ N ) at the price of minimally longer proofs.
• wherever the original theorems used the two-value function { <. 1 , X >. , <. 2 , Y >. }, I've used two-symbol words <" X Y ">, called doubletons in set.mm. I think this is where this refactoring shines, as the new expression is much shorter and much more readable.

I originally meant to include those notes in the initial comment but forgot them yesterday.

It is true that the choice ( 0 ..^ 2 ) is somewhat arbitrary, and we could also have kept { 0 , 1 }. I'm open to other proposals, especially coming from @avekens whose mathbox those theorems reside in.

[avekens]

Great job, a lot of work! Only one (minor) remark.
And don't forget to transform my appreciated ~eenglngeehlnm in a subsequent PR ;-)

[avekens]

ehl2eudisval0.0 $e |- .0. = <" 0 0 "> $.?

[jkingdon]

Seems like a nice way to write it (not blocking for this pull request, I wouldn't think, but something to think about).

[tirix]

Oh, yes, very good idea!

[jkingdon]

Seems like this is ready to merge once @tirix resolves the merge conflicts.