---

Step * 2 3 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. ¬((l 2) = 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|)} ))
6. λx.if (x =z 0) then l 2
      if (x =z 2) then -r (l 0)
      else 0
      fi  ∈ {p:ℕ3 ⟶ |r|| (¬(p = 0 ∈ (ℕ3 ⟶ |r|))) ∧ ((p . l) = 0 ∈ |r|)} 
7. λx.if (x =z 1) then l 2
      if (x =z 2) then -r (l 1)
      else 0
      fi  ∈ {p:ℕ3 ⟶ |r|| (¬(p = 0 ∈ (ℕ3 ⟶ |r|))) ∧ ((p . l) = 0 ∈ |r|)} 
8. (λx.if (x =z 0) then l 2 if (x =z 2) then -r (l 0) else 0 fi  . l) = 0 ∈ |r|
9. (λx.if (x =z 1) then l 2 if (x =z 2) then -r (l 1) else 0 fi  . l) = 0 ∈ |r|
⊢ ¬((λx.if (x =z 0) then l 2
        if (x =z 2) then -r (l 0)
        else 0
        fi  x λx.if (x =z 1) then l 2
                 if (x =z 2) then -r (l 1)
                 else 0
                 fi )
= 0
∈ (ℕ3 ⟶ |r|))
BY
{ (RepUR ``cross-product`` 0
   THEN (D 0 THENA Auto)
   THEN (ApFunToHypEquands `Z' ⌜Z 2⌝ ⌜|r|⌝ (-1)⋅ THENA Auto)
   THEN RepUR ``zero-vector`` -1
   THEN (RW RngNormC (-1) THENA Auto)
   THEN D 1
   THEN D 2
   THEN FHyp 3 [-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.  \mneg{}((l  2)  =  0)
5.  \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)\}  ))
6.  \mlambda{}x.if  (x  =\msubz{}  0)  then  l  2
            if  (x  =\msubz{}  2)  then  -r  (l  0)
            else  0
            fi    \mmember{}  \{p:\mBbbN{}3  {}\mrightarrow{}  |r||  (\mneg{}(p  =  0))  \mwedge{}  ((p  .  l)  =  0)\} 
7.  \mlambda{}x.if  (x  =\msubz{}  1)  then  l  2
            if  (x  =\msubz{}  2)  then  -r  (l  1)
            else  0
            fi    \mmember{}  \{p:\mBbbN{}3  {}\mrightarrow{}  |r||  (\mneg{}(p  =  0))  \mwedge{}  ((p  .  l)  =  0)\} 
8.  (\mlambda{}x.if  (x  =\msubz{}  0)  then  l  2  if  (x  =\msubz{}  2)  then  -r  (l  0)  else  0  fi    .  l)  =  0
9.  (\mlambda{}x.if  (x  =\msubz{}  1)  then  l  2  if  (x  =\msubz{}  2)  then  -r  (l  1)  else  0  fi    .  l)  =  0
\mvdash{}  \mneg{}((\mlambda{}x.if  (x  =\msubz{}  0)  then  l  2
                if  (x  =\msubz{}  2)  then  -r  (l  0)
                else  0
                fi    x  \mlambda{}x.if  (x  =\msubz{}  1)  then  l  2
                                  if  (x  =\msubz{}  2)  then  -r  (l  1)
                                  else  0
                                  fi  )
=  0)


By

---

Latex:
(RepUR  ``cross-product``  0
  THEN  (D  0  THENA  Auto)
  THEN  (ApFunToHypEquands  `Z'  \mkleeneopen{}Z  2\mkleeneclose{}  \mkleeneopen{}|r|\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
  THEN  RepUR  ``zero-vector``  -1
  THEN  (RW  RngNormC  (-1)  THENA  Auto)
  THEN  D  1
  THEN  D  2
  THEN  FHyp  3  [-1]
  THEN  Auto)

---

Home Index