---

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


1. r : IntegDom{i}@i'
2. eq : EqDecider(|r|)
3. m : ℕ3 ⟶ |r|@i
4. ¬(m = 0 ∈ (ℕ3 ⟶ |r|))
5. l : ℕ3 ⟶ |r|@i
6. ¬(l = 0 ∈ (ℕ3 ⟶ |r|))
7. p : ℕ3 ⟶ |r|@i
8. ¬(p = 0 ∈ (ℕ3 ⟶ |r|))
9. q : ℕ3 ⟶ |r|@i
10. ¬(q = 0 ∈ (ℕ3 ⟶ |r|))
11. (p . l) = 0 ∈ |r|
12. (q . l) = 0 ∈ |r|
13. (p . m) = 0 ∈ |r|
14. (q . m) = 0 ∈ |r|
15. l1 : ℕ3 ⟶ |r|@i
16. ¬(l1 = 0 ∈ (ℕ3 ⟶ |r|))
17. (p . l1) = 0 ∈ |r|
18. ¬((q . l1) = 0 ∈ |r|)
19. a : ℕ3 ⟶ |r|@i
20. ¬(a = 0 ∈ (ℕ3 ⟶ |r|))
21. (a . l) = 0 ∈ |r|
22. ¬((a . m) = 0 ∈ |r|)
23. ∀x,y:|r|.  Dec(x = y ∈ |r|)
24. ¬((p x q) = 0 ∈ (ℕ3 ⟶ |r|))
25. ¬((l x m) = 0 ∈ (ℕ3 ⟶ |r|))
26. ∃c1,c2:|r|. ((¬(c1 = 0 ∈ |r|)) ∧ (¬(c2 = 0 ∈ |r|)) ∧ ((c1*l) = (c2*(p x q)) ∈ (ℕ3 ⟶ |r|)))
27. ∃c1,c2:|r|. ((¬(c1 = 0 ∈ |r|)) ∧ (¬(c2 = 0 ∈ |r|)) ∧ ((c1*m) = (c2*(p x q)) ∈ (ℕ3 ⟶ |r|)))
⊢ False
BY
{ ((D -3 THEN ExRepD) THEN (RWO  "cross-product-equal-0" 0 THENA Auto) THEN (Sel 3 (D 0) THENA Auto)) }

1
1. r : IntegDom{i}@i'
2. eq : EqDecider(|r|)
3. m : ℕ3 ⟶ |r|@i
4. ¬(m = 0 ∈ (ℕ3 ⟶ |r|))
5. l : ℕ3 ⟶ |r|@i
6. ¬(l = 0 ∈ (ℕ3 ⟶ |r|))
7. p : ℕ3 ⟶ |r|@i
8. ¬(p = 0 ∈ (ℕ3 ⟶ |r|))
9. q : ℕ3 ⟶ |r|@i
10. ¬(q = 0 ∈ (ℕ3 ⟶ |r|))
11. (p . l) = 0 ∈ |r|
12. (q . l) = 0 ∈ |r|
13. (p . m) = 0 ∈ |r|
14. (q . m) = 0 ∈ |r|
15. l1 : ℕ3 ⟶ |r|@i
16. ¬(l1 = 0 ∈ (ℕ3 ⟶ |r|))
17. (p . l1) = 0 ∈ |r|
18. ¬((q . l1) = 0 ∈ |r|)
19. a : ℕ3 ⟶ |r|@i
20. ¬(a = 0 ∈ (ℕ3 ⟶ |r|))
21. (a . l) = 0 ∈ |r|
22. ¬((a . m) = 0 ∈ |r|)
23. ∀x,y:|r|.  Dec(x = y ∈ |r|)
24. ¬((p x q) = 0 ∈ (ℕ3 ⟶ |r|))
25. c3 : |r|
26. c4 : |r|
27. ¬(c3 = 0 ∈ |r|)
28. ¬(c4 = 0 ∈ |r|)
29. (c3*l) = (c4*(p x q)) ∈ (ℕ3 ⟶ |r|)
30. c1 : |r|
31. c2 : |r|
32. ¬(c1 = 0 ∈ |r|)
33. ¬(c2 = 0 ∈ |r|)
34. (c1*m) = (c2*(p x q)) ∈ (ℕ3 ⟶ |r|)
⊢ ∃c1,c2:|r|. ((¬(c1 = 0 ∈ |r|)) ∧ (¬(c2 = 0 ∈ |r|)) ∧ ((c1*l) = (c2*m) ∈ (ℕ3 ⟶ |r|)))

---

Latex:

---

Latex:

1.  r  :  IntegDom\{i\}@i'
2.  eq  :  EqDecider(|r|)
3.  m  :  \mBbbN{}3  {}\mrightarrow{}  |r|@i
4.  \mneg{}(m  =  0)
5.  l  :  \mBbbN{}3  {}\mrightarrow{}  |r|@i
6.  \mneg{}(l  =  0)
7.  p  :  \mBbbN{}3  {}\mrightarrow{}  |r|@i
8.  \mneg{}(p  =  0)
9.  q  :  \mBbbN{}3  {}\mrightarrow{}  |r|@i
10.  \mneg{}(q  =  0)
11.  (p  .  l)  =  0
12.  (q  .  l)  =  0
13.  (p  .  m)  =  0
14.  (q  .  m)  =  0
15.  l1  :  \mBbbN{}3  {}\mrightarrow{}  |r|@i
16.  \mneg{}(l1  =  0)
17.  (p  .  l1)  =  0
18.  \mneg{}((q  .  l1)  =  0)
19.  a  :  \mBbbN{}3  {}\mrightarrow{}  |r|@i
20.  \mneg{}(a  =  0)
21.  (a  .  l)  =  0
22.  \mneg{}((a  .  m)  =  0)
23.  \mforall{}x,y:|r|.    Dec(x  =  y)
24.  \mneg{}((p  x  q)  =  0)
25.  \mneg{}((l  x  m)  =  0)
26.  \mexists{}c1,c2:|r|.  ((\mneg{}(c1  =  0))  \mwedge{}  (\mneg{}(c2  =  0))  \mwedge{}  ((c1*l)  =  (c2*(p  x  q))))
27.  \mexists{}c1,c2:|r|.  ((\mneg{}(c1  =  0))  \mwedge{}  (\mneg{}(c2  =  0))  \mwedge{}  ((c1*m)  =  (c2*(p  x  q))))
\mvdash{}  False


By

---

Latex:
((D  -3  THEN  ExRepD)  THEN  (RWO    "cross-product-equal-0"  0  THENA  Auto)  THEN  (Sel  3  (D  0)  THENA  Auto))

---

Home Index