Metamath Proof Explorer

Theorem evls1vsca

Description: Univariate polynomial evaluation of a scalar product of polynomials. (Contributed by Thierry Arnoux, 25-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 )
evls1vsca.1 
|- .X. = ( .s ` W )
evls1vsca.2 
|- .x. = ( .r ` S )
evls1vsca.s 
|- ( ph -> S e. CRing )
evls1vsca.r 
|- ( ph -> R e. ( SubRing ` S ) )
evls1vsca.m 
|- ( ph -> A e. R )
evls1vsca.n 
|- ( ph -> N e. B )
evls1vsca.y 
|- ( ph -> C e. K )
Assertion evls1vsca 
|- ( ph -> ( ( Q ` ( A .X. N ) ) ` C ) = ( A .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 evls1vsca.1 
 |-  .X. = ( .s ` W )
7 evls1vsca.2 
 |-  .x. = ( .r ` S )
8 evls1vsca.s 
 |-  ( ph -> S e. CRing )
9 evls1vsca.r 
 |-  ( ph -> R e. ( SubRing ` S ) )
10 evls1vsca.m 
 |-  ( ph -> A e. R )
11 evls1vsca.n 
 |-  ( ph -> N e. B )
12 evls1vsca.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 ressply1vsca 
 |-  ( ( ph /\ ( A e. R /\ N e. B ) ) -> ( A ( .s ` W ) N ) = ( A ( .s ` ( ( Poly1 ` S ) |`s B ) ) N ) )
17 13 10 11 16 syl12anc 
 |-  ( ph -> ( A ( .s ` W ) N ) = ( A ( .s ` ( ( Poly1 ` S ) |`s B ) ) N ) )
18 6 oveqi 
 |-  ( A .X. N ) = ( A ( .s ` W ) N )
19 5 fvexi 
 |-  B e. _V
20 eqid 
 |-  ( .s ` ( Poly1 ` S ) ) = ( .s ` ( Poly1 ` S ) )
21 15 20 ressvsca 
 |-  ( B e. _V -> ( .s ` ( Poly1 ` S ) ) = ( .s ` ( ( Poly1 ` S ) |`s B ) ) )
22 19 21 ax-mp 
 |-  ( .s ` ( Poly1 ` S ) ) = ( .s ` ( ( Poly1 ` S ) |`s B ) )
23 22 oveqi 
 |-  ( A ( .s ` ( Poly1 ` S ) ) N ) = ( A ( .s ` ( ( Poly1 ` S ) |`s B ) ) N )
24 17 18 23 3eqtr4g 
 |-  ( ph -> ( A .X. N ) = ( A ( .s ` ( Poly1 ` S ) ) N ) )
25 24 fveq2d 
 |-  ( ph -> ( ( eval1 ` S ) ` ( A .X. N ) ) = ( ( eval1 ` S ) ` ( A ( .s ` ( Poly1 ` S ) ) N ) ) )
26 25 fveq1d 
 |-  ( ph -> ( ( ( eval1 ` S ) ` ( A .X. N ) ) ` C ) = ( ( ( eval1 ` S ) ` ( A ( .s ` ( 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 ` ( A .X. N ) ) = ( ( ( eval1 ` S ) |` B ) ` ( A .X. N ) ) )
30 4 subrgcrng 
 |-  ( ( S e. CRing /\ R e. ( SubRing ` S ) ) -> U e. CRing )
31 8 9 30 syl2anc 
 |-  ( ph -> U e. CRing )
32 crngring 
 |-  ( U e. CRing -> U e. Ring )
33 3 ply1lmod 
 |-  ( U e. Ring -> W e. LMod )
34 31 32 33 3syl 
 |-  ( ph -> W e. LMod )
35 2 subrgss 
 |-  ( R e. ( SubRing ` S ) -> R C_ K )
36 9 35 syl 
 |-  ( ph -> R C_ K )
37 4 2 ressbas2 
 |-  ( R C_ K -> R = ( Base ` U ) )
38 36 37 syl 
 |-  ( ph -> R = ( Base ` U ) )
39 4 ovexi 
 |-  U e. _V
40 3 ply1sca 
 |-  ( U e. _V -> U = ( Scalar ` W ) )
41 39 40 mp1i 
 |-  ( ph -> U = ( Scalar ` W ) )
42 41 fveq2d 
 |-  ( ph -> ( Base ` U ) = ( Base ` ( Scalar ` W ) ) )
43 38 42 eqtrd 
 |-  ( ph -> R = ( Base ` ( Scalar ` W ) ) )
44 10 43 eleqtrd 
 |-  ( ph -> A e. ( Base ` ( Scalar ` W ) ) )
45 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
46 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
47 5 45 6 46 lmodvscl 
 |-  ( ( W e. LMod /\ A e. ( Base ` ( Scalar ` W ) ) /\ N e. B ) -> ( A .X. N ) e. B )
48 34 44 11 47 syl3anc 
 |-  ( ph -> ( A .X. N ) e. B )
49 48 fvresd 
 |-  ( ph -> ( ( ( eval1 ` S ) |` B ) ` ( A .X. N ) ) = ( ( eval1 ` S ) ` ( A .X. N ) ) )
50 29 49 eqtr2d 
 |-  ( ph -> ( ( eval1 ` S ) ` ( A .X. N ) ) = ( Q ` ( A .X. N ) ) )
51 50 fveq1d 
 |-  ( ph -> ( ( ( eval1 ` S ) ` ( A .X. N ) ) ` C ) = ( ( Q ` ( A .X. N ) ) ` C ) )
52 eqid 
 |-  ( Base ` ( Poly1 ` S ) ) = ( Base ` ( Poly1 ` S ) )
53 eqid 
 |-  ( PwSer1 ` U ) = ( PwSer1 ` U )
54 eqid 
 |-  ( Base ` ( PwSer1 ` U ) ) = ( Base ` ( PwSer1 ` U ) )
55 14 4 3 5 9 53 54 52 ressply1bas2 
 |-  ( ph -> B = ( ( Base ` ( PwSer1 ` U ) ) i^i ( Base ` ( Poly1 ` S ) ) ) )
56 inss2 
 |-  ( ( Base ` ( PwSer1 ` U ) ) i^i ( Base ` ( Poly1 ` S ) ) ) C_ ( Base ` ( Poly1 ` S ) )
57 55 56 eqsstrdi 
 |-  ( ph -> B C_ ( Base ` ( Poly1 ` S ) ) )
58 57 11 sseldd 
 |-  ( ph -> N e. ( Base ` ( Poly1 ` S ) ) )
