Metamath Proof Explorer

Theorem cply1coe0bi

Description: A polynomial is constant (i.e. a "lifted scalar") iff all but the first coefficient 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 cply1coe0bi 
|- ( ( R e. Ring /\ M e. B ) -> ( E. s e. K M = ( A ` s ) <-> A. n e. NN ( ( coe1 ` M ) ` 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 1 2 3 4 5 cply1coe0 
 |-  ( ( R e. Ring /\ s e. K ) -> A. n e. NN ( ( coe1 ` ( A ` s ) ) ` n ) = .0. )
7 6 ad4ant13 
 |-  ( ( ( ( R e. Ring /\ M e. B ) /\ s e. K ) /\ M = ( A ` s ) ) -> A. n e. NN ( ( coe1 ` ( A ` s ) ) ` n ) = .0. )
8 fveq2 
 |-  ( M = ( A ` s ) -> ( coe1 ` M ) = ( coe1 ` ( A ` s ) ) )
9 8 fveq1d 
 |-  ( M = ( A ` s ) -> ( ( coe1 ` M ) ` n ) = ( ( coe1 ` ( A ` s ) ) ` n ) )
10 9 eqeq1d 
 |-  ( M = ( A ` s ) -> ( ( ( coe1 ` M ) ` n ) = .0. <-> ( ( coe1 ` ( A ` s ) ) ` n ) = .0. ) )
11 10 ralbidv 
 |-  ( M = ( A ` s ) -> ( A. n e. NN ( ( coe1 ` M ) ` n ) = .0. <-> A. n e. NN ( ( coe1 ` ( A ` s ) ) ` n ) = .0. ) )
12 11 adantl 
 |-  ( ( ( ( R e. Ring /\ M e. B ) /\ s e. K ) /\ M = ( A ` s ) ) -> ( A. n e. NN ( ( coe1 ` M ) ` n ) = .0. <-> A. n e. NN ( ( coe1 ` ( A ` s ) ) ` n ) = .0. ) )
13 7 12 mpbird 
 |-  ( ( ( ( R e. Ring /\ M e. B ) /\ s e. K ) /\ M = ( A ` s ) ) -> A. n e. NN ( ( coe1 ` M ) ` n ) = .0. )
14 13 rexlimdva2 
 |-  ( ( R e. Ring /\ M e. B ) -> ( E. s e. K M = ( A ` s ) -> A. n e. NN ( ( coe1 ` M ) ` n ) = .0. ) )
15 simpr 
 |-  ( ( R e. Ring /\ M e. B ) -> M e. B )
16 0nn0 
 |-  0 e. NN0
17 eqid 
 |-  ( coe1 ` M ) = ( coe1 ` M )
