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 ⊢ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) = ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) )
15 1 2 3 14 4 evlsrhm ⊢ ( ( 𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑄 ∈ ( 𝑃 RingHom ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
16 6 7 8 15 syl3anc ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 RingHom ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
17 rhmrcl1 ⊢ ( 𝑄 ∈ ( 𝑃 RingHom ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) → 𝑃 ∈ Ring )
18 eqid ⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
19 18 ringmgp ⊢ ( 𝑃 ∈ Ring → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
20 16 17 19 3syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
21 10 simpld ⊢ ( 𝜑 → 𝑀 ∈ 𝐵 )
22 18 5 mgpbas ⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑃 ) )
23 22 11 mulgnn0cl ⊢ ( ( ( mulGrp ‘ 𝑃 ) ∈ Mnd ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ 𝐵 ) → ( 𝑁 ∙ 𝑀 ) ∈ 𝐵 )
24 20 13 21 23 syl3anc ⊢ ( 𝜑 → ( 𝑁 ∙ 𝑀 ) ∈ 𝐵 )
25 eqid ⊢ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) = ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) )
26 1 2 18 11 3 14 25 4 5 6 7 8 13 21 evlspw ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝑁 ∙ 𝑀 ) ) = ( 𝑁 ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑄 ‘ 𝑀 ) ) )
27 26 fveq1d ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝑁 ∙ 𝑀 ) ) ‘ 𝐴 ) = ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑄 ‘ 𝑀 ) ) ‘ 𝐴 ) )
28 eqid ⊢ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) = ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) )
29 eqid ⊢ ( mulGrp ‘ 𝑆 ) = ( mulGrp ‘ 𝑆 )
30 eqid ⊢ ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) = ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
31 7 crngringd ⊢ ( 𝜑 → 𝑆 ∈ Ring )
32 ovexd ⊢ ( 𝜑 → ( 𝐾 ↑m 𝐼 ) ∈ V )
33 5 28 rhmf ⊢ ( 𝑄 ∈ ( 𝑃 RingHom ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) → 𝑄 : 𝐵 ⟶ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
34 16 33 syl ⊢ ( 𝜑 → 𝑄 : 𝐵 ⟶ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
35 34 21 ffvelrnd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) ∈ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
36 14 28 25 29 30 12 31 32 13 35 9 pwsexpg ⊢ ( 𝜑 → ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ) ( 𝑄 ‘ 𝑀 ) ) ‘ 𝐴 ) = ( 𝑁 ↑ ( ( 𝑄 ‘ 𝑀 ) ‘ 𝐴 ) ) )
37 10 simprd ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝑀 ) ‘ 𝐴 ) = 𝑉 )
38 37 oveq2d ⊢ ( 𝜑 → ( 𝑁 ↑ ( ( 𝑄 ‘ 𝑀 ) ‘ 𝐴 ) ) = ( 𝑁 ↑ 𝑉 ) )
39 27 36 38 3eqtrd ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝑁 ∙ 𝑀 ) ) ‘ 𝐴 ) = ( 𝑁 ↑ 𝑉 ) )
40 24 39 jca ⊢ ( 𝜑 → ( ( 𝑁 ∙ 𝑀 ) ∈ 𝐵 ∧ ( ( 𝑄 ‘ ( 𝑁 ∙ 𝑀 ) ) ‘ 𝐴 ) = ( 𝑁 ↑ 𝑉 ) ) )