Metamath Proof Explorer


Theorem evls1pw

Description: Univariate 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 evls1pw.q
|- Q = ( S evalSub1 R )
evls1pw.u
|- U = ( S |`s R )
evls1pw.w
|- W = ( Poly1 ` U )
evls1pw.g
|- G = ( mulGrp ` W )
evls1pw.k
|- K = ( Base ` S )
evls1pw.b
|- B = ( Base ` W )
evls1pw.e
|- .^ = ( .g ` G )
evls1pw.s
|- ( ph -> S e. CRing )
evls1pw.r
|- ( ph -> R e. ( SubRing ` S ) )
evls1pw.n
|- ( ph -> N e. NN0 )
evls1pw.x
|- ( ph -> X e. B )
Assertion evls1pw
|- ( ph -> ( Q ` ( N .^ X ) ) = ( N ( .g ` ( mulGrp ` ( S ^s K ) ) ) ( Q ` X ) ) )

Proof

Step Hyp Ref Expression
1 evls1pw.q
 |-  Q = ( S evalSub1 R )
2 evls1pw.u
 |-  U = ( S |`s R )
3 evls1pw.w
 |-  W = ( Poly1 ` U )
4 evls1pw.g
 |-  G = ( mulGrp ` W )
5 evls1pw.k
 |-  K = ( Base ` S )
6 evls1pw.b
 |-  B = ( Base ` W )
7 evls1pw.e
 |-  .^ = ( .g ` G )
8 evls1pw.s
 |-  ( ph -> S e. CRing )
9 evls1pw.r
 |-  ( ph -> R e. ( SubRing ` S ) )
10 evls1pw.n
 |-  ( ph -> N e. NN0 )
11 evls1pw.x
 |-  ( ph -> X e. B )
12 eqid
 |-  ( S ^s K ) = ( S ^s K )
13 1 5 12 2 3 evls1rhm
 |-  ( ( S e. CRing /\ R e. ( SubRing ` S ) ) -> Q e. ( W RingHom ( S ^s K ) ) )
14 8 9 13 syl2anc
 |-  ( ph -> Q e. ( W RingHom ( S ^s K ) ) )
15 eqid
 |-  ( mulGrp ` ( S ^s K ) ) = ( mulGrp ` ( S ^s K ) )
16 4 15 rhmmhm
 |-  ( Q e. ( W RingHom ( S ^s K ) ) -> Q e. ( G MndHom ( mulGrp ` ( S ^s K ) ) ) )
17 14 16 syl
 |-  ( ph -> Q e. ( G MndHom ( mulGrp ` ( S ^s K ) ) ) )
18 4 6 mgpbas
 |-  B = ( Base ` G )
19 eqid
 |-  ( .g ` ( mulGrp ` ( S ^s K ) ) ) = ( .g ` ( mulGrp ` ( S ^s K ) ) )
20 18 7 19 mhmmulg
 |-  ( ( Q e. ( G MndHom ( mulGrp ` ( S ^s K ) ) ) /\ N e. NN0 /\ X e. B ) -> ( Q ` ( N .^ X ) ) = ( N ( .g ` ( mulGrp ` ( S ^s K ) ) ) ( Q ` X ) ) )
21 17 10 11 20 syl3anc
 |-  ( ph -> ( Q ` ( N .^ X ) ) = ( N ( .g ` ( mulGrp ` ( S ^s K ) ) ) ( Q ` X ) ) )