18 17 4 3 1 coe1fvalcl 
 |-  ( ( M e. B /\ 0 e. NN0 ) -> ( ( coe1 ` M ) ` 0 ) e. K )
19 15 16 18 sylancl 
 |-  ( ( R e. Ring /\ M e. B ) -> ( ( coe1 ` M ) ` 0 ) e. K )
20 19 adantr 
 |-  ( ( ( R e. Ring /\ M e. B ) /\ A. n e. NN ( ( coe1 ` M ) ` n ) = .0. ) -> ( ( coe1 ` M ) ` 0 ) e. K )
21 fveq2 
 |-  ( s = ( ( coe1 ` M ) ` 0 ) -> ( A ` s ) = ( A ` ( ( coe1 ` M ) ` 0 ) ) )
22 21 eqeq2d 
 |-  ( s = ( ( coe1 ` M ) ` 0 ) -> ( M = ( A ` s ) <-> M = ( A ` ( ( coe1 ` M ) ` 0 ) ) ) )
23 22 adantl 
 |-  ( ( ( ( R e. Ring /\ M e. B ) /\ A. n e. NN ( ( coe1 ` M ) ` n ) = .0. ) /\ s = ( ( coe1 ` M ) ` 0 ) ) -> ( M = ( A ` s ) <-> M = ( A ` ( ( coe1 ` M ) ` 0 ) ) ) )
24 simpl 
 |-  ( ( R e. Ring /\ M e. B ) -> R e. Ring )
25 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
26 3 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
27 3 ply1lmod 
 |-  ( R e. Ring -> P e. LMod )
28 eqid 
 |-  ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) )
29 5 25 26 27 28 4 asclf 
 |-  ( R e. Ring -> A : ( Base ` ( Scalar ` P ) ) --> B )
30 29 adantr 
 |-  ( ( R e. Ring /\ M e. B ) -> A : ( Base ` ( Scalar ` P ) ) --> B )
31 eqid 
 |-  ( Base ` R ) = ( Base ` R )
32 17 4 3 31 coe1fvalcl 
 |-  ( ( M e. B /\ 0 e. NN0 ) -> ( ( coe1 ` M ) ` 0 ) e. ( Base ` R ) )
33 15 16 32 sylancl 
 |-  ( ( R e. Ring /\ M e. B ) -> ( ( coe1 ` M ) ` 0 ) e. ( Base ` R ) )
34 3 ply1sca 
 |-  ( R e. Ring -> R = ( Scalar ` P ) )
35 34 eqcomd 
 |-  ( R e. Ring -> ( Scalar ` P ) = R )
36 35 fveq2d 
 |-  ( R e. Ring -> ( Base ` ( Scalar ` P ) ) = ( Base ` R ) )
37 36 adantr 
 |-  ( ( R e. Ring /\ M e. B ) -> ( Base ` ( Scalar ` P ) ) = ( Base ` R ) )
38 33 37 eleqtrrd 
 |-  ( ( R e. Ring /\ M e. B ) -> ( ( coe1 ` M ) ` 0 ) e. ( Base ` ( Scalar ` P ) ) )
39 30 38 ffvelrnd 
 |-  ( ( R e. Ring /\ M e. B ) -> ( A ` ( ( coe1 ` M ) ` 0 ) ) e. B )
40 24 15 39 3jca 
 |-  ( ( R e. Ring /\ M e. B ) -> ( R e. Ring /\ M e. B /\ ( A ` ( ( coe1 ` M ) ` 0 ) ) e. B ) )
41 40 adantr 
 |-  ( ( ( R e. Ring /\ M e. B ) /\ A. n e. NN ( ( coe1 ` M ) ` n ) = .0. ) -> ( R e. Ring /\ M e. B /\ ( A ` ( ( coe1 ` M ) ` 0 ) ) e. B ) )
42 simpr 
 |-  ( ( ( ( R e. Ring /\ M e. B ) /\ n e. NN ) /\ ( ( coe1 ` M ) ` n ) = .0. ) -> ( ( coe1 ` M ) ` n ) = .0. )
43 3 5 1 2 coe1scl 
 |-  ( ( R e. Ring /\ ( ( coe1 ` M ) ` 0 ) e. K ) -> ( coe1 ` ( A ` ( ( coe1 ` M ) ` 0 ) ) ) = ( k e. NN0 |-> if ( k = 0 , ( ( coe1 ` M ) ` 0 ) , .0. ) ) )
44 19 43 syldan 
 |-  ( ( R e. Ring /\ M e. B ) -> ( coe1 ` ( A ` ( ( coe1 ` M ) ` 0 ) ) ) = ( k e. NN0 |-> if ( k = 0 , ( ( coe1 ` M ) ` 0 ) , .0. ) ) )
45 44 adantr 
 |-  ( ( ( R e. Ring /\ M e. B ) /\ n e. NN ) -> ( coe1 ` ( A ` ( ( coe1 ` M ) ` 0 ) ) ) = ( k e. NN0 |-> if ( k = 0 , ( ( coe1 ` M ) ` 0 ) , .0. ) ) )
46 nnne0 
 |-  ( n e. NN -> n =/= 0 )
47 46 neneqd 
 |-  ( n e. NN -> -. n = 0 )
48 47 adantl 
 |-  ( ( ( R e. Ring /\ M e. B ) /\ n e. NN ) -> -. n = 0 )
49 48 adantr 
 |-  ( ( ( ( R e. Ring /\ M e. B ) /\ n e. NN ) /\ k = n ) -> -. n = 0 )
50 eqeq1 
 |-  ( k = n -> ( k = 0 <-> n = 0 ) )
51 50 notbid 
 |-  ( k = n -> ( -. k = 0 <-> -. n = 0 ) )
52 51 adantl 
 |-  ( ( ( ( R e. Ring /\ M e. B ) /\ n e. NN ) /\ k = n ) -> ( -. k = 0 <-> -. n = 0 ) )
53 49 52 mpbird 
 |-  ( ( ( ( R e. Ring /\ M e. B ) /\ n e. NN ) /\ k = n ) -> -. k = 0 )
54 53 iffalsed 
 |-  ( ( ( ( R e. Ring /\ M e. B ) /\ n e. NN ) /\ k = n ) -> if ( k = 0 , ( ( coe1 ` M ) ` 0 ) , .0. ) = .0. )
55 nnnn0 
 |-  ( n e. NN -> n e. NN0 )
56 55 adantl 
 |-  ( ( ( R e. Ring /\ M e. B ) /\ n e. NN ) -> n e. NN0 )
57 2 fvexi 
 |-  .0. e. _V
58 57 a1i 
 |-  ( ( ( R e. Ring /\ M e. B ) /\ n e. NN ) -> .0. e. _V )
59 45 54 56 58 fvmptd 
 |-  ( ( ( R e. Ring /\ M e. B ) /\ n e. NN ) -> ( ( coe1 ` ( A ` ( ( coe1 ` M ) ` 0 ) ) ) ` n ) = .0. )
