Metamath Proof Explorer

Theorem deg1ldg

Description: A nonzero univariate polynomial always has a nonzero leading coefficient. (Contributed by Stefan O'Rear, 23-Mar-2015)

Ref Expression
Hypotheses deg1z.d 
|- D = ( deg1 ` R )
deg1z.p 
|- P = ( Poly1 ` R )
deg1z.z 
|- .0. = ( 0g ` P )
deg1nn0cl.b 
|- B = ( Base ` P )
deg1ldg.y 
|- Y = ( 0g ` R )
deg1ldg.a 
|- A = ( coe1 ` F )
Assertion deg1ldg 
|- ( ( R e. Ring /\ F e. B /\ F =/= .0. ) -> ( A ` ( D ` F ) ) =/= Y )

Proof

Step Hyp Ref Expression
1 deg1z.d 
 |-  D = ( deg1 ` R )
2 deg1z.p 
 |-  P = ( Poly1 ` R )
3 deg1z.z 
 |-  .0. = ( 0g ` P )
4 deg1nn0cl.b 
 |-  B = ( Base ` P )
5 deg1ldg.y 
 |-  Y = ( 0g ` R )
6 deg1ldg.a 
 |-  A = ( coe1 ` F )
7 1 deg1fval 
 |-  D = ( 1o mDeg R )
8 eqid 
 |-  ( 1o mPoly R ) = ( 1o mPoly R )
9 eqid 
 |-  ( PwSer1 ` R ) = ( PwSer1 ` R )
10 2 9 4 ply1bas 
 |-  B = ( Base ` ( 1o mPoly R ) )
11 psr1baslem 
 |-  ( NN0 ^m 1o ) = { c e. ( NN0 ^m 1o ) | ( `' c " NN ) e. Fin }
12 tdeglem2 
 |-  ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) = ( a e. ( NN0 ^m 1o ) |-> ( CCfld gsum a ) )
13 8 2 3 ply1mpl0 
 |-  .0. = ( 0g ` ( 1o mPoly R ) )
14 7 8 10 5 11 12 13 mdegldg 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= .0. ) -> E. b e. ( NN0 ^m 1o ) ( ( F ` b ) =/= Y /\ ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) = ( D ` F ) ) )
15 6 fvcoe1 
 |-  ( ( F e. B /\ b e. ( NN0 ^m 1o ) ) -> ( F ` b ) = ( A ` ( b ` (/) ) ) )
16 15 3ad2antl2 
 |-  ( ( ( R e. Ring /\ F e. B /\ F =/= .0. ) /\ b e. ( NN0 ^m 1o ) ) -> ( F ` b ) = ( A ` ( b ` (/) ) ) )
17 fveq1 
 |-  ( a = b -> ( a ` (/) ) = ( b ` (/) ) )
18 eqid 
 |-  ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) = ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) )
19 fvex 
 |-  ( b ` (/) ) e. _V
20 17 18 19 fvmpt 
 |-  ( b e. ( NN0 ^m 1o ) -> ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) = ( b ` (/) ) )
21 20 fveq2d 
 |-  ( b e. ( NN0 ^m 1o ) -> ( A ` ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) ) = ( A ` ( b ` (/) ) ) )
