Metamath Proof Explorer

Theorem evls1expd

Description: Univariate polynomial evaluation builder for an exponential. See also evl1expd . (Contributed by Thierry Arnoux, 24-Jan-2025)

Ref Expression
Hypotheses evls1expd.q ⊢ 𝑄 = ( 𝑆 evalSub1 𝑅 )
evls1expd.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
evls1expd.w ⊢ 𝑊 = ( Poly1 ‘ 𝑈 )
evls1expd.u ⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
evls1expd.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
evls1expd.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
evls1expd.r ⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
evls1expd.1 ⊢ ∧ = ( .g ‘ ( mulGrp ‘ 𝑊 ) )
evls1expd.2 ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑆 ) )
evls1expd.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
evls1expd.m ⊢ ( 𝜑 → 𝑀 ∈ 𝐵 )
evls1expd.c ⊢ ( 𝜑 → 𝐶 ∈ 𝐾 )
Assertion evls1expd ( 𝜑 → ( ( 𝑄 ‘ ( 𝑁 ∧ 𝑀 ) ) ‘ 𝐶 ) = ( 𝑁 ↑ ( ( 𝑄 ‘ 𝑀 ) ‘ 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 evls1expd.q ⊢ 𝑄 = ( 𝑆 evalSub1 𝑅 )
2 evls1expd.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
3 evls1expd.w ⊢ 𝑊 = ( Poly1 ‘ 𝑈 )
4 evls1expd.u ⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
5 evls1expd.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
6 evls1expd.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
7 evls1expd.r ⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
8 evls1expd.1 ⊢ ∧ = ( .g ‘ ( mulGrp ‘ 𝑊 ) )
9 evls1expd.2 ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑆 ) )
10 evls1expd.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
11 evls1expd.m ⊢ ( 𝜑 → 𝑀 ∈ 𝐵 )
12 evls1expd.c ⊢ ( 𝜑 → 𝐶 ∈ 𝐾 )
13 eqid ⊢ ( mulGrp ‘ 𝑊 ) = ( mulGrp ‘ 𝑊 )
14 1 4 3 13 2 5 8 6 7 10 11 evls1pw ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝑁 ∧ 𝑀 ) ) = ( 𝑁 ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s 𝐾 ) ) ) ( 𝑄 ‘ 𝑀 ) ) )
15 14 fveq1d ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝑁 ∧ 𝑀 ) ) ‘ 𝐶 ) = ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s 𝐾 ) ) ) ( 𝑄 ‘ 𝑀 ) ) ‘ 𝐶 ) )
16 eqid ⊢ ( 𝑆 ↑s 𝐾 ) = ( 𝑆 ↑s 𝐾 )
17 eqid ⊢ ( Base ‘ ( 𝑆 ↑s 𝐾 ) ) = ( Base ‘ ( 𝑆 ↑s 𝐾 ) )
18 eqid ⊢ ( mulGrp ‘ ( 𝑆 ↑s 𝐾 ) ) = ( mulGrp ‘ ( 𝑆 ↑s 𝐾 ) )
19 eqid ⊢ ( mulGrp ‘ 𝑆 ) = ( mulGrp ‘ 𝑆 )
20 eqid ⊢ ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s 𝐾 ) ) ) = ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s 𝐾 ) ) )
21 6 crngringd ⊢ ( 𝜑 → 𝑆 ∈ Ring )
22 2 fvexi ⊢ 𝐾 ∈ V
23 22 a1i ⊢ ( 𝜑 → 𝐾 ∈ V )
24 1 2 16 4 3 evls1rhm ⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑄 ∈ ( 𝑊 RingHom ( 𝑆 ↑s 𝐾 ) ) )
25 6 7 24 syl2anc ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑊 RingHom ( 𝑆 ↑s 𝐾 ) ) )
26 5 17 rhmf ⊢ ( 𝑄 ∈ ( 𝑊 RingHom ( 𝑆 ↑s 𝐾 ) ) → 𝑄 : 𝐵 ⟶ ( Base ‘ ( 𝑆 ↑s 𝐾 ) ) )
27 25 26 syl ⊢ ( 𝜑 → 𝑄 : 𝐵 ⟶ ( Base ‘ ( 𝑆 ↑s 𝐾 ) ) )
28 27 11 ffvelcdmd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) ∈ ( Base ‘ ( 𝑆 ↑s 𝐾 ) ) )
29 16 17 18 19 20 9 21 23 10 28 12 pwsexpg ⊢ ( 𝜑 → ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( 𝑆 ↑s 𝐾 ) ) ) ( 𝑄 ‘ 𝑀 ) ) ‘ 𝐶 ) = ( 𝑁 ↑ ( ( 𝑄 ‘ 𝑀 ) ‘ 𝐶 ) ) )
30 15 29 eqtrd ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝑁 ∧ 𝑀 ) ) ‘ 𝐶 ) = ( 𝑁 ↑ ( ( 𝑄 ‘ 𝑀 ) ‘ 𝐶 ) ) )