Nuprl Lemma : sq_stable__ideal_p

r:CRng. ∀a:|r| ⟶ ℙ.  ((∀x:|r|. SqStable(a x))  SqStable(a Ideal of r))


Definitions occuring in Statement :  ideal_p: Ideal of R crng: CRng rng_car: |r| sq_stable: SqStable(P) prop: all: x:A. B[x] implies:  Q apply: a function: x:A ⟶ B[x]
Definitions unfolded in proof :  ideal_p: Ideal of R all: x:A. B[x] implies:  Q uall: [x:A]. B[x] member: t ∈ T crng: CRng rng: Rng add_grp_of_rng: r↓+gp grp_car: |g| pi1: fst(t) so_lambda: λ2x.t[x] prop: subtype_rel: A ⊆B so_apply: x[s] subgrp_p: SubGrp of g and: P ∧ Q infix_ap: y
Lemmas referenced :  sq_stable__and subgrp_p_wf add_grp_of_rng_wf all_wf rng_car_wf infix_ap_wf rng_times_wf grp_id_wf grp_car_wf grp_inv_wf grp_op_wf sq_stable__all sq_stable_wf crng_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep lambdaFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin setElimination rename hypothesisEquality hypothesis isect_memberEquality lambdaEquality because_Cache functionEquality applyEquality universeEquality independent_functionElimination productEquality dependent_functionElimination cumulativity

\mforall{}r:CRng.  \mforall{}a:|r|  {}\mrightarrow{}  \mBbbP{}.    ((\mforall{}x:|r|.  SqStable(a  x))  {}\mRightarrow{}  SqStable(a  Ideal  of  r))

Date html generated: 2016_05_15-PM-00_22_52
Last ObjectModification: 2015_12_27-AM-00_01_18

Theory : rings_1

Home Index