Jon, you're on the right track but this looks overly difficult. The key
property is "associativity of convex combinations", which means that if a
point P is a convex combination of B and C, and Q is a convex combination
of A and P, then Q is a convex combination of A, B, C (and you can easily
compute the coefficients), and conversely, if a point Q is a convex
combination of A, B, C, then there exists a point P which is a convex
combination of B and C such that Q is convex combination of A and Q (again,
easily computable coefficients).
The thing is that these easy algebraic computations are cumbersome in
metamath. I just proved bj-bary1: it shows that given two distinct points
A, B in an affine line (here, the complex line), any point X has unique
normalized barycentric coordinates ("normalized" in the sense of "summing
to 1"), with the given expressions. One could do the same in two
dimensions (starting with three non-collinear points A, B, C); it would be
a bit easier (and sufficient for our purpose) to restrict to real
coefficients: the expression of the coefficients is then a bit easier, and
their positivity is seen to be equivalent to the positivity of the vector
products I mentioned above (e.g. AB vec AX).
As a warmup for the equivalence of positivity, you could prove in metamath
the following: if A < B are real numbers, then
[A, B] = { x | E. s e. RR E. t e. RR ( s >= 0 /\ t >= 0 /\ s + t = 1 /\ x
= sA + tB ) }
>From the expressions in bj-bary1, you see that t >= 0 if and only if x >= A
and s >= 0 if and only if x <= B. In two dimensions, it will be the same:
one of the three barycentric coordinates will be positive if and only if
the corresponding vector product is positive (this corresponds to the point
X being in a half-plane).
Honestly, I think that the approach you are following is not the best since
it's too coordinate-dependent. The correct way to prove these areas would
be to first prove that area is invariant under displacements (rotations,
translations, reflections), so that you can then suppose that your triangle
has one vertex at (0, 0), one at (a, 0) with a > 0, and the third at (b, c)
with c > 0, and then its area is ac/2. Obviously, the invariance under
displacements is much harder to prove, but this is the correct way to go.
Benoit
--
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/b1dd4fd0-d7a6-495e-8177-349d6aa8488b%40googlegroups.com.
