Metamath Proof Explorer

Theorem cnlnadjlem2

Description: Lemma for cnlnadji . G is a continuous linear functional. (Contributed by NM, 16-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 ) )
Assertion cnlnadjlem2 
|- ( y e. ~H -> ( G e. LinFn /\ G e. ContFn ) )

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 1 lnopfi 
 |-  T : ~H --> ~H
5 4 ffvelrni 
 |-  ( g e. ~H -> ( T ` g ) e. ~H )
6 hicl 
 |-  ( ( ( T ` g ) e. ~H /\ y e. ~H ) -> ( ( T ` g ) .ih y ) e. CC )
7 5 6 sylan 
 |-  ( ( g e. ~H /\ y e. ~H ) -> ( ( T ` g ) .ih y ) e. CC )
8 7 ancoms 
 |-  ( ( y e. ~H /\ g e. ~H ) -> ( ( T ` g ) .ih y ) e. CC )
9 8 3 fmptd 
 |-  ( y e. ~H -> G : ~H --> CC )
10 hvmulcl 
 |-  ( ( x e. CC /\ w e. ~H ) -> ( x .h w ) e. ~H )
11 1 lnopaddi 
 |-  ( ( ( x .h w ) e. ~H /\ z e. ~H ) -> ( T ` ( ( x .h w ) +h z ) ) = ( ( T ` ( x .h w ) ) +h ( T ` z ) ) )
12 11 3adant3 
 |-  ( ( ( x .h w ) e. ~H /\ z e. ~H /\ y e. ~H ) -> ( T ` ( ( x .h w ) +h z ) ) = ( ( T ` ( x .h w ) ) +h ( T ` z ) ) )
13 12 oveq1d 
 |-  ( ( ( x .h w ) e. ~H /\ z e. ~H /\ y e. ~H ) -> ( ( T ` ( ( x .h w ) +h z ) ) .ih y ) = ( ( ( T ` ( x .h w ) ) +h ( T ` z ) ) .ih y ) )
14 4 ffvelrni 
 |-  ( ( x .h w ) e. ~H -> ( T ` ( x .h w ) ) e. ~H )
15 4 ffvelrni 
 |-  ( z e. ~H -> ( T ` z ) e. ~H )
16 id 
 |-  ( y e. ~H -> y e. ~H )
17 ax-his2 
 |-  ( ( ( T ` ( x .h w ) ) e. ~H /\ ( T ` z ) e. ~H /\ y e. ~H ) -> ( ( ( T ` ( x .h w ) ) +h ( T ` z ) ) .ih y ) = ( ( ( T ` ( x .h w ) ) .ih y ) + ( ( T ` z ) .ih y ) ) )
18 14 15 16 17 syl3an 
 |-  ( ( ( x .h w ) e. ~H /\ z e. ~H /\ y e. ~H ) -> ( ( ( T ` ( x .h w ) ) +h ( T ` z ) ) .ih y ) = ( ( ( T ` ( x .h w ) ) .ih y ) + ( ( T ` z ) .ih y ) ) )
19 13 18 eqtrd 
 |-  ( ( ( x .h w ) e. ~H /\ z e. ~H /\ y e. ~H ) -> ( ( T ` ( ( x .h w ) +h z ) ) .ih y ) = ( ( ( T ` ( x .h w ) ) .ih y ) + ( ( T ` z ) .ih y ) ) )
20 19 3comr 
 |-  ( ( y e. ~H /\ ( x .h w ) e. ~H /\ z e. ~H ) -> ( ( T ` ( ( x .h w ) +h z ) ) .ih y ) = ( ( ( T ` ( x .h w ) ) .ih y ) + ( ( T ` z ) .ih y ) ) )
21 20 3expa 
 |-  ( ( ( y e. ~H /\ ( x .h w ) e. ~H ) /\ z e. ~H ) -> ( ( T ` ( ( x .h w ) +h z ) ) .ih y ) = ( ( ( T ` ( x .h w ) ) .ih y ) + ( ( T ` z ) .ih y ) ) )
22 10 21 sylanl2 
 |-  ( ( ( y e. ~H /\ ( x e. CC /\ w e. ~H ) ) /\ z e. ~H ) -> ( ( T ` ( ( x .h w ) +h z ) ) .ih y ) = ( ( ( T ` ( x .h w ) ) .ih y ) + ( ( T ` z ) .ih y ) ) )
