| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ressply.1 |
|- S = ( Poly1 ` R ) |
| 2 |
|
ressply.2 |
|- H = ( R |`s T ) |
| 3 |
|
ressply.3 |
|- U = ( Poly1 ` H ) |
| 4 |
|
ressply.4 |
|- B = ( Base ` U ) |
| 5 |
|
ressply.5 |
|- ( ph -> T e. ( SubRing ` R ) ) |
| 6 |
|
ressply10g.6 |
|- Z = ( 0g ` S ) |
| 7 |
|
eqid |
|- ( algSc ` S ) = ( algSc ` S ) |
| 8 |
|
eqid |
|- ( algSc ` U ) = ( algSc ` U ) |
| 9 |
1 7 2 3 5 8
|
subrg1ascl |
|- ( ph -> ( algSc ` U ) = ( ( algSc ` S ) |` T ) ) |
| 10 |
9
|
fveq1d |
|- ( ph -> ( ( algSc ` U ) ` ( 0g ` H ) ) = ( ( ( algSc ` S ) |` T ) ` ( 0g ` H ) ) ) |
| 11 |
|
eqid |
|- ( 0g ` H ) = ( 0g ` H ) |
| 12 |
|
eqid |
|- ( 0g ` U ) = ( 0g ` U ) |
| 13 |
2
|
subrgring |
|- ( T e. ( SubRing ` R ) -> H e. Ring ) |
| 14 |
5 13
|
syl |
|- ( ph -> H e. Ring ) |
| 15 |
3 8 11 12 14
|
ply1ascl0 |
|- ( ph -> ( ( algSc ` U ) ` ( 0g ` H ) ) = ( 0g ` U ) ) |
| 16 |
|
eqid |
|- ( 0g ` R ) = ( 0g ` R ) |
| 17 |
2 16
|
subrg0 |
|- ( T e. ( SubRing ` R ) -> ( 0g ` R ) = ( 0g ` H ) ) |
| 18 |
5 17
|
syl |
|- ( ph -> ( 0g ` R ) = ( 0g ` H ) ) |
| 19 |
|
subrgsubg |
|- ( T e. ( SubRing ` R ) -> T e. ( SubGrp ` R ) ) |
| 20 |
16
|
subg0cl |
|- ( T e. ( SubGrp ` R ) -> ( 0g ` R ) e. T ) |
| 21 |
5 19 20
|
3syl |
|- ( ph -> ( 0g ` R ) e. T ) |
| 22 |
18 21
|
eqeltrrd |
|- ( ph -> ( 0g ` H ) e. T ) |
| 23 |
22
|
fvresd |
|- ( ph -> ( ( ( algSc ` S ) |` T ) ` ( 0g ` H ) ) = ( ( algSc ` S ) ` ( 0g ` H ) ) ) |
| 24 |
10 15 23
|
3eqtr3d |
|- ( ph -> ( 0g ` U ) = ( ( algSc ` S ) ` ( 0g ` H ) ) ) |
| 25 |
18
|
fveq2d |
|- ( ph -> ( ( algSc ` S ) ` ( 0g ` R ) ) = ( ( algSc ` S ) ` ( 0g ` H ) ) ) |
| 26 |
|
subrgrcl |
|- ( T e. ( SubRing ` R ) -> R e. Ring ) |
| 27 |
5 26
|
syl |
|- ( ph -> R e. Ring ) |
| 28 |
1 7 16 6 27
|
ply1ascl0 |
|- ( ph -> ( ( algSc ` S ) ` ( 0g ` R ) ) = Z ) |
| 29 |
24 25 28
|
3eqtr2rd |
|- ( ph -> Z = ( 0g ` U ) ) |