Theorem ajval

Description: Value of the adjoint function. (Contributed by NM, 25-Jan-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ajval.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	ajval.2	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
	ajval.3	⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
	ajval.4	⊢ 𝑄 = ( ·𝑖OLD ‘ 𝑊 )
	ajval.5	⊢ 𝐴 = ( 𝑈 adj 𝑊 )
Assertion	ajval	⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → ( 𝐴 ‘ 𝑇 ) = ( ℩ 𝑠 ( 𝑠 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑇 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ajval.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		ajval.2	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
3		ajval.3	⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
4		ajval.4	⊢ 𝑄 = ( ·𝑖OLD ‘ 𝑊 )
5		ajval.5	⊢ 𝐴 = ( 𝑈 adj 𝑊 )
6		phnv	⊢ ( 𝑈 ∈ CPreHilOLD → 𝑈 ∈ NrmCVec )
7	1 2 3 4 5	ajfval	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → 𝐴 = { ⟨ 𝑡 , 𝑠 ⟩ ∣ ( 𝑡 : 𝑋 ⟶ 𝑌 ∧ 𝑠 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑡 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) } )
8	6 7	sylan	⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ 𝑊 ∈ NrmCVec ) → 𝐴 = { ⟨ 𝑡 , 𝑠 ⟩ ∣ ( 𝑡 : 𝑋 ⟶ 𝑌 ∧ 𝑠 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑡 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) } )
9	8	fveq1d	⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ 𝑊 ∈ NrmCVec ) → ( 𝐴 ‘ 𝑇 ) = ( { ⟨ 𝑡 , 𝑠 ⟩ ∣ ( 𝑡 : 𝑋 ⟶ 𝑌 ∧ 𝑠 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑡 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) } ‘ 𝑇 ) )
10	9	3adant3	⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → ( 𝐴 ‘ 𝑇 ) = ( { ⟨ 𝑡 , 𝑠 ⟩ ∣ ( 𝑡 : 𝑋 ⟶ 𝑌 ∧ 𝑠 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑡 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) } ‘ 𝑇 ) )
11	1	fvexi	⊢ 𝑋 ∈ V
12		fex	⊢ ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝑋 ∈ V ) → 𝑇 ∈ V )
13	11 12	mpan2	⊢ ( 𝑇 : 𝑋 ⟶ 𝑌 → 𝑇 ∈ V )
14		eqid	⊢ { ⟨ 𝑡 , 𝑠 ⟩ ∣ ( 𝑡 : 𝑋 ⟶ 𝑌 ∧ 𝑠 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑡 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) } = { ⟨ 𝑡 , 𝑠 ⟩ ∣ ( 𝑡 : 𝑋 ⟶ 𝑌 ∧ 𝑠 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑡 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) }
15		feq1	⊢ ( 𝑡 = 𝑇 → ( 𝑡 : 𝑋 ⟶ 𝑌 ↔ 𝑇 : 𝑋 ⟶ 𝑌 ) )
16		fveq1	⊢ ( 𝑡 = 𝑇 → ( 𝑡 ‘ 𝑥 ) = ( 𝑇 ‘ 𝑥 ) )
17	16	oveq1d	⊢ ( 𝑡 = 𝑇 → ( ( 𝑡 ‘ 𝑥 ) 𝑄 𝑦 ) = ( ( 𝑇 ‘ 𝑥 ) 𝑄 𝑦 ) )
18	17	eqeq1d	⊢ ( 𝑡 = 𝑇 → ( ( ( 𝑡 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ↔ ( ( 𝑇 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) )
19	18	2ralbidv	⊢ ( 𝑡 = 𝑇 → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑡 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑇 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) )
20	15 19	3anbi13d	⊢ ( 𝑡 = 𝑇 → ( ( 𝑡 : 𝑋 ⟶ 𝑌 ∧ 𝑠 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑡 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) ↔ ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝑠 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑇 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) ) )
21	14 20	fvopab5	⊢ ( 𝑇 ∈ V → ( { ⟨ 𝑡 , 𝑠 ⟩ ∣ ( 𝑡 : 𝑋 ⟶ 𝑌 ∧ 𝑠 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑡 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) } ‘ 𝑇 ) = ( ℩ 𝑠 ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝑠 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑇 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) ) )
22	13 21	syl	⊢ ( 𝑇 : 𝑋 ⟶ 𝑌 → ( { ⟨ 𝑡 , 𝑠 ⟩ ∣ ( 𝑡 : 𝑋 ⟶ 𝑌 ∧ 𝑠 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑡 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) } ‘ 𝑇 ) = ( ℩ 𝑠 ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝑠 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑇 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) ) )
23		3anass	⊢ ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝑠 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑇 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) ↔ ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ ( 𝑠 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑇 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) ) )
24	23	baib	⊢ ( 𝑇 : 𝑋 ⟶ 𝑌 → ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝑠 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑇 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) ↔ ( 𝑠 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑇 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) ) )
25	24	iotabidv	⊢ ( 𝑇 : 𝑋 ⟶ 𝑌 → ( ℩ 𝑠 ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝑠 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑇 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) ) = ( ℩ 𝑠 ( 𝑠 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑇 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) ) )
26	22 25	eqtrd	⊢ ( 𝑇 : 𝑋 ⟶ 𝑌 → ( { ⟨ 𝑡 , 𝑠 ⟩ ∣ ( 𝑡 : 𝑋 ⟶ 𝑌 ∧ 𝑠 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑡 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) } ‘ 𝑇 ) = ( ℩ 𝑠 ( 𝑠 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑇 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) ) )
27	26	3ad2ant3	⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → ( { ⟨ 𝑡 , 𝑠 ⟩ ∣ ( 𝑡 : 𝑋 ⟶ 𝑌 ∧ 𝑠 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑡 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) } ‘ 𝑇 ) = ( ℩ 𝑠 ( 𝑠 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑇 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) ) )
28	10 27	eqtrd	⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → ( 𝐴 ‘ 𝑇 ) = ( ℩ 𝑠 ( 𝑠 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑇 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) ) )