---

Step * 2 3 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))
⊢ triangle-axiom2(rng-pps(r;eq))
BY
{ (RepUR ``triangle-axiom2`` 0 THEN UnfoldpGeoAbbreviations 0 THEN 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|)
⊢ ¬(((l x m) . (p x q)) = 0 ∈ |r|)

---

Latex:

---

Latex:

1.  r  :  IntegDom\{i\}@i'
2.  eq  :  EqDecider(|r|)
3.  BasicProjectiveGeometryAxioms(rng-pps(r;eq))
4.  triangle-axiom1(rng-pps(r;eq))
\mvdash{}  triangle-axiom2(rng-pps(r;eq))


By

---

Latex:
(RepUR  ``triangle-axiom2``  0  THEN  UnfoldpGeoAbbreviations  0  THEN  Auto)

---

Home Index