23 hvaddcl 
 |-  ( ( ( x .h w ) e. ~H /\ z e. ~H ) -> ( ( x .h w ) +h z ) e. ~H )
24 10 23 sylan 
 |-  ( ( ( x e. CC /\ w e. ~H ) /\ z e. ~H ) -> ( ( x .h w ) +h z ) e. ~H )
25 1 2 3 cnlnadjlem1 
 |-  ( ( ( x .h w ) +h z ) e. ~H -> ( G ` ( ( x .h w ) +h z ) ) = ( ( T ` ( ( x .h w ) +h z ) ) .ih y ) )
26 24 25 syl 
 |-  ( ( ( x e. CC /\ w e. ~H ) /\ z e. ~H ) -> ( G ` ( ( x .h w ) +h z ) ) = ( ( T ` ( ( x .h w ) +h z ) ) .ih y ) )
27 26 adantll 
 |-  ( ( ( y e. ~H /\ ( x e. CC /\ w e. ~H ) ) /\ z e. ~H ) -> ( G ` ( ( x .h w ) +h z ) ) = ( ( T ` ( ( x .h w ) +h z ) ) .ih y ) )
28 4 ffvelrni 
 |-  ( w e. ~H -> ( T ` w ) e. ~H )
29 ax-his3 
 |-  ( ( x e. CC /\ ( T ` w ) e. ~H /\ y e. ~H ) -> ( ( x .h ( T ` w ) ) .ih y ) = ( x x. ( ( T ` w ) .ih y ) ) )
30 28 29 syl3an2 
 |-  ( ( x e. CC /\ w e. ~H /\ y e. ~H ) -> ( ( x .h ( T ` w ) ) .ih y ) = ( x x. ( ( T ` w ) .ih y ) ) )
31 30 3comr 
 |-  ( ( y e. ~H /\ x e. CC /\ w e. ~H ) -> ( ( x .h ( T ` w ) ) .ih y ) = ( x x. ( ( T ` w ) .ih y ) ) )
32 31 3expb 
 |-  ( ( y e. ~H /\ ( x e. CC /\ w e. ~H ) ) -> ( ( x .h ( T ` w ) ) .ih y ) = ( x x. ( ( T ` w ) .ih y ) ) )
33 1 lnopmuli 
 |-  ( ( x e. CC /\ w e. ~H ) -> ( T ` ( x .h w ) ) = ( x .h ( T ` w ) ) )
34 33 oveq1d 
 |-  ( ( x e. CC /\ w e. ~H ) -> ( ( T ` ( x .h w ) ) .ih y ) = ( ( x .h ( T ` w ) ) .ih y ) )
35 34 adantl 
 |-  ( ( y e. ~H /\ ( x e. CC /\ w e. ~H ) ) -> ( ( T ` ( x .h w ) ) .ih y ) = ( ( x .h ( T ` w ) ) .ih y ) )
36 1 2 3 cnlnadjlem1 
 |-  ( w e. ~H -> ( G ` w ) = ( ( T ` w ) .ih y ) )
37 36 oveq2d 
 |-  ( w e. ~H -> ( x x. ( G ` w ) ) = ( x x. ( ( T ` w ) .ih y ) ) )
38 37 ad2antll 
 |-  ( ( y e. ~H /\ ( x e. CC /\ w e. ~H ) ) -> ( x x. ( G ` w ) ) = ( x x. ( ( T ` w ) .ih y ) ) )
39 32 35 38 3eqtr4rd 
 |-  ( ( y e. ~H /\ ( x e. CC /\ w e. ~H ) ) -> ( x x. ( G ` w ) ) = ( ( T ` ( x .h w ) ) .ih y ) )
