Description: The zero function evaluates to zero at every point. (Contributed by Mario Carneiro, 23-Jul-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | 0pval | |- ( A e. CC -> ( 0p ` A ) = 0 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-0p | |- 0p = ( CC X. { 0 } ) |
|
2 | 1 | fveq1i | |- ( 0p ` A ) = ( ( CC X. { 0 } ) ` A ) |
3 | c0ex | |- 0 e. _V |
|
4 | 3 | fvconst2 | |- ( A e. CC -> ( ( CC X. { 0 } ) ` A ) = 0 ) |
5 | 2 4 | eqtrid | |- ( A e. CC -> ( 0p ` A ) = 0 ) |