Theorem ajfuni

Description: The adjoint function is a function. (Contributed by NM, 25-Jan-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ajfuni.5	⊢ 𝐴 = ( 𝑈 adj 𝑊 )
	ajfuni.u	⊢ 𝑈 ∈ CPreHilOLD
	ajfuni.w	⊢ 𝑊 ∈ NrmCVec
Assertion	ajfuni	⊢ Fun 𝐴

Proof

Step	Hyp	Ref	Expression
1		ajfuni.5	⊢ 𝐴 = ( 𝑈 adj 𝑊 )
2		ajfuni.u	⊢ 𝑈 ∈ CPreHilOLD
3		ajfuni.w	⊢ 𝑊 ∈ NrmCVec
4		funopab	⊢ ( Fun { ⟨ 𝑡 , 𝑠 ⟩ ∣ ( 𝑡 : ( BaseSet ‘ 𝑈 ) ⟶ ( BaseSet ‘ 𝑊 ) ∧ 𝑠 : ( BaseSet ‘ 𝑊 ) ⟶ ( BaseSet ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑦 ∈ ( BaseSet ‘ 𝑊 ) ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ( ·𝑖OLD ‘ 𝑈 ) ( 𝑠 ‘ 𝑦 ) ) ) } ↔ ∀ 𝑡 ∃* 𝑠 ( 𝑡 : ( BaseSet ‘ 𝑈 ) ⟶ ( BaseSet ‘ 𝑊 ) ∧ 𝑠 : ( BaseSet ‘ 𝑊 ) ⟶ ( BaseSet ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑦 ∈ ( BaseSet ‘ 𝑊 ) ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ( ·𝑖OLD ‘ 𝑈 ) ( 𝑠 ‘ 𝑦 ) ) ) )
5		eqid	⊢ ( BaseSet ‘ 𝑈 ) = ( BaseSet ‘ 𝑈 )
6		eqid	⊢ ( ·𝑖OLD ‘ 𝑈 ) = ( ·𝑖OLD ‘ 𝑈 )
7	5 6 2	ajmoi	⊢ ∃* 𝑠 ( 𝑠 : ( BaseSet ‘ 𝑊 ) ⟶ ( BaseSet ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑦 ∈ ( BaseSet ‘ 𝑊 ) ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ( ·𝑖OLD ‘ 𝑈 ) ( 𝑠 ‘ 𝑦 ) ) )
8		3simpc	⊢ ( ( 𝑡 : ( BaseSet ‘ 𝑈 ) ⟶ ( BaseSet ‘ 𝑊 ) ∧ 𝑠 : ( BaseSet ‘ 𝑊 ) ⟶ ( BaseSet ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑦 ∈ ( BaseSet ‘ 𝑊 ) ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ( ·𝑖OLD ‘ 𝑈 ) ( 𝑠 ‘ 𝑦 ) ) ) → ( 𝑠 : ( BaseSet ‘ 𝑊 ) ⟶ ( BaseSet ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑦 ∈ ( BaseSet ‘ 𝑊 ) ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ( ·𝑖OLD ‘ 𝑈 ) ( 𝑠 ‘ 𝑦 ) ) ) )
9	8	moimi	⊢ ( ∃* 𝑠 ( 𝑠 : ( BaseSet ‘ 𝑊 ) ⟶ ( BaseSet ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑦 ∈ ( BaseSet ‘ 𝑊 ) ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ( ·𝑖OLD ‘ 𝑈 ) ( 𝑠 ‘ 𝑦 ) ) ) → ∃* 𝑠 ( 𝑡 : ( BaseSet ‘ 𝑈 ) ⟶ ( BaseSet ‘ 𝑊 ) ∧ 𝑠 : ( BaseSet ‘ 𝑊 ) ⟶ ( BaseSet ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑦 ∈ ( BaseSet ‘ 𝑊 ) ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ( ·𝑖OLD ‘ 𝑈 ) ( 𝑠 ‘ 𝑦 ) ) ) )
10	7 9	ax-mp	⊢ ∃* 𝑠 ( 𝑡 : ( BaseSet ‘ 𝑈 ) ⟶ ( BaseSet ‘ 𝑊 ) ∧ 𝑠 : ( BaseSet ‘ 𝑊 ) ⟶ ( BaseSet ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑦 ∈ ( BaseSet ‘ 𝑊 ) ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ( ·𝑖OLD ‘ 𝑈 ) ( 𝑠 ‘ 𝑦 ) ) )
11	4 10	mpgbir	⊢ Fun { ⟨ 𝑡 , 𝑠 ⟩ ∣ ( 𝑡 : ( BaseSet ‘ 𝑈 ) ⟶ ( BaseSet ‘ 𝑊 ) ∧ 𝑠 : ( BaseSet ‘ 𝑊 ) ⟶ ( BaseSet ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑦 ∈ ( BaseSet ‘ 𝑊 ) ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ( ·𝑖OLD ‘ 𝑈 ) ( 𝑠 ‘ 𝑦 ) ) ) }
12	2	phnvi	⊢ 𝑈 ∈ NrmCVec
13		eqid	⊢ ( BaseSet ‘ 𝑊 ) = ( BaseSet ‘ 𝑊 )
14		eqid	⊢ ( ·𝑖OLD ‘ 𝑊 ) = ( ·𝑖OLD ‘ 𝑊 )
15	5 13 6 14 1	ajfval	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → 𝐴 = { ⟨ 𝑡 , 𝑠 ⟩ ∣ ( 𝑡 : ( BaseSet ‘ 𝑈 ) ⟶ ( BaseSet ‘ 𝑊 ) ∧ 𝑠 : ( BaseSet ‘ 𝑊 ) ⟶ ( BaseSet ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑦 ∈ ( BaseSet ‘ 𝑊 ) ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ( ·𝑖OLD ‘ 𝑈 ) ( 𝑠 ‘ 𝑦 ) ) ) } )
16	12 3 15	mp2an	⊢ 𝐴 = { ⟨ 𝑡 , 𝑠 ⟩ ∣ ( 𝑡 : ( BaseSet ‘ 𝑈 ) ⟶ ( BaseSet ‘ 𝑊 ) ∧ 𝑠 : ( BaseSet ‘ 𝑊 ) ⟶ ( BaseSet ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑦 ∈ ( BaseSet ‘ 𝑊 ) ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ( ·𝑖OLD ‘ 𝑈 ) ( 𝑠 ‘ 𝑦 ) ) ) }
17	16	funeqi	⊢ ( Fun 𝐴 ↔ Fun { ⟨ 𝑡 , 𝑠 ⟩ ∣ ( 𝑡 : ( BaseSet ‘ 𝑈 ) ⟶ ( BaseSet ‘ 𝑊 ) ∧ 𝑠 : ( BaseSet ‘ 𝑊 ) ⟶ ( BaseSet ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ∀ 𝑦 ∈ ( BaseSet ‘ 𝑊 ) ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ( ·𝑖OLD ‘ 𝑈 ) ( 𝑠 ‘ 𝑦 ) ) ) } )
18	11 17	mpbir	⊢ Fun 𝐴