---

Step * 2 1 of Lemma int-dot-add-right


1. u : ℤ
2. v : ℤ List
3. ∀[as,bs:ℤ List].  v ⋅ as + bs ~ v ⋅ as + v ⋅ bs supposing ||as|| = ||bs|| ∈ ℤ
4. u1 : ℤ
5. v1 : ℤ List
6. ∀[bs:ℤ List]. [u / v] ⋅ v1 + bs ~ [u / v] ⋅ v1 + [u / v] ⋅ bs supposing ||v1|| = ||bs|| ∈ ℤ
7. u2 : ℤ
8. v2 : ℤ List
9. [u / v] ⋅ [u1 / v1] + v2 ~ [u / v] ⋅ [u1 / v1] + [u / v] ⋅ v2 supposing ||[u1 / v1]|| = ||v2|| ∈ ℤ
10. (||v1|| + 1) = (||v2|| + 1) ∈ ℤ
⊢ ((u * (u1 + u2)) + v ⋅ v1 + v2) = (((u * u1) + v ⋅ v1) + (u * u2) + v ⋅ v2) ∈ ℤ
BY
{ (RWO "3" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  u  :  \mBbbZ{}
2.  v  :  \mBbbZ{}  List
3.  \mforall{}[as,bs:\mBbbZ{}  List].    v  \mcdot{}  as  +  bs  \msim{}  v  \mcdot{}  as  +  v  \mcdot{}  bs  supposing  ||as||  =  ||bs||
4.  u1  :  \mBbbZ{}
5.  v1  :  \mBbbZ{}  List
6.  \mforall{}[bs:\mBbbZ{}  List].  [u  /  v]  \mcdot{}  v1  +  bs  \msim{}  [u  /  v]  \mcdot{}  v1  +  [u  /  v]  \mcdot{}  bs  supposing  ||v1||  =  ||bs||
7.  u2  :  \mBbbZ{}
8.  v2  :  \mBbbZ{}  List
9.  [u  /  v]  \mcdot{}  [u1  /  v1]  +  v2  \msim{}  [u  /  v]  \mcdot{}  [u1  /  v1]  +  [u  /  v]  \mcdot{}  v2  supposing  ||[u1  /  v1]||  =  ||v2||
10.  (||v1||  +  1)  =  (||v2||  +  1)
\mvdash{}  ((u  *  (u1  +  u2))  +  v  \mcdot{}  v1  +  v2)  =  (((u  *  u1)  +  v  \mcdot{}  v1)  +  (u  *  u2)  +  v  \mcdot{}  v2)


By

---

Latex:
(RWO  "3"  0  THEN  Auto)

---

Home Index