Theorem 0pval

Description: The zero function evaluates to zero at every point. (Contributed by Mario Carneiro, 23-Jul-2014)

	Ref	Expression
Assertion	0pval	⊢ ( 𝐴 ∈ ℂ → ( 0𝑝 ‘ 𝐴 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		df-0p	⊢ 0𝑝 = ( ℂ × { 0 } )
2	1	fveq1i	⊢ ( 0𝑝 ‘ 𝐴 ) = ( ( ℂ × { 0 } ) ‘ 𝐴 )
3		c0ex	⊢ 0 ∈ V
4	3	fvconst2	⊢ ( 𝐴 ∈ ℂ → ( ( ℂ × { 0 } ) ‘ 𝐴 ) = 0 )
5	2 4	eqtrid	⊢ ( 𝐴 ∈ ℂ → ( 0𝑝 ‘ 𝐴 ) = 0 )