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 CPreHil OLD W NrmCVec Fun A

Proof

Step Hyp Ref Expression
1 ajfun.5 A = U adj W
2 oveq1 U = if U CPreHil OLD U + × abs U adj W = if U CPreHil OLD U + × abs adj W
3 1 2 eqtrid U = if U CPreHil OLD U + × abs A = if U CPreHil OLD U + × abs adj W
4 3 funeqd U = if U CPreHil OLD U + × abs Fun A Fun if U CPreHil OLD U + × abs adj W
5 oveq2 W = if W NrmCVec W + × abs if U CPreHil OLD U + × abs adj W = if U CPreHil OLD U + × abs adj if W NrmCVec W + × abs
6 5 funeqd W = if W NrmCVec W + × abs Fun if U CPreHil OLD U + × abs adj W Fun if U CPreHil OLD U + × abs adj if W NrmCVec W + × abs
7 eqid if U CPreHil OLD U + × abs adj if W NrmCVec W + × abs = if U CPreHil OLD U + × abs adj if W NrmCVec W + × abs
8 elimphu if U CPreHil OLD U + × abs CPreHil OLD
9 elimnvu if W NrmCVec W + × abs NrmCVec
10 7 8 9 ajfuni Fun if U CPreHil OLD U + × abs adj if W NrmCVec W + × abs
11 4 6 10 dedth2h U CPreHil OLD W NrmCVec Fun A