Step
*
of Lemma
non_munit_diff_imp_mpdivides
∀g:IAbMonoid. (Cancel(|g|;|g|;*)
⇒ (∀a,b,c:|g|. ((¬(g-unit(b)))
⇒ ((a * b) = c ∈ |g|)
⇒ (a p| c))))
BY
{ ((UnivCD) THENA Auto) }
1
1. g : IAbMonoid
2. Cancel(|g|;|g|;*)
3. a : |g|
4. b : |g|
5. c : |g|
6. ¬(g-unit(b))
7. (a * b) = c ∈ |g|
⊢ a p| c
Latex:
Latex:
\mforall{}g:IAbMonoid. (Cancel(|g|;|g|;*) {}\mRightarrow{} (\mforall{}a,b,c:|g|. ((\mneg{}(g-unit(b))) {}\mRightarrow{} ((a * b) = c) {}\mRightarrow{} (a p| c))))
By
Latex:
((UnivCD) THENA Auto)
Home
Index