Nuprl Lemma : module_hom_properties
∀A:RngSig. ∀M,N:algebra_sig{i:l}(|A|). ∀f:module_hom(A; M; N). module_hom_p(A; M; N; f)
Proof
Definitions occuring in Statement :
module_hom: module_hom(A; M; N),
module_hom_p: module_hom_p(a; m; n; f),
algebra_sig: algebra_sig{i:l}(A),
all: ∀x:A. B[x],
rng_car: |r|,
rng_sig: RngSig
Definitions unfolded in proof :
all: ∀x:A. B[x],
module_hom: module_hom(A; M; N),
member: t ∈ T,
sq_stable: SqStable(P),
implies: P ⇒ Q,
squash: ↓T,
uall: ∀[x:A]. B[x]
Lemmas referenced :
rng_sig_wf,
rng_car_wf,
algebra_sig_wf,
module_hom_wf,
sq_stable__module_hom_p
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
sqequalHypSubstitution,
setElimination,
thin,
rename,
cut,
lemma_by_obid,
dependent_functionElimination,
hypothesisEquality,
hypothesis,
independent_functionElimination,
introduction,
sqequalRule,
imageMemberEquality,
baseClosed,
imageElimination,
isectElimination
Latex:
\mforall{}A:RngSig. \mforall{}M,N:algebra\_sig\{i:l\}(|A|). \mforall{}f:module\_hom(A; M; N). module\_hom\_p(A; M; N; f)
Date html generated:
2016_05_16-AM-07_27_15
Last ObjectModification:
2016_01_16-PM-09_59_57
Theory : algebras_1
Home
Index