---

Step * 2 2 of Lemma rng-pps_wf


1. r : IntegDom{i}@i'
2. eq : EqDecider(|r|)
3. BasicProjectiveGeometryAxioms(rng-pps(r;eq))
⊢ triangle-axiom1(rng-pps(r;eq))
BY
{ (RepUR ``triangle-axiom1`` 0 THEN UnfoldpGeoAbbreviations 0 THEN Auto) }

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. ¬((r@0 . (p x q)) = 0 ∈ |r|)
⊢ ¬((p . (q x r@0)) = 0 ∈ |r|)

---

Latex:

---

Latex:

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


By

---

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

---

Home Index