---

Step * 1 1 1 of Lemma cross-product-equal-0-iff


1. r : IntegDom{i}
2. a : ℕ3 ⟶ |r|
3. b : ℕ3 ⟶ |r|
4. ∀x,y:|r|.  Dec(x = y ∈ |r|)
5. c1 : |r|
6. c2 : |r|
7. ¬(c1 = 0 ∈ |r|)
8. ¬(c2 = 0 ∈ |r|)
9. (c1*a) = (c2*b) ∈ (ℕ3 ⟶ |r|)
10. l : ℕ3 ⟶ |r|
11. 0 = (c2 * (b . l)) ∈ |r|
12. (a . l) = 0 ∈ |r|
⊢ (b . l) = 0 ∈ |r|
BY
{ ((Assert ((b . l) * c2) = 0 ∈ |r| BY (RWO "crng_times_comm" 0 THEN Auto)) THEN D 1 THEN D 2 THEN Auto) }

---

Latex:

---

Latex:

1.  r  :  IntegDom\{i\}
2.  a  :  \mBbbN{}3  {}\mrightarrow{}  |r|
3.  b  :  \mBbbN{}3  {}\mrightarrow{}  |r|
4.  \mforall{}x,y:|r|.    Dec(x  =  y)
5.  c1  :  |r|
6.  c2  :  |r|
7.  \mneg{}(c1  =  0)
8.  \mneg{}(c2  =  0)
9.  (c1*a)  =  (c2*b)
10.  l  :  \mBbbN{}3  {}\mrightarrow{}  |r|
11.  0  =  (c2  *  (b  .  l))
12.  (a  .  l)  =  0
\mvdash{}  (b  .  l)  =  0


By

---

Latex:
((Assert  ((b  .  l)  *  c2)  =  0  BY  (RWO  "crng\_times\_comm"  0  THEN  Auto))  THEN  D  1  THEN  D  2  THEN  Auto)

---

Home Index