Theorem cnlnadjlem5 9960

Description: Lemma for cnlnadj 9965. F is an adjoint of T (later, we will show it is unique).

Hypotheses

Ref	Expression
cnlnadjlem.1	|- T e. LinOp
cnlnadjlem.2	|- T e. ConOp
cnlnadjlem.3	|- G = {<.g, h>. | (g e. H~ /\ h = ((T` g) .ih y))}
cnlnadjlem.4	|- B = U.{w e. H~ | A.v e. H~ ((T` v) .ih y) = (v .ih w)}
cnlnadjlem.5	|- F = {<.y, u>. | (y e. H~ /\ u = B)}

Assertion

Ref	Expression
cnlnadjlem5	|- ((A e. H~ /\ C e. H~) -> ((T` C) .ih A) = (C .ih (F` A)))

Distinct variable groups:   g,h,u,v,w,y,A   u,B   w,F   v,G,w   T,g,h,u,v,w,y

Proof of Theorem cnlnadjlem5

Step	Hyp	Ref	Expression
1		fveq2 3719	. . . . . 6 |- (f = C -> (T` f) = (T` C))
2	1	opreq1d 3970	. . . . 5 |- (f = C -> ((T` f) .ih A) = ((T` C) .ih A))
3		opreq1 3963	. . . . 5 |- (f = C -> (f .ih (F` A)) = (C .ih (F` A)))
4	2, 3	eqeq12d 1487	. . . 4 |- (f = C -> (((T` f) .ih A) = (f .ih (F` A)) <-> ((T` C) .ih A) = (C .ih (F` A))))
5	4	imbi2d 611	. . 3 |- (f = C -> ((A e. H~ -> ((T` f) .ih A) = (f .ih (F` A))) <-> (A e. H~ -> ((T` C) .ih A) = (C .ih (F` A)))))
6		ax-17 970	. . . . . 6 |- (z e. A -> A.y z e. A)
7		ax-17 970	. . . . . . 7 |- (f e. H~ -> A.y f e. H~)
8		ax-17 970	. . . . . . . 8 |- (z e. ((T` f) .ih A) -> A.y z e. ((T` f) .ih A))
9		ax-17 970	. . . . . . . . 9 |- (z e. f -> A.y z e. f)
10		ax-17 970	. . . . . . . . 9 |- (z e. .ih -> A.y z e. .ih )
11		cnlnadjlem.5	. . . . . . . . . . 11 |- F = {<.y, u>. | (y e. H~ /\ u = B)}
12		hbopab1 2809	. . . . . . . . . . 11 |- (z e. {<.y, u>. | (y e. H~ /\ u = B)} -> A.y z e. {<.y, u>. | (y e. H~ /\ u = B)})
13	11, 12	hbxfr 1561	. . . . . . . . . 10 |- (z e. F -> A.y z e. F)
14	13, 6	hbfv 3724	. . . . . . . . 9 |- (z e. (F` A) -> A.y z e. (F` A))
15	9, 10, 14	hbopr 3976	. . . . . . . 8 |- (z e. (f .ih (F` A)) -> A.y z e. (f .ih (F` A)))
16	8, 15	hbeq 1563	. . . . . . 7 |- (((T` f) .ih A) = (f .ih (F` A)) -> A.y((T` f) .ih A) = (f .ih (F` A)))
17	7, 16	hbral 1684	. . . . . 6 |- (A.f e. H~ ((T` f) .ih A) = (f .ih (F` A)) -> A.yA.f e. H~ ((T` f) .ih A) = (f .ih (F` A)))
18		opreq2 3964	. . . . . . . 8 |- (y = A -> ((T` f) .ih y) = ((T` f) .ih A))
19		fveq2 3719	. . . . . . . . 9 |- (y = A -> (F` y) = (F` A))
20	19	opreq2d 3971	. . . . . . . 8 |- (y = A -> (f .ih (F` y)) = (f .ih (F` A)))
21	18, 20	eqeq12d 1487	. . . . . . 7 |- (y = A -> (((T` f) .ih y) = (f .ih (F` y)) <-> ((T` f) .ih A) = (f .ih (F` A))))
22	21	ralbidv 1661	. . . . . 6 |- (y = A -> (A.f e. H~ ((T` f) .ih y) = (f .ih (F` y)) <-> A.f e. H~ ((T` f) .ih A) = (f .ih (F` A))))
23		cnlnadjlem.4	. . . . . . . . . . 11 |- B = U.{w e. H~ | A.v e. H~ ((T` v) .ih y) = (v .ih w)}
24		ax-hilex 8824	. . . . . . . . . . . . 13 |- H~ e. V
25	24	rabex 2721	. . . . . . . . . . . 12 |- {w e. H~ | A.v e. H~ ((T` v) .ih y) = (v .ih w)} e. V
26	25	uniex 2866	. . . . . . . . . . 11 |- U.{w e. H~ | A.v e. H~ ((T` v) .ih y) = (v .ih w)} e. V
27	23, 26	eqeltr 1542	. . . . . . . . . 10 |- B e. V
28		fvopab2 3786	. . . . . . . . . 10 |- ((y e. H~ /\ B e. V) -> ({<.y, u>. | (y e. H~ /\ u = B)}` y) = B)
29	27, 28	mpan2 695	. . . . . . . . 9 |- (y e. H~ -> ({<.y, u>. | (y e. H~ /\ u = B)}` y) = B)
30	11	fveq1i 3720	. . . . . . . . 9 |- (F` y) = ({<.y, u>. | (y e. H~ /\ u = B)}` y)
31	29, 30	syl5eq 1517	. . . . . . . 8 |- (y e. H~ -> (F` y) = B)
32		fveq2 3719	. . . . . . . . . . . . . . 15 |- (v = f -> (T` v) = (T` f))
33	32	opreq1d 3970	. . . . . . . . . . . . . 14 |- (v = f -> ((T` v) .ih y) = ((T` f) .ih y))
34		opreq1 3963	. . . . . . . . . . . . . 14 |- (v = f -> (v .ih w) = (f .ih w))
35	33, 34	eqeq12d 1487	. . . . . . . . . . . . 13 |- (v = f -> (((T` v) .ih y) = (v .ih w) <-> ((T` f) .ih y) = (f .ih w)))
36	35	cbvralv 1797	. . . . . . . . . . . 12 |- (A.v e. H~ ((T` v) .ih y) = (v .ih w) <-> A.f e. H~ ((T` f) .ih y) = (f .ih w))
37	36	a1i 8	. . . . . . . . . . 11 |- (w e. H~ -> (A.v e. H~ ((T` v) .ih y) = (v .ih w) <-> A.f e. H~ ((T` f) .ih y) = (f .ih w)))
38	37	rabbii 1802	. . . . . . . . . 10 |- {w e. H~ | A.v e. H~ ((T` v) .ih y) = (v .ih w)} = {w e. H~ | A.f e. H~ ((T` f) .ih y) = (f .ih w)}
39	38	unieqi 2507	. . . . . . . . 9 |- U.{w e. H~ | A.v e. H~ ((T` v) .ih y) = (v .ih w)} = U.{w e. H~ | A.f e. H~ ((T` f) .ih y) = (f .ih w)}
40	23, 39	eqtr 1493	. . . . . . . 8 |- B = U.{w e. H~ | A.f e. H~ ((T` f) .ih y) = (f .ih w)}
41	31, 40	syl6req 1522	. . . . . . 7 |- (y e. H~ -> U.{w e. H~ | A.f e. H~ ((T` f) .ih y) = (f .ih w)} = (F` y))
42		opreq2 3964	. . . . . . . . . . 11 |- (w = (F` y) -> (f .ih w) = (f .ih (F` y)))
43	42	eqeq2d 1484	. . . . . . . . . 10 |- (w = (F` y) -> (((T` f) .ih y) = (f .ih w) <-> ((T` f) .ih y) = (f .ih (F` y))))
44	43	ralbidv 1661	. . . . . . . . 9 |- (w = (F` y) -> (A.f e. H~ ((T` f) .ih y) = (f .ih w) <-> A.f e. H~ ((T` f) .ih y) = (f .ih (F` y))))
45	44	reuuni2 2880	. . . . . . . 8 |- (((F` y) e. H~ /\ E!w e. H~ A.f e. H~ ((T` f) .ih y) = (f .ih w)) -> (A.f e. H~ ((T` f) .ih y) = (f .ih (F` y)) <-> U.{w e. H~ | A.f e. H~ ((T` f) .ih y) = (f .ih w)} = (F` y)))
46		cnlnadjlem.1	. . . . . . . . . 10 |- T e. LinOp
47		cnlnadjlem.2	. . . . . . . . . 10 |- T e. ConOp
48		cnlnadjlem.3	. . . . . . . . . 10 |- G = {<.g, h>. | (g e. H~ /\ h = ((T` g) .ih y))}
49	46, 47, 48, 23, 11	cnlnadjlem3 9958	. . . . . . . . 9 |- (y e. H~ -> B e. H~)
50	31, 49	eqeltrd 1546	. . . . . . . 8 |- (y e. H~ -> (F` y) e. H~)
51	46, 47, 48	cnlnadjlem2 9957	. . . . . . . . . . 11 |- (y e. H~ -> (G e. LinFn /\ G e. ConFn))
52		elin 2204	. . . . . . . . . . 11 |- (G e. (LinFn i^i ConFn) <-> (G e. LinFn /\ G e. ConFn))
53	51, 52	sylibr 200	. . . . . . . . . 10 |- (y e. H~ -> G e. (LinFn i^i ConFn))
54		riesz4t 9953	. . . . . . . . . 10 |- (G e. (LinFn i^i ConFn) -> E!w e. H~ A.f e. H~ (G` f) = (f .ih w))
55	53, 54	syl 10	. . . . . . . . 9 |- (y e. H~ -> E!w e. H~ A.f e. H~ (G` f) = (f .ih w))
56	46, 47, 48	cnlnadjlem1 9956	. . . . . . . . . . . 12 |- (f e. H~ -> (G` f) = ((T` f) .ih y))
57	56	eqeq1d 1481	. . . . . . . . . . 11 |- (f e. H~ -> ((G` f) = (f .ih w) <-> ((T` f) .ih y) = (f .ih w)))
58	57	ralbiia 1671	. . . . . . . . . 10 |- (A.f e. H~ (G` f) = (f .ih w) <-> A.f e. H~ ((T` f) .ih y) = (f .ih w))
59	58	reubii 1780	. . . . . . . . 9 |- (E!w e. H~ A.f e. H~ (G` f) = (f .ih w) <-> E!w e. H~ A.f e. H~ ((T` f) .ih y) = (f .ih w))
60	55, 59	sylib 198	. . . . . . . 8 |- (y e. H~ -> E!w e. H~ A.f e. H~ ((T` f) .ih y) = (f .ih w))
61	45, 50, 60	sylanc 471	. . . . . . 7 |- (y e. H~ -> (A.f e. H~ ((T` f) .ih y) = (f .ih (F` y)) <-> U.{w e. H~ | A.f e. H~ ((T` f) .ih y) = (f .ih w)} = (F` y)))
62	41, 61	mpbird 196	. . . . . 6 |- (y e. H~ -> A.f e. H~ ((T