Metamath Proof Explorer

Theorem coe1sclmulfv

Description: A single coefficient of a polynomial multiplied on the left by a scalar. (Contributed by Stefan O'Rear, 1-Apr-2015)

Ref Expression
Hypotheses coe1sclmul.p 
|- P = ( Poly1 ` R )
coe1sclmul.b 
|- B = ( Base ` P )
coe1sclmul.k 
|- K = ( Base ` R )
coe1sclmul.a 
|- A = ( algSc ` P )
coe1sclmul.t 
|- .xb = ( .r ` P )
coe1sclmul.u 
|- .x. = ( .r ` R )
Assertion coe1sclmulfv 
|- ( ( R e. Ring /\ ( X e. K /\ Y e. B ) /\ .0. e. NN0 ) -> ( ( coe1 ` ( ( A ` X ) .xb Y ) ) ` .0. ) = ( X .x. ( ( coe1 ` Y ) ` .0. ) ) )

Proof

Step Hyp Ref Expression
1 coe1sclmul.p 
 |-  P = ( Poly1 ` R )
2 coe1sclmul.b 
 |-  B = ( Base ` P )
3 coe1sclmul.k 
 |-  K = ( Base ` R )
4 coe1sclmul.a 
 |-  A = ( algSc ` P )
5 coe1sclmul.t 
 |-  .xb = ( .r ` P )
6 coe1sclmul.u 
 |-  .x. = ( .r ` R )
7 1 2 3 4 5 6 coe1sclmul 
 |-  ( ( R e. Ring /\ X e. K /\ Y e. B ) -> ( coe1 ` ( ( A ` X ) .xb Y ) ) = ( ( NN0 X. { X } ) oF .x. ( coe1 ` Y ) ) )
8 7 3expb 
 |-  ( ( R e. Ring /\ ( X e. K /\ Y e. B ) ) -> ( coe1 ` ( ( A ` X ) .xb Y ) ) = ( ( NN0 X. { X } ) oF .x. ( coe1 ` Y ) ) )
9 8 3adant3 
 |-  ( ( R e. Ring /\ ( X e. K /\ Y e. B ) /\ .0. e. NN0 ) -> ( coe1 ` ( ( A ` X ) .xb Y ) ) = ( ( NN0 X. { X } ) oF .x. ( coe1 ` Y ) ) )
10 9 fveq1d 
 |-  ( ( R e. Ring /\ ( X e. K /\ Y e. B ) /\ .0. e. NN0 ) -> ( ( coe1 ` ( ( A ` X ) .xb Y ) ) ` .0. ) = ( ( ( NN0 X. { X } ) oF .x. ( coe1 ` Y ) ) ` .0. ) )
11 simp3 
 |-  ( ( R e. Ring /\ ( X e. K /\ Y e. B ) /\ .0. e. NN0 ) -> .0. e. NN0 )
12 nn0ex 
 |-  NN0 e. _V
13 12 a1i 
 |-  ( ( R e. Ring /\ ( X e. K /\ Y e. B ) /\ .0. e. NN0 ) -> NN0 e. _V )
14 simp2l 
 |-  ( ( R e. Ring /\ ( X e. K /\ Y e. B ) /\ .0. e. NN0 ) -> X e. K )
15 simp2r 
 |-  ( ( R e. Ring /\ ( X e. K /\ Y e. B ) /\ .0. e. NN0 ) -> Y e. B )
16 eqid 
 |-  ( coe1 ` Y ) = ( coe1 ` Y )
17 eqid 
 |-  ( Base ` R ) = ( Base ` R )
18 16 2 1 17 coe1f 
 |-  ( Y e. B -> ( coe1 ` Y ) : NN0 --> ( Base ` R ) )
19 ffn 
 |-  ( ( coe1 ` Y ) : NN0 --> ( Base ` R ) -> ( coe1 ` Y ) Fn NN0 )
20 15 18 19 3syl 
 |-  ( ( R e. Ring /\ ( X e. K /\ Y e. B ) /\ .0. e. NN0 ) -> ( coe1 ` Y ) Fn NN0 )
21 eqidd 
 |-  ( ( ( R e. Ring /\ ( X e. K /\ Y e. B ) /\ .0. e. NN0 ) /\ .0. e. NN0 ) -> ( ( coe1 ` Y ) ` .0. ) = ( ( coe1 ` Y ) ` .0. ) )
22 13 14 20 21 ofc1 
 |-  ( ( ( R e. Ring /\ ( X e. K /\ Y e. B ) /\ .0. e. NN0 ) /\ .0. e. NN0 ) -> ( ( ( NN0 X. { X } ) oF .x. ( coe1 ` Y ) ) ` .0. ) = ( X .x. ( ( coe1 ` Y ) ` .0. ) ) )
23 11 22 mpdan 
 |-  ( ( R e. Ring /\ ( X e. K /\ Y e. B ) /\ .0. e. NN0 ) -> ( ( ( NN0 X. { X } ) oF .x. ( coe1 ` Y ) ) ` .0. ) = ( X .x. ( ( coe1 ` Y ) ` .0. ) ) )
24 10 23 eqtrd 
 |-  ( ( R e. Ring /\ ( X e. K /\ Y e. B ) /\ .0. e. NN0 ) -> ( ( coe1 ` ( ( A ` X ) .xb Y ) ) ` .0. ) = ( X .x. ( ( coe1 ` Y ) ` .0. ) ) )