---

Step * of Lemma fma_from_gcp_wf

∀g:GrpSig. ∀r:RngSig. ∀c:gcopower_sig{i:l}(g↓set;r↓+gp). ∀a:algebra{i:l}(r).
  (((a↓grp) = c.grp ∈ GrpSig) ⇒ (fma_from_gcp(g;r;c;a) ∈ fma_sig{i:l}(g;r)))
BY
{ ((Unfolds ``fma_sig fma_from_gcp`` 0 
THENM RepD 
THENM MemCD THENML [Id;MemCD]) THENA Auto) }

1
.....subterm..... T:t
1:n
1. g : GrpSig@i'
2. r : RngSig@i'
3. c : gcopower_sig{i:l}(g↓set;r↓+gp)@i'
4. a : algebra{i:l}(r)@i'
5. (a↓grp) = c.grp ∈ GrpSig@i'
⊢ a ∈ algebra_sig{i:l}(|r|)

2
.....subterm..... T:t
1:n
1. g : GrpSig@i'
2. r : RngSig@i'
3. c : gcopower_sig{i:l}(g↓set;r↓+gp)@i'
4. a : algebra{i:l}(r)@i'
5. (a↓grp) = c.grp ∈ GrpSig@i'
⊢ λp:|g|. c.inj p 1 ∈ |g| ⟶ a.car

3
.....subterm..... T:t
2:n
1. g : GrpSig@i'
2. r : RngSig@i'
3. c : gcopower_sig{i:l}(g↓set;r↓+gp)@i'
4. a : algebra{i:l}(r)@i'
5. (a↓grp) = c.grp ∈ GrpSig@i'
⊢ λa.(λh:|g| ⟶ a.car. c.umap (a↓grp) (λp:|g|. λv:|r|. a.act v (h p))) ∈ N:algebra{i:l}(r)
  ⟶ (|g| ⟶ N.car)
  ⟶ a.car
  ⟶ N.car

---

Latex:

---

Latex:
\mforall{}g:GrpSig.  \mforall{}r:RngSig.  \mforall{}c:gcopower\_sig\{i:l\}(g\mdownarrow{}set;r\mdownarrow{}+gp).  \mforall{}a:algebra\{i:l\}(r).
    (((a\mdownarrow{}grp)  =  c.grp)  {}\mRightarrow{}  (fma\_from\_gcp(g;r;c;a)  \mmember{}  fma\_sig\{i:l\}(g;r)))


By

---

Latex:
((Unfolds  ``fma\_sig  fma\_from\_gcp``  0 
THENM  RepD 
THENM  MemCD  THENML  [Id;MemCD])  THENA  Auto)

---

Home Index