---

Step * of Lemma mod_action_when_r

∀r:Rng. ∀m:r-Module. ∀u:|r|. ∀x:m.car. ∀b:𝔹.  (((when b. u) m.act x) = (when b. (u m.act x)) ∈ m.car)
BY
{ ((RepD 
THENM InvertRel 0 
THENM Unfold `rng_when` 0 
THENM RWH grp_of_moduleC 0) THENA Auto) }

1
1. r : Rng@i'
2. m : r-Module@i'
3. u : |r|@i
4. x : m.car@i
5. b : 𝔹@i
⊢ (when b. (u m.act x)) = ((when b. u) m.act x) ∈ |(m↓grp)|

---

Latex:

---

Latex:
\mforall{}r:Rng.  \mforall{}m:r-Module.  \mforall{}u:|r|.  \mforall{}x:m.car.  \mforall{}b:\mBbbB{}.    (((when  b.  u)  m.act  x)  =  (when  b.  (u  m.act  x)))


By

---

Latex:
((RepD 
THENM  InvertRel  0 
THENM  Unfold  `rng\_when`  0 
THENM  RWH  grp\_of\_moduleC  0)  THENA  Auto)

---

Home Index