---

Step * 1 1 of Lemma rng-pps_wf

.....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
BY
{ MemCD }

1
.....subterm..... T:t
1:n
1. r : IntegDom{i}@i'
2. eq : EqDecider(|r|)
⊢ rng-pp-primitives(r) ∈ ProjGeomPrimitives

2
.....subterm..... T:t
2:n
1. r : IntegDom{i}@i'
2. eq : EqDecider(|r|)
⊢ λl,a,v,v. Ax ∈ ∀l:Line. ∀a:Point.  SqStable(pgeo-plsep(rng-pp-primitives(r); a; l))

3
.....subterm..... T:t
3:n
1. r : IntegDom{i}@i'
2. eq : EqDecider(|r|)
⊢ λa,l,m. if eq (a . m) 0 then inr <a, λnp.(np Ax), λ%6.Ax>  else inl (λ%.Ax) fi  ∈ ∀a:Point. ∀l:{l:Line| 
                                                                                        pgeo-plsep(rng-pp-primitives(r);
                                                                                                   a;
                                                                                                   l)} . ∀m:Line.
                                                                            (pgeo-plsep(rng-pp-primitives(r); a; m)
                                                                            ∨ m ≠ l)

4
.....subterm..... T:t
4:n
1. r : IntegDom{i}@i'
2. eq : EqDecider(|r|)
⊢ λl,a,b. if eq (b . l) 0 then inr <l, λnp.(np Ax), λ%6.Ax>  else inl (λ%.Ax) fi  ∈ ∀l:Line. ∀a:{a:Point| l ≠ a} . ∀b:Po\000Cint.
                                                                            (pgeo-plsep(rng-pp-primitives(r); b; l)
                                                                            ∨ b ≠ a)

5
.....subterm..... T:t
5:n
1. r : IntegDom{i}@i'
2. eq : EqDecider(|r|)
⊢ λa,b,_. <(a x b), λ_.Ax, λ_.Ax> ∈ ∀a,b:Point.  (a ≠ b ⇒ (∃l:Line. (a I l ∧ b I l)))

6
.....subterm..... T:t
6:n
1. r : IntegDom{i}@i'
2. eq : EqDecider(|r|)
⊢ λa,b,_. <(a x b), λ_.Ax, λ_.Ax> ∈ ∀l,m:Line.  (l ≠ m ⇒ (∃a:Point. (a I l ∧ a I m)))

7
.....subterm..... T:t
7:n
1. r : IntegDom{i}@i'
2. eq : EqDecider(|r|)
⊢ λl.rng-pp-nontriv1(r;eq;l) ∈ ∀l:Line. ∃a,b,c:Point. (a I l ∧ b I l ∧ c I l ∧ a ≠ b ∧ b ≠ c ∧ c ≠ a)

8
.....subterm..... T:t
8:n
1. r : IntegDom{i}@i'
2. eq : EqDecider(|r|)
⊢ λa.rng-pp-nontriv2(r;eq;a) ∈ ∀a:Point. ∃l,m,n:Line. (a I l ∧ a I m ∧ a I n ∧ l ≠ m ∧ m ≠ n ∧ n ≠ l)

---

Latex:

---

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


By

---

Latex:
MemCD

---

Home Index