---

Step * 1 of Lemma rng-pps_wf


1. r : IntegDom{i}@i'
2. eq : EqDecider(|r|)
⊢ rng-pps(r;eq) ∈ ProjectivePlaneStructureComplete
BY
{ (Unfold `rng-pps` 0
   THEN (MemCD
         THENL [Id
               ; (UnfoldpGeoAbbreviations 0
                  THEN (MemTypeCD THEN Auto)
                  THEN (D 0 THENA Auto)
                  THEN (ApFunToHypEquands `Z' ⌜Z 0⌝ ⌜|r|⌝ (-1)⋅ THENA Auto)
                  THEN RepUR ``zero-vector`` -1
                  THEN D -1
                  THEN D 1
                  THEN Auto)]
        )
   ) }

1
.....subterm..... T:t
1:n
1. r : IntegDom{i}@i'
2. eq : EqDecider(|r|)
⊢ mk-pgeo(rng-pp-primitives(r);
          λl,a,v,v. Ax;
          λa,l,m. if eq (a . m) 0 then inr <a, λnp.(np Ax), λ%6.Ax>  else inl (λ%.Ax) fi ;
          λl,a,b. if eq (b . l) 0 then inr <l, λnp.(np Ax), λ%6.Ax>  else inl (λ%.Ax) fi ;
          λa,b,_. <(a x b), λ_.Ax, λ_.Ax>;
          λa,b,_. <(a x b), λ_.Ax, λ_.Ax>;
          λl.rng-pp-nontriv1(r;eq;l);
          λa.rng-pp-nontriv2(r;eq;a)) ∈ ProjectivePlaneStructure

---

Latex:

---

Latex:

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


By

---

Latex:
(Unfold  `rng-pps`  0
  THEN  (MemCD
              THENL  [Id
                          ;  (UnfoldpGeoAbbreviations  0
                                THEN  (MemTypeCD  THEN  Auto)
                                THEN  (D  0  THENA  Auto)
                                THEN  (ApFunToHypEquands  `Z'  \mkleeneopen{}Z  0\mkleeneclose{}  \mkleeneopen{}|r|\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
                                THEN  RepUR  ``zero-vector``  -1
                                THEN  D  -1
                                THEN  D  1
                                THEN  Auto)]
            )
  )

---

Home Index