22 21 adantl 
 |-  ( ( ( R e. Ring /\ F e. B /\ F =/= .0. ) /\ b e. ( NN0 ^m 1o ) ) -> ( A ` ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) ) = ( A ` ( b ` (/) ) ) )
23 16 22 eqtr4d 
 |-  ( ( ( R e. Ring /\ F e. B /\ F =/= .0. ) /\ b e. ( NN0 ^m 1o ) ) -> ( F ` b ) = ( A ` ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) ) )
24 23 neeq1d 
 |-  ( ( ( R e. Ring /\ F e. B /\ F =/= .0. ) /\ b e. ( NN0 ^m 1o ) ) -> ( ( F ` b ) =/= Y <-> ( A ` ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) ) =/= Y ) )
25 24 anbi1d 
 |-  ( ( ( R e. Ring /\ F e. B /\ F =/= .0. ) /\ b e. ( NN0 ^m 1o ) ) -> ( ( ( F ` b ) =/= Y /\ ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) = ( D ` F ) ) <-> ( ( A ` ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) ) =/= Y /\ ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) = ( D ` F ) ) ) )
26 25 biancomd 
 |-  ( ( ( R e. Ring /\ F e. B /\ F =/= .0. ) /\ b e. ( NN0 ^m 1o ) ) -> ( ( ( F ` b ) =/= Y /\ ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) = ( D ` F ) ) <-> ( ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) = ( D ` F ) /\ ( A ` ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) ) =/= Y ) ) )
27 26 rexbidva 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= .0. ) -> ( E. b e. ( NN0 ^m 1o ) ( ( F ` b ) =/= Y /\ ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) = ( D ` F ) ) <-> E. b e. ( NN0 ^m 1o ) ( ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) = ( D ` F ) /\ ( A ` ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) ) =/= Y ) ) )
28 df1o2 
 |-  1o = { (/) }
29 nn0ex 
 |-  NN0 e. _V
30 0ex 
 |-  (/) e. _V
31 28 29 30 18 mapsnf1o2 
 |-  ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) : ( NN0 ^m 1o ) -1-1-onto-> NN0
32 f1ofo 
 |-  ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) : ( NN0 ^m 1o ) -1-1-onto-> NN0 -> ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) : ( NN0 ^m 1o ) -onto-> NN0 )
33 eqeq1 
 |-  ( ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) = d -> ( ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) = ( D ` F ) <-> d = ( D ` F ) ) )
34 fveq2 
 |-  ( ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) = d -> ( A ` ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) ) = ( A ` d ) )
35 34 neeq1d 
 |-  ( ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) = d -> ( ( A ` ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) ) =/= Y <-> ( A ` d ) =/= Y ) )
36 33 35 anbi12d 
 |-  ( ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) = d -> ( ( ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) = ( D ` F ) /\ ( A ` ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) ) =/= Y ) <-> ( d = ( D ` F ) /\ ( A ` d ) =/= Y ) ) )
37 36 cbvexfo 
 |-  ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) : ( NN0 ^m 1o ) -onto-> NN0 -> ( E. b e. ( NN0 ^m 1o ) ( ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) = ( D ` F ) /\ ( A ` ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) ) =/= Y ) <-> E. d e. NN0 ( d = ( D ` F ) /\ ( A ` d ) =/= Y ) ) )
38 31 32 37 mp2b 
 |-  ( E. b e. ( NN0 ^m 1o ) ( ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) = ( D ` F ) /\ ( A ` ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) ) =/= Y ) <-> E. d e. NN0 ( d = ( D ` F ) /\ ( A ` d ) =/= Y ) )
39 27 38 bitrdi 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= .0. ) -> ( E. b e. ( NN0 ^m 1o ) ( ( F ` b ) =/= Y /\ ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) = ( D ` F ) ) <-> E. d e. NN0 ( d = ( D ` F ) /\ ( A ` d ) =/= Y ) ) )
40 1 2 3 4 deg1nn0cl 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= .0. ) -> ( D ` F ) e. NN0 )
41 fveq2 
 |-  ( d = ( D ` F ) -> ( A ` d ) = ( A ` ( D ` F ) ) )
42 41 neeq1d 
 |-  ( d = ( D ` F ) -> ( ( A ` d ) =/= Y <-> ( A ` ( D ` F ) ) =/= Y ) )
43 42 ceqsrexv 
 |-  ( ( D ` F ) e. NN0 -> ( E. d e. NN0 ( d = ( D ` F ) /\ ( A ` d ) =/= Y ) <-> ( A ` ( D ` F ) ) =/= Y ) )
44 40 43 syl 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= .0. ) -> ( E. d e. NN0 ( d = ( D ` F ) /\ ( A ` d ) =/= Y ) <-> ( A ` ( D ` F ) ) =/= Y ) )
45 39 44 bitrd 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= .0. ) -> ( E. b e. ( NN0 ^m 1o ) ( ( F ` b ) =/= Y /\ ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) = ( D ` F ) ) <-> ( A ` ( D ` F ) ) =/= Y ) )
46 14 45 mpbid 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= .0. ) -> ( A ` ( D ` F ) ) =/= Y )