Metamath Proof Explorer

Theorem evls1addd

Description: Univariate polynomial evaluation of a sum of polynomials. (Contributed by Thierry Arnoux, 8-Feb-2025)

Ref Expression
Hypotheses ressply1evl2.q 
|- Q = ( S evalSub1 R )
ressply1evl2.k 
|- K = ( Base ` S )
ressply1evl2.w 
|- W = ( Poly1 ` U )
ressply1evl2.u 
|- U = ( S |`s R )
ressply1evl2.b 
|- B = ( Base ` W )
evls1addd.1 
|- .+^ = ( +g ` W )
evls1addd.2 
|- .+ = ( +g ` S )
evls1addd.s 
|- ( ph -> S e. CRing )
evls1addd.r 
|- ( ph -> R e. ( SubRing ` S ) )
evls1addd.m 
|- ( ph -> M e. B )
evls1addd.n 
|- ( ph -> N e. B )
evls1addd.y 
|- ( ph -> C e. K )
Assertion evls1addd 
|- ( ph -> ( ( Q ` ( M .+^ N ) ) ` C ) = ( ( ( Q ` M ) ` C ) .+ ( ( Q ` N ) ` C ) ) )

Proof

Step Hyp Ref Expression
1 ressply1evl2.q 
 |-  Q = ( S evalSub1 R )
2 ressply1evl2.k 
 |-  K = ( Base ` S )
3 ressply1evl2.w 
 |-  W = ( Poly1 ` U )
4 ressply1evl2.u 
 |-  U = ( S |`s R )
5 ressply1evl2.b 
 |-  B = ( Base ` W )
6 evls1addd.1 
 |-  .+^ = ( +g ` W )
7 evls1addd.2 
 |-  .+ = ( +g ` S )
8 evls1addd.s 
 |-  ( ph -> S e. CRing )
9 evls1addd.r 
 |-  ( ph -> R e. ( SubRing ` S ) )
10 evls1addd.m 
 |-  ( ph -> M e. B )
11 evls1addd.n 
 |-  ( ph -> N e. B )
12 evls1addd.y 
 |-  ( ph -> C e. K )
13 id 
 |-  ( ph -> ph )
14 eqid 
 |-  ( Poly1 ` S ) = ( Poly1 ` S )
15 eqid 
 |-  ( ( Poly1 ` S ) |`s B ) = ( ( Poly1 ` S ) |`s B )
16 14 4 3 5 9 15 ressply1add 
 |-  ( ( ph /\ ( M e. B /\ N e. B ) ) -> ( M ( +g ` W ) N ) = ( M ( +g ` ( ( Poly1 ` S ) |`s B ) ) N ) )
17 13 10 11 16 syl12anc 
 |-  ( ph -> ( M ( +g ` W ) N ) = ( M ( +g ` ( ( Poly1 ` S ) |`s B ) ) N ) )
18 6 oveqi 
 |-  ( M .+^ N ) = ( M ( +g ` W ) N )
19 5 fvexi 
 |-  B e. _V
20 eqid 
 |-  ( +g ` ( Poly1 ` S ) ) = ( +g ` ( Poly1 ` S ) )
21 15 20 ressplusg 
 |-  ( B e. _V -> ( +g ` ( Poly1 ` S ) ) = ( +g ` ( ( Poly1 ` S ) |`s B ) ) )
22 19 21 ax-mp 
 |-  ( +g ` ( Poly1 ` S ) ) = ( +g ` ( ( Poly1 ` S ) |`s B ) )
23 22 oveqi 
 |-  ( M ( +g ` ( Poly1 ` S ) ) N ) = ( M ( +g ` ( ( Poly1 ` S ) |`s B ) ) N )
24 17 18 23 3eqtr4g 
 |-  ( ph -> ( M .+^ N ) = ( M ( +g ` ( Poly1 ` S ) ) N ) )
25 24 fveq2d 
 |-  ( ph -> ( ( eval1 ` S ) ` ( M .+^ N ) ) = ( ( eval1 ` S ) ` ( M ( +g ` ( Poly1 ` S ) ) N ) ) )
26 25 fveq1d 
 |-  ( ph -> ( ( ( eval1 ` S ) ` ( M .+^ N ) ) ` C ) = ( ( ( eval1 ` S ) ` ( M ( +g ` ( Poly1 ` S ) ) N ) ) ` C ) )
27 eqid 
 |-  ( eval1 ` S ) = ( eval1 ` S )
28 1 2 3 4 5 27 8 9 ressply1evl 
 |-  ( ph -> Q = ( ( eval1 ` S ) |` B ) )
29 28 fveq1d 
 |-  ( ph -> ( Q ` ( M .+^ N ) ) = ( ( ( eval1 ` S ) |` B ) ` ( M .+^ N ) ) )
30 4 subrgring 
 |-  ( R e. ( SubRing ` S ) -> U e. Ring )
31 3 ply1ring 
 |-  ( U e. Ring -> W e. Ring )
32 9 30 31 3syl 
 |-  ( ph -> W e. Ring )
33 32 ringgrpd 
 |-  ( ph -> W e. Grp )
34 5 6 33 10 11 grpcld 
 |-  ( ph -> ( M .+^ N ) e. B )
35 34 fvresd 
 |-  ( ph -> ( ( ( eval1 ` S ) |` B ) ` ( M .+^ N ) ) = ( ( eval1 ` S ) ` ( M .+^ N ) ) )
36 29 35 eqtr2d 
 |-  ( ph -> ( ( eval1 ` S ) ` ( M .+^ N ) ) = ( Q ` ( M .+^ N ) ) )
37 36 fveq1d 
 |-  ( ph -> ( ( ( eval1 ` S ) ` ( M .+^ N ) ) ` C ) = ( ( Q ` ( M .+^ N ) ) ` C ) )
38 eqid 
 |-  ( Base ` ( Poly1 ` S ) ) = ( Base ` ( Poly1 ` S ) )
39 eqid 
 |-  ( PwSer1 ` U ) = ( PwSer1 ` U )
40 eqid 
 |-  ( Base ` ( PwSer1 ` U ) ) = ( Base ` ( PwSer1 ` U ) )
41 14 4 3 5 9 39 40 38 ressply1bas2 
 |-  ( ph -> B = ( ( Base ` ( PwSer1 ` U ) ) i^i ( Base ` ( Poly1 ` S ) ) ) )
42 inss2 
 |-  ( ( Base ` ( PwSer1 ` U ) ) i^i ( Base ` ( Poly1 ` S ) ) ) C_ ( Base ` ( Poly1 ` S ) )
