Metamath Proof Explorer

Theorem evls1muld

Description: Univariate polynomial evaluation of a product of polynomials. (Contributed by Thierry Arnoux, 24-Jan-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 )
evls1muld.1 
|- .X. = ( .r ` W )
evls1muld.2 
|- .x. = ( .r ` S )
evls1muld.s 
|- ( ph -> S e. CRing )
evls1muld.r 
|- ( ph -> R e. ( SubRing ` S ) )
evls1muld.m 
|- ( ph -> M e. B )
evls1muld.n 
|- ( ph -> N e. B )
evls1muld.c 
|- ( ph -> C e. K )
Assertion evls1muld 
|- ( ph -> ( ( Q ` ( M .X. N ) ) ` C ) = ( ( ( Q ` M ) ` C ) .x. ( ( 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 evls1muld.1 
 |-  .X. = ( .r ` W )
7 evls1muld.2 
 |-  .x. = ( .r ` S )
8 evls1muld.s 
 |-  ( ph -> S e. CRing )
9 evls1muld.r 
 |-  ( ph -> R e. ( SubRing ` S ) )
10 evls1muld.m 
 |-  ( ph -> M e. B )
11 evls1muld.n 
 |-  ( ph -> N e. B )
12 evls1muld.c 
 |-  ( 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 ressply1mul 
 |-  ( ( ph /\ ( M e. B /\ N e. B ) ) -> ( M ( .r ` W ) N ) = ( M ( .r ` ( ( Poly1 ` S ) |`s B ) ) N ) )
17 13 10 11 16 syl12anc 
 |-  ( ph -> ( M ( .r ` W ) N ) = ( M ( .r ` ( ( Poly1 ` S ) |`s B ) ) N ) )
18 6 oveqi 
 |-  ( M .X. N ) = ( M ( .r ` W ) N )
19 5 fvexi 
 |-  B e. _V
20 eqid 
 |-  ( .r ` ( Poly1 ` S ) ) = ( .r ` ( Poly1 ` S ) )
21 15 20 ressmulr 
 |-  ( B e. _V -> ( .r ` ( Poly1 ` S ) ) = ( .r ` ( ( Poly1 ` S ) |`s B ) ) )
22 19 21 ax-mp 
 |-  ( .r ` ( Poly1 ` S ) ) = ( .r ` ( ( Poly1 ` S ) |`s B ) )
23 22 oveqi 
 |-  ( M ( .r ` ( Poly1 ` S ) ) N ) = ( M ( .r ` ( ( Poly1 ` S ) |`s B ) ) N )
24 17 18 23 3eqtr4g 
 |-  ( ph -> ( M .X. N ) = ( M ( .r ` ( Poly1 ` S ) ) N ) )
25 24 fveq2d 
 |-  ( ph -> ( ( eval1 ` S ) ` ( M .X. N ) ) = ( ( eval1 ` S ) ` ( M ( .r ` ( Poly1 ` S ) ) N ) ) )
26 25 fveq1d 
 |-  ( ph -> ( ( ( eval1 ` S ) ` ( M .X. N ) ) ` C ) = ( ( ( eval1 ` S ) ` ( M ( .r ` ( 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 .X. N ) ) = ( ( ( eval1 ` S ) |` B ) ` ( M .X. 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 5 6 32 10 11 ringcld 
 |-  ( ph -> ( M .X. N ) e. B )
34 33 fvresd 
 |-  ( ph -> ( ( ( eval1 ` S ) |` B ) ` ( M .X. N ) ) = ( ( eval1 ` S ) ` ( M .X. N ) ) )
35 29 34 eqtr2d 
 |-  ( ph -> ( ( eval1 ` S ) ` ( M .X. N ) ) = ( Q ` ( M .X. N ) ) )
36 35 fveq1d 
 |-  ( ph -> ( ( ( eval1 ` S ) ` ( M .X. N ) ) ` C ) = ( ( Q ` ( M .X. N ) ) ` C ) )
37 eqid 
 |-  ( Base ` ( Poly1 ` S ) ) = ( Base ` ( Poly1 ` S ) )
38 eqid 
 |-  ( PwSer1 ` U ) = ( PwSer1 ` U )
39 eqid 
 |-  ( Base ` ( PwSer1 ` U ) ) = ( Base ` ( PwSer1 ` U ) )
40 14 4 3 5 9 38 39 37 ressply1bas2 
 |-  ( ph -> B = ( ( Base ` ( PwSer1 ` U ) ) i^i ( Base ` ( Poly1 ` S ) ) ) )
41 inss2 
 |-  ( ( Base ` ( PwSer1 ` U ) ) i^i ( Base ` ( Poly1 ` S ) ) ) C_ ( Base ` ( Poly1 ` S ) )
