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 )