Metamath Proof Explorer


Theorem evlspw

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 ) ) )

Proof

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 ) ) )