---

Step * 1 1 2 of Lemma itop_split


1. g : IMonoid
2. a : ℤ
3. c : ℤ
4. b : {a + 1...}
5. ∀[E:{a..c-} ⟶ |g|]. (Π(*,e) a ≤ j < c. E[j] = (Π(*,e) a ≤ j < b - 1. E[j] * Π(*,e) b - 1 ≤ j < c. E[j]) ∈ |g|) 
   supposing (b - 1) ≤ c
6. b ≤ c
7. E : {a..c-} ⟶ |g|
⊢ Π(*,e) a ≤ j < c. E[j] = (Π(*,e) a ≤ j < b. E[j] * Π(*,e) b ≤ j < c. E[j]) ∈ |g|
BY
{ RW (HigherC (HypC 5)) 0 
THENM Thin 5 THENA Auto }

1
1. g : IMonoid
2. a : ℤ
3. c : ℤ
4. b : {a + 1...}
5. b ≤ c
6. E : {a..c-} ⟶ |g|
⊢ (Π(*,e) a ≤ j < b - 1. E[j] * Π(*,e) b - 1 ≤ j < c. E[j]) = (Π(*,e) a ≤ j < b. E[j] * Π(*,e) b ≤ j < c. E[j]) ∈ |g|

---

Latex:

---

Latex:

1.  g  :  IMonoid
2.  a  :  \mBbbZ{}
3.  c  :  \mBbbZ{}
4.  b  :  \{a  +  1...\}
5.  \mforall{}[E:\{a..c\msupminus{}\}  {}\mrightarrow{}  |g|]
          (\mPi{}(*,e)  a  \mleq{}  j  <  c.  E[j]  =  (\mPi{}(*,e)  a  \mleq{}  j  <  b  -  1.  E[j]  *  \mPi{}(*,e)  b  -  1  \mleq{}  j  <  c.  E[j])) 
      supposing  (b  -  1)  \mleq{}  c
6.  b  \mleq{}  c
7.  E  :  \{a..c\msupminus{}\}  {}\mrightarrow{}  |g|
\mvdash{}  \mPi{}(*,e)  a  \mleq{}  j  <  c.  E[j]  =  (\mPi{}(*,e)  a  \mleq{}  j  <  b.  E[j]  *  \mPi{}(*,e)  b  \mleq{}  j  <  c.  E[j])


By

---

Latex:
RW  (HigherC  (HypC  5))  0 
THENM  Thin  5  THENA  Auto

---

Home Index