---

Step * 1 2 1 1 2 1 1 1 of Lemma bag-summation-linear


1. T : Type
2. R : Type
3. add : R ⟶ R ⟶ R
4. mul : R ⟶ R ⟶ R
5. zero : R
6. f : T ⟶ R
7. g : T ⟶ R
8. minus : R ⟶ R
9. IsGroup(R;add;zero;minus)
10. Comm(R;add)
11. ∀[a,x,y:R].
      (((a mul (x add y)) = ((a mul x) add (a mul y)) ∈ R) ∧ (((x add y) mul a) = ((x mul a) add (y mul a)) ∈ R))
12. a : R
13. v : R
14. (a mul zero) = v ∈ R
15. (v add v) = v ∈ R
16. ((v add v) add (minus v)) = (v add (minus v)) ∈ R
⊢ v = zero ∈ R
BY
{ ((RepUR ``group_p monoid_p assoc inverse`` 9 THEN Auto)
   THEN NthHypEq  (-1)
   THEN EqCD
   THEN Auto
   THEN Symmetry
   THEN Auto) }

1
1. T : Type
2. R : Type
3. add : R ⟶ R ⟶ R
4. mul : R ⟶ R ⟶ R
5. zero : R
6. f : T ⟶ R
7. g : T ⟶ R
8. minus : R ⟶ R
9. ∀[x,y,z:R].  ((x add (y add z)) = ((x add y) add z) ∈ R)
10. Ident(R;add;zero)
11. ∀[x:R]. (((x add (minus x)) = zero ∈ R) ∧ (((minus x) add x) = zero ∈ R))
12. Comm(R;add)
13. ∀[a,x,y:R].
      (((a mul (x add y)) = ((a mul x) add (a mul y)) ∈ R) ∧ (((x add y) mul a) = ((x mul a) add (y mul a)) ∈ R))
14. a : R
15. v : R
16. (a mul zero) = v ∈ R
17. (v add v) = v ∈ R
18. ((v add v) add (minus v)) = (v add (minus v)) ∈ R
⊢ ((v add v) add (minus v)) = v ∈ R

---

Latex:

---

Latex:

1.  T  :  Type
2.  R  :  Type
3.  add  :  R  {}\mrightarrow{}  R  {}\mrightarrow{}  R
4.  mul  :  R  {}\mrightarrow{}  R  {}\mrightarrow{}  R
5.  zero  :  R
6.  f  :  T  {}\mrightarrow{}  R
7.  g  :  T  {}\mrightarrow{}  R
8.  minus  :  R  {}\mrightarrow{}  R
9.  IsGroup(R;add;zero;minus)
10.  Comm(R;add)
11.  \mforall{}[a,x,y:R].
            (((a  mul  (x  add  y))  =  ((a  mul  x)  add  (a  mul  y)))
            \mwedge{}  (((x  add  y)  mul  a)  =  ((x  mul  a)  add  (y  mul  a))))
12.  a  :  R
13.  v  :  R
14.  (a  mul  zero)  =  v
15.  (v  add  v)  =  v
16.  ((v  add  v)  add  (minus  v))  =  (v  add  (minus  v))
\mvdash{}  v  =  zero


By

---

Latex:
((RepUR  ``group\_p  monoid\_p  assoc  inverse``  9  THEN  Auto)
  THEN  NthHypEq    (-1)
  THEN  EqCD
  THEN  Auto
  THEN  Symmetry
  THEN  Auto)

---

Home Index