Theorem evl1varpw

Description: Univariate polynomial evaluation maps the exponentiation of a variable to the exponentiation of the evaluated variable. Remark: in contrast to evl1gsumadd , the proof is shorter using evls1varpw instead of proving it directly. (Contributed by AV, 15-Sep-2019)

	Ref	Expression
Hypotheses	evl1varpw.q	⊢ 𝑄 = ( eval1 ‘ 𝑅 )
	evl1varpw.w	⊢ 𝑊 = ( Poly1 ‘ 𝑅 )
	evl1varpw.g	⊢ 𝐺 = ( mulGrp ‘ 𝑊 )
	evl1varpw.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	evl1varpw.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	evl1varpw.e	⊢ ↑ = ( .g ‘ 𝐺 )
	evl1varpw.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	evl1varpw.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion	evl1varpw	⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝑁 ↑ 𝑋 ) ) = ( 𝑁 ( .g ‘ ( mulGrp ‘ ( 𝑅 ↑s 𝐵 ) ) ) ( 𝑄 ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		evl1varpw.q	⊢ 𝑄 = ( eval1 ‘ 𝑅 )
2		evl1varpw.w	⊢ 𝑊 = ( Poly1 ‘ 𝑅 )
3		evl1varpw.g	⊢ 𝐺 = ( mulGrp ‘ 𝑊 )
4		evl1varpw.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
5		evl1varpw.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
6		evl1varpw.e	⊢ ↑ = ( .g ‘ 𝐺 )
7		evl1varpw.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
8		evl1varpw.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
9	1 5	evl1fval1	⊢ 𝑄 = ( 𝑅 evalSub1 𝐵 )
10	9	a1i	⊢ ( 𝜑 → 𝑄 = ( 𝑅 evalSub1 𝐵 ) )
11	2	fveq2i	⊢ ( mulGrp ‘ 𝑊 ) = ( mulGrp ‘ ( Poly1 ‘ 𝑅 ) )
12	3 11	eqtri	⊢ 𝐺 = ( mulGrp ‘ ( Poly1 ‘ 𝑅 ) )
13	12	fveq2i	⊢ ( .g ‘ 𝐺 ) = ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝑅 ) ) )
14	6 13	eqtri	⊢ ↑ = ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝑅 ) ) )
15	5	ressid	⊢ ( 𝑅 ∈ CRing → ( 𝑅 ↾s 𝐵 ) = 𝑅 )
16	7 15	syl	⊢ ( 𝜑 → ( 𝑅 ↾s 𝐵 ) = 𝑅 )
17	16	eqcomd	⊢ ( 𝜑 → 𝑅 = ( 𝑅 ↾s 𝐵 ) )
18	17	fveq2d	⊢ ( 𝜑 → ( Poly1 ‘ 𝑅 ) = ( Poly1 ‘ ( 𝑅 ↾s 𝐵 ) ) )
19	18	fveq2d	⊢ ( 𝜑 → ( mulGrp ‘ ( Poly1 ‘ 𝑅 ) ) = ( mulGrp ‘ ( Poly1 ‘ ( 𝑅 ↾s 𝐵 ) ) ) )
20	19	fveq2d	⊢ ( 𝜑 → ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝑅 ) ) ) = ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( 𝑅 ↾s 𝐵 ) ) ) ) )
21	14 20	eqtrid	⊢ ( 𝜑 → ↑ = ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( 𝑅 ↾s 𝐵 ) ) ) ) )
22		eqidd	⊢ ( 𝜑 → 𝑁 = 𝑁 )
23	17	fveq2d	⊢ ( 𝜑 → ( var1 ‘ 𝑅 ) = ( var1 ‘ ( 𝑅 ↾s 𝐵 ) ) )
24	4 23	eqtrid	⊢ ( 𝜑 → 𝑋 = ( var1 ‘ ( 𝑅 ↾s 𝐵 ) ) )
25	21 22 24	oveq123d	⊢ ( 𝜑 → ( 𝑁 ↑ 𝑋 ) = ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( 𝑅 ↾s 𝐵 ) ) ) ) ( var1 ‘ ( 𝑅 ↾s 𝐵 ) ) ) )
26	10 25	fveq12d	⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝑁 ↑ 𝑋 ) ) = ( ( 𝑅 evalSub1 𝐵 ) ‘ ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( 𝑅 ↾s 𝐵 ) ) ) ) ( var1 ‘ ( 𝑅 ↾s 𝐵 ) ) ) ) )
27		eqid	⊢ ( 𝑅 evalSub1 𝐵 ) = ( 𝑅 evalSub1 𝐵 )
28		eqid	⊢ ( 𝑅 ↾s 𝐵 ) = ( 𝑅 ↾s 𝐵 )
29		eqid	⊢ ( Poly1 ‘ ( 𝑅 ↾s 𝐵 ) ) = ( Poly1 ‘ ( 𝑅 ↾s 𝐵 ) )
30		eqid	⊢ ( mulGrp ‘ ( Poly1 ‘ ( 𝑅 ↾s 𝐵 ) ) ) = ( mulGrp ‘ ( Poly1 ‘ ( 𝑅 ↾s 𝐵 ) ) )
31		eqid	⊢ ( var1 ‘ ( 𝑅 ↾s 𝐵 ) ) = ( var1 ‘ ( 𝑅 ↾s 𝐵 ) )
32		eqid	⊢ ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( 𝑅 ↾s 𝐵 ) ) ) ) = ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( 𝑅 ↾s 𝐵 ) ) ) )
33		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
34	5	subrgid	⊢ ( 𝑅 ∈ Ring → 𝐵 ∈ ( SubRing ‘ 𝑅 ) )
35	7 33 34	3syl	⊢ ( 𝜑 → 𝐵 ∈ ( SubRing ‘ 𝑅 ) )
36	27 28 29 30 31 5 32 7 35 8	evls1varpw	⊢ ( 𝜑 → ( ( 𝑅 evalSub1 𝐵 ) ‘ ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( 𝑅 ↾s 𝐵 ) ) ) ) ( var1 ‘ ( 𝑅 ↾s 𝐵 ) ) ) ) = ( 𝑁 ( .g ‘ ( mulGrp ‘ ( 𝑅 ↑s 𝐵 ) ) ) ( ( 𝑅 evalSub1 𝐵 ) ‘ ( var1 ‘ ( 𝑅 ↾s 𝐵 ) ) ) ) )
37	9	eqcomi	⊢ ( 𝑅 evalSub1 𝐵 ) = 𝑄
38	37	a1i	⊢ ( 𝜑 → ( 𝑅 evalSub1 𝐵 ) = 𝑄 )
39	24	eqcomd	⊢ ( 𝜑 → ( var1 ‘ ( 𝑅 ↾s 𝐵 ) ) = 𝑋 )
40	38 39	fveq12d	⊢ ( 𝜑 → ( ( 𝑅 evalSub1 𝐵 ) ‘ ( var1 ‘ ( 𝑅 ↾s 𝐵 ) ) ) = ( 𝑄 ‘ 𝑋 ) )
41	40	oveq2d	⊢ ( 𝜑 → ( 𝑁 ( .g ‘ ( mulGrp ‘ ( 𝑅 ↑s 𝐵 ) ) ) ( ( 𝑅 evalSub1 𝐵 ) ‘ ( var1 ‘ ( 𝑅 ↾s 𝐵 ) ) ) ) = ( 𝑁 ( .g ‘ ( mulGrp ‘ ( 𝑅 ↑s 𝐵 ) ) ) ( 𝑄 ‘ 𝑋 ) ) )
42	26 36 41	3eqtrd	⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝑁 ↑ 𝑋 ) ) = ( 𝑁 ( .g ‘ ( mulGrp ‘ ( 𝑅 ↑s 𝐵 ) ) ) ( 𝑄 ‘ 𝑋 ) ) )