---

Step * 2 1 of Lemma fma_from_gcp_wf

.....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'
6. p : |g|@i
⊢ c.inj p 1 ∈ a.car
BY
{ RWH grp_of_moduleC 0 
THENM ((RWTH (HypC 5) 0) THENA Auto) }

1
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|

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
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{}  a.car


By

---

Latex:
RWH  grp\_of\_moduleC  0 
THENM  ((RWTH  (HypC  5)  0)  THENA  Auto)

---

Home Index