Nuprl Lemma : idom_alt_char
∀r:CRng
((∀x,y:|r|. Dec(x = y ∈ |r|))
⇒ (IsIntegDom(r) ⇐⇒ 0 ≠ 1 ∈ |r| ∧ (∀u,v:|r|. (u = 0 ∈ |r|) ∨ (v = 0 ∈ |r|) supposing (u * v) = 0 ∈ |r|)))
Proof
Definitions occuring in Statement :
integ_dom_p: IsIntegDom(r),
crng: CRng,
rng_one: 1,
rng_times: *,
rng_zero: 0,
rng_car: |r|,
decidable: Dec(P),
uimplies: b supposing a,
infix_ap: x f y,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
nequal: a ≠ b ∈ T ,
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
equal: s = t ∈ T
Definitions unfolded in proof :
integ_dom_p: IsIntegDom(r),
all: ∀x:A. B[x],
implies: P ⇒ Q,
iff: P ⇐⇒ Q,
and: P ∧ Q,
nequal: a ≠ b ∈ T ,
not: ¬A,
false: False,
member: t ∈ T,
prop: ℙ,
uall: ∀[x:A]. B[x],
crng: CRng,
rng: Rng,
uimplies: b supposing a,
infix_ap: x f y,
so_lambda: λ2x.t[x],
so_apply: x[s],
rev_implies: P ⇐ Q,
or: P ∨ Q,
decidable: Dec(P),
guard: {T}
Lemmas referenced :
equal_wf,
rng_car_wf,
rng_zero_wf,
rng_one_wf,
rng_times_wf,
nequal_wf,
all_wf,
not_wf,
infix_ap_wf,
isect_wf,
or_wf,
decidable_wf,
crng_wf
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
lambdaFormation,
independent_pairFormation,
cut,
thin,
sqequalHypSubstitution,
hypothesis,
independent_functionElimination,
voidElimination,
introduction,
extract_by_obid,
isectElimination,
setElimination,
rename,
hypothesisEquality,
because_Cache,
isect_memberFormation,
axiomEquality,
applyEquality,
productEquality,
lambdaEquality,
functionEquality,
productElimination,
dependent_functionElimination,
equalityTransitivity,
equalitySymmetry,
unionElimination,
inrFormation,
inlFormation,
independent_isectElimination
Latex:
\mforall{}r:CRng
((\mforall{}x,y:|r|. Dec(x = y))
{}\mRightarrow{} (IsIntegDom(r) \mLeftarrow{}{}\mRightarrow{} 0 \mneq{} 1 \mmember{} |r| \mwedge{} (\mforall{}u,v:|r|. (u = 0) \mvee{} (v = 0) supposing (u * v) = 0)))
Date html generated:
2017_10_01-AM-08_18_26
Last ObjectModification:
2017_02_28-PM-02_03_20
Theory : rings_1
Home
Index