---

Step * of Lemma massoc_cancel

∀g:IAbMonoid. (Cancel(|g|;|g|;*) ⇒ (∀a,b,c:|g|.  (((a * b) ~ (a * c)) ⇒ (b ~ c))))
BY
{ ((RepUnfolds ``massoc symmetrize`` 0) THEN Auto) 
 }

1
1. g : IAbMonoid@i'
2. Cancel(|g|;|g|;*)@i
3. a : |g|@i
4. b : |g|@i
5. c : |g|@i
6. (a * b) | (a * c)@i
7. (a * c) | (a * b)@i
⊢ b | c

2
1. g : IAbMonoid@i'
2. Cancel(|g|;|g|;*)@i
3. a : |g|@i
4. b : |g|@i
5. c : |g|@i
6. (a * b) | (a * c)@i
7. (a * c) | (a * b)@i
8. b | c
⊢ c | b

---

Latex:

---

Latex:
\mforall{}g:IAbMonoid.  (Cancel(|g|;|g|;*)  {}\mRightarrow{}  (\mforall{}a,b,c:|g|.    (((a  *  b)  \msim{}  (a  *  c))  {}\mRightarrow{}  (b  \msim{}  c))))


By

---

Latex:
((RepUnfolds  ``massoc  symmetrize``  0)  THEN  Auto) 

---

Home Index