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 )