---

Step * 2 1 of Lemma rng-pps_wf


1. r : IntegDom{i}@i'
2. eq : EqDecider(|r|)
⊢ BasicProjectiveGeometryAxioms(rng-pps(r;eq))
BY
{ (UnfoldTopAb 0 THEN UnfoldpGeoAbbreviations 0) }

1
1. r : IntegDom{i}@i'
2. eq : EqDecider(|r|)
⊢ ∀m,l,p,q:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} .
    ((¬¬((p . l) = 0 ∈ |r|))
    ⇒ (¬¬((q . l) = 0 ∈ |r|))
    ⇒ (¬¬((p . m) = 0 ∈ |r|))
    ⇒ (¬¬((q . m) = 0 ∈ |r|))
    ⇒ (¬((¬¬(∃l:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} . ((¬¬((p . l) = 0 ∈ |r|)) ∧ (¬((q . l) = 0 ∈ |r|)))))
       ∧ (¬¬(∃a:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} . ((¬¬((a . l) = 0 ∈ |r|)) ∧ (¬((a . m) = 0 ∈ |r|))))))))

---

Latex:

---

Latex:

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


By

---

Latex:
(UnfoldTopAb  0  THEN  UnfoldpGeoAbbreviations  0)

---

Home Index