60 59 eqcomd 
 |-  ( ( ( R e. Ring /\ M e. B ) /\ n e. NN ) -> .0. = ( ( coe1 ` ( A ` ( ( coe1 ` M ) ` 0 ) ) ) ` n ) )
61 60 adantr 
 |-  ( ( ( ( R e. Ring /\ M e. B ) /\ n e. NN ) /\ ( ( coe1 ` M ) ` n ) = .0. ) -> .0. = ( ( coe1 ` ( A ` ( ( coe1 ` M ) ` 0 ) ) ) ` n ) )
62 42 61 eqtrd 
 |-  ( ( ( ( R e. Ring /\ M e. B ) /\ n e. NN ) /\ ( ( coe1 ` M ) ` n ) = .0. ) -> ( ( coe1 ` M ) ` n ) = ( ( coe1 ` ( A ` ( ( coe1 ` M ) ` 0 ) ) ) ` n ) )
63 62 ex 
 |-  ( ( ( R e. Ring /\ M e. B ) /\ n e. NN ) -> ( ( ( coe1 ` M ) ` n ) = .0. -> ( ( coe1 ` M ) ` n ) = ( ( coe1 ` ( A ` ( ( coe1 ` M ) ` 0 ) ) ) ` n ) ) )
64 63 ralimdva 
 |-  ( ( R e. Ring /\ M e. B ) -> ( A. n e. NN ( ( coe1 ` M ) ` n ) = .0. -> A. n e. NN ( ( coe1 ` M ) ` n ) = ( ( coe1 ` ( A ` ( ( coe1 ` M ) ` 0 ) ) ) ` n ) ) )
65 64 imp 
 |-  ( ( ( R e. Ring /\ M e. B ) /\ A. n e. NN ( ( coe1 ` M ) ` n ) = .0. ) -> A. n e. NN ( ( coe1 ` M ) ` n ) = ( ( coe1 ` ( A ` ( ( coe1 ` M ) ` 0 ) ) ) ` n ) )
66 3 5 1 ply1sclid 
 |-  ( ( R e. Ring /\ ( ( coe1 ` M ) ` 0 ) e. K ) -> ( ( coe1 ` M ) ` 0 ) = ( ( coe1 ` ( A ` ( ( coe1 ` M ) ` 0 ) ) ) ` 0 ) )
67 19 66 syldan 
 |-  ( ( R e. Ring /\ M e. B ) -> ( ( coe1 ` M ) ` 0 ) = ( ( coe1 ` ( A ` ( ( coe1 ` M ) ` 0 ) ) ) ` 0 ) )
68 67 adantr 
 |-  ( ( ( R e. Ring /\ M e. B ) /\ A. n e. NN ( ( coe1 ` M ) ` n ) = .0. ) -> ( ( coe1 ` M ) ` 0 ) = ( ( coe1 ` ( A ` ( ( coe1 ` M ) ` 0 ) ) ) ` 0 ) )
69 df-n0 
 |-  NN0 = ( NN u. { 0 } )
70 69 raleqi 
 |-  ( A. n e. NN0 ( ( coe1 ` M ) ` n ) = ( ( coe1 ` ( A ` ( ( coe1 ` M ) ` 0 ) ) ) ` n ) <-> A. n e. ( NN u. { 0 } ) ( ( coe1 ` M ) ` n ) = ( ( coe1 ` ( A ` ( ( coe1 ` M ) ` 0 ) ) ) ` n ) )
71 c0ex 
 |-  0 e. _V
72 fveq2 
 |-  ( n = 0 -> ( ( coe1 ` M ) ` n ) = ( ( coe1 ` M ) ` 0 ) )
73 fveq2 
 |-  ( n = 0 -> ( ( coe1 ` ( A ` ( ( coe1 ` M ) ` 0 ) ) ) ` n ) = ( ( coe1 ` ( A ` ( ( coe1 ` M ) ` 0 ) ) ) ` 0 ) )
74 72 73 eqeq12d 
 |-  ( n = 0 -> ( ( ( coe1 ` M ) ` n ) = ( ( coe1 ` ( A ` ( ( coe1 ` M ) ` 0 ) ) ) ` n ) <-> ( ( coe1 ` M ) ` 0 ) = ( ( coe1 ` ( A ` ( ( coe1 ` M ) ` 0 ) ) ) ` 0 ) ) )
75 74 ralunsn 
 |-  ( 0 e. _V -> ( A. n e. ( NN u. { 0 } ) ( ( coe1 ` M ) ` n ) = ( ( coe1 ` ( A ` ( ( coe1 ` M ) ` 0 ) ) ) ` n ) <-> ( A. n e. NN ( ( coe1 ` M ) ` n ) = ( ( coe1 ` ( A ` ( ( coe1 ` M ) ` 0 ) ) ) ` n ) /\ ( ( coe1 ` M ) ` 0 ) = ( ( coe1 ` ( A ` ( ( coe1 ` M ) ` 0 ) ) ) ` 0 ) ) ) )
