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 )