Metamath Proof Explorer

Theorem evlsaddval

Description: Polynomial evaluation builder for addition. (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 ⊢ ( 𝜑 → ( 𝑀 ∈ 𝐵 ∧ ( ( 𝑄 ‘ 𝑀 ) ‘ 𝐴 ) = 𝑉 ) )
evlsaddval.n ⊢ ( 𝜑 → ( 𝑁 ∈ 𝐵 ∧ ( ( 𝑄 ‘ 𝑁 ) ‘ 𝐴 ) = 𝑊 ) )
evlsaddval.g ⊢ ✚ = ( +g ‘ 𝑃 )
evlsaddval.f ⊢ + = ( +g ‘ 𝑆 )
Assertion evlsaddval ( 𝜑 → ( ( 𝑀 ✚ 𝑁 ) ∈ 𝐵 ∧ ( ( 𝑄 ‘ ( 𝑀 ✚ 𝑁 ) ) ‘ 𝐴 ) = ( 𝑉 + 𝑊 ) ) )

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 evlsaddval.n ⊢ ( 𝜑 → ( 𝑁 ∈ 𝐵 ∧ ( ( 𝑄 ‘ 𝑁 ) ‘ 𝐴 ) = 𝑊 ) )
12 evlsaddval.g ⊢ ✚ = ( +g ‘ 𝑃 )
13 evlsaddval.f ⊢ + = ( +g ‘ 𝑆 )
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 rhmghm ⊢ ( 𝑄 ∈ ( 𝑃 RingHom ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) → 𝑄 ∈ ( 𝑃 GrpHom ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
18 16 17 syl ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 GrpHom ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
19 ghmgrp1 ⊢ ( 𝑄 ∈ ( 𝑃 GrpHom ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) → 𝑃 ∈ Grp )
20 18 19 syl ⊢ ( 𝜑 → 𝑃 ∈ Grp )
21 10 simpld ⊢ ( 𝜑 → 𝑀 ∈ 𝐵 )
22 11 simpld ⊢ ( 𝜑 → 𝑁 ∈ 𝐵 )
23 5 12 grpcl ⊢ ( ( 𝑃 ∈ Grp ∧ 𝑀 ∈ 𝐵 ∧ 𝑁 ∈ 𝐵 ) → ( 𝑀 ✚ 𝑁 ) ∈ 𝐵 )
24 20 21 22 23 syl3anc ⊢ ( 𝜑 → ( 𝑀 ✚ 𝑁 ) ∈ 𝐵 )
25 eqid ⊢ ( +g ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) = ( +g ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) )
26 5 12 25 ghmlin ⊢ ( ( 𝑄 ∈ ( 𝑃 GrpHom ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ∧ 𝑀 ∈ 𝐵 ∧ 𝑁 ∈ 𝐵 ) → ( 𝑄 ‘ ( 𝑀 ✚ 𝑁 ) ) = ( ( 𝑄 ‘ 𝑀 ) ( +g ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( 𝑄 ‘ 𝑁 ) ) )
27 18 21 22 26 syl3anc ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝑀 ✚ 𝑁 ) ) = ( ( 𝑄 ‘ 𝑀 ) ( +g ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( 𝑄 ‘ 𝑁 ) ) )
28 eqid ⊢ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) = ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) )
29 ovexd ⊢ ( 𝜑 → ( 𝐾 ↑m 𝐼 ) ∈ V )
30 5 28 rhmf ⊢ ( 𝑄 ∈ ( 𝑃 RingHom ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) → 𝑄 : 𝐵 ⟶ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
31 16 30 syl ⊢ ( 𝜑 → 𝑄 : 𝐵 ⟶ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
32 31 21 ffvelrnd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) ∈ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
33 31 22 ffvelrnd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑁 ) ∈ ( Base ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) )
34 14 28 7 29 32 33 13 25 pwsplusgval ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝑀 ) ( +g ‘ ( 𝑆 ↑s ( 𝐾 ↑m 𝐼 ) ) ) ( 𝑄 ‘ 𝑁 ) ) = ( ( 𝑄 ‘ 𝑀 ) ∘f + ( 𝑄 ‘ 𝑁 ) ) )
35 27 34 eqtrd ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝑀 ✚ 𝑁 ) ) = ( ( 𝑄 ‘ 𝑀 ) ∘f + ( 𝑄 ‘ 𝑁 ) ) )
36 35 fveq1d ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝑀 ✚ 𝑁 ) ) ‘ 𝐴 ) = ( ( ( 𝑄 ‘ 𝑀 ) ∘f + ( 𝑄 ‘ 𝑁 ) ) ‘ 𝐴 ) )
37 14 4 28 7 29 32 pwselbas ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) : ( 𝐾 ↑m 𝐼 ) ⟶ 𝐾 )
38 37 ffnd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) Fn ( 𝐾 ↑m 𝐼 ) )
39 14 4 28 7 29 33 pwselbas ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑁 ) : ( 𝐾 ↑m 𝐼 ) ⟶ 𝐾 )
40 39 ffnd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑁 ) Fn ( 𝐾 ↑m 𝐼 ) )
41 fnfvof ⊢ ( ( ( ( 𝑄 ‘ 𝑀 ) Fn ( 𝐾 ↑m 𝐼 ) ∧ ( 𝑄 ‘ 𝑁 ) Fn ( 𝐾 ↑m 𝐼 ) ) ∧ ( ( 𝐾 ↑m 𝐼 ) ∈ V ∧ 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) ) ) → ( ( ( 𝑄 ‘ 𝑀 ) ∘f + ( 𝑄 ‘ 𝑁 ) ) ‘ 𝐴 ) = ( ( ( 𝑄 ‘ 𝑀 ) ‘ 𝐴 ) + ( ( 𝑄 ‘ 𝑁 ) ‘ 𝐴 ) ) )
42 38 40 29 9 41 syl22anc ⊢ ( 𝜑 → ( ( ( 𝑄 ‘ 𝑀 ) ∘f + ( 𝑄 ‘ 𝑁 ) ) ‘ 𝐴 ) = ( ( ( 𝑄 ‘ 𝑀 ) ‘ 𝐴 ) + ( ( 𝑄 ‘ 𝑁 ) ‘ 𝐴 ) ) )
43 10 simprd ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝑀 ) ‘ 𝐴 ) = 𝑉 )
44 11 simprd ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝑁 ) ‘ 𝐴 ) = 𝑊 )
45 43 44 oveq12d ⊢ ( 𝜑 → ( ( ( 𝑄 ‘ 𝑀 ) ‘ 𝐴 ) + ( ( 𝑄 ‘ 𝑁 ) ‘ 𝐴 ) ) = ( 𝑉 + 𝑊 ) )
46 36 42 45 3eqtrd ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝑀 ✚ 𝑁 ) ) ‘ 𝐴 ) = ( 𝑉 + 𝑊 ) )
47 24 46 jca ⊢ ( 𝜑 → ( ( 𝑀 ✚ 𝑁 ) ∈ 𝐵 ∧ ( ( 𝑄 ‘ ( 𝑀 ✚ 𝑁 ) ) ‘ 𝐴 ) = ( 𝑉 + 𝑊 ) ) )