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

Metamath Proof Explorer

Theorem evls1varpwval

Proof