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