Metamath Proof Explorer

Theorem evladdval

Description: Polynomial evaluation builder for addition. (Contributed by SN, 9-Feb-2025)

Ref Expression
Hypotheses evladdval.q 
|- Q = ( I eval S )
evladdval.p 
|- P = ( I mPoly S )
evladdval.k 
|- K = ( Base ` S )
evladdval.b 
|- B = ( Base ` P )
evladdval.g 
|- .+b = ( +g ` P )
evladdval.f 
|- .+ = ( +g ` S )
evladdval.i 
|- ( ph -> I e. Z )
evladdval.s 
|- ( ph -> S e. CRing )
evladdval.a 
|- ( ph -> A e. ( K ^m I ) )
evladdval.m 
|- ( ph -> ( M e. B /\ ( ( Q ` M ) ` A ) = V ) )
evladdval.n 
|- ( ph -> ( N e. B /\ ( ( Q ` N ) ` A ) = W ) )
Assertion evladdval 
|- ( ph -> ( ( M .+b N ) e. B /\ ( ( Q ` ( M .+b N ) ) ` A ) = ( V .+ W ) ) )

Proof

Step Hyp Ref Expression
1 evladdval.q 
 |-  Q = ( I eval S )
2 evladdval.p 
 |-  P = ( I mPoly S )
3 evladdval.k 
 |-  K = ( Base ` S )
4 evladdval.b 
 |-  B = ( Base ` P )
5 evladdval.g 
 |-  .+b = ( +g ` P )
6 evladdval.f 
 |-  .+ = ( +g ` S )
7 evladdval.i 
 |-  ( ph -> I e. Z )
8 evladdval.s 
 |-  ( ph -> S e. CRing )
9 evladdval.a 
 |-  ( ph -> A e. ( K ^m I ) )
10 evladdval.m 
 |-  ( ph -> ( M e. B /\ ( ( Q ` M ) ` A ) = V ) )
11 evladdval.n 
 |-  ( ph -> ( N e. B /\ ( ( Q ` N ) ` A ) = W ) )
12 eqid 
 |-  ( S ^s ( K ^m I ) ) = ( S ^s ( K ^m I ) )
13 1 3 2 12 evlrhm 
 |-  ( ( I e. Z /\ S e. CRing ) -> Q e. ( P RingHom ( S ^s ( K ^m I ) ) ) )
14 7 8 13 syl2anc 
 |-  ( ph -> Q e. ( P RingHom ( S ^s ( K ^m I ) ) ) )
15 rhmghm 
 |-  ( Q e. ( P RingHom ( S ^s ( K ^m I ) ) ) -> Q e. ( P GrpHom ( S ^s ( K ^m I ) ) ) )
16 14 15 syl 
 |-  ( ph -> Q e. ( P GrpHom ( S ^s ( K ^m I ) ) ) )
17 ghmgrp1 
 |-  ( Q e. ( P GrpHom ( S ^s ( K ^m I ) ) ) -> P e. Grp )
18 16 17 syl 
 |-  ( ph -> P e. Grp )
19 10 simpld 
 |-  ( ph -> M e. B )
20 11 simpld 
 |-  ( ph -> N e. B )
21 4 5 18 19 20 grpcld 
 |-  ( ph -> ( M .+b N ) e. B )
22 eqid 
 |-  ( +g ` ( S ^s ( K ^m I ) ) ) = ( +g ` ( S ^s ( K ^m I ) ) )
23 4 5 22 ghmlin 
 |-  ( ( Q e. ( P GrpHom ( S ^s ( K ^m I ) ) ) /\ M e. B /\ N e. B ) -> ( Q ` ( M .+b N ) ) = ( ( Q ` M ) ( +g ` ( S ^s ( K ^m I ) ) ) ( Q ` N ) ) )
24 16 19 20 23 syl3anc 
 |-  ( ph -> ( Q ` ( M .+b N ) ) = ( ( Q ` M ) ( +g ` ( S ^s ( K ^m I ) ) ) ( Q ` N ) ) )
25 eqid 
 |-  ( Base ` ( S ^s ( K ^m I ) ) ) = ( Base ` ( S ^s ( K ^m I ) ) )
26 ovexd 
 |-  ( ph -> ( K ^m I ) e. _V )
27 4 25 rhmf 
 |-  ( Q e. ( P RingHom ( S ^s ( K ^m I ) ) ) -> Q : B --> ( Base ` ( S ^s ( K ^m I ) ) ) )
28 14 27 syl 
 |-  ( ph -> Q : B --> ( Base ` ( S ^s ( K ^m I ) ) ) )
29 28 19 ffvelcdmd 
 |-  ( ph -> ( Q ` M ) e. ( Base ` ( S ^s ( K ^m I ) ) ) )
30 28 20 ffvelcdmd 
 |-  ( ph -> ( Q ` N ) e. ( Base ` ( S ^s ( K ^m I ) ) ) )
31 12 25 8 26 29 30 6 22 pwsplusgval 
 |-  ( ph -> ( ( Q ` M ) ( +g ` ( S ^s ( K ^m I ) ) ) ( Q ` N ) ) = ( ( Q ` M ) oF .+ ( Q ` N ) ) )
32 24 31 eqtrd 
 |-  ( ph -> ( Q ` ( M .+b N ) ) = ( ( Q ` M ) oF .+ ( Q ` N ) ) )
33 32 fveq1d 
 |-  ( ph -> ( ( Q ` ( M .+b N ) ) ` A ) = ( ( ( Q ` M ) oF .+ ( Q ` N ) ) ` A ) )
34 12 3 25 8 26 29 pwselbas 
 |-  ( ph -> ( Q ` M ) : ( K ^m I ) --> K )
35 34 ffnd 
 |-  ( ph -> ( Q ` M ) Fn ( K ^m I ) )
36 12 3 25 8 26 30 pwselbas 
 |-  ( ph -> ( Q ` N ) : ( K ^m I ) --> K )
37 36 ffnd 
 |-  ( ph -> ( Q ` N ) Fn ( K ^m I ) )
38 fnfvof 
 |-  ( ( ( ( Q ` M ) Fn ( K ^m I ) /\ ( Q ` N ) Fn ( K ^m I ) ) /\ ( ( K ^m I ) e. _V /\ A e. ( K ^m I ) ) ) -> ( ( ( Q ` M ) oF .+ ( Q ` N ) ) ` A ) = ( ( ( Q ` M ) ` A ) .+ ( ( Q ` N ) ` A ) ) )
39 35 37 26 9 38 syl22anc 
 |-  ( ph -> ( ( ( Q ` M ) oF .+ ( Q ` N ) ) ` A ) = ( ( ( Q ` M ) ` A ) .+ ( ( Q ` N ) ` A ) ) )
40 10 simprd 
 |-  ( ph -> ( ( Q ` M ) ` A ) = V )
41 11 simprd 
 |-  ( ph -> ( ( Q ` N ) ` A ) = W )
42 40 41 oveq12d 
 |-  ( ph -> ( ( ( Q ` M ) ` A ) .+ ( ( Q ` N ) ` A ) ) = ( V .+ W ) )
43 33 39 42 3eqtrd 
 |-  ( ph -> ( ( Q ` ( M .+b N ) ) ` A ) = ( V .+ W ) )
44 21 43 jca 
 |-  ( ph -> ( ( M .+b N ) e. B /\ ( ( Q ` ( M .+b N ) ) ` A ) = ( V .+ W ) ) )