| Step |
Hyp |
Ref |
Expression |
| 1 |
|
selvcllem4.p |
|- P = ( I mPoly R ) |
| 2 |
|
selvcllem4.b |
|- B = ( Base ` P ) |
| 3 |
|
selvcllem4.u |
|- U = ( ( I \ J ) mPoly R ) |
| 4 |
|
selvcllem4.t |
|- T = ( J mPoly U ) |
| 5 |
|
selvcllem4.c |
|- C = ( algSc ` T ) |
| 6 |
|
selvcllem4.d |
|- D = ( C o. ( algSc ` U ) ) |
| 7 |
|
selvcllem4.s |
|- S = ( T |`s ran D ) |
| 8 |
|
selvcllem4.w |
|- W = ( I mPoly S ) |
| 9 |
|
selvcllem4.x |
|- X = ( Base ` W ) |
| 10 |
|
selvcllem4.r |
|- ( ph -> R e. CRing ) |
| 11 |
|
selvcllem4.j |
|- ( ph -> J C_ I ) |
| 12 |
|
selvcllem4.f |
|- ( ph -> F e. B ) |
| 13 |
1 2
|
mplrcl |
|- ( F e. B -> I e. _V ) |
| 14 |
12 13
|
syl |
|- ( ph -> I e. _V ) |
| 15 |
14
|
difexd |
|- ( ph -> ( I \ J ) e. _V ) |
| 16 |
14 11
|
ssexd |
|- ( ph -> J e. _V ) |
| 17 |
3 4 5 6 15 16 10
|
selvcllem2 |
|- ( ph -> D e. ( R RingHom T ) ) |
| 18 |
3 4 5 6 15 16 10
|
selvcllem3 |
|- ( ph -> ran D e. ( SubRing ` T ) ) |
| 19 |
|
ssidd |
|- ( ph -> ran D C_ ran D ) |
| 20 |
7
|
resrhm2b |
|- ( ( ran D e. ( SubRing ` T ) /\ ran D C_ ran D ) -> ( D e. ( R RingHom T ) <-> D e. ( R RingHom S ) ) ) |
| 21 |
18 19 20
|
syl2anc |
|- ( ph -> ( D e. ( R RingHom T ) <-> D e. ( R RingHom S ) ) ) |
| 22 |
17 21
|
mpbid |
|- ( ph -> D e. ( R RingHom S ) ) |
| 23 |
|
rhmghm |
|- ( D e. ( R RingHom S ) -> D e. ( R GrpHom S ) ) |
| 24 |
|
ghmmhm |
|- ( D e. ( R GrpHom S ) -> D e. ( R MndHom S ) ) |
| 25 |
22 23 24
|
3syl |
|- ( ph -> D e. ( R MndHom S ) ) |
| 26 |
1 8 2 9 25 12
|
mhmcompl |
|- ( ph -> ( D o. F ) e. X ) |