Step
*
1
2
1
of Lemma
lookup_omral_scale_c
1. g : OCMon
2. r : CDRng
3. z : |g|
4. k : |g|
5. v : |r|
6. ps : |omral(g;r)|
7. d : |g|
8. ↑(d
∈b dom(ps))
9. (k * d) = z ∈ |g|
⊢ ((<k,v>* ps)[z]) = (msFor{r↓+gp} y ∈ dom(ps). when (k * y) =b z. (v * (ps[y]))) ∈ |r|
BY
{ Unfold `rng_when` 0 THEN
((RW (SweepUpC
(RevHypC 9
ORELSEC LemmaC `lookup_omral_scale_a`
ORELSEC LemmaWithC [`u',d] `fset_for_when_unique`)) 0) THENA Auto) }
1
1. g : OCMon
2. r : CDRng
3. z : |g|
4. k : |g|
5. v : |r|
6. ps : |omral(g;r)|
7. d : |g|
8. ↑(d
∈b dom(ps))
9. (k * d) = z ∈ |g|
10. v1 : |(g↓oset)|
11. ↑((k * v1) =b (k * d))
12. ↑(v1
∈b dom(ps))
⊢ v1 = d ∈ |(g↓oset)|
2
1. g : OCMon
2. r : CDRng
3. z : |g|
4. k : |g|
5. v : |r|
6. ps : |omral(g;r)|
7. d : |g|
8. ↑(d
∈b dom(ps))
9. (k * d) = z ∈ |g|
⊢ (v * (ps[d])) = (v * (ps[d])) ∈ |r|
Latex:
Latex:
1. g : OCMon
2. r : CDRng
3. z : |g|
4. k : |g|
5. v : |r|
6. ps : |omral(g;r)|
7. d : |g|
8. \muparrow{}(d
\mmember{}\msubb{} dom(ps))
9. (k * d) = z
\mvdash{} ((<k,v>* ps)[z]) = (msFor\{r\mdownarrow{}+gp\} y \mmember{} dom(ps). when (k * y) =\msubb{} z. (v * (ps[y])))
By
Latex:
Unfold `rng\_when` 0 THEN
((RW (SweepUpC
(RevHypC 9
ORELSEC LemmaC `lookup\_omral\_scale\_a`
ORELSEC LemmaWithC [`u',d] `fset\_for\_when\_unique`)) 0) THENA Auto)
Home
Index