Description: Polynomial evaluation for subrings maps the exponentiation of a polynomial to the exponentiation of the evaluated polynomial. (Contributed by SN, 29-Feb-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | evlspw.q | |- Q = ( ( I evalSub S ) ` R ) |
|
evlspw.w | |- W = ( I mPoly U ) |
||
evlspw.g | |- G = ( mulGrp ` W ) |
||
evlspw.e | |- .^ = ( .g ` G ) |
||
evlspw.u | |- U = ( S |`s R ) |
||
evlspw.p | |- P = ( S ^s ( K ^m I ) ) |
||
evlspw.h | |- H = ( mulGrp ` P ) |
||
evlspw.k | |- K = ( Base ` S ) |
||
evlspw.b | |- B = ( Base ` W ) |
||
evlspw.i | |- ( ph -> I e. V ) |
||
evlspw.s | |- ( ph -> S e. CRing ) |
||
evlspw.r | |- ( ph -> R e. ( SubRing ` S ) ) |
||
evlspw.n | |- ( ph -> N e. NN0 ) |
||
evlspw.x | |- ( ph -> X e. B ) |
||
Assertion | evlspw | |- ( ph -> ( Q ` ( N .^ X ) ) = ( N ( .g ` H ) ( Q ` X ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | evlspw.q | |- Q = ( ( I evalSub S ) ` R ) |
|
2 | evlspw.w | |- W = ( I mPoly U ) |
|
3 | evlspw.g | |- G = ( mulGrp ` W ) |
|
4 | evlspw.e | |- .^ = ( .g ` G ) |
|
5 | evlspw.u | |- U = ( S |`s R ) |
|
6 | evlspw.p | |- P = ( S ^s ( K ^m I ) ) |
|
7 | evlspw.h | |- H = ( mulGrp ` P ) |
|
8 | evlspw.k | |- K = ( Base ` S ) |
|
9 | evlspw.b | |- B = ( Base ` W ) |
|
10 | evlspw.i | |- ( ph -> I e. V ) |
|
11 | evlspw.s | |- ( ph -> S e. CRing ) |
|
12 | evlspw.r | |- ( ph -> R e. ( SubRing ` S ) ) |
|
13 | evlspw.n | |- ( ph -> N e. NN0 ) |
|
14 | evlspw.x | |- ( ph -> X e. B ) |
|
15 | 1 2 5 6 8 | evlsrhm | |- ( ( I e. V /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> Q e. ( W RingHom P ) ) |
16 | 10 11 12 15 | syl3anc | |- ( ph -> Q e. ( W RingHom P ) ) |
17 | 3 7 | rhmmhm | |- ( Q e. ( W RingHom P ) -> Q e. ( G MndHom H ) ) |
18 | 16 17 | syl | |- ( ph -> Q e. ( G MndHom H ) ) |
19 | 3 9 | mgpbas | |- B = ( Base ` G ) |
20 | eqid | |- ( .g ` H ) = ( .g ` H ) |
|
21 | 19 4 20 | mhmmulg | |- ( ( Q e. ( G MndHom H ) /\ N e. NN0 /\ X e. B ) -> ( Q ` ( N .^ X ) ) = ( N ( .g ` H ) ( Q ` X ) ) ) |
22 | 18 13 14 21 | syl3anc | |- ( ph -> ( Q ` ( N .^ X ) ) = ( N ( .g ` H ) ( Q ` X ) ) ) |