---

Step * 1 1 of Lemma itop_split


1. g : IMonoid
2. a : ℤ
3. c : ℤ
⊢ ∀b:{a...}
    ∀[E:{a..c-} ⟶ |g|]. (Π(*,e) a ≤ j < c. E[j] = (Π(*,e) a ≤ j < b. E[j] * Π(*,e) b ≤ j < c. E[j]) ∈ |g|) 
    supposing b ≤ c
BY
{ BackThruLemma `int_upper_ind` 
THENM UnivCD THENA Auto }

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

2
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|

---

Latex:

---

Latex:

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


By

---

Latex:
BackThruLemma  `int\_upper\_ind` 
THENM  UnivCD  THENA  Auto

---

Home Index