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 e. LinOp
cnlnadjlem.2 
|- T e. ContOp
cnlnadjlem.3 
|- G = ( g e. ~H |-> ( ( T ` g ) .ih y ) )
cnlnadjlem.4 
|- B = ( iota_ w e. ~H A. v e. ~H ( ( T ` v ) .ih y ) = ( v .ih w ) )
cnlnadjlem.5 
|- F = ( y e. ~H |-> B )
Assertion cnlnadjlem5 
|- ( ( A e. ~H /\ C e. ~H ) -> ( ( T ` C ) .ih A ) = ( C .ih ( F ` A ) ) )

Proof

Step Hyp Ref Expression
1 cnlnadjlem.1 
 |-  T e. LinOp
2 cnlnadjlem.2 
 |-  T e. ContOp
3 cnlnadjlem.3 
 |-  G = ( g e. ~H |-> ( ( T ` g ) .ih y ) )
4 cnlnadjlem.4 
 |-  B = ( iota_ w e. ~H A. v e. ~H ( ( T ` v ) .ih y ) = ( v .ih w ) )
5 cnlnadjlem.5 
 |-  F = ( y e. ~H |-> B )
6 nfcv 
 |-  F/_ y A
7 nfcv 
 |-  F/_ y ~H
8 nfcv 
 |-  F/_ y f
9 nfcv 
 |-  F/_ y .ih
10 nfmpt1 
 |-  F/_ y ( y e. ~H |-> B )
11 5 10 nfcxfr 
 |-  F/_ y F
12 11 6 nffv 
 |-  F/_ y ( F ` A )
13 8 9 12 nfov 
 |-  F/_ y ( f .ih ( F ` A ) )
14 13 nfeq2 
 |-  F/ y ( ( T ` f ) .ih A ) = ( f .ih ( F ` A ) )
15 7 14 nfralw 
 |-  F/ y A. f e. ~H ( ( 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 -> ( A. f e. ~H ( ( T ` f ) .ih y ) = ( f .ih ( F ` y ) ) <-> A. f e. ~H ( ( T ` f ) .ih A ) = ( f .ih ( F ` A ) ) ) )
21 riotaex 
 |-  ( iota_ w e. ~H A. v e. ~H ( ( T ` v ) .ih y ) = ( v .ih w ) ) e. _V
22 4 21 eqeltri 
 |-  B e. _V
23 5 fvmpt2 
 |-  ( ( y e. ~H /\ B e. _V ) -> ( F ` y ) = B )
24 22 23 mpan2 
 |-  ( y e. ~H -> ( 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 
 |-  ( A. v e. ~H ( ( T ` v ) .ih y ) = ( v .ih w ) <-> A. f e. ~H ( ( T ` f ) .ih y ) = ( f .ih w ) )
30 29 a1i 
 |-  ( 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 ) ) )
31 1 2 3 cnlnadjlem1 
 |-  ( f e. ~H -> ( G ` f ) = ( ( T ` f ) .ih y ) )
32 31 eqeq1d 
 |-  ( f e. ~H -> ( ( G ` f ) = ( f .ih w ) <-> ( ( T ` f ) .ih y ) = ( f .ih w ) ) )
33 32 ralbiia 
 |-  ( A. f e. ~H ( G ` f ) = ( f .ih w ) <-> A. f e. ~H ( ( T ` f ) .ih y ) = ( f .ih w ) )
34 30 33 bitr4di 
 |-  ( w e. ~H -> ( A. v e. ~H ( ( T ` v ) .ih y ) = ( v .ih w ) <-> A. f e. ~H ( G ` f ) = ( f .ih w ) ) )
35 34 riotabiia 
 |-  ( iota_ w e. ~H A. v e. ~H ( ( T ` v ) .ih y ) = ( v .ih w ) ) = ( iota_ w e. ~H A. f e. ~H ( G ` f ) = ( f .ih w ) )
36 4 35 eqtri 
 |-  B = ( iota_ w e. ~H A. f e. ~H ( G ` f ) = ( f .ih w ) )
37 1 2 3 cnlnadjlem2 
 |-  ( y e. ~H -> ( G e. LinFn /\ G e. ContFn ) )
38 elin 
 |-  ( G e. ( LinFn i^i ContFn ) <-> ( G e. LinFn /\ G e. ContFn ) )
39 37 38 sylibr 
 |-  ( y e. ~H -> G e. ( LinFn i^i ContFn ) )
40 riesz4 
 |-  ( G e. ( LinFn i^i ContFn ) -> E! w e. ~H A. f e. ~H ( G ` f ) = ( f .ih w ) )
41 riotacl2 
 |-  ( E! w e. ~H A. f e. ~H ( G ` f ) = ( f .ih w ) -> ( iota_ w e. ~H A. f e. ~H ( G ` f ) = ( f .ih w ) ) e. { w e. ~H | A. f e. ~H ( G ` f ) = ( f .ih w ) } )
42 39 40 41 3syl 
 |-  ( y e. ~H -> ( iota_ w e. ~H A. f e. ~H ( G ` f ) = ( f .ih w ) ) e. { w e. ~H | A. f e. ~H ( G ` f ) = ( f .ih w ) } )
43 36 42 eqeltrid 
 |-  ( y e. ~H -> B e. { w e. ~H | A. f e. ~H ( G ` f ) = ( f .ih w ) } )
44 24 43 eqeltrd 
 |-  ( y e. ~H -> ( F ` y ) e. { w e. ~H | A. f e. ~H ( 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 ) -> ( A. f e. ~H ( ( T ` f ) .ih y ) = ( f .ih w ) <-> A. f e. ~H ( ( T ` f ) .ih y ) = ( f .ih ( F ` y ) ) ) )
48 33 47 syl5bb 
 |-  ( w = ( F ` y ) -> ( A. f e. ~H ( G ` f ) = ( f .ih w ) <-> A. f e. ~H ( ( T ` f ) .ih y ) = ( f .ih ( F ` y ) ) ) )
49 48 elrab 
 |-  ( ( F ` y ) e. { w e. ~H | A. f e. ~H ( G ` f ) = ( f .ih w ) } <-> ( ( F ` y ) e. ~H /\ A. f e. ~H ( ( T ` f ) .ih y ) = ( f .ih ( F ` y ) ) ) )
50 49 simprbi 
 |-  ( ( F ` y ) e. { w e. ~H | A. f e. ~H ( G ` f ) = ( f .ih w ) } -> A. f e. ~H ( ( T ` f ) .ih y ) = ( f .ih ( F ` y ) ) )
51 44 50 syl 
 |-  ( y e. ~H -> A. f e. ~H ( ( T ` f ) .ih y ) = ( f .ih ( F ` y ) ) )
52 6 15 20 51 vtoclgaf 
 |-  ( A e. ~H -> A. f e. ~H ( ( 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 
 |-  ( ( A. f e. ~H ( ( T ` f ) .ih A ) = ( f .ih ( F ` A ) ) /\ C e. ~H ) -> ( ( T ` C ) .ih A ) = ( C .ih ( F ` A ) ) )
58 52 57 sylan 
 |-  ( ( A e. ~H /\ C e. ~H ) -> ( ( T ` C ) .ih A ) = ( C .ih ( F ` A ) ) )