---

Step * 1 1 5 1 1 of Lemma rng-pps_wf


1. r : IntegDom{i}@i'
2. eq : EqDecider(|r|)
3. ∀p:ℕ3 ⟶ |r|. (¬(p = 0 ∈ (ℕ3 ⟶ |r|)) ∈ 𝕌{[1 | i 0]})
4. a : ℕ3 ⟶ |r|@i
5. ¬(a = 0 ∈ (ℕ3 ⟶ |r|))
6. ∀p:ℕ3 ⟶ |r|. (¬(p = 0 ∈ (ℕ3 ⟶ |r|)) ∈ 𝕌{[1 | i 0]})
7. b : ℕ3 ⟶ |r|@i
8. ¬(b = 0 ∈ (ℕ3 ⟶ |r|))
9. l : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} @i
10. _2 : ¬¬((a . l) = 0 ∈ |r|)@i
11. _3 : ¬((b . l) = 0 ∈ |r|)@i
12. (a x b) = 0 ∈ (ℕ3 ⟶ |r|)
⊢ False
BY
{ ((Assert ∀x,y:|r|.  Dec(x = y ∈ |r|) BY
          (Intros THEN (InstLemma `deq_property` [⌜|r|⌝;⌜eq⌝]⋅ THENA Auto) THEN RWO  "-1" 0 THEN Auto))
   THEN (RWO "cross-product-equal-0" (-2) THENA Auto)
   THEN DSetVars
   THEN SplitOrHyps
   THEN Auto
   THEN ExRepD
   THEN (ApFunToHypEquands `Z' ⌜(Z . l)⌝ ⌜|r|⌝ (-2)⋅ THENA Auto)) }

1
1. r : IntegDom{i}@i'
2. eq : EqDecider(|r|)
3. ∀p:ℕ3 ⟶ |r|. (¬(p = 0 ∈ (ℕ3 ⟶ |r|)) ∈ 𝕌{[1 | i 0]})
4. a : ℕ3 ⟶ |r|@i
5. ¬(a = 0 ∈ (ℕ3 ⟶ |r|))
6. ∀p:ℕ3 ⟶ |r|. (¬(p = 0 ∈ (ℕ3 ⟶ |r|)) ∈ 𝕌{[1 | i 0]})
7. b : ℕ3 ⟶ |r|@i
8. ¬(b = 0 ∈ (ℕ3 ⟶ |r|))
9. l : ℕ3 ⟶ |r|@i
10. ¬(l = 0 ∈ (ℕ3 ⟶ |r|))
11. (a . l) = 0 ∈ |r|
12. _2 : (¬((a . l) = 0 ∈ |r|)) ⟶ False
13. _3 : ¬((b . l) = 0 ∈ |r|)@i
14. c1 : |r|
15. c2 : |r|
16. ¬(c1 = 0 ∈ |r|)
17. ¬(c2 = 0 ∈ |r|)
18. (c1*a) = (c2*b) ∈ (ℕ3 ⟶ |r|)
19. ∀x,y:|r|.  Dec(x = y ∈ |r|)
20. ((c1*a) . l) = ((c2*b) . l) ∈ |r|
⊢ False

---

Latex:

---

Latex:

1.  r  :  IntegDom\{i\}@i'
2.  eq  :  EqDecider(|r|)
3.  \mforall{}p:\mBbbN{}3  {}\mrightarrow{}  |r|.  (\mneg{}(p  =  0)  \mmember{}  \mBbbU{}\{[1  |  i  0]\})
4.  a  :  \mBbbN{}3  {}\mrightarrow{}  |r|@i
5.  \mneg{}(a  =  0)
6.  \mforall{}p:\mBbbN{}3  {}\mrightarrow{}  |r|.  (\mneg{}(p  =  0)  \mmember{}  \mBbbU{}\{[1  |  i  0]\})
7.  b  :  \mBbbN{}3  {}\mrightarrow{}  |r|@i
8.  \mneg{}(b  =  0)
9.  l  :  \{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\}  @i
10.  $_{2}$  :  \mneg{}\mneg{}((a  .  l)  =  0)@i
11.  $_{3}$  :  \mneg{}((b  .  l)  =  0)@i
12.  (a  x  b)  =  0
\mvdash{}  False


By

---

Latex:
((Assert  \mforall{}x,y:|r|.    Dec(x  =  y)  BY
                (Intros
                  THEN  (InstLemma  `deq\_property`  [\mkleeneopen{}|r|\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{}]\mcdot{}  THENA  Auto)
                  THEN  RWO    "-1"  0
                  THEN  Auto))
  THEN  (RWO  "cross-product-equal-0"  (-2)  THENA  Auto)
  THEN  DSetVars
  THEN  SplitOrHyps
  THEN  Auto
  THEN  ExRepD
  THEN  (ApFunToHypEquands  `Z'  \mkleeneopen{}(Z  .  l)\mkleeneclose{}  \mkleeneopen{}|r|\mkleeneclose{}  (-2)\mcdot{}  THENA  Auto))

---

Home Index