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 = ( BaseSet ` U )
Assertion nvo00 
|- ( ( U e. NrmCVec /\ T : X --> Y ) -> ( T = ( X X. { Z } ) <-> ran T = { Z } ) )

Proof

Step Hyp Ref Expression
1 nvo00.1 
 |-  X = ( BaseSet ` U )
2 ffn 
 |-  ( T : X --> Y -> T Fn X )
3 eqid 
 |-  ( 0vec ` U ) = ( 0vec ` U )
4 1 3 nvzcl 
 |-  ( U e. NrmCVec -> ( 0vec ` U ) e. X )
5 4 ne0d 
 |-  ( U e. NrmCVec -> X =/= (/) )
6 fconst5 
 |-  ( ( T Fn X /\ X =/= (/) ) -> ( T = ( X X. { Z } ) <-> ran T = { Z } ) )
7 2 5 6 syl2anr 
 |-  ( ( U e. NrmCVec /\ T : X --> Y ) -> ( T = ( X X. { Z } ) <-> ran T = { Z } ) )