---

Step * of Lemma scalar-triple-product-as-det

No Annotations
∀[r:CRng]. ∀[a,b,c:ℕ3 ⟶ |r|].  (|a,b,c| = |λi.[a; b; c][i]| ∈ |r|)
BY
{ (Auto
   THEN (Assert λi.[a; b; c][i] ∈ Matrix(3;3;r) BY
               (Unfold `matrix` 0 THEN Auto))
   THEN (RWO "matrix-det-is-determinant" 0 THENA Auto)
   THEN RepUR ``scalar-triple-product scalar-product cross-product`` 0
   THEN Unfold `determinant` 0
   THEN RepeatFor 2 (((RWO "primrec-unroll" 0 THENA Auto) THEN Reduce 0))
   THEN RepUR ``rng_sum mon_itop`` 0
   THEN RepeatFor 4 ((RecUnfold `itop` 0 THEN Reduce 0))
   THEN RepUR ``isEven matrix-ap matrix-minor modulus`` 0
   THEN ((Assert ∀x,y:|r|.  ((x * (-r y)) = (-r (x * y)) ∈ |r|) BY
                Auto)
         THEN (Assert ∀x:|r|. ((0 +r x) = x ∈ |r|) BY
                     Auto)
         THEN (Assert ∀x:|r|. ((x * 1) = x ∈ |r|) BY
                     Auto))
   THEN (RWW  "-1 -2 -3" 0 THENA Auto)
   THEN RepeatFor 2 (EqCDA)
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[r:CRng].  \mforall{}[a,b,c:\mBbbN{}3  {}\mrightarrow{}  |r|].    (|a,b,c|  =  |\mlambda{}i.[a;  b;  c][i]|)


By

---

Latex:
(Auto
  THEN  (Assert  \mlambda{}i.[a;  b;  c][i]  \mmember{}  Matrix(3;3;r)  BY
                          (Unfold  `matrix`  0  THEN  Auto))
  THEN  (RWO  "matrix-det-is-determinant"  0  THENA  Auto)
  THEN  RepUR  ``scalar-triple-product  scalar-product  cross-product``  0
  THEN  Unfold  `determinant`  0
  THEN  RepeatFor  2  (((RWO  "primrec-unroll"  0  THENA  Auto)  THEN  Reduce  0))
  THEN  RepUR  ``rng\_sum  mon\_itop``  0
  THEN  RepeatFor  4  ((RecUnfold  `itop`  0  THEN  Reduce  0))
  THEN  RepUR  ``isEven  matrix-ap  matrix-minor  modulus``  0
  THEN  ((Assert  \mforall{}x,y:|r|.    ((x  *  (-r  y))  =  (-r  (x  *  y)))  BY
                            Auto)
              THEN  (Assert  \mforall{}x:|r|.  ((0  +r  x)  =  x)  BY
                                      Auto)
              THEN  (Assert  \mforall{}x:|r|.  ((x  *  1)  =  x)  BY
                                      Auto))
  THEN  (RWW    "-1  -2  -3"  0  THENA  Auto)
  THEN  RepeatFor  2  (EqCDA)
  THEN  Auto)

---

Home Index