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