---

Step * 2 2 1 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. |p,q,r@0| = 0 ∈ |r|
⊢ |r@0,p,q| = 0 ∈ |r|
BY
{ (RWO "scalar-triple-product-symmetry" 0 THEN Auto) }

---

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.  |p,q,r@0|  =  0
\mvdash{}  |r@0,p,q|  =  0


By

---

Latex:
(RWO  "scalar-triple-product-symmetry"  0  THEN  Auto)

---

Home Index