Metamath Proof Explorer


Theorem 0pval

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 )

Proof

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 )