Metamath Proof Explorer


Theorem evls1varpw

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

Proof

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