Step
*
2
1
1
of Lemma
fma_from_gcp_wf
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'
6. p : |g|@i
⊢ c.inj p 1 ∈ |c.grp|
BY
{ Auto }
Latex:
Latex:
1. g : GrpSig@i'
2. r : RngSig@i'
3. c : gcopower\_sig\{i:l\}(g\mdownarrow{}set;r\mdownarrow{}+gp)@i'
4. a : algebra\{i:l\}(r)@i'
5. (a\mdownarrow{}grp) = c.grp@i'
6. p : |g|@i
\mvdash{} c.inj p 1 \mmember{} |c.grp|
By
Latex:
Auto
Home
Index