### Nuprl Lemma : mon_itop_split

`∀[g:IMonoid]. ∀[a,b,c:ℤ].`
`  (∀[E:{a..c-} ⟶ |g|]. ((Π a ≤ j < c. E[j]) = ((Π a ≤ j < b. E[j]) * (Π b ≤ j < c. E[j])) ∈ |g|)) supposing `
`     ((b ≤ c) and `
`     (a ≤ b))`

Proof

Definitions occuring in Statement :  mon_itop: `Π lb ≤ i < ub. E[i]` imon: `IMonoid` grp_op: `*` grp_car: `|g|` int_seg: `{i..j-}` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` infix_ap: `x f y` so_apply: `x[s]` le: `A ≤ B` function: `x:A ⟶ B[x]` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  mon_itop: `Π lb ≤ i < ub. E[i]`
Lemmas referenced :  itop_split
Rules used in proof :  cut lemma_by_obid sqequalHypSubstitution sqequalRule sqequalReflexivity sqequalSubstitution sqequalTransitivity computationStep hypothesis

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

Date html generated: 2016_05_15-PM-00_16_11
Last ObjectModification: 2015_12_26-PM-11_39_40

Theory : groups_1

Home Index