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 )