Nuprl Lemma : fma_from_gcp_wf
∀g:GrpSig. ∀r:RngSig. ∀c:gcopower_sig{i:l}(g↓set;r↓+gp). ∀a:algebra{i:l}(r).
(((a↓grp) = c.grp ∈ GrpSig) ⇒ (fma_from_gcp(g;r;c;a) ∈ fma_sig{i:l}(g;r)))
Proof
Definitions occuring in Statement :
fma_from_gcp: fma_from_gcp(g;r;c;a),
fma_sig: fma_sig{i:l}(G;A),
gcopower_grp: g1.grp,
gcopower_sig: gcopower_sig{i:l}(s;g),
algebra: algebra{i:l}(A),
grp_of_module: m↓grp,
all: ∀x:A. B[x],
implies: P ⇒ Q,
member: t ∈ T,
equal: s = t ∈ T,
add_grp_of_rng: r↓+gp,
rng_sig: RngSig,
dset_of_mon: g↓set,
grp_sig: GrpSig
Definitions unfolded in proof :
fma_from_gcp: fma_from_gcp(g;r;c;a),
fma_sig: fma_sig{i:l}(G;A),
all: ∀x:A. B[x],
implies: P ⇒ Q,
member: t ∈ T,
uall: ∀[x:A]. B[x],
algebra: algebra{i:l}(A),
module: A-Module,
prop: ℙ,
tlambda: λx:T. b[x],
grp_of_module: m↓grp,
add_grp_of_rng: r↓+gp,
grp_car: |g|,
pi1: fst(t),
rng_of_alg: a↓rg,
rng_car: |r|,
squash: ↓T,
true: True,
label: ...$L... t,
dset_of_mon: g↓set,
set_car: |p|,
subtype_rel: A ⊆r B,
guard: {T},
uimplies: b supposing a
Lemmas referenced :
set_car_wf,
alg_act_wf,
grp_of_module_wf2,
gcopower_umap_wf,
ext-eq_weakening,
subtype_rel_weakening,
rng_one_wf,
gcopower_inj_wf,
true_wf,
squash_wf,
rng_sig_wf,
gcopower_sig_wf,
add_grp_of_rng_wf,
dset_of_mon_wf0,
gcopower_grp_wf,
grp_of_module_wf,
grp_sig_wf,
equal_wf,
rng_car_wf,
alg_car_wf,
grp_car_wf,
algebra_wf
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
lambdaFormation,
cut,
dependent_pairEquality,
functionEquality,
lemma_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
hypothesisEquality,
hypothesis,
cumulativity,
isectElimination,
setElimination,
rename,
productEquality,
instantiate,
lambdaEquality,
applyEquality,
imageElimination,
equalityTransitivity,
equalitySymmetry,
natural_numberEquality,
imageMemberEquality,
baseClosed,
independent_isectElimination,
because_Cache
Latex:
\mforall{}g:GrpSig. \mforall{}r:RngSig. \mforall{}c:gcopower\_sig\{i:l\}(g\mdownarrow{}set;r\mdownarrow{}+gp). \mforall{}a:algebra\{i:l\}(r).
(((a\mdownarrow{}grp) = c.grp) {}\mRightarrow{} (fma\_from\_gcp(g;r;c;a) \mmember{} fma\_sig\{i:l\}(g;r)))
Date html generated:
2016_05_16-AM-08_14_50
Last ObjectModification:
2016_01_16-PM-11_41_54
Theory : polynom_1
Home
Index