Nuprl Lemma : rng_times_lsum_l

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


Proof




Definitions occuring in Statement :  rng_lsum: Σ{A,r} x ∈ as. f[x] list: List infix_ap: y so_apply: x[s] all: x:A. B[x] function: x:A ⟶ B[x] universe: Type equal: 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:  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: y true: True subtype_rel: A ⊆B uimplies: supposing a guard: {T} iff: ⇐⇒ Q rev_implies:  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|.
    ((u  *  (\mSigma{}\{A,r\}  x  \mmember{}  as.  f[x]))  =  (\mSigma{}\{A,r\}  x  \mmember{}  as.  (u  *  f[x])))



Date html generated: 2017_10_01-AM-10_00_57
Last ObjectModification: 2017_03_03-PM-01_02_14

Theory : list_3


Home Index