40 1 2 3 cnlnadjlem1 
 |-  ( z e. ~H -> ( G ` z ) = ( ( T ` z ) .ih y ) )
41 39 40 oveqan12d 
 |-  ( ( ( y e. ~H /\ ( x e. CC /\ w e. ~H ) ) /\ z e. ~H ) -> ( ( x x. ( G ` w ) ) + ( G ` z ) ) = ( ( ( T ` ( x .h w ) ) .ih y ) + ( ( T ` z ) .ih y ) ) )
42 22 27 41 3eqtr4d 
 |-  ( ( ( y e. ~H /\ ( x e. CC /\ w e. ~H ) ) /\ z e. ~H ) -> ( G ` ( ( x .h w ) +h z ) ) = ( ( x x. ( G ` w ) ) + ( G ` z ) ) )
43 42 ralrimiva 
 |-  ( ( y e. ~H /\ ( x e. CC /\ w e. ~H ) ) -> A. z e. ~H ( G ` ( ( x .h w ) +h z ) ) = ( ( x x. ( G ` w ) ) + ( G ` z ) ) )
44 43 ralrimivva 
 |-  ( y e. ~H -> A. x e. CC A. w e. ~H A. z e. ~H ( G ` ( ( x .h w ) +h z ) ) = ( ( x x. ( G ` w ) ) + ( G ` z ) ) )
45 ellnfn 
 |-  ( G e. LinFn <-> ( G : ~H --> CC /\ A. x e. CC A. w e. ~H A. z e. ~H ( G ` ( ( x .h w ) +h z ) ) = ( ( x x. ( G ` w ) ) + ( G ` z ) ) ) )
46 9 44 45 sylanbrc 
 |-  ( y e. ~H -> G e. LinFn )
47 1 2 nmcopexi 
 |-  ( normop ` T ) e. RR
48 normcl 
 |-  ( y e. ~H -> ( normh ` y ) e. RR )
49 remulcl 
 |-  ( ( ( normop ` T ) e. RR /\ ( normh ` y ) e. RR ) -> ( ( normop ` T ) x. ( normh ` y ) ) e. RR )
50 47 48 49 sylancr 
 |-  ( y e. ~H -> ( ( normop ` T ) x. ( normh ` y ) ) e. RR )
51 40 adantr 
 |-  ( ( z e. ~H /\ y e. ~H ) -> ( G ` z ) = ( ( T ` z ) .ih y ) )
52 hicl 
 |-  ( ( ( T ` z ) e. ~H /\ y e. ~H ) -> ( ( T ` z ) .ih y ) e. CC )
53 15 52 sylan 
 |-  ( ( z e. ~H /\ y e. ~H ) -> ( ( T ` z ) .ih y ) e. CC )
54 51 53 eqeltrd 
 |-  ( ( z e. ~H /\ y e. ~H ) -> ( G ` z ) e. CC )
55 54 abscld 
 |-  ( ( z e. ~H /\ y e. ~H ) -> ( abs ` ( G ` z ) ) e. RR )
56 normcl 
 |-  ( ( T ` z ) e. ~H -> ( normh ` ( T ` z ) ) e. RR )
57 15 56 syl 
 |-  ( z e. ~H -> ( normh ` ( T ` z ) ) e. RR )
58 remulcl 
 |-  ( ( ( normh ` ( T ` z ) ) e. RR /\ ( normh ` y ) e. RR ) -> ( ( normh ` ( T ` z ) ) x. ( normh ` y ) ) e. RR )
59 57 48 58 syl2an 
 |-  ( ( z e. ~H /\ y e. ~H ) -> ( ( normh ` ( T ` z ) ) x. ( normh ` y ) ) e. RR )
60 normcl 
 |-  ( z e. ~H -> ( normh ` z ) e. RR )
61 remulcl 
 |-  ( ( ( normop ` T ) e. RR /\ ( normh ` z ) e. RR ) -> ( ( normop ` T ) x. ( normh ` z ) ) e. RR )
62 47 60 61 sylancr 
 |-  ( z e. ~H -> ( ( normop ` T ) x. ( normh ` z ) ) e. RR )
63 remulcl 
 |-  ( ( ( ( normop ` T ) x. ( normh ` z ) ) e. RR /\ ( normh ` y ) e. RR ) -> ( ( ( normop ` T ) x. ( normh ` z ) ) x. ( normh ` y ) ) e. RR )
64 62 48 63 syl2an 
 |-  ( ( z e. ~H /\ y e. ~H ) -> ( ( ( normop ` T ) x. ( normh ` z ) ) x. ( normh ` y ) ) e. RR )
65 51 fveq2d 
 |-  ( ( z e. ~H /\ y e. ~H ) -> ( abs ` ( G ` z ) ) = ( abs ` ( ( T ` z ) .ih y ) ) )
