det_2D: THEORY
%------------------------------------------------------------------------------
%
% 2-Dimensional Determinant of two vectors (aka 2D-cross product)
%
%
%------------------------------------------------------------------------------
BEGIN

  IMPORTING vectors_2D,
            perpendicular_2D

  u,v,w   : VAR Vect2
  k       : VAR real
  nzu,nzv : VAR Nz_vect2

  det(u,v): real = u`x*v`y - u`y*v`x

  det_zero_left  : LEMMA det(zero,v) = 0

  det_zero_right : LEMMA det(u,zero) = 0

  det_eq_0       : LEMMA det(u,u) = 0

  det_scal_left  : LEMMA det(k*u,v) = k*det(u,v)
  det_scal_right : LEMMA det(u,k*v) = k*det(u,v)
  
  det_add_left   : LEMMA det(u+v,w) = det(u,w) + det(v,w)
  det_add_right  : LEMMA det(w,u+v) = det(w,u) + det(w,v)

  det_sub_left   : LEMMA det(u-v,w) = det(u,w) - det(v,w)
  det_sub_right  : LEMMA det(w,u-v) = det(w,u) - det(w,v)

  det_symm  : LEMMA det(u,v) = det(-u,-v)
  det_asym  : LEMMA det(u,v) = -det(v,u)

  det_symm_0 : LEMMA det(u,v) = 0 IFF det(v,u) = 0

  sq_det    : LEMMA sq(det(u,v)) = sqv(v)*sqv(u) - sq(u*v)

  det_norm  : LEMMA det(u,v) <= norm(u)*norm(v)

  det_perpR : LEMMA det(u,v) = u*perpR(v)
  det_perpL : LEMMA det(u,v) = perpL(u)*v

  dot_perpR  : LEMMA u*v = -det(u,perpR(v))
  dot_perpL  : LEMMA u*v = -det(perpL(u),v)

  perpR_dot : LEMMA perpR(u)*v = -det(u,v)
  perpL_dot : LEMMA u*perpL(v) = -det(u,v)

  det_dot_0 : LEMMA
    det(nzu,nzv) = 0 IMPLIES nzu*nzv /= 0 

  AUTO_REWRITE+ det_eq_0

END det_2D