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 2 4 ply1bas 
 |-  B = ( Base ` ( 1o mPoly R ) )
10 psr1baslem 
 |-  ( NN0 ^m 1o ) = { c e. ( NN0 ^m 1o ) | ( `' c " NN ) e. Fin }
11 tdeglem2 
 |-  ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) = ( a e. ( NN0 ^m 1o ) |-> ( CCfld gsum a ) )
12 8 2 3 ply1mpl0 
 |-  .0. = ( 0g ` ( 1o mPoly R ) )
13 7 8 9 5 10 11 12 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 ) ) )
14 6 fvcoe1 
 |-  ( ( F e. B /\ b e. ( NN0 ^m 1o ) ) -> ( F ` b ) = ( A ` ( b ` (/) ) ) )
15 14 3ad2antl2 
 |-  ( ( ( R e. Ring /\ F e. B /\ F =/= .0. ) /\ b e. ( NN0 ^m 1o ) ) -> ( F ` b ) = ( A ` ( b ` (/) ) ) )
16 fveq1 
 |-  ( a = b -> ( a ` (/) ) = ( b ` (/) ) )
17 eqid 
 |-  ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) = ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) )
18 fvex 
 |-  ( b ` (/) ) e. _V
19 16 17 18 fvmpt 
 |-  ( b e. ( NN0 ^m 1o ) -> ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) = ( b ` (/) ) )
20 19 fveq2d 
 |-  ( b e. ( NN0 ^m 1o ) -> ( A ` ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) ) = ( A ` ( b ` (/) ) ) )
21 20 adantl 
 |-  ( ( ( R e. Ring /\ F e. B /\ F =/= .0. ) /\ b e. ( NN0 ^m 1o ) ) -> ( A ` ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) ) = ( A ` ( b ` (/) ) ) )
22 15 21 eqtr4d 
 |-  ( ( ( R e. Ring /\ F e. B /\ F =/= .0. ) /\ b e. ( NN0 ^m 1o ) ) -> ( F ` b ) = ( A ` ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) ) )
23 22 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 ) )
24 23 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 ) ) ) )
25 24 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 ) ) )
26 25 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 ) ) )
27 df1o2 
 |-  1o = { (/) }
28 nn0ex 
 |-  NN0 e. _V
29 0ex 
 |-  (/) e. _V
30 27 28 29 17 mapsnf1o2 
 |-  ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) : ( NN0 ^m 1o ) -1-1-onto-> NN0
31 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 )
32 eqeq1 
 |-  ( ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) = d -> ( ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) = ( D ` F ) <-> d = ( D ` F ) ) )
33 fveq2 
 |-  ( ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) = d -> ( A ` ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) ) = ( A ` d ) )
34 33 neeq1d 
 |-  ( ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) = d -> ( ( A ` ( ( a e. ( NN0 ^m 1o ) |-> ( a ` (/) ) ) ` b ) ) =/= Y <-> ( A ` d ) =/= Y ) )
35 32 34 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 ) ) )
36 35 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 ) ) )
37 30 31 36 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 ) )
38 26 37 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 ) ) )
39 1 2 3 4 deg1nn0cl 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= .0. ) -> ( D ` F ) e. NN0 )
40 fveq2 
 |-  ( d = ( D ` F ) -> ( A ` d ) = ( A ` ( D ` F ) ) )
41 40 neeq1d 
 |-  ( d = ( D ` F ) -> ( ( A ` d ) =/= Y <-> ( A ` ( D ` F ) ) =/= Y ) )
42 41 ceqsrexv 
 |-  ( ( D ` F ) e. NN0 -> ( E. d e. NN0 ( d = ( D ` F ) /\ ( A ` d ) =/= Y ) <-> ( A ` ( D ` F ) ) =/= Y ) )
43 39 42 syl 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= .0. ) -> ( E. d e. NN0 ( d = ( D ` F ) /\ ( A ` d ) =/= Y ) <-> ( A ` ( D ` F ) ) =/= Y ) )
44 38 43 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 ) )
45 13 44 mpbid 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= .0. ) -> ( A ` ( D ` F ) ) =/= Y )