---

Step * of Lemma gcopower_properties

∀s:DSet. ∀g:AbGrp. ∀c:gcopower{i}(s;g).
  (IsEqFun(|c.grp|;=b)
  ∧ grp_p(c.grp)
  ∧ Comm(|c.grp|;*)
  ∧ (∀j:|s|. IsMonHom{g,c.grp}(c.inj j))
  ∧ (∀h:AbGrp. ∀f:|s| ⟶ MonHom(g,h).
       (c.umap h f) = !v:|c.grp| ⟶ |h|. (IsMonHom{c.grp,h}(v) ∧ (∀j:|s|. ((f j) = (v o (c.inj j)) ∈ (|g| ⟶ |h|))))))
BY
{ (Auto THEN DVar `c' THEN Unhide THEN Auto THEN Try (BackThruSomeHyp)) }

1
1. s : DSet@i'
2. g : AbGrp@i'
3. c : gcopower_sig{i:l}(s;g)@i'
4. [%2] : IsEqFun(|c.grp|;=b)
∧ grp_p(c.grp)
∧ Comm(|c.grp|;*)
∧ (∀j:|s|. IsMonHom{g,c.grp}(c.inj j))
∧ (∀h:AbGrp. ∀f:|s| ⟶ MonHom(g,h).
     (c.umap h f) = !v:|c.grp| ⟶ |h|. (IsMonHom{c.grp,h}(v) ∧ (∀j:|s|. ((f j) = (v o (c.inj j)) ∈ (|g| ⟶ |h|)))))@i'
5. IsEqFun(|c.grp|;=b)
⊢ SqStable(grp_p(c.grp))

---

Latex:

---

Latex:
\mforall{}s:DSet.  \mforall{}g:AbGrp.  \mforall{}c:gcopower\{i\}(s;g).
    (IsEqFun(|c.grp|;=\msubb{})
    \mwedge{}  grp\_p(c.grp)
    \mwedge{}  Comm(|c.grp|;*)
    \mwedge{}  (\mforall{}j:|s|.  IsMonHom\{g,c.grp\}(c.inj  j))
    \mwedge{}  (\mforall{}h:AbGrp.  \mforall{}f:|s|  {}\mrightarrow{}  MonHom(g,h).
              (c.umap  h  f)  =  !v:|c.grp|  {}\mrightarrow{}  |h|
                                                (IsMonHom\{c.grp,h\}(v)  \mwedge{}  (\mforall{}j:|s|.  ((f  j)  =  (v  o  (c.inj  j)))))))


By

---

Latex:
(Auto  THEN  DVar  `c'  THEN  Unhide  THEN  Auto  THEN  Try  (BackThruSomeHyp))

---

Home Index