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	eqtrid	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → 𝐴 = { ⟨ 𝑡 , 𝑠 ⟩ ∣ ( 𝑡 : 𝑋 ⟶ 𝑌 ∧ 𝑠 : 𝑌 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( ( 𝑡 ‘ 𝑥 ) 𝑄 𝑦 ) = ( 𝑥 𝑃 ( 𝑠 ‘ 𝑦 ) ) ) } )