Nuprl Lemma : compose_wf_for_mon_hom

[A,B,C:IMonoid]. ∀[f:MonHom(A,B)]. ∀[g:MonHom(B,C)].  (g f ∈ MonHom(A,C))


Proof




Definitions occuring in Statement :  monoid_hom: MonHom(M1,M2) imon: IMonoid compose: g uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T imon: IMonoid monoid_hom: MonHom(M1,M2) prop: monoid_hom_p: IsMonHom{M1,M2}(f) fun_thru_2op: FunThru2op(A;B;opa;opb;f) and: P ∧ Q cand: c∧ B compose: g squash: T true: True subtype_rel: A ⊆B uimplies: supposing a guard: {T} iff: ⇐⇒ Q rev_implies:  Q implies:  Q
Lemmas referenced :  monoid_hom_wf imon_wf compose_wf grp_car_wf monoid_hom_p_wf monoid_hom_properties and_wf equal_wf squash_wf true_wf infix_ap_wf grp_op_wf iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution hypothesis sqequalRule axiomEquality equalityTransitivity equalitySymmetry extract_by_obid isectElimination thin setElimination rename hypothesisEquality isect_memberEquality because_Cache dependent_set_memberEquality functionExtensionality applyEquality productElimination independent_pairFormation hyp_replacement applyLambdaEquality lambdaEquality imageElimination universeEquality natural_numberEquality imageMemberEquality baseClosed independent_isectElimination independent_functionElimination

Latex:
\mforall{}[A,B,C:IMonoid].  \mforall{}[f:MonHom(A,B)].  \mforall{}[g:MonHom(B,C)].    (g  o  f  \mmember{}  MonHom(A,C))



Date html generated: 2017_10_01-AM-08_14_17
Last ObjectModification: 2017_02_28-PM-01_58_41

Theory : groups_1


Home Index