Metamath Proof Explorer

Theorem ajfun

Description: The adjoint function is a function. This is not immediately apparent from df-aj but results from the uniqueness shown by ajmoi . (Contributed by NM, 26-Jan-2008) (New usage is discouraged.)

Ref Expression
Hypothesis ajfun.5 
|- A = ( U adj W )
Assertion ajfun 
|- ( ( U e. CPreHilOLD /\ W e. NrmCVec ) -> Fun A )

Proof

Step Hyp Ref Expression
1 ajfun.5 
 |-  A = ( U adj W )
2 oveq1 
 |-  ( U = if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) -> ( U adj W ) = ( if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) adj W ) )
3 1 2 eqtrid 
 |-  ( U = if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) -> A = ( if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) adj W ) )
4 3 funeqd 
 |-  ( U = if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) -> ( Fun A <-> Fun ( if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) adj W ) ) )
5 oveq2 
 |-  ( W = if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) -> ( if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) adj W ) = ( if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) adj if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) )
6 5 funeqd 
 |-  ( W = if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) -> ( Fun ( if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) adj W ) <-> Fun ( if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) adj if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) ) )
7 eqid 
 |-  ( if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) adj if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) ) = ( if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) adj if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) )
8 elimphu 
 |-  if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) e. CPreHilOLD
9 elimnvu 
 |-  if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) e. NrmCVec
10 7 8 9 ajfuni 
 |-  Fun ( if ( U e. CPreHilOLD , U , <. <. + , x. >. , abs >. ) adj if ( W e. NrmCVec , W , <. <. + , x. >. , abs >. ) )
11 4 6 10 dedth2h 
 |-  ( ( U e. CPreHilOLD /\ W e. NrmCVec ) -> Fun A )