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