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	syl5eq	⊢ ( 𝑈 = 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 𝐴 )