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