Theorem 0oval

Description: Value of the zero operator. (Contributed by NM, 28-Nov-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	0oval.1	|- X = ( BaseSet ` U )
	0oval.6	|- Z = ( 0vec ` W )
	0oval.0	|- O = ( U 0op W )
Assertion	0oval	|- ( ( U e. NrmCVec /\ W e. NrmCVec /\ A e. X ) -> ( O ` A ) = 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	1 2 3	0ofval	|- ( ( U e. NrmCVec /\ W e. NrmCVec ) -> O = ( X X. { Z } ) )
5	4	fveq1d	|- ( ( U e. NrmCVec /\ W e. NrmCVec ) -> ( O ` A ) = ( ( X X. { Z } ) ` A ) )
6	5	3adant3	|- ( ( U e. NrmCVec /\ W e. NrmCVec /\ A e. X ) -> ( O ` A ) = ( ( X X. { Z } ) ` A ) )
7	2	fvexi	|- Z e. _V
8	7	fvconst2	|- ( A e. X -> ( ( X X. { Z } ) ` A ) = Z )
9	8	3ad2ant3	|- ( ( U e. NrmCVec /\ W e. NrmCVec /\ A e. X ) -> ( ( X X. { Z } ) ` A ) = Z )
10	6 9	eqtrd	|- ( ( U e. NrmCVec /\ W e. NrmCVec /\ A e. X ) -> ( O ` A ) = Z )