Step
*
2
of Lemma
omral_minus_wf
1. g : OCMon
2. r : CDRng
3. ps : |omral(g;r)|
⊢ --ps ∈ |oal(g↓set;r↓+gp)|
BY
{ (Assert r↓+gp ∈ AbDGrp BY
(DVar `r' THEN MemTypeCD THEN Auto)) }
1
1. g : OCMon
2. r : CDRng
3. ps : |omral(g;r)|
4. r↓+gp ∈ AbDGrp
⊢ --ps ∈ |oal(g↓set;r↓+gp)|
Latex:
Latex:
1. g : OCMon
2. r : CDRng
3. ps : |omral(g;r)|
\mvdash{} --ps \mmember{} |oal(g\mdownarrow{}set;r\mdownarrow{}+gp)|
By
Latex:
(Assert r\mdownarrow{}+gp \mmember{} AbDGrp BY
(DVar `r' THEN MemTypeCD THEN Auto))
Home
Index