Theorem cnlnadjlem2 27556

Description: Lemma for cnlnadji 27564. G is a continuous linear functional. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.)

Hypotheses

Ref	Expression
cnlnadjlem.1	|- T e. LinOp
cnlnadjlem.2	|- T e. ConOp
cnlnadjlem.3	|- G = ( g e. ~H |-> ( ( T ` g ) .ih y ) )

Assertion

Ref	Expression
cnlnadjlem2	|- ( y e. ~H -> ( G e. LinFn /\ G e. ConFn ) )

Distinct variable group:   y, g, T

Allowed substitution hints:   G( y, g)

Proof of Theorem cnlnadjlem2

Dummy variables w z x are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cnlnadjlem.1	. . . . . . . 8 |- T e. LinOp
2	1	lnopfi 27457	. . . . . . 7 |- T : ~H --> ~H
3	2	ffvelrni 6036	. . . . . 6 |- ( g e. ~H -> ( T ` g ) e. ~H )
4		hicl 26568	. . . . . 6 |- ( ( ( T ` g ) e. ~H /\ y e. ~H ) -> ( ( T ` g ) .ih y ) e. CC )
5	3, 4	sylan 473	. . . . 5 |- ( ( g e. ~H /\ y e. ~H ) -> ( ( T ` g ) .ih y ) e. CC )
6	5	ancoms 454	. . . 4 |- ( ( y e. ~H /\ g e. ~H ) -> ( ( T ` g ) .ih y ) e. CC )
7		cnlnadjlem.3	. . . 4 |- G = ( g e. ~H |-> ( ( T ` g ) .ih y ) )
8	6, 7	fmptd 6061	. . 3 |- ( y e. ~H -> G : ~H --> CC )
9		hvmulcl 26501	. . . . . . 7 |- ( ( x e. CC /\ w e. ~H ) -> ( x .h w ) e. ~H )
10	1	lnopaddi 27459	. . . . . . . . . . . 12 |- ( ( ( x .h w ) e. ~H /\ z e. ~H ) -> ( T ` ( ( x .h w ) +h z ) ) = ( ( T ` ( x .h w ) ) +h ( T ` z ) ) )
11	10	3adant3 1025	. . . . . . . . . . 11 |- ( ( ( x .h w ) e. ~H /\ z e. ~H /\ y e. ~H ) -> ( T ` ( ( x .h w ) +h z ) ) = ( ( T ` ( x .h w ) ) +h ( T ` z ) ) )
12	11	oveq1d 6320	. . . . . . . . . 10 |- ( ( ( 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 ) )
13	2	ffvelrni 6036	. . . . . . . . . . 11 |- ( ( x .h w ) e. ~H -> ( T ` ( x .h w ) ) e. ~H )
14	2	ffvelrni 6036	. . . . . . . . . . 11 |- ( z e. ~H -> ( T ` z ) e. ~H )
15		id 23	. . . . . . . . . . 11 |- ( y e. ~H -> y e. ~H )
16		ax-his2 26571	. . . . . . . . . . 11 |- ( ( ( 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 ) ) )
17	13, 14, 15, 16	syl3an 1306	. . . . . . . . . 10 |- ( ( ( 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 ) ) )
18	12, 17	eqtrd 2470	. . . . . . . . 9 |- ( ( ( 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 ) ) )
19	18	3comr 1213	. . . . . . . 8 |- ( ( 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 ) ) )
20	19	3expa 1205	. . . . . . 7 |- ( ( ( 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	9, 20	sylanl2 655	. . . . . 6 |- ( ( ( 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 ) ) )
22		hvaddcl 26500	. . . . . . . . 9 |- ( ( ( x .h w ) e. ~H /\ z e. ~H ) -> ( ( x .h w ) +h z ) e. ~H )
23	9, 22	sylan 473	. . . . . . . 8 |- ( ( ( x e. CC /\ w e. ~H ) /\ z e. ~H ) -> ( ( x .h w ) +h z ) e. ~H )
24		cnlnadjlem.2	. . . . . . . . 9 |- T e. ConOp
25	1, 24, 7	cnlnadjlem1 27555	. . . . . . . 8 |- ( ( ( x .h w ) +h z ) e. ~H -> ( G ` ( ( x .h w ) +h z ) ) = ( ( T ` ( ( x .h w ) +h z ) ) .ih y ) )
26	23, 25	syl 17	. . . . . . 7 |- ( ( ( 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 718	. . . . . 6 |- ( ( ( 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	2	ffvelrni 6036	. . . . . . . . . . 11 |- ( w e. ~H -> ( T ` w ) e. ~H )
29		ax-his3 26572	. . . . . . . . . . 11 |- ( ( 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 1298	. . . . . . . . . 10 |- ( ( x e. CC /\ w e. ~H /\ y e. ~H ) -> ( ( x .h ( T ` w ) ) .ih y ) = ( x x. ( ( T ` w ) .ih y ) ) )
31	30	3comr 1213	. . . . . . . . 9 |- ( ( y e. ~H /\ x e. CC /\ w e. ~H ) -> ( ( x .h ( T ` w ) ) .ih y ) = ( x x. ( ( T ` w ) .ih y ) ) )
32	31	3expb 1206	. . . . . . . 8 |- ( ( y e. ~H /\ ( x e. CC /\ w e. ~H ) ) -> ( ( x .h ( T ` w ) ) .ih y ) = ( x x. ( ( T ` w ) .ih y ) ) )
33	1	lnopmuli 27460	. . . . . . . . . 10 |- ( ( x e. CC /\ w e. ~H ) -> ( T ` ( x .h w ) ) = ( x .h ( T ` w ) ) )
34	33	oveq1d 6320	. . . . . . . . 9 |- ( ( x e. CC /\ w e. ~H ) -> ( ( T ` ( x .h w ) ) .ih y ) = ( ( x .h ( T ` w ) ) .ih y ) )
35	34	adantl 467	. . . . . . . 8 |- ( ( y e. ~H /\ ( x e. CC /\ w e. ~H ) ) -> ( ( T ` ( x .h w ) ) .ih y ) = ( ( x .h ( T ` w ) ) .ih y ) )
36	1, 24, 7	cnlnadjlem1 27555	. . . . . . . . . 10 |- ( w e. ~H -> ( G ` w ) = ( ( T ` w ) .ih y ) )
37	36	oveq2d 6321	. . . . . . . . 9 |- ( w e. ~H -> ( x x. ( G ` w ) ) = ( x x. ( ( T ` w ) .ih y ) ) )
38	37	ad2antll 733	. . . . . . . 8 |- ( ( y e. ~H /\ ( x e. CC /\ w e. ~H ) ) -> ( x x. ( G ` w ) ) = ( x x. ( ( T ` w ) .ih y ) ) )
39	32, 35, 38	3eqtr4rd 2481	. . . . . . 7 |- ( ( y e. ~H /\ ( x e. CC /\ w e. ~H ) ) -> ( x x. ( G ` w ) ) = ( ( T ` ( x .h w ) ) .ih y ) )
40	1, 24, 7	cnlnadjlem1 27555	. . . . . . 7 |- ( z e. ~H -> ( G ` z ) = ( ( T ` z ) .ih y ) )
41	39, 40	oveqan12d 6324	. . . . . 6 |- ( ( ( 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	21, 27, 41	3eqtr4d 2480	. . . . 5 |- ( ( ( 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 2846	. . . 4 |- ( ( 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 2853	. . 3 |- ( 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 27371	. . 3 |- ( 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	8, 44, 45	sylanbrc 668	. 2 |- ( y e. ~H -> G e. LinFn )
47	1, 24	nmcopexi 27515	. . . . 5 |- ( normop ` T ) e. RR
48		normcl 26613	. . . . 5 |- ( y e. ~H -> ( normh ` y ) e. RR )
49		remulcl 9623	. . . . 5 |- ( ( ( normop ` T ) e. RR /\ ( normh ` y ) e. RR ) -> ( ( normop ` T ) x. ( normh ` y ) ) e. RR )
50	47, 48, 49	sylancr 667	. . . 4 |- ( y e. ~H -> ( ( normop ` T ) x. ( normh ` y ) ) e. RR )
51	40	adantr 466	. . . . . . . . . 10 |- ( ( z e. ~H /\ y e. ~H ) -> ( G ` z ) = ( ( T ` z ) .ih y ) )
52		hicl 26568	. . . . . . . . . . 11 |- ( ( ( T ` z ) e. ~H /\ y e. ~H ) -> ( ( T ` z ) .ih y ) e. CC )
53	14, 52	sylan 473	. . . . . . . . . 10 |- ( ( z e. ~H /\ y e. ~H ) -> ( ( T ` z ) .ih y ) e. CC )
54	51, 53	eqeltrd 2517	. . . . . . . . 9 |- ( ( z e. ~H /\ y e. ~H ) -> ( G ` z ) e. CC )
55	54	abscld 13476	. . . . . . . 8 |- ( ( z e. ~H /\ y e. ~H ) -> ( abs ` ( G ` z ) ) e. RR )
56		normcl 26613	. . . . . . . . . 10 |- ( ( T ` z ) e. ~H -> ( normh ` ( T ` z ) ) e. RR )
57	14, 56	syl 17	. . . . . . . . 9 |- ( z e. ~H -> ( normh ` ( T ` z ) ) e. RR )
58		remulcl 9623	. . . . . . . . 9 |- ( ( ( normh ` ( T ` z ) ) e. RR /\ ( normh ` y ) e. RR ) -> ( ( normh ` ( T ` z ) ) x. ( normh ` y ) ) e. RR )
59	57, 48, 58	syl2an 479	. . . . . . . 8 |- ( ( z e. ~H /\ y e. ~H ) -> ( ( normh ` ( T ` z ) ) x. ( normh ` y ) ) e. RR )
60		normcl 26613	. . . . . . . . . 10 |- ( z e. ~H -> ( normh ` z ) e. RR )
61		remulcl 9623	. . . . . . . . . 10 |- ( ( ( normop ` T ) e. RR /\ ( normh ` z ) e. RR ) -> ( ( normop ` T ) x. ( normh ` z ) ) e. RR )
62	47, 60, 61	sylancr 667	. . . . . . . . 9 |- ( z e. ~H -> ( ( normop ` T ) x. ( normh ` z ) ) e. RR )
63		remulcl 9623	. . . . . . . . 9 |- ( ( ( ( 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 479	. . . . . . . 8 |- ( ( z e. ~H /\ y e. ~H ) -> ( ( ( normop ` T ) x. ( normh ` z ) ) x. ( normh ` y ) ) e. RR )
65	51	fveq2d 5885	. . . . . . . . 9 |- ( ( z e. ~H /\ y e. ~H ) -> ( abs ` ( G ` z ) ) = ( abs ` ( ( T ` z ) .ih y ) ) )
66		bcs 26669	. . . . . . . . . 10 |- ( ( ( T ` z ) e. ~H /\ y e. ~H ) -> ( abs ` ( ( T ` z ) .ih y ) ) <_ ( ( normh ` ( T ` z ) ) x. ( normh ` y ) ) )
67	14, 66	sylan 473	. . . . . . . . 9 |- ( ( z e. ~H /\ y e. ~H ) -> ( abs ` ( ( T ` z ) .ih y ) ) <_ ( ( normh ` ( T ` z ) ) x. ( normh ` y ) ) )
68	65, 67	eqbrtrd 4446	. . . . . . . 8 |- ( ( z e. ~H /\ y e. ~H ) -> ( abs ` ( G ` z ) ) <_ ( ( normh ` ( T ` z ) ) x. ( normh ` y ) ) )
69	57	adantr 466	. . . . . . . . 9 |- ( ( z e. ~H /\ y e. ~H ) -> ( normh ` ( T ` z ) ) e. RR )
70	62	adantr 466	. . . . . . . . 9 |- ( ( z e. ~H /\ y e. ~H ) -> ( ( normop ` T ) x. ( normh ` z ) ) e. RR )
71		normge0 26614	. . . . . . . . . . 11 |- ( y e. ~H -> 0 <_ ( normh ` y ) )
72	48, 71	jca 534	. . . . . . . . . 10 |- ( y e. ~H -> ( ( normh ` y ) e. RR /\ 0 <_ ( normh ` y ) ) )
73	72	adantl 467	. . . . . . . . 9 |- ( ( z e. ~H /\ y e. ~H ) -> ( ( normh ` y ) e. RR /\ 0 <_ ( normh ` y ) ) )
74	1, 24	nmcoplbi 27516	. . . . . . . . . 10 |- ( z e. ~H -> ( normh ` ( T ` z ) ) <_ ( ( normop ` T ) x. ( normh ` z ) ) )
75	74	adantr 466	. . . . . . . . 9 |- ( ( z e. ~H /\ y e. ~H ) -> ( normh ` ( T ` z ) ) <_ ( ( normop ` T ) x. ( normh ` z ) ) )
76		lemul1a 10458	. . . . . . . . 9 |- ( ( ( ( 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 1267	. . . . . . . 8 |- ( ( 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 9791	. . . . . . 7 |- ( ( z e. ~H /\ y e. ~H ) -> ( abs ` ( G ` z ) ) <_ ( ( ( normop ` T ) x. ( normh ` z ) ) x. ( normh ` y ) ) )
79	60	recnd 9668	. . . . . . . 8 |- ( z e. ~H -> ( normh ` z ) e. CC )
80	48	recnd 9668	. . . . . . . 8 |- ( y e. ~H -> ( normh ` y ) e. CC )
81	47	recni 9654	. . . . . . . . 9 |- ( normop ` T ) e. CC
82		mul32 9799	. . . . . . . . 9 |- ( ( ( 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 1347	. . . . . . . 8 |- ( ( ( 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 479	. . . . . . 7 |- ( ( 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 4450	. . . . . 6 |- ( ( z e. ~H /\ y e. ~H ) -> ( abs ` ( G ` z ) ) <_ ( ( ( normop ` T ) x. ( normh ` y ) ) x. ( normh ` z ) ) )
86	85	ancoms 454	. . . . 5 |- ( ( y e. ~H /\ z e. ~H ) -> ( abs ` ( G ` z ) ) <_ ( ( ( normop ` T ) x. ( normh ` y ) ) x. ( normh ` z ) ) )
87	86	ralrimiva 2846	. . . 4 |- ( y e. ~H -> A. z e. ~H ( abs ` ( G ` z ) ) <_ ( ( ( normop ` T ) x. ( normh ` y ) ) x. ( normh ` z ) ) )
88		oveq1 6312	. . . . . . 7 |- ( x = ( ( normop ` T ) x. ( normh ` y ) ) -> ( x x. ( normh ` z ) ) = ( ( ( normop ` T ) x. ( normh ` y ) ) x. ( normh ` z ) ) )
89	88	breq2d 4438	. . . . . 6 |- ( 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 2871	. . . . 5 |- ( 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 3188	. . . 4 |- ( ( ( ( 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 665	. . 3 |- ( y e. ~H -> E. x e. RR A. z e. ~H ( abs ` ( G ` z ) ) <_ ( x x. ( normh ` z ) ) )
93		lnfncon 27544	. . . 4 |- ( G e. LinFn -> ( G e. ConFn <-> E. x e. RR A. z e. ~H ( abs ` ( G ` z ) ) <_ ( x x. ( normh ` z ) ) ) )
94	46, 93	syl 17	. . 3 |- ( y e. ~H -> ( G e. ConFn <-> E. x e. RR A. z e. ~H ( abs ` ( G ` z ) ) <_ ( x x. ( normh ` z ) ) ) )
95	92, 94	mpbird 235	. 2 |- ( y e. ~H -> G e. ConFn )
96	46, 95	jca 534	1 |- ( y e. ~H -> ( G e. LinFn /\ G e. ConFn ) )

Syntax hints:   -> wi 4   <-> wb 187   /\ wa 370   /\ w3a 982   = wceq 1437   e. wcel 1870   A.wral 2782   E.wrex 2783   class class class wbr 4426   |-> cmpt 4484   -->wf 5597   ` cfv 5601  (class class class)co 6305   CCcc 9536   RRcr 9537   0cc0 9538   + caddc 9541   x. cmul 9543   <_ cle 9675   abscabs 13276   ~Hchil 26407   +h cva 26408   .h csm 26409   .ih csp 26410   normhcno 26411   normopcnop 26433   ConOpccop 26434   LinOpclo 26435   ConFnccnfn 26441   LinFnclf 26442

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-rep 4538  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  ax-un 6597  ax-inf2 8146  ax-cnex 9594  ax-resscn 9595  ax-1cn 9596  ax-icn 9597  ax-addcl 9598  ax-addrcl 9599  ax-mulcl 9600  ax-mulrcl 9601  ax-mulcom 9602  ax-addass 9603  ax-mulass 9604  ax-distr 9605  ax-i2m1 9606  ax-1ne0 9607  ax-1rid 9608  ax-rnegex 9609  ax-rrecex 9610  ax-cnre 9611  ax-pre-lttri 9612  ax-pre-lttrn 9613  ax-pre-ltadd 9614  ax-pre-mulgt0 9615  ax-pre-sup 9616  ax-addf 9617  ax-mulf 9618  ax-hilex 26487  ax-hfvadd 26488  ax-hvcom 26489  ax-hvass 26490  ax-hv0cl 26491  ax-hvaddid 26492  ax-hfvmul 26493  ax-hvmulid 26494  ax-hvmulass 26495  ax-hvdistr1 26496  ax-hvdistr2 26497  ax-hvmul0 26498  ax-hfi 26567  ax-his1 26570  ax-his2 26571  ax-his3 26572  ax-his4 26573

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-nel 2628  df-ral 2787  df-rex 2788  df-reu 2789  df-rmo 2790  df-rab 2791  df-v 3089  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-pss 3458  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-tp 4007  df-op 4009  df-uni 4223  df-int 4259  df-iun 4304  df-iin 4305  df-br 4427  df-opab 4485  df-mpt 4486  df-tr 4521  df-eprel 4765  df-id 4769  df-po 4775  df-so 4776  df-fr 4813  df-se 4814  df-we 4815  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-isom 5610  df-riota 6267  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-of 6545  df-om 6707  df-1st 6807  df-2nd 6808  df-supp 6926  df-wrecs 7036  df-recs 7098  df-rdg 7136  df-1o 7190  df-2o 7191  df-oadd 7194  df-er 7371  df-map 7482  df-ixp 7531  df-en 7578  df-dom 7579  df-sdom 7580  df-fin 7581  df-fsupp 7890  df-fi 7931  df-sup 7962  df-oi 8025  df-card 8372  df-cda 8596  df-pnf 9676  df-mnf 9677  df-xr 9678  df-ltxr 9679  df-le 9680  df-sub 9861  df-neg 9862  df-div 10269  df-nn 10610  df-2 10668  df-3 10669  df-4 10670  df-5 10671  df-6 10672  df-7 10673  df-8 10674  df-9 10675  df-10 10676  df-n0 10870  df-z 10938  df-dec 11052  df-uz 11160  df-q 11265  df-rp 11303  df-xneg 11409  df-xadd 11410  df-xmul 11411  df-ioo 11639  df-icc 11642  df-fz 11783  df-fzo 11914  df-seq 12211  df-exp 12270  df-hash 12513  df-cj 13141  df-re 13142  df-im 13143  df-sqrt 13277  df-abs 13278  df-clim 13530  df-sum 13731  df-struct 15086  df-ndx 15087  df-slot 15088  df-base 15089  df-sets 15090  df-ress 15091  df-plusg 15165  df-mulr 15166  df-starv 15167  df-sca 15168  df-vsca 15169  df-ip 15170  df-tset 15171  df-ple 15172  df-ds 15174  df-unif 15175  df-hom 15176  df-cco 15177  df-rest 15280  df-topn 15281  df-0g 15299  df-gsum 15300  df-topgen 15301  df-pt 15302  df-prds 15305  df-xrs 15359  df-qtop 15364  df-imas 15365  df-xps 15367  df-mre 15443  df-mrc 15444  df-acs 15446  df-mgm 16439  df-sgrp 16478  df-mnd 16488  df-submnd 16534  df-mulg 16627  df-cntz 16922  df-cmn 17367  df-psmet 18897  df-xmet 18898  df-met 18899  df-bl 18900  df-mopn 18901  df-cnfld 18906  df-top 19852  df-bases 19853  df-topon 19854  df-topsp 19855  df-cld 19965  df-ntr 19966  df-cls 19967  df-cn 20174  df-cnp 20175  df-t1 20261  df-haus 20262  df-tx 20508  df-hmeo 20701  df-xms 21266  df-ms 21267  df-tms 21268  df-grpo 25764  df-gid 25765  df-ginv 25766  df-gdiv 25767  df-ablo 25855  df-vc 26010  df-nv 26056  df-va 26059  df-ba 26060  df-sm 26061  df-0v 26062  df-vs 26063  df-nmcv 26064  df-ims 26065  df-dip 26182  df-ph 26299  df-hnorm 26456  df-hba 26457  df-hvsub 26459  df-nmop 27327  df-cnop 27328  df-lnop 27329  df-nmfn 27333  df-cnfn 27335  df-lnfn 27336

This theorem is referenced by:  cnlnadjlem3  27557  cnlnadjlem5  27559