Step * 1 1 of Lemma mdivides_cancel


1. IAbMonoid
2. ∀[u,v,w:|g|].  v ∈ |g| supposing (w u) (w v) ∈ |g|
3. |g|
4. |g|
5. |g|
6. |g|
7. (a c) ((a b) d) ∈ |g|
⊢ c
BY
((RW MonNormC 7) THENA Auto) 
THEN ((FHyp [7]) THEN Auto) }

1
1. IAbMonoid
2. ∀[u,v,w:|g|].  v ∈ |g| supposing (w u) (w v) ∈ |g|
3. |g|
4. |g|
5. |g|
6. |g|
7. (a c) (a (b d)) ∈ |g|
8. (b d) ∈ |g|
⊢ c


Latex:


Latex:

1.  g  :  IAbMonoid
2.  \mforall{}[u,v,w:|g|].    u  =  v  supposing  (w  *  u)  =  (w  *  v)
3.  a  :  |g|
4.  b  :  |g|
5.  c  :  |g|
6.  d  :  |g|
7.  (a  *  c)  =  ((a  *  b)  *  d)
\mvdash{}  b  |  c


By


Latex:
((RW  MonNormC  7)  THENA  Auto) 
THEN  ((FHyp  2  [7])  THEN  Auto)




Home Index