42 40 41 eqsstrdi 
 |-  ( ph -> B C_ ( Base ` ( Poly1 ` S ) ) )
43 42 10 sseldd 
 |-  ( ph -> M e. ( Base ` ( Poly1 ` S ) ) )
44 28 fveq1d 
 |-  ( ph -> ( Q ` M ) = ( ( ( eval1 ` S ) |` B ) ` M ) )
45 10 fvresd 
 |-  ( ph -> ( ( ( eval1 ` S ) |` B ) ` M ) = ( ( eval1 ` S ) ` M ) )
46 44 45 eqtr2d 
 |-  ( ph -> ( ( eval1 ` S ) ` M ) = ( Q ` M ) )
47 46 fveq1d 
 |-  ( ph -> ( ( ( eval1 ` S ) ` M ) ` C ) = ( ( Q ` M ) ` C ) )
48 43 47 jca 
 |-  ( ph -> ( M e. ( Base ` ( Poly1 ` S ) ) /\ ( ( ( eval1 ` S ) ` M ) ` C ) = ( ( Q ` M ) ` C ) ) )
49 42 11 sseldd 
 |-  ( ph -> N e. ( Base ` ( Poly1 ` S ) ) )
50 28 fveq1d 
 |-  ( ph -> ( Q ` N ) = ( ( ( eval1 ` S ) |` B ) ` N ) )
51 11 fvresd 
 |-  ( ph -> ( ( ( eval1 ` S ) |` B ) ` N ) = ( ( eval1 ` S ) ` N ) )
52 50 51 eqtr2d 
 |-  ( ph -> ( ( eval1 ` S ) ` N ) = ( Q ` N ) )
53 52 fveq1d 
 |-  ( ph -> ( ( ( eval1 ` S ) ` N ) ` C ) = ( ( Q ` N ) ` C ) )
54 49 53 jca 
 |-  ( ph -> ( N e. ( Base ` ( Poly1 ` S ) ) /\ ( ( ( eval1 ` S ) ` N ) ` C ) = ( ( Q ` N ) ` C ) ) )
55 27 14 2 37 8 12 48 54 20 7 evl1muld 
 |-  ( ph -> ( ( M ( .r ` ( Poly1 ` S ) ) N ) e. ( Base ` ( Poly1 ` S ) ) /\ ( ( ( eval1 ` S ) ` ( M ( .r ` ( Poly1 ` S ) ) N ) ) ` C ) = ( ( ( Q ` M ) ` C ) .x. ( ( Q ` N ) ` C ) ) ) )
56 55 simprd 
 |-  ( ph -> ( ( ( eval1 ` S ) ` ( M ( .r ` ( Poly1 ` S ) ) N ) ) ` C ) = ( ( ( Q ` M ) ` C ) .x. ( ( Q ` N ) ` C ) ) )
57 26 36 56 3eqtr3d 
 |-  ( ph -> ( ( Q ` ( M .X. N ) ) ` C ) = ( ( ( Q ` M ) ` C ) .x. ( ( Q ` N ) ` C ) ) )