59 28 fveq1d 
 |-  ( ph -> ( Q ` N ) = ( ( ( eval1 ` S ) |` B ) ` N ) )
60 11 fvresd 
 |-  ( ph -> ( ( ( eval1 ` S ) |` B ) ` N ) = ( ( eval1 ` S ) ` N ) )
61 59 60 eqtr2d 
 |-  ( ph -> ( ( eval1 ` S ) ` N ) = ( Q ` N ) )
62 61 fveq1d 
 |-  ( ph -> ( ( ( eval1 ` S ) ` N ) ` C ) = ( ( Q ` N ) ` C ) )
63 58 62 jca 
 |-  ( ph -> ( N e. ( Base ` ( Poly1 ` S ) ) /\ ( ( ( eval1 ` S ) ` N ) ` C ) = ( ( Q ` N ) ` C ) ) )
64 36 10 sseldd 
 |-  ( ph -> A e. K )
65 27 14 2 52 8 12 63 64 20 7 evl1vsd 
 |-  ( ph -> ( ( A ( .s ` ( Poly1 ` S ) ) N ) e. ( Base ` ( Poly1 ` S ) ) /\ ( ( ( eval1 ` S ) ` ( A ( .s ` ( Poly1 ` S ) ) N ) ) ` C ) = ( A .x. ( ( Q ` N ) ` C ) ) ) )
66 65 simprd 
 |-  ( ph -> ( ( ( eval1 ` S ) ` ( A ( .s ` ( Poly1 ` S ) ) N ) ) ` C ) = ( A .x. ( ( Q ` N ) ` C ) ) )
67 26 51 66 3eqtr3d 
 |-  ( ph -> ( ( Q ` ( A .X. N ) ) ` C ) = ( A .x. ( ( Q ` N ) ` C ) ) )