Metamath Proof Explorer


Theorem cnlnadjlem5

Description: Lemma for cnlnadji . F is an adjoint of T (later, we will show it is unique). (Contributed by NM, 18-Feb-2006) (New usage is discouraged.)

Ref Expression
Hypotheses cnlnadjlem.1 T LinOp
cnlnadjlem.2 T ContOp
cnlnadjlem.3 G = g T g ih y
cnlnadjlem.4 B = ι w | v T v ih y = v ih w
cnlnadjlem.5 F = y B
Assertion cnlnadjlem5 A C T C ih A = C ih F A

Proof

Step Hyp Ref Expression
1 cnlnadjlem.1 T LinOp
2 cnlnadjlem.2 T ContOp
3 cnlnadjlem.3 G = g T g ih y
4 cnlnadjlem.4 B = ι w | v T v ih y = v ih w
5 cnlnadjlem.5 F = y B
6 nfcv _ y A
7 nfcv _ y
8 nfcv _ y f
9 nfcv _ y ih
10 nfmpt1 _ y y B
11 5 10 nfcxfr _ y F
12 11 6 nffv _ y F A
13 8 9 12 nfov _ y f ih F A
14 13 nfeq2 y T f ih A = f ih F A
15 7 14 nfralw y f T f ih A = f ih F A
16 oveq2 y = A T f ih y = T f ih A
17 fveq2 y = A F y = F A
18 17 oveq2d y = A f ih F y = f ih F A
19 16 18 eqeq12d y = A T f ih y = f ih F y T f ih A = f ih F A
20 19 ralbidv y = A f T f ih y = f ih F y f T f ih A = f ih F A
21 riotaex ι w | v T v ih y = v ih w V
22 4 21 eqeltri B V
23 5 fvmpt2 y B V F y = B
24 22 23 mpan2 y F y = B
25 fveq2 v = f T v = T f
26 25 oveq1d v = f T v ih y = T f ih y
27 oveq1 v = f v ih w = f ih w
28 26 27 eqeq12d v = f T v ih y = v ih w T f ih y = f ih w
29 28 cbvralvw v T v ih y = v ih w f T f ih y = f ih w
30 29 a1i w v T v ih y = v ih w f T f ih y = f ih w
31 1 2 3 cnlnadjlem1 f G f = T f ih y
32 31 eqeq1d f G f = f ih w T f ih y = f ih w
33 32 ralbiia f G f = f ih w f T f ih y = f ih w
34 30 33 bitr4di w v T v ih y = v ih w f G f = f ih w
35 34 riotabiia ι w | v T v ih y = v ih w = ι w | f G f = f ih w
36 4 35 eqtri B = ι w | f G f = f ih w
37 1 2 3 cnlnadjlem2 y G LinFn G ContFn
38 elin G LinFn ContFn G LinFn G ContFn
39 37 38 sylibr y G LinFn ContFn
40 riesz4 G LinFn ContFn ∃! w f G f = f ih w
41 riotacl2 ∃! w f G f = f ih w ι w | f G f = f ih w w | f G f = f ih w
42 39 40 41 3syl y ι w | f G f = f ih w w | f G f = f ih w
43 36 42 eqeltrid y B w | f G f = f ih w
44 24 43 eqeltrd y F y w | f G f = f ih w
45 oveq2 w = F y f ih w = f ih F y
46 45 eqeq2d w = F y T f ih y = f ih w T f ih y = f ih F y
47 46 ralbidv w = F y f T f ih y = f ih w f T f ih y = f ih F y
48 33 47 syl5bb w = F y f G f = f ih w f T f ih y = f ih F y
49 48 elrab F y w | f G f = f ih w F y f T f ih y = f ih F y
50 49 simprbi F y w | f G f = f ih w f T f ih y = f ih F y
51 44 50 syl y f T f ih y = f ih F y
52 6 15 20 51 vtoclgaf A f T f ih A = f ih F A
53 fveq2 f = C T f = T C
54 53 oveq1d f = C T f ih A = T C ih A
55 oveq1 f = C f ih F A = C ih F A
56 54 55 eqeq12d f = C T f ih A = f ih F A T C ih A = C ih F A
57 56 rspccva f T f ih A = f ih F A C T C ih A = C ih F A
58 52 57 sylan A C T C ih A = C ih F A