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

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 ⊢ 𝐴 = ( 𝑈 adj 𝑊 )
Assertion ajfun ( ( 𝑈 ∈ CPreHilOLD ∧ 𝑊 ∈ NrmCVec ) → Fun 𝐴 )

Proof

Step Hyp Ref Expression
1 ajfun.5 ⊢ 𝐴 = ( 𝑈 adj 𝑊 )
2 oveq1 ⊢ ( 𝑈 = if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( 𝑈 adj 𝑊 ) = ( if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) adj 𝑊 ) )
3 1 2 eqtrid ⊢ ( 𝑈 = if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → 𝐴 = ( if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) adj 𝑊 ) )
4 3 funeqd ⊢ ( 𝑈 = if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( Fun 𝐴 ↔ Fun ( if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) adj 𝑊 ) ) )
5 oveq2 ⊢ ( 𝑊 = if ( 𝑊 ∈ NrmCVec , 𝑊 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) adj 𝑊 ) = ( if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) adj if ( 𝑊 ∈ NrmCVec , 𝑊 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) )
6 5 funeqd ⊢ ( 𝑊 = if ( 𝑊 ∈ NrmCVec , 𝑊 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( Fun ( if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) adj 𝑊 ) ↔ Fun ( if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) adj if ( 𝑊 ∈ NrmCVec , 𝑊 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ) )
7 eqid ⊢ ( if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) adj if ( 𝑊 ∈ NrmCVec , 𝑊 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) = ( if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) adj if ( 𝑊 ∈ NrmCVec , 𝑊 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) )
8 elimphu ⊢ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ∈ CPreHilOLD
9 elimnvu ⊢ if ( 𝑊 ∈ NrmCVec , 𝑊 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ∈ NrmCVec
10 7 8 9 ajfuni ⊢ Fun ( if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) adj if ( 𝑊 ∈ NrmCVec , 𝑊 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) )
11 4 6 10 dedth2h ⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ 𝑊 ∈ NrmCVec ) → Fun 𝐴 )