43 41 42 eqsstrdi 
 |-  ( ph -> B C_ ( Base ` ( Poly1 ` S ) ) )
44 43 10 sseldd 
 |-  ( ph -> M e. ( Base ` ( Poly1 ` S ) ) )
45 28 fveq1d 
 |-  ( ph -> ( Q ` M ) = ( ( ( eval1 ` S ) |` B ) ` M ) )
46 10 fvresd 
 |-  ( ph -> ( ( ( eval1 ` S ) |` B ) ` M ) = ( ( eval1 ` S ) ` M ) )
47 45 46 eqtr2d 
 |-  ( ph -> ( ( eval1 ` S ) ` M ) = ( Q ` M ) )
48 47 fveq1d 
 |-  ( ph -> ( ( ( eval1 ` S ) ` M ) ` C ) = ( ( Q ` M ) ` C ) )
49 44 48 jca 
 |-  ( ph -> ( M e. ( Base ` ( Poly1 ` S ) ) /\ ( ( ( eval1 ` S ) ` M ) ` C ) = ( ( Q ` M ) ` C ) ) )
50 43 11 sseldd 
 |-  ( ph -> N e. ( Base ` ( Poly1 ` S ) ) )
51 28 fveq1d 
 |-  ( ph -> ( Q ` N ) = ( ( ( eval1 ` S ) |` B ) ` N ) )
52 11 fvresd 
 |-  ( ph -> ( ( ( eval1 ` S ) |` B ) ` N ) = ( ( eval1 ` S ) ` N ) )
53 51 52 eqtr2d 
 |-  ( ph -> ( ( eval1 ` S ) ` N ) = ( Q ` N ) )
54 53 fveq1d 
 |-  ( ph -> ( ( ( eval1 ` S ) ` N ) ` C ) = ( ( Q ` N ) ` C ) )
55 50 54 jca 
 |-  ( ph -> ( N e. ( Base ` ( Poly1 ` S ) ) /\ ( ( ( eval1 ` S ) ` N ) ` C ) = ( ( Q ` N ) ` C ) ) )
56 27 14 2 38 8 12 49 55 20 7 evl1addd 
 |-  ( ph -> ( ( M ( +g ` ( Poly1 ` S ) ) N ) e. ( Base ` ( Poly1 ` S ) ) /\ ( ( ( eval1 ` S ) ` ( M ( +g ` ( Poly1 ` S ) ) N ) ) ` C ) = ( ( ( Q ` M ) ` C ) .+ ( ( Q ` N ) ` C ) ) ) )
57 56 simprd 
 |-  ( ph -> ( ( ( eval1 ` S ) ` ( M ( +g ` ( Poly1 ` S ) ) N ) ) ` C ) = ( ( ( Q ` M ) ` C ) .+ ( ( Q ` N ) ` C ) ) )
58 26 37 57 3eqtr3d 
 |-  ( ph -> ( ( Q ` ( M .+^ N ) ) ` C ) = ( ( ( Q ` M ) ` C ) .+ ( ( Q ` N ) ` C ) ) )