Theorem evls1varpwval

Description: Univariate polynomial evaluation for subrings maps the exponentiation of a variable to the exponentiation of the evaluated variable. See evl1varpwval . (Contributed by Thierry Arnoux, 24-Jan-2025)

	Ref	Expression
Hypotheses	evls1varpwval.q	|- Q = ( S evalSub1 R )
	evls1varpwval.u	|- U = ( S |`s R )
	evls1varpwval.w	|- W = ( Poly1 ` U )
	evls1varpwval.x	|- X = ( var1 ` U )
	evls1varpwval.b	|- B = ( Base ` S )
	evls1varpwval.e	|- ./\ = ( .g ` ( mulGrp ` W ) )
	evls1varpwval.f	|- .^ = ( .g ` ( mulGrp ` S ) )
	evls1varpwval.s	|- ( ph -> S e. CRing )
	evls1varpwval.r	|- ( ph -> R e. ( SubRing ` S ) )
	evls1varpwval.n	|- ( ph -> N e. NN0 )
	evls1varpwval.c	|- ( ph -> C e. B )
Assertion	evls1varpwval	|- ( ph -> ( ( Q ` ( N ./\ X ) ) ` C ) = ( N .^ C ) )

Proof

Step	Hyp	Ref	Expression
1		evls1varpwval.q	|- Q = ( S evalSub1 R )
2		evls1varpwval.u	|- U = ( S |`s R )
3		evls1varpwval.w	|- W = ( Poly1 ` U )
4		evls1varpwval.x	|- X = ( var1 ` U )
5		evls1varpwval.b	|- B = ( Base ` S )
6		evls1varpwval.e	|- ./\ = ( .g ` ( mulGrp ` W ) )
7		evls1varpwval.f	|- .^ = ( .g ` ( mulGrp ` S ) )
8		evls1varpwval.s	|- ( ph -> S e. CRing )
9		evls1varpwval.r	|- ( ph -> R e. ( SubRing ` S ) )
10		evls1varpwval.n	|- ( ph -> N e. NN0 )
11		evls1varpwval.c	|- ( ph -> C e. B )
12		eqid	|- ( Base ` W ) = ( Base ` W )
13	2	subrgring	|- ( R e. ( SubRing ` S ) -> U e. Ring )
14	4 3 12	vr1cl	|- ( U e. Ring -> X e. ( Base ` W ) )
15	9 13 14	3syl	|- ( ph -> X e. ( Base ` W ) )
16	1 5 3 2 12 8 9 6 7 10 15 11	evls1expd	|- ( ph -> ( ( Q ` ( N ./\ X ) ) ` C ) = ( N .^ ( ( Q ` X ) ` C ) ) )
17	1 4 2 5 8 9	evls1var	|- ( ph -> ( Q ` X ) = ( _I |` B ) )
18	17	fveq1d	|- ( ph -> ( ( Q ` X ) ` C ) = ( ( _I |` B ) ` C ) )
19		fvresi	|- ( C e. B -> ( ( _I |` B ) ` C ) = C )
20	11 19	syl	|- ( ph -> ( ( _I |` B ) ` C ) = C )
21	18 20	eqtrd	|- ( ph -> ( ( Q ` X ) ` C ) = C )
22	21	oveq2d	|- ( ph -> ( N .^ ( ( Q ` X ) ` C ) ) = ( N .^ C ) )
23	16 22	eqtrd	|- ( ph -> ( ( Q ` ( N ./\ X ) ) ` C ) = ( N .^ C ) )