Step
*
of Lemma
r2-det-is-dot-product
∀[a,b,c:ℝ^2].  (|abc| = a - b⋅λi.if (i =z 0) then -(c - b 1) else c - b 0 fi )
BY
{ (Auto
   THEN RepUR ``r2-det real-vec-sub dot-product`` 0
   THEN (RWO "rsum-split-first" 0 THENA Auto)
   THEN Reduce 0
   THEN RWO "rsum-single" 0
   THEN Reduce 0
   THEN Auto) }
Latex:
Latex:
\mforall{}[a,b,c:\mBbbR{}\^{}2].    (|abc|  =  a  -  b\mcdot{}\mlambda{}i.if  (i  =\msubz{}  0)  then  -(c  -  b  1)  else  c  -  b  0  fi  )
By
Latex:
(Auto
  THEN  RepUR  ``r2-det  real-vec-sub  dot-product``  0
  THEN  (RWO  "rsum-split-first"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  RWO  "rsum-single"  0
  THEN  Reduce  0
  THEN  Auto)
Home
Index