Nuprl Lemma : rng-pps_wf
∀r:IntegDom{i}. ∀[eq:EqDecider(|r|)]. (rng-pps(r;eq) ∈ ProjectivePlane)
Proof
Definitions occuring in Statement :
rng-pps: rng-pps(r;eq),
projective-plane: ProjectivePlane,
deq: EqDecider(T),
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
member: t ∈ T,
integ_dom: IntegDom{i},
rng_car: |r|
Definitions unfolded in proof :
all: ∀x:A. B[x],
uall: ∀[x:A]. B[x],
member: t ∈ T,
projective-plane: ProjectivePlane,
and: P ∧ Q,
subtype_rel: A ⊆r B,
guard: {T},
uimplies: b supposing a,
prop: ℙ,
basic-projective-plane: BasicProjectivePlane,
integ_dom: IntegDom{i},
crng: CRng,
rng: Rng,
zero-vector: 0,
true: True,
squash: ↓T,
less_than: a < b,
less_than': less_than'(a;b),
le: A ≤ B,
lelt: i ≤ j < k,
int_seg: {i..j-},
false: False,
exists: ∃x:A. B[x],
satisfiable_int_formula: satisfiable_int_formula(fmla),
or: P ∨ Q,
decidable: Dec(P),
implies: P ⇒ Q,
not: ¬A,
btrue: tt,
mk-pgeo-prim: mk-pgeo-prim,
bfalse: ff,
ifthenelse: if b then t else f fi ,
eq_atom: x =a y,
top: Top,
pgeo-point: Point,
mk-pgeo: mk-pgeo(p; ss; por; lor; j; m; p3; l3),
rng-pp-primitives: rng-pp-primitives(r),
rng-pps: rng-pps(r;eq),
integ_dom_p: IsIntegDom(r),
nequal: a ≠ b ∈ T ,
nat: ℕ,
sq_stable: SqStable(P),
pgeo-line: Line,
pgeo-plsep: pgeo-plsep(p; a; b),
so_apply: x[s],
so_lambda: λ2x.t[x],
assert: ↑b,
bnot: ¬bb,
sq_type: SQType(T),
eqof: eqof(d),
uiff: uiff(P;Q),
it: ⋅,
unit: Unit,
bool: 𝔹,
exposed-it: exposed-it,
deq: EqDecider(T),
pgeo-incident: a I b,
pgeo-lsep: l ≠ m,
pgeo-lpsep: a ≠ b,
pgeo-psep: a ≠ b,
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
infix_ap: x f y,
scalar-triple-product: |a,b,c|,
cand: A c∧ B,
basic-pgeo-axioms: BasicProjectiveGeometryAxioms(g),
pgeo-leq: a ≡ b,
pgeo-peq: a ≡ b,
mk-complete-pgeo: mk-complete-pgeo(pg;p),
pi1: fst(t),
pgeo-join: p ∨ q,
triangle-axiom1: triangle-axiom1(g),
pgeo-meet: l ∧ m,
triangle-axiom2: triangle-axiom2(g)
Lemmas referenced :
basic-pgeo-axioms_wf,
projective-plane-structure_subtype,
projective-plane-structure-complete_subtype,
subtype_rel_transitivity,
projective-plane-structure-complete_wf,
projective-plane-structure_wf,
pgeo-primitives_wf,
triangle-axiom1_wf,
triangle-axiom2_wf,
deq_wf,
rng_car_wf,
integ_dom_wf,
not_wf,
zero-vector_wf,
equal_wf,
lelt_wf,
false_wf,
int_formula_prop_wf,
int_term_value_constant_lemma,
int_formula_prop_eq_lemma,
int_formula_prop_not_lemma,
itermConstant_wf,
intformeq_wf,
intformnot_wf,
full-omega-unsat,
decidable__equal_int,
int_seg_wf,
rng_one_wf,
rec_select_update_lemma,
mk-complete-pgeo_wf,
mk-pgeo_wf,
rng-pp-primitives_wf,
squash_wf,
rng_zero_wf,
le_wf,
scalar-product_wf,
exists_wf,
assert-bnot,
bool_subtype_base,
subtype_base_sq,
bool_cases_sqequal,
eqff_to_assert,
safe-assert-deq,
eqtt_to_assert,
bool_wf,
cross-product_wf,
decidable__assert,
assert_wf,
cross-product-equal-0,
deq_property,
decidable_functionality,
iff_weakening_uiff,
iff_weakening_equal,
rng_times_zero,
rng_times_wf,
true_wf,
scalar-product-mul,
subtype_rel_self,
crng_times_comm,
scalar-product-0,
scalar-product-comm,
scalar-triple-product-symmetry,
nat_wf,
rng_wf,
cross-product-same,
rng-pp-nontriv1_wf,
rng-pp-nontriv2_wf,
deq-implies,
cross-product-equal-0-iff,
iff_wf,
triple-cross-product-zero,
vector-mul_wf,
vector-mul-mul,
rng_sig_wf,
set_wf,
scalar-triple-product_wf,
rng_minus_wf,
infix_ap_wf,
rng_plus_wf,
Binet-Cauchy-identity,
rng_minus_zero,
rng_plus_zero
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
isect_memberFormation,
introduction,
cut,
dependent_set_memberEquality,
productEquality,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
applyEquality,
hypothesis,
instantiate,
independent_isectElimination,
sqequalRule,
dependent_functionElimination,
because_Cache,
axiomEquality,
equalityTransitivity,
equalitySymmetry,
setElimination,
rename,
functionEquality,
equalityElimination,
baseClosed,
imageMemberEquality,
independent_pairFormation,
intEquality,
dependent_pairFormation,
independent_functionElimination,
approximateComputation,
unionElimination,
functionExtensionality,
applyLambdaEquality,
natural_numberEquality,
lambdaEquality,
voidEquality,
voidElimination,
isect_memberEquality,
productElimination,
setEquality,
imageElimination,
inlEquality,
cumulativity,
promote_hyp,
independent_pairEquality,
dependent_pairEquality,
inrEquality,
levelHypothesis,
equalityUniverse,
universeEquality,
hyp_replacement,
inrFormation
Latex:
\mforall{}r:IntegDom\{i\}. \mforall{}[eq:EqDecider(|r|)]. (rng-pps(r;eq) \mmember{} ProjectivePlane)
Date html generated:
2019_10_16-PM-02_14_01
Last ObjectModification:
2018_08_23-PM-02_17_59
Theory : euclidean!plane!geometry
Home
Index