MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ipcnlem2 Structured version   Visualization version   Unicode version

Theorem ipcnlem2 22263
Description: The inner product operation of a complex pre-Hilbert space is continuous. (Contributed by Mario Carneiro, 13-Oct-2015.)
Hypotheses
Ref Expression
ipcn.v  |-  V  =  ( Base `  W
)
ipcn.h  |-  .,  =  ( .i `  W )
ipcn.d  |-  D  =  ( dist `  W
)
ipcn.n  |-  N  =  ( norm `  W
)
ipcn.t  |-  T  =  ( ( R  / 
2 )  /  (
( N `  A
)  +  1 ) )
ipcn.u  |-  U  =  ( ( R  / 
2 )  /  (
( N `  B
)  +  T ) )
ipcn.w  |-  ( ph  ->  W  e.  CPreHil )
ipcn.a  |-  ( ph  ->  A  e.  V )
ipcn.b  |-  ( ph  ->  B  e.  V )
ipcn.r  |-  ( ph  ->  R  e.  RR+ )
ipcn.x  |-  ( ph  ->  X  e.  V )
ipcn.y  |-  ( ph  ->  Y  e.  V )
ipcn.1  |-  ( ph  ->  ( A D X )  <  U )
ipcn.2  |-  ( ph  ->  ( B D Y )  <  T )
Assertion
Ref Expression
ipcnlem2  |-  ( ph  ->  ( abs `  (
( A  .,  B
)  -  ( X 
.,  Y ) ) )  <  R )

Proof of Theorem ipcnlem2
StepHypRef Expression
1 ipcn.w . . 3  |-  ( ph  ->  W  e.  CPreHil )
2 ipcn.a . . 3  |-  ( ph  ->  A  e.  V )
3 ipcn.b . . 3  |-  ( ph  ->  B  e.  V )
4 ipcn.v . . . 4  |-  V  =  ( Base `  W
)
5 ipcn.h . . . 4  |-  .,  =  ( .i `  W )
64, 5cphipcl 22217 . . 3  |-  ( ( W  e.  CPreHil  /\  A  e.  V  /\  B  e.  V )  ->  ( A  .,  B )  e.  CC )
71, 2, 3, 6syl3anc 1276 . 2  |-  ( ph  ->  ( A  .,  B
)  e.  CC )
8 ipcn.x . . 3  |-  ( ph  ->  X  e.  V )
9 ipcn.y . . 3  |-  ( ph  ->  Y  e.  V )
104, 5cphipcl 22217 . . 3  |-  ( ( W  e.  CPreHil  /\  X  e.  V  /\  Y  e.  V )  ->  ( X  .,  Y )  e.  CC )
111, 8, 9, 10syl3anc 1276 . 2  |-  ( ph  ->  ( X  .,  Y
)  e.  CC )
124, 5cphipcl 22217 . . 3  |-  ( ( W  e.  CPreHil  /\  A  e.  V  /\  Y  e.  V )  ->  ( A  .,  Y )  e.  CC )
131, 2, 9, 12syl3anc 1276 . 2  |-  ( ph  ->  ( A  .,  Y
)  e.  CC )
14 ipcn.r . . 3  |-  ( ph  ->  R  e.  RR+ )
1514rpred 11369 . 2  |-  ( ph  ->  R  e.  RR )
167, 13subcld 10011 . . . 4  |-  ( ph  ->  ( ( A  .,  B )  -  ( A  .,  Y ) )  e.  CC )
1716abscld 13546 . . 3  |-  ( ph  ->  ( abs `  (
( A  .,  B
)  -  ( A 
.,  Y ) ) )  e.  RR )
18 cphnlm 22198 . . . . . . . . 9  |-  ( W  e.  CPreHil  ->  W  e. NrmMod )
191, 18syl 17 . . . . . . . 8  |-  ( ph  ->  W  e. NrmMod )
20 nlmngp 21728 . . . . . . . 8  |-  ( W  e. NrmMod  ->  W  e. NrmGrp )
2119, 20syl 17 . . . . . . 7  |-  ( ph  ->  W  e. NrmGrp )
22 ipcn.n . . . . . . . 8  |-  N  =  ( norm `  W
)
234, 22nmcl 21677 . . . . . . 7  |-  ( ( W  e. NrmGrp  /\  A  e.  V )  ->  ( N `  A )  e.  RR )
2421, 2, 23syl2anc 671 . . . . . 6  |-  ( ph  ->  ( N `  A
)  e.  RR )
254, 22nmge0 21678 . . . . . . 7  |-  ( ( W  e. NrmGrp  /\  A  e.  V )  ->  0  <_  ( N `  A
) )
2621, 2, 25syl2anc 671 . . . . . 6  |-  ( ph  ->  0  <_  ( N `  A ) )
2724, 26ge0p1rpd 11396 . . . . 5  |-  ( ph  ->  ( ( N `  A )  +  1 )  e.  RR+ )
2827rpred 11369 . . . 4  |-  ( ph  ->  ( ( N `  A )  +  1 )  e.  RR )
29 ngpms 21662 . . . . . 6  |-  ( W  e. NrmGrp  ->  W  e.  MetSp )
3021, 29syl 17 . . . . 5  |-  ( ph  ->  W  e.  MetSp )
31 ipcn.d . . . . . 6  |-  D  =  ( dist `  W
)
324, 31mscl 21524 . . . . 5  |-  ( ( W  e.  MetSp  /\  B  e.  V  /\  Y  e.  V )  ->  ( B D Y )  e.  RR )
3330, 3, 9, 32syl3anc 1276 . . . 4  |-  ( ph  ->  ( B D Y )  e.  RR )
3428, 33remulcld 9696 . . 3  |-  ( ph  ->  ( ( ( N `
 A )  +  1 )  x.  ( B D Y ) )  e.  RR )
3515rehalfcld 10887 . . 3  |-  ( ph  ->  ( R  /  2
)  e.  RR )
3624, 33remulcld 9696 . . . 4  |-  ( ph  ->  ( ( N `  A )  x.  ( B D Y ) )  e.  RR )
37 eqid 2461 . . . . . . . 8  |-  ( -g `  W )  =  (
-g `  W )
385, 4, 37cphsubdi 22234 . . . . . . 7  |-  ( ( W  e.  CPreHil  /\  ( A  e.  V  /\  B  e.  V  /\  Y  e.  V )
)  ->  ( A  .,  ( B ( -g `  W ) Y ) )  =  ( ( A  .,  B )  -  ( A  .,  Y ) ) )
391, 2, 3, 9, 38syl13anc 1278 . . . . . 6  |-  ( ph  ->  ( A  .,  ( B ( -g `  W
) Y ) )  =  ( ( A 
.,  B )  -  ( A  .,  Y ) ) )
4039fveq2d 5891 . . . . 5  |-  ( ph  ->  ( abs `  ( A  .,  ( B (
-g `  W ) Y ) ) )  =  ( abs `  (
( A  .,  B
)  -  ( A 
.,  Y ) ) ) )
41 ngpgrp 21661 . . . . . . . . 9  |-  ( W  e. NrmGrp  ->  W  e.  Grp )
4221, 41syl 17 . . . . . . . 8  |-  ( ph  ->  W  e.  Grp )
434, 37grpsubcl 16782 . . . . . . . 8  |-  ( ( W  e.  Grp  /\  B  e.  V  /\  Y  e.  V )  ->  ( B ( -g `  W ) Y )  e.  V )
4442, 3, 9, 43syl3anc 1276 . . . . . . 7  |-  ( ph  ->  ( B ( -g `  W ) Y )  e.  V )
454, 5, 22ipcau 22260 . . . . . . 7  |-  ( ( W  e.  CPreHil  /\  A  e.  V  /\  ( B ( -g `  W
) Y )  e.  V )  ->  ( abs `  ( A  .,  ( B ( -g `  W
) Y ) ) )  <_  ( ( N `  A )  x.  ( N `  ( B ( -g `  W
) Y ) ) ) )
461, 2, 44, 45syl3anc 1276 . . . . . 6  |-  ( ph  ->  ( abs `  ( A  .,  ( B (
-g `  W ) Y ) ) )  <_  ( ( N `
 A )  x.  ( N `  ( B ( -g `  W
) Y ) ) ) )
4722, 4, 37, 31ngpds 21665 . . . . . . . 8  |-  ( ( W  e. NrmGrp  /\  B  e.  V  /\  Y  e.  V )  ->  ( B D Y )  =  ( N `  ( B ( -g `  W
) Y ) ) )
4821, 3, 9, 47syl3anc 1276 . . . . . . 7  |-  ( ph  ->  ( B D Y )  =  ( N `
 ( B (
-g `  W ) Y ) ) )
4948oveq2d 6330 . . . . . 6  |-  ( ph  ->  ( ( N `  A )  x.  ( B D Y ) )  =  ( ( N `
 A )  x.  ( N `  ( B ( -g `  W
) Y ) ) ) )
5046, 49breqtrrd 4442 . . . . 5  |-  ( ph  ->  ( abs `  ( A  .,  ( B (
-g `  W ) Y ) ) )  <_  ( ( N `
 A )  x.  ( B D Y ) ) )
5140, 50eqbrtrrd 4438 . . . 4  |-  ( ph  ->  ( abs `  (
( A  .,  B
)  -  ( A 
.,  Y ) ) )  <_  ( ( N `  A )  x.  ( B D Y ) ) )
52 msxms 21517 . . . . . . 7  |-  ( W  e.  MetSp  ->  W  e.  *MetSp )
5330, 52syl 17 . . . . . 6  |-  ( ph  ->  W  e.  *MetSp )
544, 31xmsge0 21526 . . . . . 6  |-  ( ( W  e.  *MetSp  /\  B  e.  V  /\  Y  e.  V )  ->  0  <_  ( B D Y ) )
5553, 3, 9, 54syl3anc 1276 . . . . 5  |-  ( ph  ->  0  <_  ( B D Y ) )
5624lep1d 10565 . . . . 5  |-  ( ph  ->  ( N `  A
)  <_  ( ( N `  A )  +  1 ) )
5724, 28, 33, 55, 56lemul1ad 10573 . . . 4  |-  ( ph  ->  ( ( N `  A )  x.  ( B D Y ) )  <_  ( ( ( N `  A )  +  1 )  x.  ( B D Y ) ) )
5817, 36, 34, 51, 57letrd 9817 . . 3  |-  ( ph  ->  ( abs `  (
( A  .,  B
)  -  ( A 
.,  Y ) ) )  <_  ( (
( N `  A
)  +  1 )  x.  ( B D Y ) ) )
59 ipcn.2 . . . . 5  |-  ( ph  ->  ( B D Y )  <  T )
60 ipcn.t . . . . 5  |-  T  =  ( ( R  / 
2 )  /  (
( N `  A
)  +  1 ) )
6159, 60syl6breq 4455 . . . 4  |-  ( ph  ->  ( B D Y )  <  ( ( R  /  2 )  /  ( ( N `
 A )  +  1 ) ) )
6233, 35, 27ltmuldiv2d 11414 . . . 4  |-  ( ph  ->  ( ( ( ( N `  A )  +  1 )  x.  ( B D Y ) )  <  ( R  /  2 )  <->  ( B D Y )  <  (
( R  /  2
)  /  ( ( N `  A )  +  1 ) ) ) )
6361, 62mpbird 240 . . 3  |-  ( ph  ->  ( ( ( N `
 A )  +  1 )  x.  ( B D Y ) )  <  ( R  / 
2 ) )
6417, 34, 35, 58, 63lelttrd 9818 . 2  |-  ( ph  ->  ( abs `  (
( A  .,  B
)  -  ( A 
.,  Y ) ) )  <  ( R  /  2 ) )
6513, 11subcld 10011 . . . 4  |-  ( ph  ->  ( ( A  .,  Y )  -  ( X  .,  Y ) )  e.  CC )
6665abscld 13546 . . 3  |-  ( ph  ->  ( abs `  (
( A  .,  Y
)  -  ( X 
.,  Y ) ) )  e.  RR )
674, 31mscl 21524 . . . . 5  |-  ( ( W  e.  MetSp  /\  A  e.  V  /\  X  e.  V )  ->  ( A D X )  e.  RR )
6830, 2, 8, 67syl3anc 1276 . . . 4  |-  ( ph  ->  ( A D X )  e.  RR )
694, 22nmcl 21677 . . . . . 6  |-  ( ( W  e. NrmGrp  /\  B  e.  V )  ->  ( N `  B )  e.  RR )
7021, 3, 69syl2anc 671 . . . . 5  |-  ( ph  ->  ( N `  B
)  e.  RR )
7114rphalfcld 11381 . . . . . . . 8  |-  ( ph  ->  ( R  /  2
)  e.  RR+ )
7271, 27rpdivcld 11386 . . . . . . 7  |-  ( ph  ->  ( ( R  / 
2 )  /  (
( N `  A
)  +  1 ) )  e.  RR+ )
7360, 72syl5eqel 2543 . . . . . 6  |-  ( ph  ->  T  e.  RR+ )
7473rpred 11369 . . . . 5  |-  ( ph  ->  T  e.  RR )
7570, 74readdcld 9695 . . . 4  |-  ( ph  ->  ( ( N `  B )  +  T
)  e.  RR )
7668, 75remulcld 9696 . . 3  |-  ( ph  ->  ( ( A D X )  x.  (
( N `  B
)  +  T ) )  e.  RR )
774, 22nmcl 21677 . . . . . 6  |-  ( ( W  e. NrmGrp  /\  Y  e.  V )  ->  ( N `  Y )  e.  RR )
7821, 9, 77syl2anc 671 . . . . 5  |-  ( ph  ->  ( N `  Y
)  e.  RR )
7968, 78remulcld 9696 . . . 4  |-  ( ph  ->  ( ( A D X )  x.  ( N `  Y )
)  e.  RR )
805, 4, 37cphsubdir 22233 . . . . . . 7  |-  ( ( W  e.  CPreHil  /\  ( A  e.  V  /\  X  e.  V  /\  Y  e.  V )
)  ->  ( ( A ( -g `  W
) X )  .,  Y )  =  ( ( A  .,  Y
)  -  ( X 
.,  Y ) ) )
811, 2, 8, 9, 80syl13anc 1278 . . . . . 6  |-  ( ph  ->  ( ( A (
-g `  W ) X )  .,  Y
)  =  ( ( A  .,  Y )  -  ( X  .,  Y ) ) )
8281fveq2d 5891 . . . . 5  |-  ( ph  ->  ( abs `  (
( A ( -g `  W ) X ) 
.,  Y ) )  =  ( abs `  (
( A  .,  Y
)  -  ( X 
.,  Y ) ) ) )
834, 37grpsubcl 16782 . . . . . . . 8  |-  ( ( W  e.  Grp  /\  A  e.  V  /\  X  e.  V )  ->  ( A ( -g `  W ) X )  e.  V )
8442, 2, 8, 83syl3anc 1276 . . . . . . 7  |-  ( ph  ->  ( A ( -g `  W ) X )  e.  V )
854, 5, 22ipcau 22260 . . . . . . 7  |-  ( ( W  e.  CPreHil  /\  ( A ( -g `  W
) X )  e.  V  /\  Y  e.  V )  ->  ( abs `  ( ( A ( -g `  W
) X )  .,  Y ) )  <_ 
( ( N `  ( A ( -g `  W
) X ) )  x.  ( N `  Y ) ) )
861, 84, 9, 85syl3anc 1276 . . . . . 6  |-  ( ph  ->  ( abs `  (
( A ( -g `  W ) X ) 
.,  Y ) )  <_  ( ( N `
 ( A (
-g `  W ) X ) )  x.  ( N `  Y
) ) )
8722, 4, 37, 31ngpds 21665 . . . . . . . 8  |-  ( ( W  e. NrmGrp  /\  A  e.  V  /\  X  e.  V )  ->  ( A D X )  =  ( N `  ( A ( -g `  W
) X ) ) )
8821, 2, 8, 87syl3anc 1276 . . . . . . 7  |-  ( ph  ->  ( A D X )  =  ( N `
 ( A (
-g `  W ) X ) ) )
8988oveq1d 6329 . . . . . 6  |-  ( ph  ->  ( ( A D X )  x.  ( N `  Y )
)  =  ( ( N `  ( A ( -g `  W
) X ) )  x.  ( N `  Y ) ) )
9086, 89breqtrrd 4442 . . . . 5  |-  ( ph  ->  ( abs `  (
( A ( -g `  W ) X ) 
.,  Y ) )  <_  ( ( A D X )  x.  ( N `  Y
) ) )
9182, 90eqbrtrrd 4438 . . . 4  |-  ( ph  ->  ( abs `  (
( A  .,  Y
)  -  ( X 
.,  Y ) ) )  <_  ( ( A D X )  x.  ( N `  Y
) ) )
924, 31xmsge0 21526 . . . . . 6  |-  ( ( W  e.  *MetSp  /\  A  e.  V  /\  X  e.  V )  ->  0  <_  ( A D X ) )
9353, 2, 8, 92syl3anc 1276 . . . . 5  |-  ( ph  ->  0  <_  ( A D X ) )
9478, 70resubcld 10074 . . . . . . 7  |-  ( ph  ->  ( ( N `  Y )  -  ( N `  B )
)  e.  RR )
954, 22, 37nm2dif 21686 . . . . . . . . 9  |-  ( ( W  e. NrmGrp  /\  Y  e.  V  /\  B  e.  V )  ->  (
( N `  Y
)  -  ( N `
 B ) )  <_  ( N `  ( Y ( -g `  W
) B ) ) )
9621, 9, 3, 95syl3anc 1276 . . . . . . . 8  |-  ( ph  ->  ( ( N `  Y )  -  ( N `  B )
)  <_  ( N `  ( Y ( -g `  W ) B ) ) )
9722, 4, 37, 31ngpdsr 21666 . . . . . . . . 9  |-  ( ( W  e. NrmGrp  /\  B  e.  V  /\  Y  e.  V )  ->  ( B D Y )  =  ( N `  ( Y ( -g `  W
) B ) ) )
9821, 3, 9, 97syl3anc 1276 . . . . . . . 8  |-  ( ph  ->  ( B D Y )  =  ( N `
 ( Y (
-g `  W ) B ) ) )
9996, 98breqtrrd 4442 . . . . . . 7  |-  ( ph  ->  ( ( N `  Y )  -  ( N `  B )
)  <_  ( B D Y ) )
10033, 74, 59ltled 9808 . . . . . . 7  |-  ( ph  ->  ( B D Y )  <_  T )
10194, 33, 74, 99, 100letrd 9817 . . . . . 6  |-  ( ph  ->  ( ( N `  Y )  -  ( N `  B )
)  <_  T )
10278, 70, 74lesubadd2d 10239 . . . . . 6  |-  ( ph  ->  ( ( ( N `
 Y )  -  ( N `  B ) )  <_  T  <->  ( N `  Y )  <_  (
( N `  B
)  +  T ) ) )
103101, 102mpbid 215 . . . . 5  |-  ( ph  ->  ( N `  Y
)  <_  ( ( N `  B )  +  T ) )
10478, 75, 68, 93, 103lemul2ad 10574 . . . 4  |-  ( ph  ->  ( ( A D X )  x.  ( N `  Y )
)  <_  ( ( A D X )  x.  ( ( N `  B )  +  T
) ) )
10566, 79, 76, 91, 104letrd 9817 . . 3  |-  ( ph  ->  ( abs `  (
( A  .,  Y
)  -  ( X 
.,  Y ) ) )  <_  ( ( A D X )  x.  ( ( N `  B )  +  T
) ) )
106 ipcn.1 . . . . 5  |-  ( ph  ->  ( A D X )  <  U )
107 ipcn.u . . . . 5  |-  U  =  ( ( R  / 
2 )  /  (
( N `  B
)  +  T ) )
108106, 107syl6breq 4455 . . . 4  |-  ( ph  ->  ( A D X )  <  ( ( R  /  2 )  /  ( ( N `
 B )  +  T ) ) )
109 0red 9669 . . . . . 6  |-  ( ph  ->  0  e.  RR )
1104, 22nmge0 21678 . . . . . . 7  |-  ( ( W  e. NrmGrp  /\  B  e.  V )  ->  0  <_  ( N `  B
) )
11121, 3, 110syl2anc 671 . . . . . 6  |-  ( ph  ->  0  <_  ( N `  B ) )
11270, 73ltaddrpd 11399 . . . . . 6  |-  ( ph  ->  ( N `  B
)  <  ( ( N `  B )  +  T ) )
113109, 70, 75, 111, 112lelttrd 9818 . . . . 5  |-  ( ph  ->  0  <  ( ( N `  B )  +  T ) )
114 ltmuldiv 10505 . . . . 5  |-  ( ( ( A D X )  e.  RR  /\  ( R  /  2
)  e.  RR  /\  ( ( ( N `
 B )  +  T )  e.  RR  /\  0  <  ( ( N `  B )  +  T ) ) )  ->  ( (
( A D X )  x.  ( ( N `  B )  +  T ) )  <  ( R  / 
2 )  <->  ( A D X )  <  (
( R  /  2
)  /  ( ( N `  B )  +  T ) ) ) )
11568, 35, 75, 113, 114syl112anc 1280 . . . 4  |-  ( ph  ->  ( ( ( A D X )  x.  ( ( N `  B )  +  T
) )  <  ( R  /  2 )  <->  ( A D X )  <  (
( R  /  2
)  /  ( ( N `  B )  +  T ) ) ) )
116108, 115mpbird 240 . . 3  |-  ( ph  ->  ( ( A D X )  x.  (
( N `  B
)  +  T ) )  <  ( R  /  2 ) )
11766, 76, 35, 105, 116lelttrd 9818 . 2  |-  ( ph  ->  ( abs `  (
( A  .,  Y
)  -  ( X 
.,  Y ) ) )  <  ( R  /  2 ) )
1187, 11, 13, 15, 64, 117abs3lemd 13571 1  |-  ( ph  ->  ( abs `  (
( A  .,  B
)  -  ( X 
.,  Y ) ) )  <  R )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    = wceq 1454    e. wcel 1897   class class class wbr 4415   ` cfv 5600  (class class class)co 6314   CCcc 9562   RRcr 9563   0cc0 9564   1c1 9565    + caddc 9567    x. cmul 9569    < clt 9700    <_ cle 9701    - cmin 9885    / cdiv 10296   2c2 10686   RR+crp 11330   abscabs 13345   Basecbs 15169   .icip 15243   distcds 15247   Grpcgrp 16717   -gcsg 16719   *MetSpcxme 21380   MetSpcmt 21381   normcnm 21639  NrmGrpcngp 21640  NrmModcnlm 21643   CPreHilccph 22192
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-8 1899  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-rep 4528  ax-sep 4538  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6609  ax-cnex 9620  ax-resscn 9621  ax-1cn 9622  ax-icn 9623  ax-addcl 9624  ax-addrcl 9625  ax-mulcl 9626  ax-mulrcl 9627  ax-mulcom 9628  ax-addass 9629  ax-mulass 9630  ax-distr 9631  ax-i2m1 9632  ax-1ne0 9633  ax-1rid 9634  ax-rnegex 9635  ax-rrecex 9636  ax-cnre 9637  ax-pre-lttri 9638  ax-pre-lttrn 9639  ax-pre-ltadd 9640  ax-pre-mulgt0 9641  ax-pre-sup 9642  ax-addf 9643  ax-mulf 9644
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-nel 2635  df-ral 2753  df-rex 2754  df-reu 2755  df-rmo 2756  df-rab 2757  df-v 3058  df-sbc 3279  df-csb 3375  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-pss 3431  df-nul 3743  df-if 3893  df-pw 3964  df-sn 3980  df-pr 3982  df-tp 3984  df-op 3986  df-uni 4212  df-int 4248  df-iun 4293  df-br 4416  df-opab 4475  df-mpt 4476  df-tr 4511  df-eprel 4763  df-id 4767  df-po 4773  df-so 4774  df-fr 4811  df-we 4813  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-pred 5398  df-ord 5444  df-on 5445  df-lim 5446  df-suc 5447  df-iota 5564  df-fun 5602  df-fn 5603  df-f 5604  df-f1 5605  df-fo 5606  df-f1o 5607  df-fv 5608  df-riota 6276  df-ov 6317  df-oprab 6318  df-mpt2 6319  df-om 6719  df-1st 6819  df-2nd 6820  df-tpos 6998  df-wrecs 7053  df-recs 7115  df-rdg 7153  df-1o 7207  df-oadd 7211  df-er 7388  df-map 7499  df-en 7595  df-dom 7596  df-sdom 7597  df-fin 7598  df-sup 7981  df-inf 7982  df-pnf 9702  df-mnf 9703  df-xr 9704  df-ltxr 9705  df-le 9706  df-sub 9887  df-neg 9888  df-div 10297  df-nn 10637  df-2 10695  df-3 10696  df-4 10697  df-5 10698  df-6 10699  df-7 10700  df-8 10701  df-9 10702  df-10 10703  df-n0 10898  df-z 10966  df-dec 11080  df-uz 11188  df-q 11293  df-rp 11331  df-xneg 11437  df-xadd 11438  df-xmul 11439  df-ico 11669  df-fz 11813  df-seq 12245  df-exp 12304  df-cj 13210  df-re 13211  df-im 13212  df-sqrt 13346  df-abs 13347  df-struct 15171  df-ndx 15172  df-slot 15173  df-base 15174  df-sets 15175  df-ress 15176  df-plusg 15251  df-mulr 15252  df-starv 15253  df-sca 15254  df-vsca 15255  df-ip 15256  df-tset 15257  df-ple 15258  df-ds 15260  df-unif 15261  df-0g 15388  df-topgen 15390  df-xrs 15448  df-mgm 16536  df-sgrp 16575  df-mnd 16585  df-mhm 16630  df-grp 16721  df-minusg 16722  df-sbg 16723  df-subg 16862  df-ghm 16929  df-cmn 17480  df-abl 17481  df-mgp 17772  df-ur 17784  df-ring 17830  df-cring 17831  df-oppr 17899  df-dvdsr 17917  df-unit 17918  df-invr 17948  df-dvr 17959  df-rnghom 17991  df-drng 18025  df-subrg 18054  df-staf 18121  df-srng 18122  df-lmod 18141  df-lmhm 18293  df-lvec 18374  df-sra 18443  df-rgmod 18444  df-psmet 19010  df-xmet 19011  df-met 19012  df-bl 19013  df-mopn 19014  df-cnfld 19019  df-phl 19241  df-top 19969  df-bases 19970  df-topon 19971  df-topsp 19972  df-xms 21383  df-ms 21384  df-nm 21645  df-ngp 21646  df-tng 21647  df-nlm 21649  df-clm 22142  df-cph 22194  df-tch 22195
This theorem is referenced by:  ipcnlem1  22264
  Copyright terms: Public domain W3C validator