Theorem ajfval 8465

Description: The adjoint function.

Hypotheses

Ref	Expression
ajfval.1	|- X = (Base` U)
ajfval.2	|- Y = (Base` W)
ajfval.3	|- P = (.i` U)
ajfval.4	|- Q = (.i` W)
ajfval.5	|- A = (UadjW)

Assertion

Ref	Expression
ajfval	|- ((U e. NrmCVec /\ W e. NrmCVec) -> A = {<.t, s>. | (t:X-->Y /\ s:Y-->X /\ A.x e. X A.y e. Y ((t` x)Qy) = (xP(s` y)))})

Distinct variable groups:   t,s,x,y,U   W,s,t,x,y   X,s,t,x   Y,s,t,y

Proof of Theorem ajfval

Step	Hyp	Ref	Expression
1		df-xp 3190	. . . . . 6 |- ((Y ^m X) X. (X ^m Y)) = {<.t, s>. | (t e. (Y ^m X) /\ s e. (X ^m Y))}
2		ajfval.2	. . . . . . . . . 10 |- Y = (Base` W)
3		fvex 3738	. . . . . . . . . 10 |- (Base` W) e. V
4	2, 3	eqeltr 1547	. . . . . . . . 9 |- Y e. V
5		ajfval.1	. . . . . . . . . 10 |- X = (Base` U)
6		fvex 3738	. . . . . . . . . 10 |- (Base` U) e. V
7	5, 6	eqeltr 1547	. . . . . . . . 9 |- X e. V
8	4, 7	elmap 4340	. . . . . . . 8 |- (t e. (Y ^m X) <-> t:X-->Y)
9	7, 4	elmap 4340	. . . . . . . 8 |- (s e. (X ^m Y) <-> s:Y-->X)
10	8, 9	anbi12i 484	. . . . . . 7 |- ((t e. (Y ^m X) /\ s e. (X ^m Y)) <-> (t:X-->Y /\ s:Y-->X))
11	10	opabbii 2676	. . . . . 6 |- {<.t, s>. | (t e. (Y ^m X) /\ s e. (X ^m Y))} = {<.t, s>. | (t:X-->Y /\ s:Y-->X)}
12	1, 11	eqtr2 1499	. . . . 5 |- {<.t, s>. | (t:X-->Y /\ s:Y-->X)} = ((Y ^m X) X. (X ^m Y))
13		oprex 3989	. . . . . 6 |- (Y ^m X) e. V
14		oprex 3989	. . . . . 6 |- (X ^m Y) e. V
15	13, 14	xpex 3266	. . . . 5 |- ((Y ^m X) X. (X ^m Y)) e. V
16	12, 15	eqeltr 1547	. . . 4 |- {<.t, s>. | (t:X-->Y /\ s:Y-->X)} e. V
17		3simpa 787	. . . . 5 |- ((t:X-->Y /\ s:Y-->X /\ A.x e. X A.y e. Y ((t` x)Qy) = (xP(s` y))) -> (t:X-->Y /\ s:Y-->X))
18	17	ssopab2i 2829	. . . 4 |- {<.t, s>. | (t:X-->Y /\ s:Y-->X /\ A.x e. X A.y e. Y ((t` x)Qy) = (xP(s` y)))} (_ {<.t, s>. | (t:X-->Y /\ s:Y-->X)}
19	16, 18	ssexi 2725	. . 3 |- {<.t, s>. | (t:X-->Y /\ s:Y-->X /\ A.x e. X A.y e. Y ((t` x)Qy) = (xP(s` y)))} e. V
20		fveq2 3730	. . . . . . 7 |- (u = U -> (Base` u) = (Base` U))
21	20, 5	syl6eqr 1528	. . . . . 6 |- (u = U -> (Base` u) = X)
22		feq2 3627	. . . . . 6 |- ((Base` u) = X -> (t:(Base` u)-->(Base` w) <-> t:X-->(Base` w)))
23	21, 22	syl 10	. . . . 5 |- (u = U -> (t:(Base` u)-->(Base` w) <-> t:X-->(Base` w)))
24		feq3 3628	. . . . . 6 |- ((Base` u) = X -> (s:(Base` w)-->(Base` u) <-> s:(Base` w)-->X))
25	21, 24	syl 10	. . . . 5 |- (u = U -> (s:(Base` w)-->(Base` u) <-> s:(Base` w)-->X))
26		fveq2 3730	. . . . . . . . . 10 |- (u = U -> (.i` u) = (.i` U))
27		ajfval.3	. . . . . . . . . 10 |- P = (.i` U)
28	26, 27	syl6eqr 1528	. . . . . . . . 9 |- (u = U -> (.i` u) = P)
29	28	opreqd 3983	. . . . . . . 8 |- (u = U -> (x(.i` u)(s` y)) = (xP(s` y)))
30	29	eqeq2d 1489	. . . . . . 7 |- (u = U -> (((t` x)(.i` w)y) = (x(.i` u)(s` y)) <-> ((t` x)(.i` w)y) = (xP(s` y))))
31	30	ralbidv 1666	. . . . . 6 |- (u = U -> (A.y e. (Base` w)((t` x)(.i` w)y) = (x(.i` u)(s` y)) <-> A.y e. (Base` w)((t` x)(.i` w)y) = (xP(s` y))))
32	21, 31	raleq12d 1797	. . . . 5 |- (u = U -> (A.x e. (Base` u)A.y e. (Base` w)((t` x)(.i` w)y) = (x(.i` u)(s` y)) <-> A.x e. X A.y e. (Base` w)((t` x)(.i` w)y) = (xP(s` y))))
33	23, 25, 32	3anbi123d 895	. . . 4 |- (u = U -> ((t:(Base` u)-->(Base` w) /\ s:(Base` w)-->(Base` u) /\ A.x e. (Base` u)A.y e. (Base` w)((t` x)(.i` w)y) = (x(.i` u)(s` y))) <-> (t:X-->(Base` w) /\ s:(Base` w)-->X /\ A.x e. X A.y e. (Base` w)((t` x)(.i` w)y) = (xP(s` y)))))
34	33	opabbidv 2675	. . 3 |- (u = U -> {<.t, s>. | (t:(Base` u)-->(Base` w) /\ s:(Base` w)-->(Base` u) /\ A.x e. (Base` u)A.y e. (Base` w)((t` x)(.i` w)y) = (x(.i` u)(s` y)))} = {<.t, s>. | (t:X-->(Base` w) /\ s:(Base` w)-->X /\ A.x e. X A.y e. (Base` w)((t` x)(.i` w)y) = (xP(s` y)))})
35		fveq2 3730	. . . . . . 7 |- (w = W -> (Base` w) = (Base` W))
36	35, 2	syl6eqr 1528	. . . . . 6 |- (w = W -> (Base` w) = Y)
37		feq3 3628	. . . . . 6 |- ((Base` w) = Y -> (t:X-->(Base` w) <-> t:X-->Y))
38	36, 37	syl 10	. . . . 5 |- (w = W -> (t:X-->(Base` w) <-> t:X-->Y))
39		feq2 3627	. . . . . 6 |- ((Base` w) = Y -> (s:(Base` w)-->X <-> s:Y-->X))
40	36, 39	syl 10	. . . . 5 |- (w = W -> (s:(Base` w)-->X <-> s:Y-->X))
41		fveq2 3730	. . . . . . . . . 10 |- (w = W -> (.i` w) = (.i` W))
42		ajfval.4	. . . . . . . . . 10 |- Q = (.i` W)
43	41, 42	syl6eqr 1528	. . . . . . . . 9 |- (w = W -> (.i` w) = Q)
44	43	opreqd 3983	. . . . . . . 8 |- (w = W -> ((t` x)(.i` w)y) = ((t` x)Qy))
45	44	eqeq1d 1486	. . . . . . 7 |- (w = W -> (((t` x)(.i` w)y) = (xP(s` y)) <-> ((t` x)Qy) = (xP(s` y))))
46	36, 45	raleq12d 1797	. . . . . 6 |- (w = W -> (A.y e. (Base` w)((t` x)(.i` w)y) = (xP(s` y)) <-> A.y e. Y ((t` x)Qy) = (xP(s` y))))
47	46	ralbidv 1666	. . . . 5 |- (w = W -> (A.x e. X A.y e. (Base` w)((t` x)(.i` w)y) = (xP(s` y)) <-> A.x e. X A.y e. Y ((t` x)Qy) = (xP(s` y))))
48	38, 40, 47	3anbi123d 895	. . . 4 |- (w = W -> ((t:X-->(Base` w) /\ s:(Base` w)-->X /\ A.x e. X A.y e. (Base` w)((t` x)(.i` w)y) = (xP(s` y))) <-> (t:X-->Y /\ s:Y-->X /\ A.x e. X A.y e. Y ((t` x)Qy) = (xP(s` y)))))
49	48	opabbidv 2675	. . 3 |- (w = W -> {<.t, s>. | (t:X-->(Base` w) /\ s:(Base` w)-->X /\ A.x e. X A.y e. (Base` w)((t` x)(.i` w)y) = (xP(s` y)))} = {<.t, s>. | (t:X-->Y /\ s:Y-->X /\ A.x e. X A.y e. Y ((t` x)Qy) = (xP(s` y)))})
50		df-aj 8407	. . 3 |- adj = {<.<.u, w>., a>. | ((u e. NrmCVec /\ w e. NrmCVec) /\ a = {<.t, s>. | (t:(Base` u)-->(Base` w) /\ s:(Base` w)-->(Base` u) /\ A.x e. (Base` u)A.y e. (Base` w)((t` x)(.i` w)y) = (x(.i` u)(s` y)))})}
51	19, 34, 49, 50	oprabval2 4034	. 2 |- ((U e. NrmCVec /\ W e. NrmCVec) -> (UadjW) = {<.t, s>. | (t:X-->Y /\ s:Y-->