Metamath Proof Explorer

Theorem evls1subd

Description: Univariate polynomial evaluation of a difference of polynomials. (Contributed by Thierry Arnoux, 25-Apr-2025)

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

Proof

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