---

Step * 1 1 6 2 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. _ : ∃a@0:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} . ((¬¬((a@0 . a) = 0 ∈ |r|)) ∧ (¬((a@0 . b) = 0 ∈ |r|)))@i
10. _1 : ¬(((a x b) . a) = 0 ∈ |r|)@i
⊢ Ax ∈ False
BY
{ ((RWO "scalar-product-comm" (-1) THENA Auto)
   THEN 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{}a@0:\{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\}  .  ((\mneg{}\mneg{}((a@0  .  a)  =  0))  \mwedge{}  (\mneg{}((a@0  .  b)  =  \000C0)))@i
10.  $_{1}$  :  \mneg{}(((a  x  b)  .  a)  =  0)@i
\mvdash{}  Ax  \mmember{}  False


By

---

Latex:
((RWO  "scalar-product-comm"  (-1)  THENA  Auto)
  THEN  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