66 bcs 
 |-  ( ( ( T ` z ) e. ~H /\ y e. ~H ) -> ( abs ` ( ( T ` z ) .ih y ) ) <_ ( ( normh ` ( T ` z ) ) x. ( normh ` y ) ) )
67 15 66 sylan 
 |-  ( ( z e. ~H /\ y e. ~H ) -> ( abs ` ( ( T ` z ) .ih y ) ) <_ ( ( normh ` ( T ` z ) ) x. ( normh ` y ) ) )
68 65 67 eqbrtrd 
 |-  ( ( z e. ~H /\ y e. ~H ) -> ( abs ` ( G ` z ) ) <_ ( ( normh ` ( T ` z ) ) x. ( normh ` y ) ) )
69 57 adantr 
 |-  ( ( z e. ~H /\ y e. ~H ) -> ( normh ` ( T ` z ) ) e. RR )
70 62 adantr 
 |-  ( ( z e. ~H /\ y e. ~H ) -> ( ( normop ` T ) x. ( normh ` z ) ) e. RR )
71 normge0 
 |-  ( y e. ~H -> 0 <_ ( normh ` y ) )
72 48 71 jca 
 |-  ( y e. ~H -> ( ( normh ` y ) e. RR /\ 0 <_ ( normh ` y ) ) )
73 72 adantl 
 |-  ( ( z e. ~H /\ y e. ~H ) -> ( ( normh ` y ) e. RR /\ 0 <_ ( normh ` y ) ) )
74 1 2 nmcoplbi 
 |-  ( z e. ~H -> ( normh ` ( T ` z ) ) <_ ( ( normop ` T ) x. ( normh ` z ) ) )
75 74 adantr 
 |-  ( ( z e. ~H /\ y e. ~H ) -> ( normh ` ( T ` z ) ) <_ ( ( normop ` T ) x. ( normh ` z ) ) )
76 lemul1a 
 |-  ( ( ( ( normh ` ( T ` z ) ) e. RR /\ ( ( normop ` T ) x. ( normh ` z ) ) e. RR /\ ( ( normh ` y ) e. RR /\ 0 <_ ( normh ` y ) ) ) /\ ( normh ` ( T ` z ) ) <_ ( ( normop ` T ) x. ( normh ` z ) ) ) -> ( ( normh ` ( T ` z ) ) x. ( normh ` y ) ) <_ ( ( ( normop ` T ) x. ( normh ` z ) ) x. ( normh ` y ) ) )
77 69 70 73 75 76 syl31anc 
 |-  ( ( z e. ~H /\ y e. ~H ) -> ( ( normh ` ( T ` z ) ) x. ( normh ` y ) ) <_ ( ( ( normop ` T ) x. ( normh ` z ) ) x. ( normh ` y ) ) )
78 55 59 64 68 77 letrd 
 |-  ( ( z e. ~H /\ y e. ~H ) -> ( abs ` ( G ` z ) ) <_ ( ( ( normop ` T ) x. ( normh ` z ) ) x. ( normh ` y ) ) )
79 60 recnd 
 |-  ( z e. ~H -> ( normh ` z ) e. CC )
80 48 recnd 
 |-  ( y e. ~H -> ( normh ` y ) e. CC )
81 47 recni 
 |-  ( normop ` T ) e. CC
82 mul32 
 |-  ( ( ( normop ` T ) e. CC /\ ( normh ` z ) e. CC /\ ( normh ` y ) e. CC ) -> ( ( ( normop ` T ) x. ( normh ` z ) ) x. ( normh ` y ) ) = ( ( ( normop ` T ) x. ( normh ` y ) ) x. ( normh ` z ) ) )
83 81 82 mp3an1 
 |-  ( ( ( normh ` z ) e. CC /\ ( normh ` y ) e. CC ) -> ( ( ( normop ` T ) x. ( normh ` z ) ) x. ( normh ` y ) ) = ( ( ( normop ` T ) x. ( normh ` y ) ) x. ( normh ` z ) ) )
84 79 80 83 syl2an 
 |-  ( ( z e. ~H /\ y e. ~H ) -> ( ( ( normop ` T ) x. ( normh ` z ) ) x. ( normh ` y ) ) = ( ( ( normop ` T ) x. ( normh ` y ) ) x. ( normh ` z ) ) )
85 78 84 breqtrd 
 |-  ( ( z e. ~H /\ y e. ~H ) -> ( abs ` ( G ` z ) ) <_ ( ( ( normop ` T ) x. ( normh ` y ) ) x. ( normh ` z ) ) )
86 85 ancoms 
 |-  ( ( y e. ~H /\ z e. ~H ) -> ( abs ` ( G ` z ) ) <_ ( ( ( normop ` T ) x. ( normh ` y ) ) x. ( normh ` z ) ) )
87 86 ralrimiva 
 |-  ( y e. ~H -> A. z e. ~H ( abs ` ( G ` z ) ) <_ ( ( ( normop ` T ) x. ( normh ` y ) ) x. ( normh ` z ) ) )
88 oveq1 
 |-  ( x = ( ( normop ` T ) x. ( normh ` y ) ) -> ( x x. ( normh ` z ) ) = ( ( ( normop ` T ) x. ( normh ` y ) ) x. ( normh ` z ) ) )
89 88 breq2d 
 |-  ( x = ( ( normop ` T ) x. ( normh ` y ) ) -> ( ( abs ` ( G ` z ) ) <_ ( x x. ( normh ` z ) ) <-> ( abs ` ( G ` z ) ) <_ ( ( ( normop ` T ) x. ( normh ` y ) ) x. ( normh ` z ) ) ) )
90 89 ralbidv 
 |-  ( x = ( ( normop ` T ) x. ( normh ` y ) ) -> ( A. z e. ~H ( abs ` ( G ` z ) ) <_ ( x x. ( normh ` z ) ) <-> A. z e. ~H ( abs ` ( G ` z ) ) <_ ( ( ( normop ` T ) x. ( normh ` y ) ) x. ( normh ` z ) ) ) )
91 90 rspcev 
 |-  ( ( ( ( normop ` T ) x. ( normh ` y ) ) e. RR /\ A. z e. ~H ( abs ` ( G ` z ) ) <_ ( ( ( normop ` T ) x. ( normh ` y ) ) x. ( normh ` z ) ) ) -> E. x e. RR A. z e. ~H ( abs ` ( G ` z ) ) <_ ( x x. ( normh ` z ) ) )
92 50 87 91 syl2anc 
 |-  ( y e. ~H -> E. x e. RR A. z e. ~H ( abs ` ( G ` z ) ) <_ ( x x. ( normh ` z ) ) )
93 lnfncon 
 |-  ( G e. LinFn -> ( G e. ContFn <-> E. x e. RR A. z e. ~H ( abs ` ( G ` z ) ) <_ ( x x. ( normh ` z ) ) ) )
94 46 93 syl 
 |-  ( y e. ~H -> ( G e. ContFn <-> E. x e. RR A. z e. ~H ( abs ` ( G ` z ) ) <_ ( x x. ( normh ` z ) ) ) )
95 92 94 mpbird 
 |-  ( y e. ~H -> G e. ContFn )
96 46 95 jca 
 |-  ( y e. ~H -> ( G e. LinFn /\ G e. ContFn ) )