### Nuprl Lemma : rng_times_lsum_r

`∀r:Rng. ∀A:Type. ∀as:A List. ∀f:A ⟶ |r|. ∀u:|r|.  (((Σ{A,r} x ∈ as. f[x]) * u) = (Σ{A,r} x ∈ as. (f[x] * u)) ∈ |r|)`

Proof

Definitions occuring in Statement :  rng_lsum: `Σ{A,r} x ∈ as. f[x]` list: `T List` infix_ap: `x f y` so_apply: `x[s]` all: `∀x:A. B[x]` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T` rng: `Rng` rng_times: `*` rng_car: `|r|`
Definitions unfolded in proof :  all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` member: `t ∈ T` so_lambda: `λ2x.t[x]` rng: `Rng` so_apply: `x[s]` implies: `P `` Q` rng_lsum: `Σ{A,r} x ∈ as. f[x]` top: `Top` add_grp_of_rng: `r↓+gp` grp_id: `e` pi2: `snd(t)` pi1: `fst(t)` and: `P ∧ Q` grp_op: `*` squash: `↓T` prop: `ℙ` infix_ap: `x f y` true: `True` subtype_rel: `A ⊆r B` uimplies: `b supposing a` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q`
Lemmas referenced :  list_induction all_wf rng_car_wf equal_wf infix_ap_wf rng_times_wf rng_lsum_wf list_wf mon_for_nil_lemma rng_times_zero mon_for_cons_lemma squash_wf true_wf rng_plus_wf iff_weakening_equal rng_times_over_plus rng_plus_comm rng_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut thin introduction extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality sqequalRule lambdaEquality functionEquality cumulativity setElimination rename because_Cache hypothesis dependent_functionElimination applyEquality functionExtensionality independent_functionElimination isect_memberEquality voidElimination voidEquality productElimination imageElimination equalityTransitivity equalitySymmetry universeEquality natural_numberEquality imageMemberEquality baseClosed independent_isectElimination

Latex:
\mforall{}r:Rng.  \mforall{}A:Type.  \mforall{}as:A  List.  \mforall{}f:A  {}\mrightarrow{}  |r|.  \mforall{}u:|r|.
(((\mSigma{}\{A,r\}  x  \mmember{}  as.  f[x])  *  u)  =  (\mSigma{}\{A,r\}  x  \mmember{}  as.  (f[x]  *  u)))

Date html generated: 2017_10_01-AM-10_00_58
Last ObjectModification: 2017_03_03-PM-01_02_13

Theory : list_3

Home Index