---

Step * 1 1 5 1 1 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|) ⟶ 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. 0 = (c2 * (b . l)) ∈ |r|
⊢ (b . l) = 0 ∈ |r|
BY
{ (Assert ((b . l) * c2) = 0 ∈ |r| BY
         (Symmetry THEN NthHypEq (-1) THEN EqCDA THEN 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|) ⟶ 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. 0 = (c2 * (b . l)) ∈ |r|
21. ((b . l) * c2) = 0 ∈ |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}$  :  ((b  .  l)  =  0)  {}\mrightarrow{}  False
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.  0  =  (c2  *  (b  .  l))
\mvdash{}  (b  .  l)  =  0


By

---

Latex:
(Assert  ((b  .  l)  *  c2)  =  0  BY
              (Symmetry  THEN  NthHypEq  (-1)  THEN  EqCDA  THEN  Auto))

---

Home Index