Nuprl Lemma : int-vs_wf
ℤ ∈ VectorSpace(ℤ-rng)
Proof
Definitions occuring in Statement :
int-vs: ℤ,
vector-space: VectorSpace(K),
member: t ∈ T,
int_ring: ℤ-rng
Definitions unfolded in proof :
member: t ∈ T,
uall: ∀[x:A]. B[x],
subtype_rel: A ⊆r B,
integ_dom: IntegDom{i},
crng: CRng
Lemmas referenced :
one-dim-int-vs,
one-dim-vs_wf,
int_ring_wf
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
cut,
introduction,
extract_by_obid,
hypothesis,
sqequalTransitivity,
computationStep,
sqequalHypSubstitution,
isectElimination,
thin,
applyEquality,
lambdaEquality_alt,
setElimination,
rename,
hypothesisEquality,
inhabitedIsType,
equalityTransitivity,
equalitySymmetry
Latex:
\mBbbZ{} \mmember{} VectorSpace(\mBbbZ{}-rng)
Date html generated:
2019_10_31-AM-06_26_44
Last ObjectModification:
2019_08_02-PM-03_59_15
Theory : linear!algebra
Home
Index