Metamath Proof Explorer

Theorem coe1tmfv2

Description: Zero coefficient of a polynomial term. (Contributed by Stefan O'Rear, 27-Mar-2015)

Ref Expression
Hypotheses coe1tm.z 
|- .0. = ( 0g ` R )
coe1tm.k 
|- K = ( Base ` R )
coe1tm.p 
|- P = ( Poly1 ` R )
coe1tm.x 
|- X = ( var1 ` R )
coe1tm.m 
|- .x. = ( .s ` P )
coe1tm.n 
|- N = ( mulGrp ` P )
coe1tm.e 
|- .^ = ( .g ` N )
coe1tmfv2.r 
|- ( ph -> R e. Ring )
coe1tmfv2.c 
|- ( ph -> C e. K )
coe1tmfv2.d 
|- ( ph -> D e. NN0 )
coe1tmfv2.f 
|- ( ph -> F e. NN0 )
coe1tmfv2.q 
|- ( ph -> D =/= F )
Assertion coe1tmfv2 
|- ( ph -> ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` F ) = .0. )

Proof

Step Hyp Ref Expression
1 coe1tm.z 
 |-  .0. = ( 0g ` R )
2 coe1tm.k 
 |-  K = ( Base ` R )
3 coe1tm.p 
 |-  P = ( Poly1 ` R )
4 coe1tm.x 
 |-  X = ( var1 ` R )
5 coe1tm.m 
 |-  .x. = ( .s ` P )
6 coe1tm.n 
 |-  N = ( mulGrp ` P )
7 coe1tm.e 
 |-  .^ = ( .g ` N )
8 coe1tmfv2.r 
 |-  ( ph -> R e. Ring )
9 coe1tmfv2.c 
 |-  ( ph -> C e. K )
10 coe1tmfv2.d 
 |-  ( ph -> D e. NN0 )
11 coe1tmfv2.f 
 |-  ( ph -> F e. NN0 )
12 coe1tmfv2.q 
 |-  ( ph -> D =/= F )
13 1 2 3 4 5 6 7 coe1tm 
 |-  ( ( R e. Ring /\ C e. K /\ D e. NN0 ) -> ( coe1 ` ( C .x. ( D .^ X ) ) ) = ( x e. NN0 |-> if ( x = D , C , .0. ) ) )
14 8 9 10 13 syl3anc 
 |-  ( ph -> ( coe1 ` ( C .x. ( D .^ X ) ) ) = ( x e. NN0 |-> if ( x = D , C , .0. ) ) )
15 14 fveq1d 
 |-  ( ph -> ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` F ) = ( ( x e. NN0 |-> if ( x = D , C , .0. ) ) ` F ) )
16 eqid 
 |-  ( x e. NN0 |-> if ( x = D , C , .0. ) ) = ( x e. NN0 |-> if ( x = D , C , .0. ) )
17 eqeq1 
 |-  ( x = F -> ( x = D <-> F = D ) )
18 17 ifbid 
 |-  ( x = F -> if ( x = D , C , .0. ) = if ( F = D , C , .0. ) )
19 2 1 ring0cl 
 |-  ( R e. Ring -> .0. e. K )
20 8 19 syl 
 |-  ( ph -> .0. e. K )
21 9 20 ifcld 
 |-  ( ph -> if ( F = D , C , .0. ) e. K )
22 16 18 11 21 fvmptd3 
 |-  ( ph -> ( ( x e. NN0 |-> if ( x = D , C , .0. ) ) ` F ) = if ( F = D , C , .0. ) )
23 12 necomd 
 |-  ( ph -> F =/= D )
24 23 neneqd 
 |-  ( ph -> -. F = D )
25 24 iffalsed 
 |-  ( ph -> if ( F = D , C , .0. ) = .0. )
26 15 22 25 3eqtrd 
 |-  ( ph -> ( ( coe1 ` ( C .x. ( D .^ X ) ) ) ` F ) = .0. )