Step * 1 2 1 of Lemma mon_nat_op_hom_swap


1. IMonoid
2. IMonoid
3. MonHom(g,h)
4. ∀[a1,a2:|g|].  ((f (a1 a2)) ((f a1) (f a2)) ∈ |h|)
5. (f e) e ∈ |h|
6. |g|
7. : ℤ
8. 0 < n
9. ((n 1) ⋅ (f u)) (f ((n 1) ⋅ u)) ∈ |h|
⊢ (((n 1) ⋅ (f u)) (f u)) (f (((n 1) ⋅ u) u)) ∈ |h|
BY
((RWW "9 4" 0) THEN Auto) }


Latex:


Latex:

1.  g  :  IMonoid
2.  h  :  IMonoid
3.  f  :  MonHom(g,h)
4.  \mforall{}[a1,a2:|g|].    ((f  (a1  *  a2))  =  ((f  a1)  *  (f  a2)))
5.  (f  e)  =  e
6.  u  :  |g|
7.  n  :  \mBbbZ{}
8.  0  <  n
9.  ((n  -  1)  \mcdot{}  (f  u))  =  (f  ((n  -  1)  \mcdot{}  u))
\mvdash{}  (((n  -  1)  \mcdot{}  (f  u))  *  (f  u))  =  (f  (((n  -  1)  \mcdot{}  u)  *  u))


By


Latex:
((RWW  "9  4"  0)  THEN  Auto)




Home Index