Metamath Proof Explorer

Theorem cply1coe0

Description: All but the first coefficient of a constant polynomial ( i.e. a "lifted scalar") are zero. (Contributed by AV, 16-Nov-2019)

Ref Expression
Hypotheses cply1coe0.k 
|- K = ( Base ` R )
cply1coe0.0 
|- .0. = ( 0g ` R )
cply1coe0.p 
|- P = ( Poly1 ` R )
cply1coe0.b 
|- B = ( Base ` P )
cply1coe0.a 
|- A = ( algSc ` P )
Assertion cply1coe0 
|- ( ( R e. Ring /\ S e. K ) -> A. n e. NN ( ( coe1 ` ( A ` S ) ) ` n ) = .0. )

Proof

Step Hyp Ref Expression
1 cply1coe0.k 
 |-  K = ( Base ` R )
2 cply1coe0.0 
 |-  .0. = ( 0g ` R )
3 cply1coe0.p 
 |-  P = ( Poly1 ` R )
4 cply1coe0.b 
 |-  B = ( Base ` P )
5 cply1coe0.a 
 |-  A = ( algSc ` P )
6 3 5 1 2 coe1scl 
 |-  ( ( R e. Ring /\ S e. K ) -> ( coe1 ` ( A ` S ) ) = ( k e. NN0 |-> if ( k = 0 , S , .0. ) ) )
7 6 adantr 
 |-  ( ( ( R e. Ring /\ S e. K ) /\ n e. NN ) -> ( coe1 ` ( A ` S ) ) = ( k e. NN0 |-> if ( k = 0 , S , .0. ) ) )
8 nnne0 
 |-  ( n e. NN -> n =/= 0 )
9 8 neneqd 
 |-  ( n e. NN -> -. n = 0 )
10 9 adantl 
 |-  ( ( ( R e. Ring /\ S e. K ) /\ n e. NN ) -> -. n = 0 )
11 10 adantr 
 |-  ( ( ( ( R e. Ring /\ S e. K ) /\ n e. NN ) /\ k = n ) -> -. n = 0 )
12 eqeq1 
 |-  ( k = n -> ( k = 0 <-> n = 0 ) )
13 12 notbid 
 |-  ( k = n -> ( -. k = 0 <-> -. n = 0 ) )
14 13 adantl 
 |-  ( ( ( ( R e. Ring /\ S e. K ) /\ n e. NN ) /\ k = n ) -> ( -. k = 0 <-> -. n = 0 ) )
15 11 14 mpbird 
 |-  ( ( ( ( R e. Ring /\ S e. K ) /\ n e. NN ) /\ k = n ) -> -. k = 0 )
16 15 iffalsed 
 |-  ( ( ( ( R e. Ring /\ S e. K ) /\ n e. NN ) /\ k = n ) -> if ( k = 0 , S , .0. ) = .0. )
17 nnnn0 
 |-  ( n e. NN -> n e. NN0 )
18 17 adantl 
 |-  ( ( ( R e. Ring /\ S e. K ) /\ n e. NN ) -> n e. NN0 )
19 2 fvexi 
 |-  .0. e. _V
20 19 a1i 
 |-  ( ( ( R e. Ring /\ S e. K ) /\ n e. NN ) -> .0. e. _V )
21 7 16 18 20 fvmptd 
 |-  ( ( ( R e. Ring /\ S e. K ) /\ n e. NN ) -> ( ( coe1 ` ( A ` S ) ) ` n ) = .0. )
22 21 ralrimiva 
 |-  ( ( R e. Ring /\ S e. K ) -> A. n e. NN ( ( coe1 ` ( A ` S ) ) ` n ) = .0. )