### Nuprl Lemma : quot_by_prime_ideal

`∀r:CRng. ∀p:Ideal(r){i}. ∀d:detach_fun(|r|;p).  ((∀u:|r|. SqStable(p u)) `` (IsPrimeIdeal(r;p) `⇐⇒` IsIntegDom(r / d)))`

Proof

Definitions occuring in Statement :  prime_ideal_p: `IsPrimeIdeal(R;P)` quot_ring: `r / d` ideal: `Ideal(r){i}` integ_dom_p: `IsIntegDom(r)` crng: `CRng` rng_car: `|r|` detach_fun: `detach_fun(T;A)` sq_stable: `SqStable(P)` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` implies: `P `` Q` apply: `f a`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` prop: `ℙ` uall: `∀[x:A]. B[x]` crng: `CRng` rng: `Rng` so_lambda: `λ2x.t[x]` ideal: `Ideal(r){i}` so_apply: `x[s]` integ_dom_p: `IsIntegDom(r)` nequal: `a ≠ b ∈ T ` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` subtype_rel: `A ⊆r B` guard: `{T}` uimplies: `b supposing a` infix_ap: `x f y` type_inj: `[x]{T}` quot_ring: `r / d` rng_one: `1` pi2: `snd(t)` pi1: `fst(t)` rng_zero: `0` rng_times: `*` true: `True` squash: `↓T` or: `P ∨ Q` false: `False` not: `¬A` cand: `A c∧ B` decidable: `Dec(P)` prime_ideal_p: `IsPrimeIdeal(R;P)`
Lemmas referenced :  all_wf rng_car_wf sq_stable_wf detach_fun_wf ideal_wf crng_wf not_functionality_wrt_iff equal_wf quot_ring_wf rng_subtype_rng_sig crng_subtype_rng subtype_rel_transitivity rng_wf rng_sig_wf type_inj_wf_for_qrng rng_one_wf rng_zero_wf rng_plus_wf rng_minus_wf quot_ring_car_elim_b rng_times_wf not_wf prime_ideal_p_wf subtype_rel_self all_rng_quot_elim_a rev_implies_wf sq_stable__all sq_stable__equal squash_wf true_wf rng_plus_zero iff_weakening_equal rng_plus_comm rng_minus_zero or_wf dec_alt_char iff_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin setElimination rename hypothesisEquality hypothesis sqequalRule lambdaEquality applyEquality because_Cache productElimination independent_pairFormation independent_functionElimination instantiate independent_isectElimination dependent_functionElimination cumulativity universeEquality productEquality functionEquality equalityTransitivity equalitySymmetry natural_numberEquality imageElimination imageMemberEquality baseClosed voidElimination inlFormation inrFormation unionElimination addLevel

Latex:
\mforall{}r:CRng.  \mforall{}p:Ideal(r)\{i\}.  \mforall{}d:detach\_fun(|r|;p).
((\mforall{}u:|r|.  SqStable(p  u))  {}\mRightarrow{}  (IsPrimeIdeal(r;p)  \mLeftarrow{}{}\mRightarrow{}  IsIntegDom(r  /  d)))

Date html generated: 2019_10_15-AM-10_33_56
Last ObjectModification: 2018_08_29-AM-10_10_15

Theory : rings_1

Home Index