Description: Univariate polynomial evaluation for subrings maps the exponentiation of a variable to the exponentiation of the evaluated variable. (Contributed by AV, 14-Sep-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | evls1varpw.q | |- Q = ( S evalSub1 R ) |
|
evls1varpw.u | |- U = ( S |`s R ) |
||
evls1varpw.w | |- W = ( Poly1 ` U ) |
||
evls1varpw.g | |- G = ( mulGrp ` W ) |
||
evls1varpw.x | |- X = ( var1 ` U ) |
||
evls1varpw.b | |- B = ( Base ` S ) |
||
evls1varpw.e | |- .^ = ( .g ` G ) |
||
evls1varpw.s | |- ( ph -> S e. CRing ) |
||
evls1varpw.r | |- ( ph -> R e. ( SubRing ` S ) ) |
||
evls1varpw.n | |- ( ph -> N e. NN0 ) |
||
Assertion | evls1varpw | |- ( ph -> ( Q ` ( N .^ X ) ) = ( N ( .g ` ( mulGrp ` ( S ^s B ) ) ) ( Q ` X ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | evls1varpw.q | |- Q = ( S evalSub1 R ) |
|
2 | evls1varpw.u | |- U = ( S |`s R ) |
|
3 | evls1varpw.w | |- W = ( Poly1 ` U ) |
|
4 | evls1varpw.g | |- G = ( mulGrp ` W ) |
|
5 | evls1varpw.x | |- X = ( var1 ` U ) |
|
6 | evls1varpw.b | |- B = ( Base ` S ) |
|
7 | evls1varpw.e | |- .^ = ( .g ` G ) |
|
8 | evls1varpw.s | |- ( ph -> S e. CRing ) |
|
9 | evls1varpw.r | |- ( ph -> R e. ( SubRing ` S ) ) |
|
10 | evls1varpw.n | |- ( ph -> N e. NN0 ) |
|
11 | eqid | |- ( Base ` W ) = ( Base ` W ) |
|
12 | 2 | subrgring | |- ( R e. ( SubRing ` S ) -> U e. Ring ) |
13 | 5 3 11 | vr1cl | |- ( U e. Ring -> X e. ( Base ` W ) ) |
14 | 9 12 13 | 3syl | |- ( ph -> X e. ( Base ` W ) ) |
15 | 1 2 3 4 6 11 7 8 9 10 14 | evls1pw | |- ( ph -> ( Q ` ( N .^ X ) ) = ( N ( .g ` ( mulGrp ` ( S ^s B ) ) ) ( Q ` X ) ) ) |