---

Step * 2 of Lemma rng-pp-nontrivial-2


1. r : IntegDom{i}
2. ∀x,y:|r|.  Dec(x = y ∈ |r|)
3. l : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
4. a : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
5. b : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
6. (a . l) = 0 ∈ |r|
7. (b . l) = 0 ∈ |r|
8. ¬((a x b) = 0 ∈ (ℕ3 ⟶ |r|))
9. (a . l) = 0 ∈ |r|
10. (b . l) = 0 ∈ |r|
⊢ ((a + b) . l) = 0 ∈ |r|
BY
{ (RWW "scalar-product-add-left -1 -2" 0 THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(RWW  "scalar-product-add-left  -1  -2"  0  THEN  Auto)

---

Home Index