Description: The value of the algebra scalar lifting function for (univariate) polynomials applied to a scalar results in a constant polynomial. (Contributed by AV, 27-Nov-2019)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | ply1scl.p | |- P = ( Poly1 ` R ) |
|
| ply1scl.a | |- A = ( algSc ` P ) |
||
| coe1scl.k | |- K = ( Base ` R ) |
||
| ply1sclf.b | |- B = ( Base ` P ) |
||
| Assertion | ply1sclcl | |- ( ( R e. Ring /\ S e. K ) -> ( A ` S ) e. B ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ply1scl.p | |- P = ( Poly1 ` R ) |
|
| 2 | ply1scl.a | |- A = ( algSc ` P ) |
|
| 3 | coe1scl.k | |- K = ( Base ` R ) |
|
| 4 | ply1sclf.b | |- B = ( Base ` P ) |
|
| 5 | 1 2 3 4 | ply1sclf | |- ( R e. Ring -> A : K --> B ) |
| 6 | 5 | ffvelcdmda | |- ( ( R e. Ring /\ S e. K ) -> ( A ` S ) e. B ) |