### Nuprl Lemma : fg-hom-append

`∀[X:Type]. ∀[G:Group{i}]. ∀[f:X ⟶ |G|]. ∀[a,b:(X + X) List].`
`  (fg-hom(G;f;a @ b) = (fg-hom(G;f;a) * fg-hom(G;f;b)) ∈ |G|)`

Proof

Definitions occuring in Statement :  fg-hom: `fg-hom(G;f;w)` append: `as @ bs` list: `T List` uall: `∀[x:A]. B[x]` infix_ap: `x f y` function: `x:A ⟶ B[x]` union: `left + right` universe: `Type` equal: `s = t ∈ T` grp: `Group{i}` grp_op: `*` grp_car: `|g|`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` fg-hom: `fg-hom(G;f;w)` subtype_rel: `A ⊆r B` uimplies: `b supposing a` top: `Top` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` grp: `Group{i}` mon: `Mon` infix_ap: `x f y` all: `∀x:A. B[x]` implies: `P `` Q` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` imon: `IMonoid` and: `P ∧ Q` squash: `↓T` true: `True` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q`
Lemmas referenced :  list_accum_append subtype_rel_list top_wf list_accum_wf grp_car_wf grp_id_wf grp_op_wf grp_inv_wf equal_wf list_wf grp_wf list_induction all_wf list_accum_nil_lemma mon_ident grp_sig_wf monoid_p_wf inverse_wf list_accum_cons_lemma squash_wf true_wf subtype_rel_self iff_weakening_equal mon_assoc
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality applyEquality unionEquality hypothesis independent_isectElimination lambdaEquality isect_memberEquality voidElimination voidEquality because_Cache setElimination rename equalityTransitivity equalitySymmetry lambdaFormation unionElimination dependent_functionElimination independent_functionElimination axiomEquality functionEquality universeEquality setEquality cumulativity productElimination imageElimination natural_numberEquality imageMemberEquality baseClosed instantiate

Latex:
\mforall{}[X:Type].  \mforall{}[G:Group\{i\}].  \mforall{}[f:X  {}\mrightarrow{}  |G|].  \mforall{}[a,b:(X  +  X)  List].
(fg-hom(G;f;a  @  b)  =  (fg-hom(G;f;a)  *  fg-hom(G;f;b)))

Date html generated: 2020_05_20-AM-08_23_01
Last ObjectModification: 2018_08_21-PM-02_02_33

Theory : free!groups

Home Index