Metamath Proof Explorer

Theorem evl1vsd

Description: Polynomial evaluation builder for scalar multiplication of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015)

Ref Expression
Hypotheses evl1addd.q 
|- O = ( eval1 ` R )
evl1addd.p 
|- P = ( Poly1 ` R )
evl1addd.b 
|- B = ( Base ` R )
evl1addd.u 
|- U = ( Base ` P )
evl1addd.1 
|- ( ph -> R e. CRing )
evl1addd.2 
|- ( ph -> Y e. B )
evl1addd.3 
|- ( ph -> ( M e. U /\ ( ( O ` M ) ` Y ) = V ) )
evl1vsd.4 
|- ( ph -> N e. B )
evl1vsd.s 
|- .xb = ( .s ` P )
evl1vsd.t 
|- .x. = ( .r ` R )
Assertion evl1vsd 
|- ( ph -> ( ( N .xb M ) e. U /\ ( ( O ` ( N .xb M ) ) ` Y ) = ( N .x. V ) ) )

Proof

Step Hyp Ref Expression
1 evl1addd.q 
 |-  O = ( eval1 ` R )
2 evl1addd.p 
 |-  P = ( Poly1 ` R )
3 evl1addd.b 
 |-  B = ( Base ` R )
4 evl1addd.u 
 |-  U = ( Base ` P )
5 evl1addd.1 
 |-  ( ph -> R e. CRing )
6 evl1addd.2 
 |-  ( ph -> Y e. B )
7 evl1addd.3 
 |-  ( ph -> ( M e. U /\ ( ( O ` M ) ` Y ) = V ) )
8 evl1vsd.4 
 |-  ( ph -> N e. B )
9 evl1vsd.s 
 |-  .xb = ( .s ` P )
10 evl1vsd.t 
 |-  .x. = ( .r ` R )
11 eqid 
 |-  ( algSc ` P ) = ( algSc ` P )
12 1 2 3 11 4 5 8 6 evl1scad 
 |-  ( ph -> ( ( ( algSc ` P ) ` N ) e. U /\ ( ( O ` ( ( algSc ` P ) ` N ) ) ` Y ) = N ) )
13 eqid 
 |-  ( .r ` P ) = ( .r ` P )
14 1 2 3 4 5 6 12 7 13 10 evl1muld 
 |-  ( ph -> ( ( ( ( algSc ` P ) ` N ) ( .r ` P ) M ) e. U /\ ( ( O ` ( ( ( algSc ` P ) ` N ) ( .r ` P ) M ) ) ` Y ) = ( N .x. V ) ) )
15 2 ply1assa 
 |-  ( R e. CRing -> P e. AssAlg )
16 5 15 syl 
 |-  ( ph -> P e. AssAlg )
17 2 ply1sca 
 |-  ( R e. CRing -> R = ( Scalar ` P ) )
18 5 17 syl 
 |-  ( ph -> R = ( Scalar ` P ) )
19 18 fveq2d 
 |-  ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) )
20 3 19 eqtrid 
 |-  ( ph -> B = ( Base ` ( Scalar ` P ) ) )
21 8 20 eleqtrd 
 |-  ( ph -> N e. ( Base ` ( Scalar ` P ) ) )
22 7 simpld 
 |-  ( ph -> M e. U )
23 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
24 eqid 
 |-  ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) )
25 11 23 24 4 13 9 asclmul1 
 |-  ( ( P e. AssAlg /\ N e. ( Base ` ( Scalar ` P ) ) /\ M e. U ) -> ( ( ( algSc ` P ) ` N ) ( .r ` P ) M ) = ( N .xb M ) )
26 16 21 22 25 syl3anc 
 |-  ( ph -> ( ( ( algSc ` P ) ` N ) ( .r ` P ) M ) = ( N .xb M ) )
27 26 eleq1d 
 |-  ( ph -> ( ( ( ( algSc ` P ) ` N ) ( .r ` P ) M ) e. U <-> ( N .xb M ) e. U ) )
28 26 fveq2d 
 |-  ( ph -> ( O ` ( ( ( algSc ` P ) ` N ) ( .r ` P ) M ) ) = ( O ` ( N .xb M ) ) )
29 28 fveq1d 
 |-  ( ph -> ( ( O ` ( ( ( algSc ` P ) ` N ) ( .r ` P ) M ) ) ` Y ) = ( ( O ` ( N .xb M ) ) ` Y ) )
30 29 eqeq1d 
 |-  ( ph -> ( ( ( O ` ( ( ( algSc ` P ) ` N ) ( .r ` P ) M ) ) ` Y ) = ( N .x. V ) <-> ( ( O ` ( N .xb M ) ) ` Y ) = ( N .x. V ) ) )
31 27 30 anbi12d 
 |-  ( ph -> ( ( ( ( ( algSc ` P ) ` N ) ( .r ` P ) M ) e. U /\ ( ( O ` ( ( ( algSc ` P ) ` N ) ( .r ` P ) M ) ) ` Y ) = ( N .x. V ) ) <-> ( ( N .xb M ) e. U /\ ( ( O ` ( N .xb M ) ) ` Y ) = ( N .x. V ) ) ) )
32 14 31 mpbid 
 |-  ( ph -> ( ( N .xb M ) e. U /\ ( ( O ` ( N .xb M ) ) ` Y ) = ( N .x. V ) ) )