---

Step * of Lemma rng_times_when_r

∀[r:Rng]. ∀[u,v:|r|]. ∀[b:𝔹].  (((when b. u) * v) = (when b. (u * v)) ∈ |r|)
BY
{ ((RepD THENM RepUnfolds ``mon_when rng_when`` 0 
THENM OnVar `b' BoolCases THENM AbReduce 0) THENA Auto) }

1
1. r : Rng
2. u : |r|
3. v : |r|
⊢ (u * v) = (u * v) ∈ |r|

2
1. r : Rng
2. u : |r|
3. v : |r|
⊢ (0 * v) = 0 ∈ |r|

---

Latex:

---

Latex:
\mforall{}[r:Rng].  \mforall{}[u,v:|r|].  \mforall{}[b:\mBbbB{}].    (((when  b.  u)  *  v)  =  (when  b.  (u  *  v)))


By

---

Latex:
((RepD  THENM  RepUnfolds  ``mon\_when  rng\_when``  0 
THENM  OnVar  `b'  BoolCases  THENM  AbReduce  0)  THENA  Auto)

---

Home Index