evlsexpval

Description: Polynomial evaluation builder for exponentiation. (Contributed by SN, 27-Jul-2024)

	Ref	Expression
Hypotheses	evlsaddval.q	⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
	evlsaddval.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑈 )
	evlsaddval.u	⊢ 𝑈 = ( 𝑆 ↾_s 𝑅 )
	evlsaddval.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
	evlsaddval.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	evlsaddval.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑍 )
	evlsaddval.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
	evlsaddval.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
	evlsaddval.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐾 ↑_m 𝐼 ) )
	evlsaddval.m	⊢ ( 𝜑 → ( 𝑀 ∈ 𝐵 ∧ ( ( 𝑄 ‘ 𝑀 ) ‘ 𝐴 ) = 𝑉 ) )
	evlsexpval.g	⊢ ∙ = ( ._g ‘ ( mulGrp ‘ 𝑃 ) )
	evlsexpval.f	⊢ ↑ = ( ._g ‘ ( mulGrp ‘ 𝑆 ) )
	evlsexpval.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ₀ )
Assertion	evlsexpval	⊢ ( 𝜑 → ( ( 𝑁 ∙ 𝑀 ) ∈ 𝐵 ∧ ( ( 𝑄 ‘ ( 𝑁 ∙ 𝑀 ) ) ‘ 𝐴 ) = ( 𝑁 ↑ 𝑉 ) ) )

Proof

