Description: The scalar injection function in a subring algebra is the same up to a restriction to the subring. (Contributed by Mario Carneiro, 4-Jul-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | subrg1ascl.p | |- P = ( Poly1 ` R ) |
|
| subrg1ascl.a | |- A = ( algSc ` P ) |
||
| subrg1ascl.h | |- H = ( R |`s T ) |
||
| subrg1ascl.u | |- U = ( Poly1 ` H ) |
||
| subrg1ascl.r | |- ( ph -> T e. ( SubRing ` R ) ) |
||
| subrg1ascl.c | |- C = ( algSc ` U ) |
||
| Assertion | subrg1ascl | |- ( ph -> C = ( A |` T ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | subrg1ascl.p | |- P = ( Poly1 ` R ) |
|
| 2 | subrg1ascl.a | |- A = ( algSc ` P ) |
|
| 3 | subrg1ascl.h | |- H = ( R |`s T ) |
|
| 4 | subrg1ascl.u | |- U = ( Poly1 ` H ) |
|
| 5 | subrg1ascl.r | |- ( ph -> T e. ( SubRing ` R ) ) |
|
| 6 | subrg1ascl.c | |- C = ( algSc ` U ) |
|
| 7 | eqid | |- ( 1o mPoly R ) = ( 1o mPoly R ) |
|
| 8 | 1 2 | ply1ascl | |- A = ( algSc ` ( 1o mPoly R ) ) |
| 9 | eqid | |- ( 1o mPoly H ) = ( 1o mPoly H ) |
|
| 10 | 1on | |- 1o e. On |
|
| 11 | 10 | a1i | |- ( ph -> 1o e. On ) |
| 12 | 4 6 | ply1ascl | |- C = ( algSc ` ( 1o mPoly H ) ) |
| 13 | 7 8 3 9 11 5 12 | subrgascl | |- ( ph -> C = ( A |` T ) ) |