Metamath Proof Explorer

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 ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → ( 𝐴 ‘ 𝑇 ) = ( ℩ 𝑠 ( 𝑠 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑇 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) ) )