Hilbert Space Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HSE Home  >  Th. List  >  cnlnadjlem2 Unicode version

 Description: Lemma for cnlnadji 22672. is a continuous linear functional. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.)
Hypotheses
Ref Expression
Assertion
Ref Expression
Distinct variable group:   ,,
Allowed substitution hints:   (,)

Proof of Theorem cnlnadjlem2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cnlnadjlem.1 . . . . . . . 8
21lnopfi 22565 . . . . . . 7
32ffvelrni 5680 . . . . . 6
4 hicl 21675 . . . . . 6
53, 4sylan 457 . . . . 5
65ancoms 439 . . . 4
7 cnlnadjlem.3 . . . 4
86, 7fmptd 5700 . . 3
9 hvmulcl 21609 . . . . . . 7
101lnopaddi 22567 . . . . . . . . . . . 12
11103adant3 975 . . . . . . . . . . 11
1211oveq1d 5889 . . . . . . . . . 10
132ffvelrni 5680 . . . . . . . . . . 11
142ffvelrni 5680 . . . . . . . . . . 11
15 id 19 . . . . . . . . . . 11
16 ax-his2 21678 . . . . . . . . . . 11
1713, 14, 15, 16syl3an 1224 . . . . . . . . . 10
1812, 17eqtrd 2328 . . . . . . . . 9
19183comr 1159 . . . . . . . 8
20193expa 1151 . . . . . . 7
219, 20sylanl2 632 . . . . . 6
22 hvaddcl 21608 . . . . . . . . 9
239, 22sylan 457 . . . . . . . 8
24 cnlnadjlem.2 . . . . . . . . 9
251, 24, 7cnlnadjlem1 22663 . . . . . . . 8
2623, 25syl 15 . . . . . . 7
2726adantll 694 . . . . . 6
282ffvelrni 5680 . . . . . . . . . . 11
29 ax-his3 21679 . . . . . . . . . . 11
3028, 29syl3an2 1216 . . . . . . . . . 10
31303comr 1159 . . . . . . . . 9
32313expb 1152 . . . . . . . 8
331lnopmuli 22568 . . . . . . . . . 10
3433oveq1d 5889 . . . . . . . . 9
3534adantl 452 . . . . . . . 8
361, 24, 7cnlnadjlem1 22663 . . . . . . . . . 10
3736oveq2d 5890 . . . . . . . . 9
3837ad2antll 709 . . . . . . . 8
3932, 35, 383eqtr4rd 2339 . . . . . . 7
401, 24, 7cnlnadjlem1 22663 . . . . . . 7
4139, 40oveqan12d 5893 . . . . . 6
4221, 27, 413eqtr4d 2338 . . . . 5
4342ralrimiva 2639 . . . 4
4443ralrimivva 2648 . . 3
45 ellnfn 22479 . . 3
468, 44, 45sylanbrc 645 . 2
471, 24nmcopexi 22623 . . . . 5
48 normcl 21720 . . . . 5
49 remulcl 8838 . . . . 5
5047, 48, 49sylancr 644 . . . 4
5140adantr 451 . . . . . . . . . 10
52 hicl 21675 . . . . . . . . . . 11
5314, 52sylan 457 . . . . . . . . . 10
5451, 53eqeltrd 2370 . . . . . . . . 9
5554abscld 11934 . . . . . . . 8
56 normcl 21720 . . . . . . . . . 10
5714, 56syl 15 . . . . . . . . 9
58 remulcl 8838 . . . . . . . . 9
5957, 48, 58syl2an 463 . . . . . . . 8
60 normcl 21720 . . . . . . . . . 10
61 remulcl 8838 . . . . . . . . . 10
6247, 60, 61sylancr 644 . . . . . . . . 9
63 remulcl 8838 . . . . . . . . 9
6462, 48, 63syl2an 463 . . . . . . . 8
6551fveq2d 5545 . . . . . . . . 9
66 bcs 21776 . . . . . . . . . 10
6714, 66sylan 457 . . . . . . . . 9
6865, 67eqbrtrd 4059 . . . . . . . 8
6957adantr 451 . . . . . . . . 9
7062adantr 451 . . . . . . . . 9
71 normge0 21721 . . . . . . . . . . 11
7248, 71jca 518 . . . . . . . . . 10
7372adantl 452 . . . . . . . . 9
741, 24nmcoplbi 22624 . . . . . . . . . 10
7574adantr 451 . . . . . . . . 9
76 lemul1a 9626 . . . . . . . . 9
7769, 70, 73, 75, 76syl31anc 1185 . . . . . . . 8
7855, 59, 64, 68, 77letrd 8989 . . . . . . 7
7960recnd 8877 . . . . . . . 8
8048recnd 8877 . . . . . . . 8
8147recni 8865 . . . . . . . . 9
82 mul32 8995 . . . . . . . . 9
8381, 82mp3an1 1264 . . . . . . . 8
8479, 80, 83syl2an 463 . . . . . . 7
8578, 84breqtrd 4063 . . . . . 6
8685ancoms 439 . . . . 5
8786ralrimiva 2639 . . . 4
88 oveq1 5881 . . . . . . 7
8988breq2d 4051 . . . . . 6
9089ralbidv 2576 . . . . 5
9190rspcev 2897 . . . 4
9250, 87, 91syl2anc 642 . . 3
93 lnfncon 22652 . . . 4
9446, 93syl 15 . . 3
9592, 94mpbird 223 . 2
9646, 95jca 518 1