// verify the ET and EF axioms over a Euclidean field.

u,v,w,p,q  will be 2-vectors
a,b,c   will be scalars
(a,b)  is a vector


Axioms:

neg(a = 0) -> a*i(a) = 1
i(a)*a = 1
1*a = a
a*1 = a
0*a = 0
a*0 = 0
a*(b*c) = (a*b)*c
a*b = b*a
a+0=a
0+a = a
a + (-a) = 0
a+b = b+a
a+(b+c) = (a+b)+c
a*(b+c) = a*b + a*c
(a+b)*c = a*c + b*c

a < b & b < c -> a < c
neg(a < a)
0 < a ->  sqrt(a) * sqrt(a) = a
0 < a -> 0 < sqrt(a)
0 < a & 0 < b -> 0 < a+b
0 < a & 0 < b -> 0 < a*b

Definitions

a-b = a + (-b)
(a,b)+(c,d) = (a+c,b+d)
(a,b)-(c,d) = (a-c,b-d)
dot((a,b),(c,d)) = a*c + b*d
cross((a,b),(c,d)) = a*d-b*c
abs((a,b)) = sqrt(a*a + b*b)
area(p,q,r) = i(2) * abs(cross(p-q,r-q))
dsq((a,b),(c,d)) =  (c-a)*(c-a),(d-b)*(d-b)
d(p,q) = sqrt(dsq(p,q))

Theorems
a*(b-c) = a*b-a*c
(a-b)*c = a*c - b*c
(a-b)*c = a*c-b*c
a - (b+c) = (a-b)-c
a - (b-c) = a-b+c
-(-a) = a
a-(-b) = a+b

ETpermutation

area(p,q,r) = area(q,r,p)
Proof:
    Let p = (a,b), q = (c,d), r = (e,f).
    Then cross(p-q,r-q) = cross((a,b)-(c,d),(e,f)-(c,d))
                        = cross((a-c,b-d),(e-c,f-d))
                        = (a-c)*(f-d)-(b-d)*(e-c) 
                        = (a-c)*f - (a-c)*d - ((b-d)*e - (b-d)*c)
                        = (a-c)*f - (a-c)*d  -(b-d)*e + (b-d)*c
                        = a*f -c*f - (a*d -c*d) -(b*e-d*e) + b*c-d*c
                        = a*f-c*f-a*d+c*d -b*e +d*e + b*c-d*c
                        = a*f-c*f-a*d -b*e +d*e + b*c +c*d -d*c
                        = a*f-c*f-a*d -b*e +d*e + b*c  +c*d - c*d
                        = a*f-c*f-a*d -b*e +d*e + b*c  + 0
                        = a*f-c*f-a*d -b*e +d*e + b*c 
    and
         cross(q-r,p-r) = cross((c,d)-(e,f),(a,b)-(e,f)) 
                         = cross((c-e,d-f),(a-e,b-f))
                         = (c-e)*(b-f)-(d-f)*(a-e)
                         = c*b-e*b -c*f+e*f - d*a + d*e+f*a-f*e
                         = b*c-b*e -c*f +e*f -a*d + d*e + a*f - f*e
                         = b*c- b*e - c*f - a*d + d*e + a*f + e*f - f*e 
                          =b*c- b*e - c*f - a*d + d*e + a*f + (e*f-f*e)
                          =b*c- b*e - c*f - a*d + d*e + a*f  + 0
                          = b*c- b*e - c*f + a*d + d*e + a*f
                          = a*f-c*f -a*d -b*e+d*e+b*c 
                         = cross(p-q,r-q)
    Hence area(p,q,r) area(q,r,p)