Theorem 0ofval

Description: The zero operator between two normed complex vector spaces. (Contributed by NM, 28-Nov-2007) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	0oval.1	|- X = ( BaseSet ` U )
	0oval.6	|- Z = ( 0vec ` W )
	0oval.0	|- O = ( U 0op W )
Assertion	0ofval	|- ( ( U e. NrmCVec /\ W e. NrmCVec ) -> O = ( X X. { Z } ) )

Proof

Step	Hyp	Ref	Expression
1		0oval.1	|- X = ( BaseSet ` U )
2		0oval.6	|- Z = ( 0vec ` W )
3		0oval.0	|- O = ( U 0op W )
4		fveq2	|- ( u = U -> ( BaseSet ` u ) = ( BaseSet ` U ) )
5	4 1	eqtr4di	|- ( u = U -> ( BaseSet ` u ) = X )
6	5	xpeq1d	|- ( u = U -> ( ( BaseSet ` u ) X. { ( 0vec ` w ) } ) = ( X X. { ( 0vec ` w ) } ) )
7		fveq2	|- ( w = W -> ( 0vec ` w ) = ( 0vec ` W ) )
8	7 2	eqtr4di	|- ( w = W -> ( 0vec ` w ) = Z )
9	8	sneqd	|- ( w = W -> { ( 0vec ` w ) } = { Z } )
10	9	xpeq2d	|- ( w = W -> ( X X. { ( 0vec ` w ) } ) = ( X X. { Z } ) )
11		df-0o	|- 0op = ( u e. NrmCVec , w e. NrmCVec |-> ( ( BaseSet ` u ) X. { ( 0vec ` w ) } ) )
12	1	fvexi	|- X e. _V
13		snex	|- { Z } e. _V
14	12 13	xpex	|- ( X X. { Z } ) e. _V
15	6 10 11 14	ovmpo	|- ( ( U e. NrmCVec /\ W e. NrmCVec ) -> ( U 0op W ) = ( X X. { Z } ) )
16	3 15	syl5eq	|- ( ( U e. NrmCVec /\ W e. NrmCVec ) -> O = ( X X. { Z } ) )