---

Step * 1 1 of Lemma vs-add-assoc


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)
BY
{ (Symmetry THEN Auto) }

---

Latex:

---

Latex:

1.  K  :  RngSig
2.  vs  :  self:"Point":Type
                "0":Point(self)
                "+":\{f:Point(self)  {}\mrightarrow{}  Point(self)  {}\mrightarrow{}  Point(self)| 
                          (\mforall{}x,y,z:Point(self).    ((f  x  (f  y  z))  =  (f  (f  x  y)  z)))
                          \mwedge{}  (\mforall{}x,y:Point(self).    ((f  x  y)  =  (f  y  x)))\}    \mcap{}  x:Atom  {}\mrightarrow{}  if  x  =a  "*"
                                                                                                                                  then  \{m:|K|
                                                                                                                                              {}\mrightarrow{}  Point(self)
                                                                                                                                              {}\mrightarrow{}  Point(self)| 
                                                                                                                                              (\mforall{}a:|K|.  \mforall{}x,y:Point(self).
                                                                                                                                                    ((m  a  (self."+"  x  y))
                                                                                                                                                    =  (self."+"  (m  a  x) 
                                                                                                                                                          (m  a  y))))
                                                                                                                                              \mwedge{}  (\mforall{}x:Point(self)
                                                                                                                                                        (((m  1  x)  =  x)
                                                                                                                                                        \mwedge{}  ((m  0  x)  =  self."0")
                                                                                                                                                        \mwedge{}  (\mforall{}a,b:|K|.
                                                                                                                                                                  ((m  a  (m  b  x))
                                                                                                                                                                  =  (m  (a  *  b)  x)))
                                                                                                                                                        \mwedge{}  (\mforall{}a,b:|K|.
                                                                                                                                                                  ((m  (a  +K  b)  x)
                                                                                                                                                                  =  (self."+" 
                                                                                                                                                                        (m  a  x) 
                                                                                                                                                                        (m  b  x))))))\} 
                                                                                                                                  else  Top
                                                                                                                                  fi 
3.  vs  \mmember{}  record(x.Top)
4.  x  :  Point(vs)
5.  y  :  Point(vs)
6.  z  :  Point(vs)
7.  vs  \mmember{}  VectorSpace(K)
8.  vs."Point"  \mmember{}  Type
9.  vs."0"  \mmember{}  Point(vs)
10.  vs."+"  =  vs."+"
11.  \mforall{}x,y,z:Point(vs).    ((vs."+"  x  (vs."+"  y  z))  =  (vs."+"  (vs."+"  x  y)  z))
12.  \mforall{}x,y:Point(vs).    ((vs."+"  x  y)  =  (vs."+"  y  x))
13.  vs."*"  \mmember{}  \{m:|K|  {}\mrightarrow{}  Point(vs)  {}\mrightarrow{}  Point(vs)| 
                            (\mforall{}a:|K|.  \mforall{}x,y:Point(vs).    ((m  a  (vs."+"  x  y))  =  (vs."+"  (m  a  x)  (m  a  y))))
                            \mwedge{}  (\mforall{}x:Point(vs)
                                      (((m  1  x)  =  x)
                                      \mwedge{}  ((m  0  x)  =  vs."0")
                                      \mwedge{}  (\mforall{}a,b:|K|.    ((m  a  (m  b  x))  =  (m  (a  *  b)  x)))
                                      \mwedge{}  (\mforall{}a,b:|K|.    ((m  (a  +K  b)  x)  =  (vs."+"  (m  a  x)  (m  b  x))))))\} 
\mvdash{}  (vs."+"  (vs."+"  x  y)  z)  =  (vs."+"  x  (vs."+"  y  z))


By

---

Latex:
(Symmetry  THEN  Auto)

---

Home Index