This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \in ℂ \to 0_{𝑝} (A) = 0$

Step	Hyp	Ref	Expression
1		df-0p	$⊢ 0_{𝑝} = ℂ \times \{0\}$
2	1	fveq1i	$⊢ 0_{𝑝} (A) = (ℂ \times \{0\}) (A)$
3		c0ex	$⊢ 0 \in V$
4	3	fvconst2	$⊢ A \in ℂ \to (ℂ \times \{0\}) (A) = 0$
5	2 4	eqtrid	$⊢ A \in ℂ \to 0_{𝑝} (A) = 0$