---

Step * 1 2 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 ∈ ℤ)
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|
BY
{ (((RWO "scalar-product-3" 0 THENA Auto) THEN Reduce 0)
   THEN (OnVar `i1' IntSegCases THEN OnVar `j' IntSegCases)
   THEN Reduce 0
   THEN RW CRngNormC 0
   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)
9.  \mneg{}((\mlambda{}x.if  (x  =\msubz{}  j)  then  l  i1  if  (x  =\msubz{}  i1)  then  -r  (l  j)  else  0  fi  )  =  0)
\mvdash{}  (\mlambda{}x.if  (x  =\msubz{}  j)  then  l  i1  if  (x  =\msubz{}  i1)  then  -r  (l  j)  else  0  fi    .  l)  =  0


By

---

Latex:
(((RWO  "scalar-product-3"  0  THENA  Auto)  THEN  Reduce  0)
  THEN  (OnVar  `i1'  IntSegCases  THEN  OnVar  `j'  IntSegCases)
  THEN  Reduce  0
  THEN  RW  CRngNormC  0
  THEN  Auto)

---

Home Index