---

Step * 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. (u m.act x)) = ((when b. u) m.act x) ∈ |(m↓grp)|
BY
{ Unfold `infix_ap` 0  
THENM RWH RevCurryC 0 }

1
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)|

---

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.  (u  m.act  x))  =  ((when  b.  u)  m.act  x)


By

---

Latex:
Unfold  `infix\_ap`  0   
THENM  RWH  RevCurryC  0

---

Home Index