Nuprl Lemma : free-group-generators
∀[X:Type]
∀G:Group{i}
∀[f,g:MonHom(free-group(X),G)].
f = g ∈ MonHom(free-group(X),G) supposing ∀x:X. ((f free-letter(x)) = (g free-letter(x)) ∈ |G|)
Proof
Definitions occuring in Statement :
free-letter: free-letter(x),
free-group: free-group(X),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
apply: f a,
universe: Type,
equal: s = t ∈ T,
monoid_hom: MonHom(M1,M2),
grp: Group{i},
grp_car: |g|
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
all: ∀x:A. B[x],
uimplies: b supposing a,
subtype_rel: A ⊆r B,
grp: Group{i},
mon: Mon,
monoid_hom: MonHom(M1,M2),
prop: ℙ,
so_lambda: λ2x.t[x],
free-word: free-word(X),
quotient: x,y:A//B[x; y],
grp_car: |g|,
pi1: fst(t),
free-group: free-group(X),
guard: {T},
so_apply: x[s],
implies: P ⇒ Q,
cand: A c∧ B,
and: P ∧ Q,
squash: ↓T,
true: True,
equiv_rel: EquivRel(T;x,y.E[x; y]),
refl: Refl(T;x,y.E[x; y]),
word-equiv: word-equiv(X;w1;w2),
exists: ∃x:A. B[x],
transitive-reflexive-closure: R^*,
or: P ∨ Q,
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
rel_implies: R1 => R2,
infix_ap: x f y,
trans: Trans(T;x,y.E[x; y]),
word-rel: word-rel(X;w1;w2),
free-append: w + w',
grp_inv: ~,
pi2: snd(t),
monoid_hom_p: IsMonHom{M1,M2}(f),
grp_op: *,
grp_id: e,
fun_thru_2op: FunThru2op(A;B;opa;opb;f),
listp: A List+,
imon: IMonoid,
append: as @ bs,
so_lambda: so_lambda3,
top: Top,
so_apply: x[s1;s2;s3],
free-word-inv: free-word-inv(w),
inverse-letters: a = -b,
free-0: 0,
free-letter: free-letter(x)
Lemmas referenced :
monoid_hom_properties,
free-group_wf,
monoid_hom_p_wf,
all_wf,
equal_wf,
grp_car_wf,
free-letter_wf,
subtype_rel_self,
mon_subtype_grp_sig,
grp_subtype_mon,
subtype_rel_transitivity,
grp_wf,
mon_wf,
grp_sig_wf,
monoid_hom_wf,
word-equiv-equiv,
list_wf,
word-equiv_wf,
equal-wf-base,
squash_wf,
true_wf,
subtype_quotient,
iff_weakening_equal,
transitive-closure-minimal,
word-rel_wf,
grp_hom_inv,
grp_subtype_igrp,
free-append_wf,
cons_wf_listp,
cons_wf,
nil_wf,
subtype_rel_set,
free-word_wf,
less_than_wf,
length_wf,
grp_op_wf,
infix_ap_wf,
monoid_p_wf,
grp_id_wf,
inverse_wf,
grp_inv_wf,
mon_ident,
list_ind_cons_lemma,
list_ind_nil_lemma,
reverse-cons,
reverse_nil_lemma,
map_cons_lemma,
map_nil_lemma,
decide_wf,
free-word-inv_wf,
grp_inverse,
uall_wf,
free-0_wf,
list_induction
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
lambdaFormation,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
hypothesis,
applyEquality,
because_Cache,
sqequalRule,
setElimination,
rename,
dependent_set_memberEquality,
lambdaEquality,
instantiate,
independent_isectElimination,
isect_memberEquality,
axiomEquality,
equalityTransitivity,
equalitySymmetry,
dependent_functionElimination,
universeEquality,
functionExtensionality,
unionEquality,
promote_hyp,
independent_pairFormation,
pointwiseFunctionality,
pertypeElimination,
productElimination,
independent_functionElimination,
productEquality,
imageElimination,
natural_numberEquality,
imageMemberEquality,
baseClosed,
unionElimination,
cumulativity,
hyp_replacement,
applyLambdaEquality,
setEquality,
voidElimination,
voidEquality,
inlEquality,
inrEquality,
equalityUniverse,
levelHypothesis
Latex:
\mforall{}[X:Type]
\mforall{}G:Group\{i\}
\mforall{}[f,g:MonHom(free-group(X),G)]. f = g supposing \mforall{}x:X. ((f free-letter(x)) = (g free-letter(x)))
Date html generated:
2020_05_20-AM-08_22_58
Last ObjectModification:
2018_08_21-PM-03_50_05
Theory : free!groups
Home
Index