---

Step * 1 1 of Lemma mod_action_when_r


1. r : Rng@i'
2. m : r-Module@i'
3. u : |r|@i
4. x : m.car@i
5. b : 𝔹@i
⊢ (when b. ((λx,y. (m.act y x)) x u)) = ((λx,y. (m.act y x)) x (when b. u)) ∈ |(m↓grp)|
BY
{ ((BLemma `mon_when_hom_swap`) THENA Auto) }

---

Latex:

---

Latex:

1.  r  :  Rng@i'
2.  m  :  r-Module@i'
3.  u  :  |r|@i
4.  x  :  m.car@i
5.  b  :  \mBbbB{}@i
\mvdash{}  (when  b.  ((\mlambda{}x,y.  (m.act  y  x))  x  u))  =  ((\mlambda{}x,y.  (m.act  y  x))  x  (when  b.  u))


By

---

Latex:
((BLemma  `mon\_when\_hom\_swap`)  THENA  Auto)

---

Home Index