76 71 75 mp1i 
 |-  ( ( ( R e. Ring /\ M e. B ) /\ A. n e. NN ( ( coe1 ` M ) ` n ) = .0. ) -> ( A. n e. ( NN u. { 0 } ) ( ( coe1 ` M ) ` n ) = ( ( coe1 ` ( A ` ( ( coe1 ` M ) ` 0 ) ) ) ` n ) <-> ( A. n e. NN ( ( coe1 ` M ) ` n ) = ( ( coe1 ` ( A ` ( ( coe1 ` M ) ` 0 ) ) ) ` n ) /\ ( ( coe1 ` M ) ` 0 ) = ( ( coe1 ` ( A ` ( ( coe1 ` M ) ` 0 ) ) ) ` 0 ) ) ) )
77 70 76 syl5bb 
 |-  ( ( ( R e. Ring /\ M e. B ) /\ A. n e. NN ( ( coe1 ` M ) ` n ) = .0. ) -> ( A. n e. NN0 ( ( coe1 ` M ) ` n ) = ( ( coe1 ` ( A ` ( ( coe1 ` M ) ` 0 ) ) ) ` n ) <-> ( A. n e. NN ( ( coe1 ` M ) ` n ) = ( ( coe1 ` ( A ` ( ( coe1 ` M ) ` 0 ) ) ) ` n ) /\ ( ( coe1 ` M ) ` 0 ) = ( ( coe1 ` ( A ` ( ( coe1 ` M ) ` 0 ) ) ) ` 0 ) ) ) )
78 65 68 77 mpbir2and 
 |-  ( ( ( R e. Ring /\ M e. B ) /\ A. n e. NN ( ( coe1 ` M ) ` n ) = .0. ) -> A. n e. NN0 ( ( coe1 ` M ) ` n ) = ( ( coe1 ` ( A ` ( ( coe1 ` M ) ` 0 ) ) ) ` n ) )
79 eqid 
 |-  ( coe1 ` ( A ` ( ( coe1 ` M ) ` 0 ) ) ) = ( coe1 ` ( A ` ( ( coe1 ` M ) ` 0 ) ) )
80 3 4 17 79 eqcoe1ply1eq 
 |-  ( ( R e. Ring /\ M e. B /\ ( A ` ( ( coe1 ` M ) ` 0 ) ) e. B ) -> ( A. n e. NN0 ( ( coe1 ` M ) ` n ) = ( ( coe1 ` ( A ` ( ( coe1 ` M ) ` 0 ) ) ) ` n ) -> M = ( A ` ( ( coe1 ` M ) ` 0 ) ) ) )
81 41 78 80 sylc 
 |-  ( ( ( R e. Ring /\ M e. B ) /\ A. n e. NN ( ( coe1 ` M ) ` n ) = .0. ) -> M = ( A ` ( ( coe1 ` M ) ` 0 ) ) )
82 20 23 81 rspcedvd 
 |-  ( ( ( R e. Ring /\ M e. B ) /\ A. n e. NN ( ( coe1 ` M ) ` n ) = .0. ) -> E. s e. K M = ( A ` s ) )
83 82 ex 
 |-  ( ( R e. Ring /\ M e. B ) -> ( A. n e. NN ( ( coe1 ` M ) ` n ) = .0. -> E. s e. K M = ( A ` s ) ) )
84 14 83 impbid 
 |-  ( ( R e. Ring /\ M e. B ) -> ( E. s e. K M = ( A ` s ) <-> A. n e. NN ( ( coe1 ` M ) ` n ) = .0. ) )