Hi Benoit, nice idea to start a new thread to talk about this stuff. This is an answer to you too Theirry :)
The goals I have been working towards with this area of a triangle stuff are 1. supporting Heron <http://us.metamath.org/mpeuni/heron.html>'s theorem and 2. working towards Pick's theorem from the 100 list, however that is supposedly very hard <https://www.cl.cam.ac.uk/~jrh13/papers/pick.pdf> so it's a long way off. So far I have done areaquad <http://us.metamath.org/mpegif/areaquad.html>, to explain how it works look at the left image here <https://i.imgur.com/CvuWUQl.png>. It says given a quadrilateral with sides parallel to the y-axis the area is 1/2 x. (F + E - (D + C)) x. (B - A), where those are all just single real numbers, for example the top left vertex is at (A,F) e. RR^2. If you have the situation where one side is 0 length, for example E = C, then this reduces to area = 1/2 x. (F - C) x. (B - A), which is 1/2 x. base x. height as expected. If you look at the right diagram you can see how any triangle can be expressed as two of these quads connected together. For this shape we get, I think, 1/2 x. (W - Y) x. (R - P). This is a slightly odd result and not how areas of triangles are usually expressed. My guess would be it would be good to take this result and then change it into a more familiar form. I think the way area is expressed in Heron is quite natural, where the area of triangle is basically the cross product, |A||B|sin theta where A and B are two of the sides as vectors and theta is the angle between them. Benoit I like your way of using barycentric coordinates to express the interior of the triangle, that is quite elegant. I am not sure how to fit it into this scheme though, if you look at U and V in areaquad <http://us.metamath.org/mpegif/areaquad.html> those are the upper and lower lines of the quad and defining things parallel to the y axis makes the area calculation much easier. I was imagining continuing to use that definition but with more pieces, having the left part and the right part of the triangle defined separately, however I am aware of how inelegant that is. Thierry I hope I have answered some questions about what the final formula would look like. I am sorry I don't understand your triangle formulation here <https://groups.google.com/d/msg/metamath/DDN4noc0TYU/1bs81kSoAwAJ>, I think maybe you are using cross product somewhere? I like the idea of starting with just 3 complex numbers, that has a nice feel to it, and is the same as Heron. In general I really like working collaboratively so I am grateful for all the help so far and if anyone wants to collaborate on moving these things forward I would like that, I am not so strong in metamath in general. :) -- 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/bc0b60d6-ea00-4847-8f02-b9fa96e349f6%40googlegroups.com.
