---

Step * of Lemma mod_action_when_l

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

---

Latex:

---

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


By

---

Latex:
((RepD 
THENM  InvertRel  0 
THENM  RWH  grp\_of\_moduleC  0 
THENM  BLemma  `mon\_when\_hom\_swap`)  THENA  Auto)

---

Home Index