---

Step * 1 1 1 2 1 1 1 1 1 2 of Lemma cross-product-non-zero-implies


1. i : ℕ3
2. r : IntegDom{i}
3. ∀x,y:|r|.  Dec(x = y ∈ |r|)
4. a : ℕ3 ⟶ |r|
5. b : ℕ3 ⟶ |r|
6. ¬(a = 0 ∈ (ℕ3 ⟶ |r|))
7. ¬(b = 0 ∈ (ℕ3 ⟶ |r|))
8. ∀a:ℕ3 ⟶ |r|. ((¬(a = 0 ∈ (ℕ3 ⟶ |r|))) ⇒ (∃i:ℕ3. (¬((a i) = 0 ∈ |r|))))
9. ∀x,y:|r|.  ((x +r (-r y)) = 0 ∈ |r| ⇐⇒ x = y ∈ |r|)
10. ¬((a i) = 0 ∈ |r|)
11. ¬((b i) = 0 ∈ |r|)
12. ¬((b i*a) = (a i*b) ∈ (ℕ3 ⟶ |r|))
13. j : ℕ3
14. ¬(((b i) * (a j)) = ((a i) * (b j)) ∈ |r|)
15. ¬(i = j ∈ ℤ)
⊢ ((a . λx.if (x =z i) then a j if (x =z j) then -r (a i) else 0 fi ) = 0 ∈ |r|)
∧ (¬((b . λx.if (x =z i) then a j if (x =z j) then -r (a i) else 0 fi ) = 0 ∈ |r|))
BY
{ (RepeatFor 2 (MoveToConcl (-1))
   THEN (RWO "scalar-product-3" 0 THENA Auto)
   THEN Reduce 0
   THEN (OnVar `i' IntSegCases THEN Reduce 0)
   THEN OnVar `j' IntSegCases
   THEN Reduce 0
   THEN GenConclTerms Auto [⌜a 0⌝;⌜a 1⌝;⌜a 2⌝;⌜b 0⌝;⌜b 1⌝;⌜b 2⌝]⋅
   THEN (D 0 THENA Auto)
   THEN (RWO "9<" (-1) THENA Auto)
   THEN (D 0 THENA Auto)
   THEN Try ((D -1 THEN Fold `member` 0 THEN MemCD))
   THEN (D 0 THENL [(RW CRngNormC 0 THEN Auto); (ParallelOp -2 THEN RW CRngNormC (-1) THEN Auto)])) }

---

Latex:

---

Latex:

1.  i  :  \mBbbN{}3
2.  r  :  IntegDom\{i\}
3.  \mforall{}x,y:|r|.    Dec(x  =  y)
4.  a  :  \mBbbN{}3  {}\mrightarrow{}  |r|
5.  b  :  \mBbbN{}3  {}\mrightarrow{}  |r|
6.  \mneg{}(a  =  0)
7.  \mneg{}(b  =  0)
8.  \mforall{}a:\mBbbN{}3  {}\mrightarrow{}  |r|.  ((\mneg{}(a  =  0))  {}\mRightarrow{}  (\mexists{}i:\mBbbN{}3.  (\mneg{}((a  i)  =  0))))
9.  \mforall{}x,y:|r|.    ((x  +r  (-r  y))  =  0  \mLeftarrow{}{}\mRightarrow{}  x  =  y)
10.  \mneg{}((a  i)  =  0)
11.  \mneg{}((b  i)  =  0)
12.  \mneg{}((b  i*a)  =  (a  i*b))
13.  j  :  \mBbbN{}3
14.  \mneg{}(((b  i)  *  (a  j))  =  ((a  i)  *  (b  j)))
15.  \mneg{}(i  =  j)
\mvdash{}  ((a  .  \mlambda{}x.if  (x  =\msubz{}  i)  then  a  j  if  (x  =\msubz{}  j)  then  -r  (a  i)  else  0  fi  )  =  0)
\mwedge{}  (\mneg{}((b  .  \mlambda{}x.if  (x  =\msubz{}  i)  then  a  j  if  (x  =\msubz{}  j)  then  -r  (a  i)  else  0  fi  )  =  0))


By

---

Latex:
(RepeatFor  2  (MoveToConcl  (-1))
  THEN  (RWO  "scalar-product-3"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  (OnVar  `i'  IntSegCases  THEN  Reduce  0)
  THEN  OnVar  `j'  IntSegCases
  THEN  Reduce  0
  THEN  GenConclTerms  Auto  [\mkleeneopen{}a  0\mkleeneclose{};\mkleeneopen{}a  1\mkleeneclose{};\mkleeneopen{}a  2\mkleeneclose{};\mkleeneopen{}b  0\mkleeneclose{};\mkleeneopen{}b  1\mkleeneclose{};\mkleeneopen{}b  2\mkleeneclose{}]\mcdot{}
  THEN  (D  0  THENA  Auto)
  THEN  (RWO  "9<"  (-1)  THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  Try  ((D  -1  THEN  Fold  `member`  0  THEN  MemCD))
  THEN  (D  0  THENL  [(RW  CRngNormC  0  THEN  Auto);  (ParallelOp  -2  THEN  RW  CRngNormC  (-1)  THEN  Auto)]))

---

Home Index