---

Step * 1 1 5 3 of Lemma rng-pps_wf

.....subterm..... T:t
1:n
1. r : IntegDom{i}@i'
2. eq : EqDecider(|r|)
3. ∀p:ℕ3 ⟶ |r|. (¬(p = 0 ∈ (ℕ3 ⟶ |r|)) ∈ 𝕌{[1 | i 0]})
4. a : ℕ3 ⟶ |r|@i
5. ¬(a = 0 ∈ (ℕ3 ⟶ |r|))
6. ∀p:ℕ3 ⟶ |r|. (¬(p = 0 ∈ (ℕ3 ⟶ |r|)) ∈ 𝕌{[1 | i 0]})
7. b : ℕ3 ⟶ |r|@i
8. ¬(b = 0 ∈ (ℕ3 ⟶ |r|))
9. _ : ∃l:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} . ((¬¬((a . l) = 0 ∈ |r|)) ∧ (¬((b . l) = 0 ∈ |r|)))@i
10. _1 : ¬((b . (a x b)) = 0 ∈ |r|)@i
⊢ Ax ∈ False
BY
{ (Fold `scalar-triple-product` (-1)
   THEN (RWO "scalar-triple-product-symmetry" (-1) THENA Auto)
   THEN Unfold `scalar-triple-product` -1
   THEN (RWW "cross-product-same" (-1) THENA Auto)
   THEN D -1
   THEN Auto) }

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  r  :  IntegDom\{i\}@i'
2.  eq  :  EqDecider(|r|)
3.  \mforall{}p:\mBbbN{}3  {}\mrightarrow{}  |r|.  (\mneg{}(p  =  0)  \mmember{}  \mBbbU{}\{[1  |  i  0]\})
4.  a  :  \mBbbN{}3  {}\mrightarrow{}  |r|@i
5.  \mneg{}(a  =  0)
6.  \mforall{}p:\mBbbN{}3  {}\mrightarrow{}  |r|.  (\mneg{}(p  =  0)  \mmember{}  \mBbbU{}\{[1  |  i  0]\})
7.  b  :  \mBbbN{}3  {}\mrightarrow{}  |r|@i
8.  \mneg{}(b  =  0)
9.  $_{}$  :  \mexists{}l:\{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\}  .  ((\mneg{}\mneg{}((a  .  l)  =  0))  \mwedge{}  (\mneg{}((b  .  l)  =  0)))@i
10.  $_{1}$  :  \mneg{}((b  .  (a  x  b))  =  0)@i
\mvdash{}  Ax  \mmember{}  False


By

---

Latex:
(Fold  `scalar-triple-product`  (-1)
  THEN  (RWO  "scalar-triple-product-symmetry"  (-1)  THENA  Auto)
  THEN  Unfold  `scalar-triple-product`  -1
  THEN  (RWW  "cross-product-same"  (-1)  THENA  Auto)
  THEN  D  -1
  THEN  Auto)

---

Home Index