Step * of Lemma r2-det-is-dot-product

[a,b,c:ℝ^2].  (|abc| b⋅λi.if (i =z 0) then -(c 1) else fi )
BY
(Auto
   THEN RepUR ``r2-det real-vec-sub dot-product`` 0
   THEN (RWO "rsum-split-first" 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