---

Step * 1 1 of Lemma rng-pp-nontrivial-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|))
BY
{ ((D 0 THENA Auto)
   THEN (ApFunToHypEquands `Z' ⌜Z j⌝ ⌜|r|⌝ (-1)⋅ THENA Auto)
   THEN RepUR ``zero-vector`` -1
   THEN SplitOnHypITE -1 
   THEN Auto) }

---

Latex:

---

Latex:

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)\} 
5.  i1  :  \mBbbN{}3@i
6.  j  :  \mBbbN{}3@i
7.  \mneg{}((l  i1)  =  0)
8.  \mneg{}(i1  =  j)
\mvdash{}  \mneg{}((\mlambda{}x.if  (x  =\msubz{}  j)  then  l  i1  if  (x  =\msubz{}  i1)  then  -r  (l  j)  else  0  fi  )  =  0)


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (ApFunToHypEquands  `Z'  \mkleeneopen{}Z  j\mkleeneclose{}  \mkleeneopen{}|r|\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
  THEN  RepUR  ``zero-vector``  -1
  THEN  SplitOnHypITE  -1 
  THEN  Auto)

---

Home Index