---

Step * of Lemma rng_times_when_l

∀[r:Rng]. ∀[u,v:|r|]. ∀[b:𝔹].  ((u * (when b. 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|
⊢ (u * 0) = 0 ∈ |r|

---

Latex:

---

Latex:
\mforall{}[r:Rng].  \mforall{}[u,v:|r|].  \mforall{}[b:\mBbbB{}].    ((u  *  (when  b.  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