Theorem nvo00

Description: Two ways to express a zero operator. (Contributed by NM, 27-Nov-2007) (New usage is discouraged.)

	Ref	Expression
Hypothesis	nvo00.1	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
Assertion	nvo00	$$⊢\left(U\in \mathrm{NrmCVec}\wedge T:X⟶Y\right)\to \left(T=X\times \left\{Z\right\}\leftrightarrow \mathrm{ran}T=\left\{Z\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		nvo00.1	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
2		ffn	$$⊢T:X⟶Y\to TFnX$$
3		eqid	$$⊢0_{\mathrm{vec}}\left(U\right)=0_{\mathrm{vec}}\left(U\right)$$
4	1 3	nvzcl	$$⊢U\in \mathrm{NrmCVec}\to 0_{\mathrm{vec}}\left(U\right)\in X$$
5	4	ne0d	$$⊢U\in \mathrm{NrmCVec}\to X\ne \varnothing$$
6		fconst5	$$⊢\left(TFnX\wedge X\ne \varnothing \right)\to \left(T=X\times \left\{Z\right\}\leftrightarrow \mathrm{ran}T=\left\{Z\right\}\right)$$
7	2 5 6	syl2anr	$$⊢\left(U\in \mathrm{NrmCVec}\wedge T:X⟶Y\right)\to \left(T=X\times \left\{Z\right\}\leftrightarrow \mathrm{ran}T=\left\{Z\right\}\right)$$