Metamath Proof Explorer

Theorem evlsaddval

Description: Polynomial evaluation builder for addition. (Contributed by SN, 27-Jul-2024)

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

Proof

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