---

Step * 2 2 1 of Lemma rng-pps_wf


1. r : IntegDom{i}@i'
2. eq : EqDecider(|r|)
3. BasicProjectiveGeometryAxioms(rng-pps(r;eq))
4. p : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} @i
5. q : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} @i
6. r@0 : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} @i
7. s : ∃l:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} . ((¬¬((p . l) = 0 ∈ |r|)) ∧ (¬((q . l) = 0 ∈ |r|)))@i
8. s1 : ∃l:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} . ((¬¬((q . l) = 0 ∈ |r|)) ∧ (¬((r@0 . l) = 0 ∈ |r|)))@i
9. ¬((r@0 . (p x q)) = 0 ∈ |r|)
⊢ ¬((p . (q x r@0)) = 0 ∈ |r|)
BY
{ (Fold `scalar-triple-product` (-1) THEN Fold `scalar-triple-product` 0 THEN ParallelLast) }

1
1. r : IntegDom{i}@i'
2. eq : EqDecider(|r|)
3. BasicProjectiveGeometryAxioms(rng-pps(r;eq))
4. p : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} @i
5. q : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} @i
6. r@0 : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} @i
7. s : ∃l:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} . ((¬¬((p . l) = 0 ∈ |r|)) ∧ (¬((q . l) = 0 ∈ |r|)))@i
8. s1 : ∃l:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} . ((¬¬((q . l) = 0 ∈ |r|)) ∧ (¬((r@0 . l) = 0 ∈ |r|)))@i
9. |p,q,r@0| = 0 ∈ |r|
⊢ |r@0,p,q| = 0 ∈ |r|

---

Latex:

---

Latex:

1.  r  :  IntegDom\{i\}@i'
2.  eq  :  EqDecider(|r|)
3.  BasicProjectiveGeometryAxioms(rng-pps(r;eq))
4.  p  :  \{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\}  @i
5.  q  :  \{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\}  @i
6.  r@0  :  \{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\}  @i
7.  s  :  \mexists{}l:\{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\}  .  ((\mneg{}\mneg{}((p  .  l)  =  0))  \mwedge{}  (\mneg{}((q  .  l)  =  0)))@i
8.  s1  :  \mexists{}l:\{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\}  .  ((\mneg{}\mneg{}((q  .  l)  =  0))  \mwedge{}  (\mneg{}((r@0  .  l)  =  0)))@i
9.  \mneg{}((r@0  .  (p  x  q))  =  0)
\mvdash{}  \mneg{}((p  .  (q  x  r@0))  =  0)


By

---

Latex:
(Fold  `scalar-triple-product`  (-1)  THEN  Fold  `scalar-triple-product`  0  THEN  ParallelLast)

---

Home Index