Metamath Proof Explorer

Theorem 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 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
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 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
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 ⊢ ( 𝜑 → ( ( 𝑁 ∙ 𝑀 ) ∈ 𝐵 ∧ ( ( 𝑄 ‘ ( 𝑁 ∙ 𝑀 ) ) ‘ 𝐴 ) = ( 𝑁 ↑ 𝑉 ) ) )