---

Step * 1 1 5 1 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 : ℕ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
BY
{ D 13 }

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|) ⟶ False
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|
⊢ (b . l) = 0 ∈ |r|

---

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  :  \mBbbN{}3  {}\mrightarrow{}  |r|@i
10.  \mneg{}(l  =  0)
11.  (a  .  l)  =  0
12.  $_{2}$  :  (\mneg{}((a  .  l)  =  0))  {}\mrightarrow{}  False
13.  $_{3}$  :  \mneg{}((b  .  l)  =  0)@i
14.  c1  :  |r|
15.  c2  :  |r|
16.  \mneg{}(c1  =  0)
17.  \mneg{}(c2  =  0)
18.  (c1*a)  =  (c2*b)
19.  \mforall{}x,y:|r|.    Dec(x  =  y)
20.  ((c1*a)  .  l)  =  ((c2*b)  .  l)
\mvdash{}  False


By

---

Latex:
D  13

---

Home Index