---

Step * 1 of Lemma mon_reduce_functionality_wrt_permr


1. g : IAbMonoid
2. xs : |g| List
3. ys : |g| List
4. xs ≡(|g|) ys
⊢ (Π xs) = (Π ys) ∈ |g|
BY
{ ((D 4 THEN D 5) THEN (RWH (LemmaC `mon_reduce_eq_itop`) 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 < ||ys||. ys[i]) ∈ |g|

---

Latex:

---

Latex:

1.  g  :  IAbMonoid
2.  xs  :  |g|  List
3.  ys  :  |g|  List
4.  xs  \mequiv{}(|g|)  ys
\mvdash{}  (\mPi{}  xs)  =  (\mPi{}  ys)


By

---

Latex:
((D  4  THEN  D  5)  THEN  (RWH  (LemmaC  `mon\_reduce\_eq\_itop`)  0  THENA  Auto))

---

Home Index