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

Metamath Proof Explorer

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 eqtrid 
 |-  ( ( U e. NrmCVec /\ W e. NrmCVec ) -> O = ( X X. { Z } ) )