---

Step * 1 1 of Lemma mon_itop_txpose_invar


1. g : IAbMonoid
2. n : ℕ
3. E : ℕn ⟶ |g|
4. x : ℕ+n
⊢ (Π 0 ≤ j < n. E[swap{n}(x;0) j]) = (Π 0 ≤ j < n. E[j]) ∈ |g|
BY
{ (RWH (LemmaWithC [`b',x] `mon_itop_split_el`) 0 THENA Auto) }

1
1. g : IAbMonoid
2. n : ℕ
3. E : ℕn ⟶ |g|
4. x : ℕ+n
⊢ ((Π 0 ≤ j < x. E[swap{n}(x;0) j]) * (E[swap{n}(x;0) x] * (Π x + 1 ≤ j < n. E[swap{n}(x;0) j])))
= ((Π 0 ≤ j < x. E[j]) * (E[x] * (Π x + 1 ≤ j < n. E[j])))
∈ |g|

---

Latex:

---

Latex:

1.  g  :  IAbMonoid
2.  n  :  \mBbbN{}
3.  E  :  \mBbbN{}n  {}\mrightarrow{}  |g|
4.  x  :  \mBbbN{}\msupplus{}n
\mvdash{}  (\mPi{}  0  \mleq{}  j  <  n.  E[swap\{n\}(x;0)  j])  =  (\mPi{}  0  \mleq{}  j  <  n.  E[j])


By

---

Latex:
(RWH  (LemmaWithC  [`b',x]  `mon\_itop\_split\_el`)  0  THENA  Auto)

---

Home Index