# Metamath Proof Explorer

## 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}×\left\{{Z}\right\}↔\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 {T}Fn{X}$
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({T}Fn{X}\wedge {X}\ne \varnothing \right)\to \left({T}={X}×\left\{{Z}\right\}↔\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}×\left\{{Z}\right\}↔\mathrm{ran}{T}=\left\{{Z}\right\}\right)$