---

Step * 1 1 of Lemma mreducible_elim


1. g : IAbMonoid
2. Cancel(|g|;|g|;*)
3. a : |g|
⊢ ∃b:|g|. ((¬(g-unit(b))) ∧ (∃c:|g|. ((¬(g-unit(c))) ∧ (a = (b * c) ∈ |g|)))) ⇐⇒ ∃b:|g|. ((¬(g-unit(b))) ∧ (b p| a))
BY
{ (Auto THEN ExRepD THEN (With ⌜b⌝ (D 0)⋅ THEN Auto)⋅) }

1
1. g : IAbMonoid
2. Cancel(|g|;|g|;*)
3. a : |g|
4. b : |g|
5. ¬(g-unit(b))
6. c : |g|
7. ¬(g-unit(c))
8. a = (b * c) ∈ |g|
9. ¬(g-unit(b))
⊢ b p| a

2
1. g : IAbMonoid
2. Cancel(|g|;|g|;*)
3. a : |g|
4. b : |g|
5. ¬(g-unit(b))
6. b p| a
7. ¬(g-unit(b))
⊢ ∃c:|g|. ((¬(g-unit(c))) ∧ (a = (b * c) ∈ |g|))

---

Latex:

---

Latex:

1.  g  :  IAbMonoid
2.  Cancel(|g|;|g|;*)
3.  a  :  |g|
\mvdash{}  \mexists{}b:|g|.  ((\mneg{}(g-unit(b)))  \mwedge{}  (\mexists{}c:|g|.  ((\mneg{}(g-unit(c)))  \mwedge{}  (a  =  (b  *  c)))))
\mLeftarrow{}{}\mRightarrow{}  \mexists{}b:|g|.  ((\mneg{}(g-unit(b)))  \mwedge{}  (b  p|  a))


By

---

Latex:
(Auto  THEN  ExRepD  THEN  (With  \mkleeneopen{}b\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)\mcdot{})

---

Home Index