---

Step * 2 3 1 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. (((p . l) * (q . m)) +r (-r (0 * 0))) = 0 ∈ |r|
⊢ False
BY
{ (RW RngNormC (-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)) = 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.  (p  .  m)  =  0
14.  (q  .  l)  =  0
15.  (((p  .  l)  *  (q  .  m))  +r  (-r  (0  *  0)))  =  0
\mvdash{}  False


By

---

Latex:
(RW  RngNormC  (-1)  THENA  Auto)

---

Home Index