---

Step * of Lemma rng-pp-nontrivial-1

∀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
{ (Auto
   THEN RenameVar `eq' 2
   THEN (Evaluate ⌜i = non-zero-component(r;eq;3;l) ∈ {i:ℕ3| ¬((l i) = 0 ∈ |r|)} ⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN Assert ⌜∀i,j:ℕ3.
                  ((¬((l i) = 0 ∈ |r|))
                  ⇒ (¬(i = j ∈ ℤ))
                  ⇒ (λx.if (x =z j) then l i
                         if (x =z i) then -r (l j)
                         else 0
                         fi  ∈ {p:ℕ3 ⟶ |r|| (¬(p = 0 ∈ (ℕ3 ⟶ |r|))) ∧ ((p . l) = 0 ∈ |r|)} ))⌝⋅) }

1
.....assertion..... 
1. r : IntegDom{i}@i'
2. eq : ∀x,y:|r|.  Dec(x = y ∈ |r|)@i
3. l : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} @i
4. i : {i:ℕ3| ¬((l i) = 0 ∈ |r|)} 
⊢ ∀i,j:ℕ3.
    ((¬((l i) = 0 ∈ |r|))
    ⇒ (¬(i = j ∈ ℤ))
    ⇒ (λx.if (x =z j) then l i
           if (x =z i) then -r (l j)
           else 0
           fi  ∈ {p:ℕ3 ⟶ |r|| (¬(p = 0 ∈ (ℕ3 ⟶ |r|))) ∧ ((p . l) = 0 ∈ |r|)} ))

2
1. r : IntegDom{i}@i'
2. eq : ∀x,y:|r|.  Dec(x = y ∈ |r|)@i
3. l : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} @i
4. i : {i:ℕ3| ¬((l i) = 0 ∈ |r|)} 
5. ∀i,j:ℕ3.
     ((¬((l i) = 0 ∈ |r|))
     ⇒ (¬(i = j ∈ ℤ))
     ⇒ (λx.if (x =z j) then l i
            if (x =z i) then -r (l j)
            else 0
            fi  ∈ {p:ℕ3 ⟶ |r|| (¬(p = 0 ∈ (ℕ3 ⟶ |r|))) ∧ ((p . l) = 0 ∈ |r|)} ))
⊢ ∃a:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} . (∃b:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))}  [(((a . l) = 0 ∈ |r|) ∧ ((b . l)\000C = 0 ∈ |r|) ∧ (¬((a x b) = 0 ∈ (ℕ3 ⟶ |r|))))])

---

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:
(Auto
  THEN  RenameVar  `eq'  2
  THEN  (Evaluate  \mkleeneopen{}i  =  non-zero-component(r;eq;3;l)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  Assert  \mkleeneopen{}\mforall{}i,j:\mBbbN{}3.
                                ((\mneg{}((l  i)  =  0))
                                {}\mRightarrow{}  (\mneg{}(i  =  j))
                                {}\mRightarrow{}  (\mlambda{}x.if  (x  =\msubz{}  j)  then  l  i
                                              if  (x  =\msubz{}  i)  then  -r  (l  j)
                                              else  0
                                              fi    \mmember{}  \{p:\mBbbN{}3  {}\mrightarrow{}  |r||  (\mneg{}(p  =  0))  \mwedge{}  ((p  .  l)  =  0)\}  ))\mkleeneclose{}\mcdot{})

---

Home Index