---

Step * of Lemma rng-pp-nontrivial-1-ext

∀r:IntegDom{i}
  ((∀x,y:|r|.  Dec(x = y ∈ |r|))
  ⇒ (∀l:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
        ∃a:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
         (∃b:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))}  [(((a . l) = 0 ∈ |r|)
                                               ∧ ((b . l) = 0 ∈ |r|)
                                               ∧ (¬((a x b) = 0 ∈ (ℕ3 ⟶ |r|))))])))
BY
{ Extract of Obid: rng-pp-nontrivial-1
  not unfolding  cross-product rng_zero rng_minus non-zero-component
  finishing with Auto
  normalizes to:
  
  λr,eq,l. eval i = non-zero-component(r;eq;3;l) in
           if i=0
           then <λx.if x=1 then l 0 else if x=0 then -r (l 1) else 0
                , λx.if x=2 then l 0 else if x=0 then -r (l 2) else 0
                >
           else if i=1
                then <λx.if x=0 then l 1 else if x=1 then -r (l 0) else 0
                     , λx.if x=2 then l 1 else if x=1 then -r (l 2) else 0
                     >
                else if i=2
                     then <λx.if x=0 then l 2 else if x=2 then -r (l 0) else 0
                          , λx.if x=1 then l 2 else if x=2 then -r (l 1) else 0
                          >
                     else Ax }

---

Latex:

---

Latex:
\mforall{}r:IntegDom\{i\}
    ((\mforall{}x,y:|r|.    Dec(x  =  y))
    {}\mRightarrow{}  (\mforall{}l:\{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\} 
                \mexists{}a:\{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\}  .  (\mexists{}b:\{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\}    [(((a  .  l)  =  0)  \mwedge{}  ((b  .  l)  =  0)  \mwedge{}  \000C(\mneg{}((a  x  b)  =  0)))])))


By

---

Latex:
Extract  of  Obid:  rng-pp-nontrivial-1
not  unfolding    cross-product  rng\_zero  rng\_minus  non-zero-component
finishing  with  Auto
normalizes  to:

\mlambda{}r,eq,l.  eval  i  =  non-zero-component(r;eq;3;l)  in
                  if  i=0
                  then  <\mlambda{}x.if  x=1  then  l  0  else  if  x=0  then  -r  (l  1)  else  0
                            ,  \mlambda{}x.if  x=2  then  l  0  else  if  x=0  then  -r  (l  2)  else  0
                            >
                  else  if  i=1
                            then  <\mlambda{}x.if  x=0  then  l  1  else  if  x=1  then  -r  (l  0)  else  0
                                      ,  \mlambda{}x.if  x=2  then  l  1  else  if  x=1  then  -r  (l  2)  else  0
                                      >
                            else  if  i=2
                                      then  <\mlambda{}x.if  x=0  then  l  2  else  if  x=2  then  -r  (l  0)  else  0
                                                ,  \mlambda{}x.if  x=1  then  l  2  else  if  x=2  then  -r  (l  1)  else  0
                                                >
                                      else  Ax

---

Home Index