---

Step * 1 1 of Lemma rng-pp-nontrivial-2


1. r : IntegDom{i}
2. ∀x,y:|r|.  Dec(x = y ∈ |r|)
3. l : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
4. a : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
5. b : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
6. (a . l) = 0 ∈ |r|
7. (b . l) = 0 ∈ |r|
8. (a + b) = 0 ∈ (ℕ3 ⟶ |r|)
⊢ (a x b) = 0 ∈ (ℕ3 ⟶ |r|)
BY
{ (Assert a = (-r 1*b) ∈ (ℕ3 ⟶ |r|) BY
         ((FunExt THEN Auto)
          THEN RepUR ``vector-mul`` 0
          THEN (ApFunToHypEquands `Z' ⌜(Z x) +r ((-r 1) * (b x))⌝ ⌜|r|⌝ (-2)⋅ THENA Auto)
          THEN RepUR ``vector-add vector-mul zero-vector`` -1
          THEN (RW RngNormC (-1) THEN Auto)
          THEN RW RngNormC 0
          THEN Auto)) }

1
1. r : IntegDom{i}
2. ∀x,y:|r|.  Dec(x = y ∈ |r|)
3. l : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
4. a : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
5. b : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
6. (a . l) = 0 ∈ |r|
7. (b . l) = 0 ∈ |r|
8. (a + b) = 0 ∈ (ℕ3 ⟶ |r|)
9. a = (-r 1*b) ∈ (ℕ3 ⟶ |r|)
⊢ (a x b) = 0 ∈ (ℕ3 ⟶ |r|)

---

Latex:

---

Latex:

1.  r  :  IntegDom\{i\}
2.  \mforall{}x,y:|r|.    Dec(x  =  y)
3.  l  :  \{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\} 
4.  a  :  \{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\} 
5.  b  :  \{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\} 
6.  (a  .  l)  =  0
7.  (b  .  l)  =  0
8.  (a  +  b)  =  0
\mvdash{}  (a  x  b)  =  0


By

---

Latex:
(Assert  a  =  (-r  1*b)  BY
              ((FunExt  THEN  Auto)
                THEN  RepUR  ``vector-mul``  0
                THEN  (ApFunToHypEquands  `Z'  \mkleeneopen{}(Z  x)  +r  ((-r  1)  *  (b  x))\mkleeneclose{}  \mkleeneopen{}|r|\mkleeneclose{}  (-2)\mcdot{}  THENA  Auto)
                THEN  RepUR  ``vector-add  vector-mul  zero-vector``  -1
                THEN  (RW  RngNormC  (-1)  THEN  Auto)
                THEN  RW  RngNormC  0
                THEN  Auto))

---

Home Index