---

Step * 2 3 1 1 of Lemma rng-pps_wf


1. r : IntegDom{i}@i'
2. eq : EqDecider(|r|)
3. BasicProjectiveGeometryAxioms(rng-pps(r;eq))
4. triangle-axiom1(rng-pps(r;eq))
5. p : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} @i
6. q : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} @i
7. l : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} @i
8. m : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} @i
9. s : ∃l:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} . ((¬¬((p . l) = 0 ∈ |r|)) ∧ (¬((q . l) = 0 ∈ |r|)))@i
10. s1 : ∃a:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} . ((¬¬((a . l) = 0 ∈ |r|)) ∧ (¬((a . m) = 0 ∈ |r|)))@i
11. ¬((p . l) = 0 ∈ |r|)
12. ¬((q . m) = 0 ∈ |r|)
13. ¬¬((p . m) = 0 ∈ |r|)
14. ¬¬((q . l) = 0 ∈ |r|)
15. ((l x m) . (p x q)) = 0 ∈ |r|
⊢ False
BY
{ ((∀h:hyp. (SupposeMore h THENA Auto)  THEN (RWO "scalar-product-comm" (-1) THENA Auto))
   THEN (RWW "Binet-Cauchy-identity -2 -3" (-1) THENA Auto)
   ) }

1
1. r : IntegDom{i}@i'
2. eq : EqDecider(|r|)
3. BasicProjectiveGeometryAxioms(rng-pps(r;eq))
4. triangle-axiom1(rng-pps(r;eq))
5. p : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} @i
6. q : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} @i
7. l : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} @i
8. m : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} @i
9. s : ∃l:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} . ((¬¬((p . l) = 0 ∈ |r|)) ∧ (¬((q . l) = 0 ∈ |r|)))@i
10. s1 : ∃a:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} . ((¬¬((a . l) = 0 ∈ |r|)) ∧ (¬((a . m) = 0 ∈ |r|)))@i
11. ¬((p . l) = 0 ∈ |r|)
12. ¬((q . m) = 0 ∈ |r|)
13. (p . m) = 0 ∈ |r|
14. (q . l) = 0 ∈ |r|
15. (((p . l) * (q . m)) +r (-r (0 * 0))) = 0 ∈ |r|
⊢ False

---

Latex:

---

Latex:

1.  r  :  IntegDom\{i\}@i'
2.  eq  :  EqDecider(|r|)
3.  BasicProjectiveGeometryAxioms(rng-pps(r;eq))
4.  triangle-axiom1(rng-pps(r;eq))
5.  p  :  \{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\}  @i
6.  q  :  \{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\}  @i
7.  l  :  \{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\}  @i
8.  m  :  \{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\}  @i
9.  s  :  \mexists{}l:\{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\}  .  ((\mneg{}\mneg{}((p  .  l)  =  0))  \mwedge{}  (\mneg{}((q  .  l)  =  0)))@i
10.  s1  :  \mexists{}a:\{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\}  .  ((\mneg{}\mneg{}((a  .  l)  =  0))  \mwedge{}  (\mneg{}((a  .  m)  =  0)))@i
11.  \mneg{}((p  .  l)  =  0)
12.  \mneg{}((q  .  m)  =  0)
13.  \mneg{}\mneg{}((p  .  m)  =  0)
14.  \mneg{}\mneg{}((q  .  l)  =  0)
15.  ((l  x  m)  .  (p  x  q))  =  0
\mvdash{}  False


By

---

Latex:
((\mforall{}h:hyp.  (SupposeMore  h  THENA  Auto)    THEN  (RWO  "scalar-product-comm"  (-1)  THENA  Auto))
  THEN  (RWW  "Binet-Cauchy-identity  -2  -3"  (-1)  THENA  Auto)
  )

---

Home Index