Metamath Proof Explorer

Theorem mon1pval

Description: Value of the set of monic polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015)

Ref Expression
Hypotheses uc1pval.p 
|- P = ( Poly1 ` R )
uc1pval.b 
|- B = ( Base ` P )
uc1pval.z 
|- .0. = ( 0g ` P )
uc1pval.d 
|- D = ( deg1 ` R )
mon1pval.m 
|- M = ( Monic1p ` R )
mon1pval.o 
|- .1. = ( 1r ` R )
Assertion mon1pval 
|- M = { f e. B | ( f =/= .0. /\ ( ( coe1 ` f ) ` ( D ` f ) ) = .1. ) }

Proof

Step Hyp Ref Expression
1 uc1pval.p 
 |-  P = ( Poly1 ` R )
2 uc1pval.b 
 |-  B = ( Base ` P )
3 uc1pval.z 
 |-  .0. = ( 0g ` P )
4 uc1pval.d 
 |-  D = ( deg1 ` R )
5 mon1pval.m 
 |-  M = ( Monic1p ` R )
6 mon1pval.o 
 |-  .1. = ( 1r ` R )
7 fveq2 
 |-  ( r = R -> ( Poly1 ` r ) = ( Poly1 ` R ) )
8 7 1 eqtr4di 
 |-  ( r = R -> ( Poly1 ` r ) = P )
9 8 fveq2d 
 |-  ( r = R -> ( Base ` ( Poly1 ` r ) ) = ( Base ` P ) )
10 9 2 eqtr4di 
 |-  ( r = R -> ( Base ` ( Poly1 ` r ) ) = B )
11 8 fveq2d 
 |-  ( r = R -> ( 0g ` ( Poly1 ` r ) ) = ( 0g ` P ) )
12 11 3 eqtr4di 
 |-  ( r = R -> ( 0g ` ( Poly1 ` r ) ) = .0. )
13 12 neeq2d 
 |-  ( r = R -> ( f =/= ( 0g ` ( Poly1 ` r ) ) <-> f =/= .0. ) )
14 fveq2 
 |-  ( r = R -> ( deg1 ` r ) = ( deg1 ` R ) )
15 14 4 eqtr4di 
 |-  ( r = R -> ( deg1 ` r ) = D )
16 15 fveq1d 
 |-  ( r = R -> ( ( deg1 ` r ) ` f ) = ( D ` f ) )
17 16 fveq2d 
 |-  ( r = R -> ( ( coe1 ` f ) ` ( ( deg1 ` r ) ` f ) ) = ( ( coe1 ` f ) ` ( D ` f ) ) )
18 fveq2 
 |-  ( r = R -> ( 1r ` r ) = ( 1r ` R ) )
19 18 6 eqtr4di 
 |-  ( r = R -> ( 1r ` r ) = .1. )
20 17 19 eqeq12d 
 |-  ( r = R -> ( ( ( coe1 ` f ) ` ( ( deg1 ` r ) ` f ) ) = ( 1r ` r ) <-> ( ( coe1 ` f ) ` ( D ` f ) ) = .1. ) )
21 13 20 anbi12d 
 |-  ( r = R -> ( ( f =/= ( 0g ` ( Poly1 ` r ) ) /\ ( ( coe1 ` f ) ` ( ( deg1 ` r ) ` f ) ) = ( 1r ` r ) ) <-> ( f =/= .0. /\ ( ( coe1 ` f ) ` ( D ` f ) ) = .1. ) ) )
22 10 21 rabeqbidv 
 |-  ( r = R -> { f e. ( Base ` ( Poly1 ` r ) ) | ( f =/= ( 0g ` ( Poly1 ` r ) ) /\ ( ( coe1 ` f ) ` ( ( deg1 ` r ) ` f ) ) = ( 1r ` r ) ) } = { f e. B | ( f =/= .0. /\ ( ( coe1 ` f ) ` ( D ` f ) ) = .1. ) } )
23 df-mon1 
 |-  Monic1p = ( r e. _V |-> { f e. ( Base ` ( Poly1 ` r ) ) | ( f =/= ( 0g ` ( Poly1 ` r ) ) /\ ( ( coe1 ` f ) ` ( ( deg1 ` r ) ` f ) ) = ( 1r ` r ) ) } )
24 2 fvexi 
 |-  B e. _V
25 24 rabex 
 |-  { f e. B | ( f =/= .0. /\ ( ( coe1 ` f ) ` ( D ` f ) ) = .1. ) } e. _V
26 22 23 25 fvmpt 
 |-  ( R e. _V -> ( Monic1p ` R ) = { f e. B | ( f =/= .0. /\ ( ( coe1 ` f ) ` ( D ` f ) ) = .1. ) } )
27 fvprc 
 |-  ( -. R e. _V -> ( Monic1p ` R ) = (/) )
28 ssrab2 
 |-  { f e. B | ( f =/= .0. /\ ( ( coe1 ` f ) ` ( D ` f ) ) = .1. ) } C_ B
29 fvprc 
 |-  ( -. R e. _V -> ( Poly1 ` R ) = (/) )
30 1 29 syl5eq 
 |-  ( -. R e. _V -> P = (/) )
31 30 fveq2d 
 |-  ( -. R e. _V -> ( Base ` P ) = ( Base ` (/) ) )
32 2 31 syl5eq 
 |-  ( -. R e. _V -> B = ( Base ` (/) ) )
33 base0 
 |-  (/) = ( Base ` (/) )
34 32 33 eqtr4di 
 |-  ( -. R e. _V -> B = (/) )
35 28 34 sseqtrid 
 |-  ( -. R e. _V -> { f e. B | ( f =/= .0. /\ ( ( coe1 ` f ) ` ( D ` f ) ) = .1. ) } C_ (/) )
36 ss0 
 |-  ( { f e. B | ( f =/= .0. /\ ( ( coe1 ` f ) ` ( D ` f ) ) = .1. ) } C_ (/) -> { f e. B | ( f =/= .0. /\ ( ( coe1 ` f ) ` ( D ` f ) ) = .1. ) } = (/) )
37 35 36 syl 
 |-  ( -. R e. _V -> { f e. B | ( f =/= .0. /\ ( ( coe1 ` f ) ` ( D ` f ) ) = .1. ) } = (/) )
38 27 37 eqtr4d 
 |-  ( -. R e. _V -> ( Monic1p ` R ) = { f e. B | ( f =/= .0. /\ ( ( coe1 ` f ) ` ( D ` f ) ) = .1. ) } )
39 26 38 pm2.61i 
 |-  ( Monic1p ` R ) = { f e. B | ( f =/= .0. /\ ( ( coe1 ` f ) ` ( D ` f ) ) = .1. ) }
40 5 39 eqtri 
 |-  M = { f e. B | ( f =/= .0. /\ ( ( coe1 ` f ) ` ( D ` f ) ) = .1. ) }