Metamath Proof Explorer

Theorem uc1pval

Description: Value of the set of unitic 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 )
uc1pval.c 
|- C = ( Unic1p ` R )
uc1pval.u 
|- U = ( Unit ` R )
Assertion uc1pval 
|- C = { f e. B | ( f =/= .0. /\ ( ( coe1 ` f ) ` ( D ` f ) ) e. U ) }

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 uc1pval.c 
 |-  C = ( Unic1p ` R )
6 uc1pval.u 
 |-  U = ( Unit ` 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 -> ( Unit ` r ) = ( Unit ` R ) )
19 18 6 eqtr4di 
 |-  ( r = R -> ( Unit ` r ) = U )
20 17 19 eleq12d 
 |-  ( r = R -> ( ( ( coe1 ` f ) ` ( ( deg1 ` r ) ` f ) ) e. ( Unit ` r ) <-> ( ( coe1 ` f ) ` ( D ` f ) ) e. U ) )
21 13 20 anbi12d 
 |-  ( r = R -> ( ( f =/= ( 0g ` ( Poly1 ` r ) ) /\ ( ( coe1 ` f ) ` ( ( deg1 ` r ) ` f ) ) e. ( Unit ` r ) ) <-> ( f =/= .0. /\ ( ( coe1 ` f ) ` ( D ` f ) ) e. U ) ) )
22 10 21 rabeqbidv 
 |-  ( r = R -> { f e. ( Base ` ( Poly1 ` r ) ) | ( f =/= ( 0g ` ( Poly1 ` r ) ) /\ ( ( coe1 ` f ) ` ( ( deg1 ` r ) ` f ) ) e. ( Unit ` r ) ) } = { f e. B | ( f =/= .0. /\ ( ( coe1 ` f ) ` ( D ` f ) ) e. U ) } )
23 df-uc1p 
 |-  Unic1p = ( r e. _V |-> { f e. ( Base ` ( Poly1 ` r ) ) | ( f =/= ( 0g ` ( Poly1 ` r ) ) /\ ( ( coe1 ` f ) ` ( ( deg1 ` r ) ` f ) ) e. ( Unit ` r ) ) } )
24 2 fvexi 
 |-  B e. _V
25 24 rabex 
 |-  { f e. B | ( f =/= .0. /\ ( ( coe1 ` f ) ` ( D ` f ) ) e. U ) } e. _V
26 22 23 25 fvmpt 
 |-  ( R e. _V -> ( Unic1p ` R ) = { f e. B | ( f =/= .0. /\ ( ( coe1 ` f ) ` ( D ` f ) ) e. U ) } )
27 fvprc 
 |-  ( -. R e. _V -> ( Unic1p ` R ) = (/) )
28 ssrab2 
 |-  { f e. B | ( f =/= .0. /\ ( ( coe1 ` f ) ` ( D ` f ) ) e. U ) } 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 base0 
 |-  (/) = ( Base ` (/) )
33 31 32 eqtr4di 
 |-  ( -. R e. _V -> ( Base ` P ) = (/) )
34 2 33 syl5eq 
 |-  ( -. R e. _V -> B = (/) )
35 28 34 sseqtrid 
 |-  ( -. R e. _V -> { f e. B | ( f =/= .0. /\ ( ( coe1 ` f ) ` ( D ` f ) ) e. U ) } C_ (/) )
36 ss0 
 |-  ( { f e. B | ( f =/= .0. /\ ( ( coe1 ` f ) ` ( D ` f ) ) e. U ) } C_ (/) -> { f e. B | ( f =/= .0. /\ ( ( coe1 ` f ) ` ( D ` f ) ) e. U ) } = (/) )
37 35 36 syl 
 |-  ( -. R e. _V -> { f e. B | ( f =/= .0. /\ ( ( coe1 ` f ) ` ( D ` f ) ) e. U ) } = (/) )
38 27 37 eqtr4d 
 |-  ( -. R e. _V -> ( Unic1p ` R ) = { f e. B | ( f =/= .0. /\ ( ( coe1 ` f ) ` ( D ` f ) ) e. U ) } )
39 26 38 pm2.61i 
 |-  ( Unic1p ` R ) = { f e. B | ( f =/= .0. /\ ( ( coe1 ` f ) ` ( D ` f ) ) e. U ) }
40 5 39 eqtri 
 |-  C = { f e. B | ( f =/= .0. /\ ( ( coe1 ` f ) ` ( D ` f ) ) e. U ) }