Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sitgaddlemb Structured version   Visualization version   Unicode version

Theorem sitgaddlemb 29230
Description: Lemma for * sitgadd . (Contributed by Thierry Arnoux, 10-Mar-2019.)
Hypotheses
Ref Expression
sitgval.b  |-  B  =  ( Base `  W
)
sitgval.j  |-  J  =  ( TopOpen `  W )
sitgval.s  |-  S  =  (sigaGen `  J )
sitgval.0  |-  .0.  =  ( 0g `  W )
sitgval.x  |-  .x.  =  ( .s `  W )
sitgval.h  |-  H  =  (RRHom `  (Scalar `  W
) )
sitgval.1  |-  ( ph  ->  W  e.  V )
sitgval.2  |-  ( ph  ->  M  e.  U. ran measures )
sitgadd.1  |-  ( ph  ->  W  e.  TopSp )
sitgadd.2  |-  ( ph  ->  ( Wv  ( H "
( 0 [,) +oo ) ) )  e. SLMod
)
sitgadd.3  |-  ( ph  ->  J  e.  Fre )
sitgadd.4  |-  ( ph  ->  F  e.  dom  ( Wsitg M ) )
sitgadd.5  |-  ( ph  ->  G  e.  dom  ( Wsitg M ) )
sitgadd.6  |-  ( ph  ->  (Scalar `  W )  e. ℝExt  )
sitgadd.7  |-  .+  =  ( +g  `  W )
Assertion
Ref Expression
sitgaddlemb  |-  ( (
ph  /\  p  e.  ( ( ran  F  X.  ran  G )  \  { <.  .0.  ,  .0.  >. } ) )  -> 
( ( H `  ( M `  ( ( `' F " { ( 1st `  p ) } )  i^i  ( `' G " { ( 2nd `  p ) } ) ) ) )  .x.  ( 2nd `  p ) )  e.  B )

Proof of Theorem sitgaddlemb
StepHypRef Expression
1 sitgadd.2 . . 3  |-  ( ph  ->  ( Wv  ( H "
( 0 [,) +oo ) ) )  e. SLMod
)
21adantr 471 . 2  |-  ( (
ph  /\  p  e.  ( ( ran  F  X.  ran  G )  \  { <.  .0.  ,  .0.  >. } ) )  -> 
( Wv  ( H "
( 0 [,) +oo ) ) )  e. SLMod
)
3 simpl 463 . . . . 5  |-  ( (
ph  /\  p  e.  ( ( ran  F  X.  ran  G )  \  { <.  .0.  ,  .0.  >. } ) )  ->  ph )
4 sitgadd.6 . . . . . . . 8  |-  ( ph  ->  (Scalar `  W )  e. ℝExt  )
5 eqid 2462 . . . . . . . . 9  |-  ( Base `  (Scalar `  W )
)  =  ( Base `  (Scalar `  W )
)
65rrhfe 28865 . . . . . . . 8  |-  ( (Scalar `  W )  e. ℝExt  ->  (RRHom `  (Scalar `  W )
) : RR --> ( Base `  (Scalar `  W )
) )
74, 6syl 17 . . . . . . 7  |-  ( ph  ->  (RRHom `  (Scalar `  W
) ) : RR --> ( Base `  (Scalar `  W
) ) )
8 sitgval.h . . . . . . . 8  |-  H  =  (RRHom `  (Scalar `  W
) )
98feq1i 5742 . . . . . . 7  |-  ( H : RR --> ( Base `  (Scalar `  W )
)  <->  (RRHom `  (Scalar `  W
) ) : RR --> ( Base `  (Scalar `  W
) ) )
107, 9sylibr 217 . . . . . 6  |-  ( ph  ->  H : RR --> ( Base `  (Scalar `  W )
) )
11 ffn 5751 . . . . . 6  |-  ( H : RR --> ( Base `  (Scalar `  W )
)  ->  H  Fn  RR )
1210, 11syl 17 . . . . 5  |-  ( ph  ->  H  Fn  RR )
133, 12syl 17 . . . 4  |-  ( (
ph  /\  p  e.  ( ( ran  F  X.  ran  G )  \  { <.  .0.  ,  .0.  >. } ) )  ->  H  Fn  RR )
14 rge0ssre 11769 . . . . 5  |-  ( 0 [,) +oo )  C_  RR
1514a1i 11 . . . 4  |-  ( (
ph  /\  p  e.  ( ( ran  F  X.  ran  G )  \  { <.  .0.  ,  .0.  >. } ) )  -> 
( 0 [,) +oo )  C_  RR )
16 simpr 467 . . . . . . 7  |-  ( (
ph  /\  p  e.  ( ( ran  F  X.  ran  G )  \  { <.  .0.  ,  .0.  >. } ) )  ->  p  e.  ( ( ran  F  X.  ran  G
)  \  { <.  .0.  ,  .0.  >. } ) )
1716eldifad 3428 . . . . . 6  |-  ( (
ph  /\  p  e.  ( ( ran  F  X.  ran  G )  \  { <.  .0.  ,  .0.  >. } ) )  ->  p  e.  ( ran  F  X.  ran  G ) )
18 xp1st 6850 . . . . . 6  |-  ( p  e.  ( ran  F  X.  ran  G )  -> 
( 1st `  p
)  e.  ran  F
)
1917, 18syl 17 . . . . 5  |-  ( (
ph  /\  p  e.  ( ( ran  F  X.  ran  G )  \  { <.  .0.  ,  .0.  >. } ) )  -> 
( 1st `  p
)  e.  ran  F
)
20 xp2nd 6851 . . . . . 6  |-  ( p  e.  ( ran  F  X.  ran  G )  -> 
( 2nd `  p
)  e.  ran  G
)
2117, 20syl 17 . . . . 5  |-  ( (
ph  /\  p  e.  ( ( ran  F  X.  ran  G )  \  { <.  .0.  ,  .0.  >. } ) )  -> 
( 2nd `  p
)  e.  ran  G
)
2216eldifbd 3429 . . . . . . . 8  |-  ( (
ph  /\  p  e.  ( ( ran  F  X.  ran  G )  \  { <.  .0.  ,  .0.  >. } ) )  ->  -.  p  e.  { <.  .0. 
,  .0.  >. } )
23 vex 3060 . . . . . . . . . 10  |-  p  e. 
_V
2423elsnc 4004 . . . . . . . . 9  |-  ( p  e.  { <.  .0.  ,  .0.  >. }  <->  p  =  <.  .0.  ,  .0.  >. )
2524notbii 302 . . . . . . . 8  |-  ( -.  p  e.  { <.  .0. 
,  .0.  >. }  <->  -.  p  =  <.  .0.  ,  .0.  >.
)
2622, 25sylib 201 . . . . . . 7  |-  ( (
ph  /\  p  e.  ( ( ran  F  X.  ran  G )  \  { <.  .0.  ,  .0.  >. } ) )  ->  -.  p  =  <.  .0. 
,  .0.  >. )
27 eqopi 6854 . . . . . . . . . 10  |-  ( ( p  e.  ( ran 
F  X.  ran  G
)  /\  ( ( 1st `  p )  =  .0.  /\  ( 2nd `  p )  =  .0.  ) )  ->  p  =  <.  .0.  ,  .0.  >.
)
2827ex 440 . . . . . . . . 9  |-  ( p  e.  ( ran  F  X.  ran  G )  -> 
( ( ( 1st `  p )  =  .0. 
/\  ( 2nd `  p
)  =  .0.  )  ->  p  =  <.  .0.  ,  .0.  >. ) )
2928con3d 140 . . . . . . . 8  |-  ( p  e.  ( ran  F  X.  ran  G )  -> 
( -.  p  = 
<.  .0.  ,  .0.  >.  ->  -.  ( ( 1st `  p
)  =  .0.  /\  ( 2nd `  p )  =  .0.  ) ) )
3029imp 435 . . . . . . 7  |-  ( ( p  e.  ( ran 
F  X.  ran  G
)  /\  -.  p  =  <.  .0.  ,  .0.  >.
)  ->  -.  (
( 1st `  p
)  =  .0.  /\  ( 2nd `  p )  =  .0.  ) )
3117, 26, 30syl2anc 671 . . . . . 6  |-  ( (
ph  /\  p  e.  ( ( ran  F  X.  ran  G )  \  { <.  .0.  ,  .0.  >. } ) )  ->  -.  ( ( 1st `  p
)  =  .0.  /\  ( 2nd `  p )  =  .0.  ) )
32 ianor 495 . . . . . . 7  |-  ( -.  ( ( 1st `  p
)  =  .0.  /\  ( 2nd `  p )  =  .0.  )  <->  ( -.  ( 1st `  p )  =  .0.  \/  -.  ( 2nd `  p )  =  .0.  ) )
33 df-ne 2635 . . . . . . . 8  |-  ( ( 1st `  p )  =/=  .0.  <->  -.  ( 1st `  p )  =  .0.  )
34 df-ne 2635 . . . . . . . 8  |-  ( ( 2nd `  p )  =/=  .0.  <->  -.  ( 2nd `  p )  =  .0.  )
3533, 34orbi12i 528 . . . . . . 7  |-  ( ( ( 1st `  p
)  =/=  .0.  \/  ( 2nd `  p )  =/=  .0.  )  <->  ( -.  ( 1st `  p )  =  .0.  \/  -.  ( 2nd `  p )  =  .0.  ) )
3632, 35bitr4i 260 . . . . . 6  |-  ( -.  ( ( 1st `  p
)  =  .0.  /\  ( 2nd `  p )  =  .0.  )  <->  ( ( 1st `  p )  =/= 
.0.  \/  ( 2nd `  p )  =/=  .0.  ) )
3731, 36sylib 201 . . . . 5  |-  ( (
ph  /\  p  e.  ( ( ran  F  X.  ran  G )  \  { <.  .0.  ,  .0.  >. } ) )  -> 
( ( 1st `  p
)  =/=  .0.  \/  ( 2nd `  p )  =/=  .0.  ) )
38 sitgval.b . . . . . 6  |-  B  =  ( Base `  W
)
39 sitgval.j . . . . . 6  |-  J  =  ( TopOpen `  W )
40 sitgval.s . . . . . 6  |-  S  =  (sigaGen `  J )
41 sitgval.0 . . . . . 6  |-  .0.  =  ( 0g `  W )
42 sitgval.x . . . . . 6  |-  .x.  =  ( .s `  W )
43 sitgval.1 . . . . . 6  |-  ( ph  ->  W  e.  V )
44 sitgval.2 . . . . . 6  |-  ( ph  ->  M  e.  U. ran measures )
45 sitgadd.4 . . . . . 6  |-  ( ph  ->  F  e.  dom  ( Wsitg M ) )
46 sitgadd.5 . . . . . 6  |-  ( ph  ->  G  e.  dom  ( Wsitg M ) )
47 sitgadd.1 . . . . . 6  |-  ( ph  ->  W  e.  TopSp )
48 sitgadd.3 . . . . . 6  |-  ( ph  ->  J  e.  Fre )
4938, 39, 40, 41, 42, 8, 43, 44, 45, 46, 47, 48sibfinima 29221 . . . . 5  |-  ( ( ( ph  /\  ( 1st `  p )  e. 
ran  F  /\  ( 2nd `  p )  e. 
ran  G )  /\  ( ( 1st `  p
)  =/=  .0.  \/  ( 2nd `  p )  =/=  .0.  ) )  ->  ( M `  ( ( `' F " { ( 1st `  p
) } )  i^i  ( `' G " { ( 2nd `  p
) } ) ) )  e.  ( 0 [,) +oo ) )
503, 19, 21, 37, 49syl31anc 1279 . . . 4  |-  ( (
ph  /\  p  e.  ( ( ran  F  X.  ran  G )  \  { <.  .0.  ,  .0.  >. } ) )  -> 
( M `  (
( `' F " { ( 1st `  p
) } )  i^i  ( `' G " { ( 2nd `  p
) } ) ) )  e.  ( 0 [,) +oo ) )
51 fnfvima 6168 . . . 4  |-  ( ( H  Fn  RR  /\  ( 0 [,) +oo )  C_  RR  /\  ( M `  ( ( `' F " { ( 1st `  p ) } )  i^i  ( `' G " { ( 2nd `  p ) } ) ) )  e.  ( 0 [,) +oo ) )  ->  ( H `  ( M `  ( ( `' F " { ( 1st `  p
) } )  i^i  ( `' G " { ( 2nd `  p
) } ) ) ) )  e.  ( H " ( 0 [,) +oo ) ) )
5213, 15, 50, 51syl3anc 1276 . . 3  |-  ( (
ph  /\  p  e.  ( ( ran  F  X.  ran  G )  \  { <.  .0.  ,  .0.  >. } ) )  -> 
( H `  ( M `  ( ( `' F " { ( 1st `  p ) } )  i^i  ( `' G " { ( 2nd `  p ) } ) ) ) )  e.  ( H
" ( 0 [,) +oo ) ) )
53 imassrn 5198 . . . . . 6  |-  ( H
" ( 0 [,) +oo ) )  C_  ran  H
54 frn 5758 . . . . . . 7  |-  ( H : RR --> ( Base `  (Scalar `  W )
)  ->  ran  H  C_  ( Base `  (Scalar `  W
) ) )
5510, 54syl 17 . . . . . 6  |-  ( ph  ->  ran  H  C_  ( Base `  (Scalar `  W
) ) )
5653, 55syl5ss 3455 . . . . 5  |-  ( ph  ->  ( H " (
0 [,) +oo )
)  C_  ( Base `  (Scalar `  W )
) )
57 eqid 2462 . . . . . 6  |-  ( (Scalar `  W )s  ( H "
( 0 [,) +oo ) ) )  =  ( (Scalar `  W
)s  ( H " (
0 [,) +oo )
) )
5857, 5ressbas2 15229 . . . . 5  |-  ( ( H " ( 0 [,) +oo ) ) 
C_  ( Base `  (Scalar `  W ) )  -> 
( H " (
0 [,) +oo )
)  =  ( Base `  ( (Scalar `  W
)s  ( H " (
0 [,) +oo )
) ) ) )
5956, 58syl 17 . . . 4  |-  ( ph  ->  ( H " (
0 [,) +oo )
)  =  ( Base `  ( (Scalar `  W
)s  ( H " (
0 [,) +oo )
) ) ) )
603, 59syl 17 . . 3  |-  ( (
ph  /\  p  e.  ( ( ran  F  X.  ran  G )  \  { <.  .0.  ,  .0.  >. } ) )  -> 
( H " (
0 [,) +oo )
)  =  ( Base `  ( (Scalar `  W
)s  ( H " (
0 [,) +oo )
) ) ) )
6152, 60eleqtrd 2542 . 2  |-  ( (
ph  /\  p  e.  ( ( ran  F  X.  ran  G )  \  { <.  .0.  ,  .0.  >. } ) )  -> 
( H `  ( M `  ( ( `' F " { ( 1st `  p ) } )  i^i  ( `' G " { ( 2nd `  p ) } ) ) ) )  e.  ( Base `  ( (Scalar `  W
)s  ( H " (
0 [,) +oo )
) ) ) )
6238, 39, 40, 41, 42, 8, 43, 44, 46sibff 29218 . . . . . 6  |-  ( ph  ->  G : U. dom  M --> U. J )
6338, 39tpsuni 20002 . . . . . . 7  |-  ( W  e.  TopSp  ->  B  =  U. J )
64 feq3 5734 . . . . . . 7  |-  ( B  =  U. J  -> 
( G : U. dom  M --> B  <->  G : U. dom  M --> U. J
) )
6547, 63, 643syl 18 . . . . . 6  |-  ( ph  ->  ( G : U. dom  M --> B  <->  G : U. dom  M --> U. J
) )
6662, 65mpbird 240 . . . . 5  |-  ( ph  ->  G : U. dom  M --> B )
67 frn 5758 . . . . 5  |-  ( G : U. dom  M --> B  ->  ran  G  C_  B
)
6866, 67syl 17 . . . 4  |-  ( ph  ->  ran  G  C_  B
)
6968adantr 471 . . 3  |-  ( (
ph  /\  p  e.  ( ( ran  F  X.  ran  G )  \  { <.  .0.  ,  .0.  >. } ) )  ->  ran  G  C_  B )
7069, 21sseldd 3445 . 2  |-  ( (
ph  /\  p  e.  ( ( ran  F  X.  ran  G )  \  { <.  .0.  ,  .0.  >. } ) )  -> 
( 2nd `  p
)  e.  B )
71 fvex 5898 . . . . 5  |-  (RRHom `  (Scalar `  W ) )  e.  _V
728, 71eqeltri 2536 . . . 4  |-  H  e. 
_V
73 imaexg 6757 . . . 4  |-  ( H  e.  _V  ->  ( H " ( 0 [,) +oo ) )  e.  _V )
74 eqid 2462 . . . . 5  |-  ( Wv  ( H " ( 0 [,) +oo ) ) )  =  ( Wv  ( H " ( 0 [,) +oo ) ) )
7574, 38resvbas 28644 . . . 4  |-  ( ( H " ( 0 [,) +oo ) )  e.  _V  ->  B  =  ( Base `  ( Wv  ( H " ( 0 [,) +oo ) ) ) ) )
7672, 73, 75mp2b 10 . . 3  |-  B  =  ( Base `  ( Wv  ( H " ( 0 [,) +oo ) ) ) )
77 eqid 2462 . . . . 5  |-  (Scalar `  W )  =  (Scalar `  W )
7874, 77, 5resvsca 28642 . . . 4  |-  ( ( H " ( 0 [,) +oo ) )  e.  _V  ->  (
(Scalar `  W )s  ( H " ( 0 [,) +oo ) ) )  =  (Scalar `  ( Wv  ( H " ( 0 [,) +oo ) ) ) ) )
7972, 73, 78mp2b 10 . . 3  |-  ( (Scalar `  W )s  ( H "
( 0 [,) +oo ) ) )  =  (Scalar `  ( Wv  ( H " ( 0 [,) +oo ) ) ) )
8074, 42resvvsca 28646 . . . 4  |-  ( ( H " ( 0 [,) +oo ) )  e.  _V  ->  .x.  =  ( .s `  ( Wv  ( H " ( 0 [,) +oo ) ) ) ) )
8172, 73, 80mp2b 10 . . 3  |-  .x.  =  ( .s `  ( Wv  ( H " ( 0 [,) +oo ) ) ) )
82 eqid 2462 . . 3  |-  ( Base `  ( (Scalar `  W
)s  ( H " (
0 [,) +oo )
) ) )  =  ( Base `  (
(Scalar `  W )s  ( H " ( 0 [,) +oo ) ) ) )
8376, 79, 81, 82slmdvscl 28579 . 2  |-  ( ( ( Wv  ( H "
( 0 [,) +oo ) ) )  e. SLMod  /\  ( H `  ( M `  ( ( `' F " { ( 1st `  p ) } )  i^i  ( `' G " { ( 2nd `  p ) } ) ) ) )  e.  ( Base `  ( (Scalar `  W
)s  ( H " (
0 [,) +oo )
) ) )  /\  ( 2nd `  p )  e.  B )  -> 
( ( H `  ( M `  ( ( `' F " { ( 1st `  p ) } )  i^i  ( `' G " { ( 2nd `  p ) } ) ) ) )  .x.  ( 2nd `  p ) )  e.  B )
842, 61, 70, 83syl3anc 1276 1  |-  ( (
ph  /\  p  e.  ( ( ran  F  X.  ran  G )  \  { <.  .0.  ,  .0.  >. } ) )  -> 
( ( H `  ( M `  ( ( `' F " { ( 1st `  p ) } )  i^i  ( `' G " { ( 2nd `  p ) } ) ) ) )  .x.  ( 2nd `  p ) )  e.  B )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 189    \/ wo 374    /\ wa 375    = wceq 1455    e. wcel 1898    =/= wne 2633   _Vcvv 3057    \ cdif 3413    i^i cin 3415    C_ wss 3416   {csn 3980   <.cop 3986   U.cuni 4212    X. cxp 4851   `'ccnv 4852   dom cdm 4853   ran crn 4854   "cima 4856    Fn wfn 5596   -->wf 5597   ` cfv 5601  (class class class)co 6315   1stc1st 6818   2ndc2nd 6819   RRcr 9564   0cc0 9565   +oocpnf 9698   [,)cico 11666   Basecbs 15170   ↾s cress 15171   +g cplusg 15239  Scalarcsca 15242   .scvsca 15243   TopOpenctopn 15369   0gc0g 15387   TopSpctps 19968   Frect1 20372  SLModcslmd 28565   ↾v cresv 28636  RRHomcrrh 28846   ℝExt crrext 28847  sigaGencsigagen 29009  measurescmeas 29066  sitgcsitg 29211
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-rep 4529  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-inf2 8172  ax-ac2 8919  ax-cnex 9621  ax-resscn 9622  ax-1cn 9623  ax-icn 9624  ax-addcl 9625  ax-addrcl 9626  ax-mulcl 9627  ax-mulrcl 9628  ax-mulcom 9629  ax-addass 9630  ax-mulass 9631  ax-distr 9632  ax-i2m1 9633  ax-1ne0 9634  ax-1rid 9635  ax-rnegex 9636  ax-rrecex 9637  ax-cnre 9638  ax-pre-lttri 9639  ax-pre-lttrn 9640  ax-pre-ltadd 9641  ax-pre-mulgt0 9642  ax-pre-sup 9643  ax-addf 9644  ax-mulf 9645
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-fal 1461  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rmo 2757  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-int 4249  df-iun 4294  df-iin 4295  df-disj 4388  df-br 4417  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-se 4813  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  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 6277  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-of 6558  df-om 6720  df-1st 6820  df-2nd 6821  df-supp 6942  df-tpos 6999  df-wrecs 7054  df-recs 7116  df-rdg 7154  df-1o 7208  df-2o 7209  df-oadd 7212  df-er 7389  df-map 7500  df-pm 7501  df-ixp 7549  df-en 7596  df-dom 7597  df-sdom 7598  df-fin 7599  df-fsupp 7910  df-fi 7951  df-sup 7982  df-inf 7983  df-oi 8051  df-card 8399  df-acn 8402  df-ac 8573  df-cda 8624  df-pnf 9703  df-mnf 9704  df-xr 9705  df-ltxr 9706  df-le 9707  df-sub 9888  df-neg 9889  df-div 10298  df-nn 10638  df-2 10696  df-3 10697  df-4 10698  df-5 10699  df-6 10700  df-7 10701  df-8 10702  df-9 10703  df-10 10704  df-n0 10899  df-z 10967  df-dec 11081  df-uz 11189  df-q 11294  df-rp 11332  df-xneg 11438  df-xadd 11439  df-xmul 11440  df-ioo 11668  df-ioc 11669  df-ico 11670  df-icc 11671  df-fz 11814  df-fzo 11947  df-fl 12060  df-mod 12129  df-seq 12246  df-exp 12305  df-fac 12492  df-bc 12520  df-hash 12548  df-shft 13179  df-cj 13211  df-re 13212  df-im 13213  df-sqrt 13347  df-abs 13348  df-limsup 13575  df-clim 13601  df-rlim 13602  df-sum 13802  df-ef 14170  df-sin 14172  df-cos 14173  df-pi 14175  df-dvds 14355  df-gcd 14518  df-numer 14733  df-denom 14734  df-gz 14923  df-struct 15172  df-ndx 15173  df-slot 15174  df-base 15175  df-sets 15176  df-ress 15177  df-plusg 15252  df-mulr 15253  df-starv 15254  df-sca 15255  df-vsca 15256  df-ip 15257  df-tset 15258  df-ple 15259  df-ds 15261  df-unif 15262  df-hom 15263  df-cco 15264  df-rest 15370  df-topn 15371  df-0g 15389  df-gsum 15390  df-topgen 15391  df-pt 15392  df-prds 15395  df-ordt 15448  df-xrs 15449  df-qtop 15455  df-imas 15456  df-xps 15459  df-mre 15541  df-mrc 15542  df-acs 15544  df-ps 16495  df-tsr 16496  df-plusf 16536  df-mgm 16537  df-sgrp 16576  df-mnd 16586  df-mhm 16631  df-submnd 16632  df-grp 16722  df-minusg 16723  df-sbg 16724  df-mulg 16725  df-subg 16863  df-ghm 16930  df-cntz 17020  df-od 17221  df-cmn 17481  df-abl 17482  df-mgp 17773  df-ur 17785  df-ring 17831  df-cring 17832  df-oppr 17900  df-dvdsr 17918  df-unit 17919  df-invr 17949  df-dvr 17960  df-rnghom 17992  df-drng 18026  df-subrg 18055  df-abv 18094  df-lmod 18142  df-scaf 18143  df-sra 18444  df-rgmod 18445  df-nzr 18531  df-psmet 19011  df-xmet 19012  df-met 19013  df-bl 19014  df-mopn 19015  df-fbas 19016  df-fg 19017  df-metu 19018  df-cnfld 19020  df-zring 19089  df-zrh 19124  df-zlm 19125  df-chr 19126  df-refld 19222  df-top 19970  df-bases 19971  df-topon 19972  df-topsp 19973  df-cld 20083  df-ntr 20084  df-cls 20085  df-nei 20163  df-lp 20201  df-perf 20202  df-cn 20292  df-cnp 20293  df-t1 20379  df-haus 20380  df-reg 20381  df-cmp 20451  df-tx 20626  df-hmeo 20819  df-fil 20910  df-fm 21002  df-flim 21003  df-flf 21004  df-fcls 21005  df-cnext 21124  df-tmd 21136  df-tgp 21137  df-tsms 21190  df-trg 21223  df-ust 21264  df-utop 21295  df-uss 21320  df-usp 21321  df-ucn 21340  df-cfilu 21351  df-cusp 21362  df-xms 21384  df-ms 21385  df-tms 21386  df-nm 21646  df-ngp 21647  df-nrg 21649  df-nlm 21650  df-ii 21958  df-cncf 21959  df-cfil 22274  df-cmet 22276  df-cms 22352  df-limc 22870  df-dv 22871  df-log 23555  df-slmd 28566  df-resv 28637  df-qqh 28826  df-rrh 28848  df-rrext 28852  df-esum 28898  df-siga 28979  df-sigagen 29010  df-meas 29067  df-mbfm 29122  df-sitg 29212
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator