### 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_lambda(x,y,z.t[x; y; z])` 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: 2019_10_31-AM-07_23_46
Last ObjectModification: 2018_08_21-PM-03_50_05

Theory : free!groups

Home Index