---

Step * 1 1 of Lemma mon_reduce_functionality_wrt_permr


1. g : IAbMonoid
2. xs : |g| List
3. ys : |g| List
4. ||xs|| = ||ys|| ∈ ℤ
5. p : Sym(||xs||)
6. ∀i:ℕ||xs||. (xs[p.f i] = ys[i] ∈ |g|)
⊢ (Π 0 ≤ i < ||xs||. xs[i]) = (Π 0 ≤ i < ||ys||. ys[i]) ∈ |g|
BY
{ (RWH (RevHypC 6 ORELSEC RevHypC 4) 0 THENA Auto') }

1
1. g : IAbMonoid
2. xs : |g| List
3. ys : |g| List
4. ||xs|| = ||ys|| ∈ ℤ
5. p : Sym(||xs||)
6. ∀i:ℕ||xs||. (xs[p.f i] = ys[i] ∈ |g|)
⊢ (Π 0 ≤ i < ||xs||. xs[i]) = (Π 0 ≤ i < ||xs||. xs[p.f i]) ∈ |g|

---

Latex:

---

Latex:

1.  g  :  IAbMonoid
2.  xs  :  |g|  List
3.  ys  :  |g|  List
4.  ||xs||  =  ||ys||
5.  p  :  Sym(||xs||)
6.  \mforall{}i:\mBbbN{}||xs||.  (xs[p.f  i]  =  ys[i])
\mvdash{}  (\mPi{}  0  \mleq{}  i  <  ||xs||.  xs[i])  =  (\mPi{}  0  \mleq{}  i  <  ||ys||.  ys[i])


By

---

Latex:
(RWH  (RevHypC  6  ORELSEC  RevHypC  4)  0  THENA  Auto')

---

Home Index