Step	Hyp	Ref	Expression
1		evlsaddval.q	⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
2		evlsaddval.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑈 )
3		evlsaddval.u	⊢ 𝑈 = ( 𝑆 ↾_s 𝑅 )
4		evlsaddval.k	⊢ 𝐾 = ( Base ‘ 𝑆 )
5		evlsaddval.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
6		evlsaddval.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑍 )
7		evlsaddval.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
8		evlsaddval.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
9		evlsaddval.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐾 ↑_m 𝐼 ) )
10		evlsaddval.m	⊢ ( 𝜑 → ( 𝑀 ∈ 𝐵 ∧ ( ( 𝑄 ‘ 𝑀 ) ‘ 𝐴 ) = 𝑉 ) )
11		evlsexpval.g	⊢ ∙ = ( ._g ‘ ( mulGrp ‘ 𝑃 ) )
12		evlsexpval.f	⊢ ↑ = ( ._g ‘ ( mulGrp ‘ 𝑆 ) )
13		evlsexpval.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ₀ )
14		eqid	⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
15	14 5	mgpbas	⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑃 ) )
16		eqid	⊢ ( 𝑆 ↑_s ( 𝐾 ↑_m 𝐼 ) ) = ( 𝑆 ↑_s ( 𝐾 ↑_m 𝐼 ) )
17	1 2 3 16 4	evlsrhm	⊢ ( ( 𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑄 ∈ ( 𝑃 RingHom ( 𝑆 ↑_s ( 𝐾 ↑_m 𝐼 ) ) ) )
18	6 7 8 17	syl3anc	⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 RingHom ( 𝑆 ↑_s ( 𝐾 ↑_m 𝐼 ) ) ) )
19		rhmrcl1	⊢ ( 𝑄 ∈ ( 𝑃 RingHom ( 𝑆 ↑_s ( 𝐾 ↑_m 𝐼 ) ) ) → 𝑃 ∈ Ring )
20	14	ringmgp	⊢ ( 𝑃 ∈ Ring → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
21	18 19 20	3syl	⊢ ( 𝜑 → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
22	10	simpld	⊢ ( 𝜑 → 𝑀 ∈ 𝐵 )
23	15 11 21 13 22	mulgnn0cld	⊢ ( 𝜑 → ( 𝑁 ∙ 𝑀 ) ∈ 𝐵 )
24		eqid	⊢ ( mulGrp ‘ ( 𝑆 ↑_s ( 𝐾 ↑_m 𝐼 ) ) ) = ( mulGrp ‘ ( 𝑆 ↑_s ( 𝐾 ↑_m 𝐼 ) ) )
25	1 2 14 11 3 16 24 4 5 6 7 8 13 22	evlspw	⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝑁 ∙ 𝑀 ) ) = ( 𝑁 ( ._g ‘ ( mulGrp ‘ ( 𝑆 ↑_s ( 𝐾 ↑_m 𝐼 ) ) ) ) ( 𝑄 ‘ 𝑀 ) ) )
26	25	fveq1d	⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝑁 ∙ 𝑀 ) ) ‘ 𝐴 ) = ( ( 𝑁 ( ._g ‘ ( mulGrp ‘ ( 𝑆 ↑_s ( 𝐾 ↑_m 𝐼 ) ) ) ) ( 𝑄 ‘ 𝑀 ) ) ‘ 𝐴 ) )
27		eqid	⊢ ( Base ‘ ( 𝑆 ↑_s ( 𝐾 ↑_m 𝐼 ) ) ) = ( Base ‘ ( 𝑆 ↑_s ( 𝐾 ↑_m 𝐼 ) ) )
28		eqid	⊢ ( mulGrp ‘ 𝑆 ) = ( mulGrp ‘ 𝑆 )
29		eqid	⊢ ( ._g ‘ ( mulGrp ‘ ( 𝑆 ↑_s ( 𝐾 ↑_m 𝐼 ) ) ) ) = ( ._g ‘ ( mulGrp ‘ ( 𝑆 ↑_s ( 𝐾 ↑_m 𝐼 ) ) ) )
30	7	crngringd	⊢ ( 𝜑 → 𝑆 ∈ Ring )
31		ovexd	⊢ ( 𝜑 → ( 𝐾 ↑_m 𝐼 ) ∈ V )
32	5 27	rhmf	⊢ ( 𝑄 ∈ ( 𝑃 RingHom ( 𝑆 ↑_s ( 𝐾 ↑_m 𝐼 ) ) ) → 𝑄 : 𝐵 ⟶ ( Base ‘ ( 𝑆 ↑_s ( 𝐾 ↑_m 𝐼 ) ) ) )
33	18 32	syl	⊢ ( 𝜑 → 𝑄 : 𝐵 ⟶ ( Base ‘ ( 𝑆 ↑_s ( 𝐾 ↑_m 𝐼 ) ) ) )
34	33 22	ffvelcdmd	⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) ∈ ( Base ‘ ( 𝑆 ↑_s ( 𝐾 ↑_m 𝐼 ) ) ) )
35	16 27 24 28 29 12 30 31 13 34 9	pwsexpg	⊢ ( 𝜑 → ( ( 𝑁 ( ._g ‘ ( mulGrp ‘ ( 𝑆 ↑_s ( 𝐾 ↑_m 𝐼 ) ) ) ) ( 𝑄 ‘ 𝑀 ) ) ‘ 𝐴 ) = ( 𝑁 ↑ ( ( 𝑄 ‘ 𝑀 ) ‘ 𝐴 ) ) )
36	10	simprd	⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝑀 ) ‘ 𝐴 ) = 𝑉 )
37	36	oveq2d	⊢ ( 𝜑 → ( 𝑁 ↑ ( ( 𝑄 ‘ 𝑀 ) ‘ 𝐴 ) ) = ( 𝑁 ↑ 𝑉 ) )
38	26 35 37	3eqtrd	⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝑁 ∙ 𝑀 ) ) ‘ 𝐴 ) = ( 𝑁 ↑ 𝑉 ) )
39	23 38	jca	⊢ ( 𝜑 → ( ( 𝑁 ∙ 𝑀 ) ∈ 𝐵 ∧ ( ( 𝑄 ‘ ( 𝑁 ∙ 𝑀 ) ) ‘ 𝐴 ) = ( 𝑁 ↑ 𝑉 ) ) )

Metamath Proof Explorer

Theorem evlsexpval

Proof