Nuprl Lemma : mk_fabmon
∀s:DSet. ∀g:AbMon. ∀i:|s| ⟶ |g|. ∀U:g':AbMon ⟶ (|s| ⟶ |g'|) ⟶ |g| ⟶ |g'|.
  ((∀g':AbMon. ∀f:|s| ⟶ |g'|.
      (IsMonHom{g,g'}(U g' f)
      ∧ (((U g' f) o i) = f ∈ (|s| ⟶ |g'|))
      ∧ (∀u:|g| ⟶ |g'|. (IsMonHom{g,g'}(u) 
⇒ ((u o i) = f ∈ (|s| ⟶ |g'|)) 
⇒ (u = (U g' f) ∈ (|g| ⟶ |g'|))))))
  
⇒ (<g, i, U> ∈ FAbMon(s)))
Proof
Definitions occuring in Statement : 
free_abmonoid: FAbMon(S)
, 
compose: f o g
, 
all: ∀x:A. B[x]
, 
implies: P 
⇒ Q
, 
and: P ∧ Q
, 
member: t ∈ T
, 
apply: f a
, 
function: x:A ⟶ B[x]
, 
pair: <a, b>
, 
equal: s = t ∈ T
, 
monoid_hom_p: IsMonHom{M1,M2}(f)
, 
abmonoid: AbMon
, 
grp_car: |g|
, 
dset: DSet
, 
set_car: |p|
Definitions unfolded in proof : 
free_abmonoid: FAbMon(S)
, 
all: ∀x:A. B[x]
, 
implies: P 
⇒ Q
, 
member: t ∈ T
, 
uall: ∀[x:A]. B[x]
, 
dset: DSet
, 
subtype_rel: A ⊆r B
, 
abmonoid: AbMon
, 
mon: Mon
, 
so_lambda: λ2x.t[x]
, 
monoid_hom: MonHom(M1,M2)
, 
so_apply: x[s]
, 
prop: ℙ
, 
and: P ∧ Q
, 
unique_set: {!x:T | P[x]}
, 
cand: A c∧ B
, 
guard: {T}
Lemmas referenced : 
set_car_wf, 
abmonoid_wf, 
grp_car_wf, 
unique_set_wf, 
monoid_hom_wf, 
equal_wf, 
compose_wf, 
all_wf, 
monoid_hom_p_wf, 
dset_wf, 
monoid_hom_properties
Rules used in proof : 
sqequalSubstitution, 
sqequalRule, 
sqequalReflexivity, 
sqequalTransitivity, 
computationStep, 
lambdaFormation, 
cut, 
dependent_pairEquality, 
hypothesisEquality, 
functionExtensionality, 
applyEquality, 
introduction, 
extract_by_obid, 
sqequalHypSubstitution, 
isectElimination, 
thin, 
setElimination, 
rename, 
because_Cache, 
hypothesis, 
functionEquality, 
lambdaEquality, 
cumulativity, 
universeEquality, 
productEquality, 
instantiate, 
dependent_set_memberEquality, 
independent_pairFormation, 
dependent_functionElimination, 
productElimination, 
independent_functionElimination
Latex:
\mforall{}s:DSet.  \mforall{}g:AbMon.  \mforall{}i:|s|  {}\mrightarrow{}  |g|.  \mforall{}U:g':AbMon  {}\mrightarrow{}  (|s|  {}\mrightarrow{}  |g'|)  {}\mrightarrow{}  |g|  {}\mrightarrow{}  |g'|.
    ((\mforall{}g':AbMon.  \mforall{}f:|s|  {}\mrightarrow{}  |g'|.
            (IsMonHom\{g,g'\}(U  g'  f)
            \mwedge{}  (((U  g'  f)  o  i)  =  f)
            \mwedge{}  (\mforall{}u:|g|  {}\mrightarrow{}  |g'|.  (IsMonHom\{g,g'\}(u)  {}\mRightarrow{}  ((u  o  i)  =  f)  {}\mRightarrow{}  (u  =  (U  g'  f))))))
    {}\mRightarrow{}  (<g,  i,  U>  \mmember{}  FAbMon(s)))
Date html generated:
2017_10_01-AM-10_01_14
Last ObjectModification:
2017_03_03-PM-01_03_32
Theory : polynom_1
Home
Index