Metamath Proof Explorer

Theorem ajfval

Description: The adjoint function. (Contributed by NM, 25-Jan-2008) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses ajfval.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
ajfval.2 ⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
ajfval.3 ⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
ajfval.4 ⊢ 𝑄 = ( ·𝑖OLD ‘ 𝑊 )
ajfval.5 ⊢ 𝐴 = ( 𝑈 adj 𝑊 )
Assertion ajfval ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → 𝐴 = { ⟨ 𝑡 , 𝑠 ⟩ ∣ ( 𝑡 : 𝑋 ⟶ 𝑌 ∧ 𝑠 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑡 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) } )

Proof

Step Hyp Ref Expression
1 ajfval.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 ajfval.2 ⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
3 ajfval.3 ⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
4 ajfval.4 ⊢ 𝑄 = ( ·𝑖OLD ‘ 𝑊 )
5 ajfval.5 ⊢ 𝐴 = ( 𝑈 adj 𝑊 )
6 fveq2 ⊢ ( 𝑢 = 𝑈 → ( BaseSet ‘ 𝑢 ) = ( BaseSet ‘ 𝑈 ) )
7 6 1 eqtr4di ⊢ ( 𝑢 = 𝑈 → ( BaseSet ‘ 𝑢 ) = 𝑋 )
8 7 feq2d ⊢ ( 𝑢 = 𝑈 → ( 𝑡 : ( BaseSet ‘ 𝑢 ) ⟶ ( BaseSet ‘ 𝑤 ) ↔ 𝑡 : 𝑋 ⟶ ( BaseSet ‘ 𝑤 ) ) )
9 7 feq3d ⊢ ( 𝑢 = 𝑈 → ( 𝑠 : ( BaseSet ‘ 𝑤 ) ⟶ ( BaseSet ‘ 𝑢 ) ↔ 𝑠 : ( BaseSet ‘ 𝑤 ) ⟶ 𝑋 ) )
10 fveq2 ⊢ ( 𝑢 = 𝑈 → ( ·𝑖OLD ‘ 𝑢 ) = ( ·𝑖OLD ‘ 𝑈 ) )
11 10 3 eqtr4di ⊢ ( 𝑢 = 𝑈 → ( ·𝑖OLD ‘ 𝑢 ) = 𝑃 )
12 11 oveqd ⊢ ( 𝑢 = 𝑈 → ( 𝑥 ( ·𝑖OLD ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) )
13 12 eqeq2d ⊢ ( 𝑢 = 𝑈 → ( ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑤 ) 𝑦 ) = ( 𝑥 ( ·𝑖OLD ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ↔ ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑤 ) 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) )
14 13 ralbidv ⊢ ( 𝑢 = 𝑈 → ( ∀ 𝑦 ∈ ( BaseSet ‘ 𝑤 ) ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑤 ) 𝑦 ) = ( 𝑥 ( ·𝑖OLD ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ ( BaseSet ‘ 𝑤 ) ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑤 ) 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) )
15 7 14 raleqbidv ⊢ ( 𝑢 = 𝑈 → ( ∀ 𝑥 ∈ ( BaseSet ‘ 𝑢 ) ∀ 𝑦 ∈ ( BaseSet ‘ 𝑤 ) ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑤 ) 𝑦 ) = ( 𝑥 ( ·𝑖OLD ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ ( BaseSet ‘ 𝑤 ) ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑤 ) 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) )
16 8 9 15 3anbi123d ⊢ ( 𝑢 = 𝑈 → ( ( 𝑡 : ( BaseSet ‘ 𝑢 ) ⟶ ( BaseSet ‘ 𝑤 ) ∧ 𝑠 : ( BaseSet ‘ 𝑤 ) ⟶ ( BaseSet ‘ 𝑢 ) ∧ ∀ 𝑥 ∈ ( BaseSet ‘ 𝑢 ) ∀ 𝑦 ∈ ( BaseSet ‘ 𝑤 ) ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑤 ) 𝑦 ) = ( 𝑥 ( ·𝑖OLD ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ) ↔ ( 𝑡 : 𝑋 ⟶ ( BaseSet ‘ 𝑤 ) ∧ 𝑠 : ( BaseSet ‘ 𝑤 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ ( BaseSet ‘ 𝑤 ) ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑤 ) 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) ) )
17 16 opabbidv ⊢ ( 𝑢 = 𝑈 → { ⟨ 𝑡 , 𝑠 ⟩ ∣ ( 𝑡 : ( BaseSet ‘ 𝑢 ) ⟶ ( BaseSet ‘ 𝑤 ) ∧ 𝑠 : ( BaseSet ‘ 𝑤 ) ⟶ ( BaseSet ‘ 𝑢 ) ∧ ∀ 𝑥 ∈ ( BaseSet ‘ 𝑢 ) ∀ 𝑦 ∈ ( BaseSet ‘ 𝑤 ) ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑤 ) 𝑦 ) = ( 𝑥 ( ·𝑖OLD ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ) } = { ⟨ 𝑡 , 𝑠 ⟩ ∣ ( 𝑡 : 𝑋 ⟶ ( BaseSet ‘ 𝑤 ) ∧ 𝑠 : ( BaseSet ‘ 𝑤 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ ( BaseSet ‘ 𝑤 ) ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑤 ) 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) } )
18 fveq2 ⊢ ( 𝑤 = 𝑊 → ( BaseSet ‘ 𝑤 ) = ( BaseSet ‘ 𝑊 ) )
19 18 2 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( BaseSet ‘ 𝑤 ) = 𝑌 )
20 19 feq3d ⊢ ( 𝑤 = 𝑊 → ( 𝑡 : 𝑋 ⟶ ( BaseSet ‘ 𝑤 ) ↔ 𝑡 : 𝑋 ⟶ 𝑌 ) )
21 19 feq2d ⊢ ( 𝑤 = 𝑊 → ( 𝑠 : ( BaseSet ‘ 𝑤 ) ⟶ 𝑋 ↔ 𝑠 : 𝑌 ⟶ 𝑋 ) )
22 fveq2 ⊢ ( 𝑤 = 𝑊 → ( ·𝑖OLD ‘ 𝑤 ) = ( ·𝑖OLD ‘ 𝑊 ) )
23 22 4 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( ·𝑖OLD ‘ 𝑤 ) = 𝑄 )
24 23 oveqd ⊢ ( 𝑤 = 𝑊 → ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑤 ) 𝑦 ) = ( ( 𝑡 ‘ 𝑥 ) 𝑄 𝑦 ) )
25 24 eqeq1d ⊢ ( 𝑤 = 𝑊 → ( ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑤 ) 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ↔ ( ( 𝑡 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) )
26 19 25 raleqbidv ⊢ ( 𝑤 = 𝑊 → ( ∀ 𝑦 ∈ ( BaseSet ‘ 𝑤 ) ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑤 ) 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝑌 ( ( 𝑡 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) )
27 26 ralbidv ⊢ ( 𝑤 = 𝑊 → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ ( BaseSet ‘ 𝑤 ) ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑤 ) 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑡 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) )
28 20 21 27 3anbi123d ⊢ ( 𝑤 = 𝑊 → ( ( 𝑡 : 𝑋 ⟶ ( BaseSet ‘ 𝑤 ) ∧ 𝑠 : ( BaseSet ‘ 𝑤 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ ( BaseSet ‘ 𝑤 ) ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑤 ) 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) ↔ ( 𝑡 : 𝑋 ⟶ 𝑌 ∧ 𝑠 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑡 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) ) )
29 28 opabbidv ⊢ ( 𝑤 = 𝑊 → { ⟨ 𝑡 , 𝑠 ⟩ ∣ ( 𝑡 : 𝑋 ⟶ ( BaseSet ‘ 𝑤 ) ∧ 𝑠 : ( BaseSet ‘ 𝑤 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ ( BaseSet ‘ 𝑤 ) ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑤 ) 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) } = { ⟨ 𝑡 , 𝑠 ⟩ ∣ ( 𝑡 : 𝑋 ⟶ 𝑌 ∧ 𝑠 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑡 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) } )
30 df-aj ⊢ adj = ( 𝑢 ∈ NrmCVec , 𝑤 ∈ NrmCVec ↦ { ⟨ 𝑡 , 𝑠 ⟩ ∣ ( 𝑡 : ( BaseSet ‘ 𝑢 ) ⟶ ( BaseSet ‘ 𝑤 ) ∧ 𝑠 : ( BaseSet ‘ 𝑤 ) ⟶ ( BaseSet ‘ 𝑢 ) ∧ ∀ 𝑥 ∈ ( BaseSet ‘ 𝑢 ) ∀ 𝑦 ∈ ( BaseSet ‘ 𝑤 ) ( ( 𝑡 ‘ 𝑥 ) ( ·𝑖OLD ‘ 𝑤 ) 𝑦 ) = ( 𝑥 ( ·𝑖OLD ‘ 𝑢 ) ( 𝑠 ‘ 𝑦 ) ) ) } )
31 ovex ⊢ ( 𝑌 ↑m 𝑋 ) ∈ V
32 ovex ⊢ ( 𝑋 ↑m 𝑌 ) ∈ V
33 31 32 xpex ⊢ ( ( 𝑌 ↑m 𝑋 ) × ( 𝑋 ↑m 𝑌 ) ) ∈ V
34 2 fvexi ⊢ 𝑌 ∈ V
35 1 fvexi ⊢ 𝑋 ∈ V
36 34 35 elmap ⊢ ( 𝑡 ∈ ( 𝑌 ↑m 𝑋 ) ↔ 𝑡 : 𝑋 ⟶ 𝑌 )
37 35 34 elmap ⊢ ( 𝑠 ∈ ( 𝑋 ↑m 𝑌 ) ↔ 𝑠 : 𝑌 ⟶ 𝑋 )
38 36 37 anbi12i ⊢ ( ( 𝑡 ∈ ( 𝑌 ↑m 𝑋 ) ∧ 𝑠 ∈ ( 𝑋 ↑m 𝑌 ) ) ↔ ( 𝑡 : 𝑋 ⟶ 𝑌 ∧ 𝑠 : 𝑌 ⟶ 𝑋 ) )
39 38 biimpri ⊢ ( ( 𝑡 : 𝑋 ⟶ 𝑌 ∧ 𝑠 : 𝑌 ⟶ 𝑋 ) → ( 𝑡 ∈ ( 𝑌 ↑m 𝑋 ) ∧ 𝑠 ∈ ( 𝑋 ↑m 𝑌 ) ) )
40 39 3adant3 ⊢ ( ( 𝑡 : 𝑋 ⟶ 𝑌 ∧ 𝑠 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑡 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) → ( 𝑡 ∈ ( 𝑌 ↑m 𝑋 ) ∧ 𝑠 ∈ ( 𝑋 ↑m 𝑌 ) ) )
41 40 ssopab2i ⊢ { ⟨ 𝑡 , 𝑠 ⟩ ∣ ( 𝑡 : 𝑋 ⟶ 𝑌 ∧ 𝑠 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑡 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) } ⊆ { ⟨ 𝑡 , 𝑠 ⟩ ∣ ( 𝑡 ∈ ( 𝑌 ↑m 𝑋 ) ∧ 𝑠 ∈ ( 𝑋 ↑m 𝑌 ) ) }
42 df-xp ⊢ ( ( 𝑌 ↑m 𝑋 ) × ( 𝑋 ↑m 𝑌 ) ) = { ⟨ 𝑡 , 𝑠 ⟩ ∣ ( 𝑡 ∈ ( 𝑌 ↑m 𝑋 ) ∧ 𝑠 ∈ ( 𝑋 ↑m 𝑌 ) ) }
43 41 42 sseqtrri ⊢ { ⟨ 𝑡 , 𝑠 ⟩ ∣ ( 𝑡 : 𝑋 ⟶ 𝑌 ∧ 𝑠 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑡 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) } ⊆ ( ( 𝑌 ↑m 𝑋 ) × ( 𝑋 ↑m 𝑌 ) )
44 33 43 ssexi ⊢ { ⟨ 𝑡 , 𝑠 ⟩ ∣ ( 𝑡 : 𝑋 ⟶ 𝑌 ∧ 𝑠 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑡 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) } ∈ V
45 17 29 30 44 ovmpo ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → ( 𝑈 adj 𝑊 ) = { ⟨ 𝑡 , 𝑠 ⟩ ∣ ( 𝑡 : 𝑋 ⟶ 𝑌 ∧ 𝑠 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑡 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) } )
46 5 45 syl5eq ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → 𝐴 = { ⟨ 𝑡 , 𝑠 ⟩ ∣ ( 𝑡 : 𝑋 ⟶ 𝑌 ∧ 𝑠 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑡 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) } )