---

Step * 1 of Lemma rng-pp-nontrivial-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|)} ))
BY
{ (Intros THEN MemTypeCD THEN Auto) }

1
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. i1 : ℕ3@i
6. j : ℕ3@i
7. ¬((l i1) = 0 ∈ |r|)
8. ¬(i1 = j ∈ ℤ)
⊢ ¬((λx.if (x =z j) then l i1 if (x =z i1) then -r (l j) else 0 fi ) = 0 ∈ (ℕ3 ⟶ |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. i1 : ℕ3@i
6. j : ℕ3@i
7. ¬((l i1) = 0 ∈ |r|)
8. ¬(i1 = j ∈ ℤ)
9. ¬((λx.if (x =z j) then l i1 if (x =z i1) then -r (l j) else 0 fi ) = 0 ∈ (ℕ3 ⟶ |r|))
⊢ (λx.if (x =z j) then l i1 if (x =z i1) then -r (l j) else 0 fi  . l) = 0 ∈ |r|

---

Latex:

---

Latex:
.....assertion..... 
1.  r  :  IntegDom\{i\}@i'
2.  eq  :  \mforall{}x,y:|r|.    Dec(x  =  y)@i
3.  l  :  \{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\}  @i
4.  i  :  \{i:\mBbbN{}3|  \mneg{}((l  i)  =  0)\} 
\mvdash{}  \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)\}  ))


By

---

Latex:
(Intros  THEN  MemTypeCD  THEN  Auto)

---

Home Index