Step
*
1
1
of Lemma
mdivides_cancel
1. g : IAbMonoid
2. ∀[u,v,w:|g|]. u = v ∈ |g| supposing (w * u) = (w * v) ∈ |g|
3. a : |g|
4. b : |g|
5. c : |g|
6. d : |g|
7. (a * c) = ((a * b) * d) ∈ |g|
⊢ b | c
BY
{ ((RW MonNormC 7) THENA Auto)
THEN ((FHyp 2 [7]) THEN Auto) }
1
1. g : IAbMonoid
2. ∀[u,v,w:|g|]. u = v ∈ |g| supposing (w * u) = (w * v) ∈ |g|
3. a : |g|
4. b : |g|
5. c : |g|
6. d : |g|
7. (a * c) = (a * (b * d)) ∈ |g|
8. c = (b * d) ∈ |g|
⊢ b | 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