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

Metamath Proof Explorer

Theorem 0oo

Description: The zero operator is an operator. (Contributed by NM, 28-Nov-2007) (New usage is discouraged.)

Ref Expression
Hypotheses 0oo.1 
|- X = ( BaseSet ` U )
0oo.2 
|- Y = ( BaseSet ` W )
0oo.0 
|- Z = ( U 0op W )
Assertion 0oo 
|- ( ( U e. NrmCVec /\ W e. NrmCVec ) -> Z : X --> Y )

Proof

Step Hyp Ref Expression
1 0oo.1 
 |-  X = ( BaseSet ` U )
2 0oo.2 
 |-  Y = ( BaseSet ` W )
3 0oo.0 
 |-  Z = ( U 0op W )
4 fvex 
 |-  ( 0vec ` W ) e. _V
5 4 fconst 
 |-  ( X X. { ( 0vec ` W ) } ) : X --> { ( 0vec ` W ) }
6 eqid 
 |-  ( 0vec ` W ) = ( 0vec ` W )
7 2 6 nvzcl 
 |-  ( W e. NrmCVec -> ( 0vec ` W ) e. Y )
8 7 snssd 
 |-  ( W e. NrmCVec -> { ( 0vec ` W ) } C_ Y )
9 fss 
 |-  ( ( ( X X. { ( 0vec ` W ) } ) : X --> { ( 0vec ` W ) } /\ { ( 0vec ` W ) } C_ Y ) -> ( X X. { ( 0vec ` W ) } ) : X --> Y )
10 5 8 9 sylancr 
 |-  ( W e. NrmCVec -> ( X X. { ( 0vec ` W ) } ) : X --> Y )
11 10 adantl 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec ) -> ( X X. { ( 0vec ` W ) } ) : X --> Y )
12 1 6 3 0ofval 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec ) -> Z = ( X X. { ( 0vec ` W ) } ) )
13 12 feq1d 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec ) -> ( Z : X --> Y <-> ( X X. { ( 0vec ` W ) } ) : X --> Y ) )
14 11 13 mpbird 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec ) -> Z : X --> Y )