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

Metamath Proof Explorer

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 )