Theorem evl1varpwval

Description: Value of a univariate polynomial evaluation mapping the exponentiation of a variable to the exponentiation of the evaluated variable. (Contributed by AV, 14-Sep-2019)

	Ref	Expression
Hypotheses	evl1varpw.q	|- Q = ( eval1 ` R )
	evl1varpw.w	|- W = ( Poly1 ` R )
	evl1varpw.g	|- G = ( mulGrp ` W )
	evl1varpw.x	|- X = ( var1 ` R )
	evl1varpw.b	|- B = ( Base ` R )
	evl1varpw.e	|- .^ = ( .g ` G )
	evl1varpw.r	|- ( ph -> R e. CRing )
	evl1varpw.n	|- ( ph -> N e. NN0 )
	evl1varpwval.c	|- ( ph -> C e. B )
	evl1varpwval.h	|- H = ( mulGrp ` R )
	evl1varpwval.e	|- E = ( .g ` H )
Assertion	evl1varpwval	|- ( ph -> ( ( Q ` ( N .^ X ) ) ` C ) = ( N E C ) )

Proof

Step	Hyp	Ref	Expression
1		evl1varpw.q	|- Q = ( eval1 ` R )
2		evl1varpw.w	|- W = ( Poly1 ` R )
3		evl1varpw.g	|- G = ( mulGrp ` W )
4		evl1varpw.x	|- X = ( var1 ` R )
5		evl1varpw.b	|- B = ( Base ` R )
6		evl1varpw.e	|- .^ = ( .g ` G )
7		evl1varpw.r	|- ( ph -> R e. CRing )
8		evl1varpw.n	|- ( ph -> N e. NN0 )
9		evl1varpwval.c	|- ( ph -> C e. B )
10		evl1varpwval.h	|- H = ( mulGrp ` R )
11		evl1varpwval.e	|- E = ( .g ` H )
12		eqid	|- ( Base ` W ) = ( Base ` W )
13	1 4 5 2 12 7 9	evl1vard	|- ( ph -> ( X e. ( Base ` W ) /\ ( ( Q ` X ) ` C ) = C ) )
14	3	fveq2i	|- ( .g ` G ) = ( .g ` ( mulGrp ` W ) )
15	6 14	eqtri	|- .^ = ( .g ` ( mulGrp ` W ) )
16	10	fveq2i	|- ( .g ` H ) = ( .g ` ( mulGrp ` R ) )
17	11 16	eqtri	|- E = ( .g ` ( mulGrp ` R ) )
18	1 2 5 12 7 9 13 15 17 8	evl1expd	|- ( ph -> ( ( N .^ X ) e. ( Base ` W ) /\ ( ( Q ` ( N .^ X ) ) ` C ) = ( N E C ) ) )
19	18	simprd	|- ( ph -> ( ( Q ` ( N .^ X ) ) ` C ) = ( N E C ) )