---

Step * 1 of Lemma vs-add-assoc


1. K : RngSig
2. vs : VectorSpace(K)
3. x : Point(vs)
4. y : Point(vs)
5. z : Point(vs)
6. vs ∈ VectorSpace(K)
⊢ x + y + z = x + y + z ∈ Point(vs)
BY
{ ((D 2 THEN Auto) THEN Unfold `vs-add` 0 THEN MemTypeHD (-2) THEN Auto) }

1
1. K : RngSig
2. vs : self:"Point":Type
        "0":Point(self)
        "+":{f:Point(self) ⟶ Point(self) ⟶ Point(self)| 
             (∀x,y,z:Point(self).  ((f x (f y z)) = (f (f x y) z) ∈ Point(self)))
             ∧ (∀x,y:Point(self).  ((f x y) = (f y x) ∈ Point(self)))}  ⋂ x:Atom ⟶ if x =a "*"
                                                                               then {m:|K|
                                                                                     ⟶ Point(self)
                                                                                     ⟶ Point(self)| 
                                                                                     (∀a:|K|. ∀x,y:Point(self).
                                                                                        ((m a (self."+" x y))
                                                                                        = (self."+" (m a x) (m a y))
                                                                                        ∈ Point(self)))
                                                                                     ∧ (∀x:Point(self)
                                                                                          (((m 1 x) = x ∈ Point(self))
                                                                                          ∧ ((m 0 x)
                                                                                            = self."0"
                                                                                            ∈ Point(self))
                                                                                          ∧ (∀a,b:|K|.
                                                                                               ((m a (m b x))
                                                                                               = (m (a * b) x)
                                                                                               ∈ Point(self)))
                                                                                          ∧ (∀a,b:|K|.
                                                                                               ((m (a +K b) x)
                                                                                               = (self."+" (m a x) 
                                                                                                  (m b x))
                                                                                               ∈ Point(self)))))} 
                                                                               else Top
                                                                               fi 
3. vs ∈ record(x.Top)
4. x : Point(vs)
5. y : Point(vs)
6. z : Point(vs)
7. vs ∈ VectorSpace(K)
8. vs."Point" ∈ Type
9. vs."0" ∈ Point(vs)
10. vs."+" = vs."+" ∈ (Point(vs) ⟶ Point(vs) ⟶ Point(vs))
11. ∀x,y,z:Point(vs).  ((vs."+" x (vs."+" y z)) = (vs."+" (vs."+" x y) z) ∈ Point(vs))
12. ∀x,y:Point(vs).  ((vs."+" x y) = (vs."+" y x) ∈ Point(vs))
13. vs."*" ∈ {m:|K| ⟶ Point(vs) ⟶ Point(vs)| 
              (∀a:|K|. ∀x,y:Point(vs).  ((m a (vs."+" x y)) = (vs."+" (m a x) (m a y)) ∈ Point(vs)))
              ∧ (∀x:Point(vs)
                   (((m 1 x) = x ∈ Point(vs))
                   ∧ ((m 0 x) = vs."0" ∈ Point(vs))
                   ∧ (∀a,b:|K|.  ((m a (m b x)) = (m (a * b) x) ∈ Point(vs)))
                   ∧ (∀a,b:|K|.  ((m (a +K b) x) = (vs."+" (m a x) (m b x)) ∈ Point(vs)))))} 
⊢ (vs."+" (vs."+" x y) z) = (vs."+" x (vs."+" y z)) ∈ Point(vs)

---

Latex:

---

Latex:

1.  K  :  RngSig
2.  vs  :  VectorSpace(K)
3.  x  :  Point(vs)
4.  y  :  Point(vs)
5.  z  :  Point(vs)
6.  vs  \mmember{}  VectorSpace(K)
\mvdash{}  x  +  y  +  z  =  x  +  y  +  z


By

---

Latex:
((D  2  THEN  Auto)  THEN  Unfold  `vs-add`  0  THEN  MemTypeHD  (-2)  THEN  Auto)

---

Home Index