Theorem measdivcst 24532

Description: Division of a measure by a positive constant is a measure. (Contributed by Thierry Arnoux, 25-Dec-2016.) (Revised by Thierry Arnoux, 30-Jan-2017.)

Assertion

Ref	Expression
measdivcst	|- ( ( M e. (measures ` S ) /\ A e. RR+ ) -> ( M∘𝑓/𝑐 /𝑒 A ) e. (measures ` S ) )

Proof of Theorem measdivcst

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

Step	Hyp	Ref	Expression
1		ofcfval3 24438	. . 3 |- ( ( M e. (measures ` S ) /\ A e. RR+ ) -> ( M∘𝑓/𝑐 /𝑒 A ) = ( x e. dom M |-> ( ( M ` x ) /𝑒 A ) ) )
2		measfrge0 24510	. . . . . 6 |- ( M e. (measures ` S ) -> M : S --> ( 0 [,] +oo ) )
3		fdm 5554	. . . . . 6 |- ( M : S --> ( 0 [,] +oo ) -> dom M = S )
4	2, 3	syl 16	. . . . 5 |- ( M e. (measures ` S ) -> dom M = S )
5	4	adantr 452	. . . 4 |- ( ( M e. (measures ` S ) /\ A e. RR+ ) -> dom M = S )
6	5	mpteq1d 4250	. . 3 |- ( ( M e. (measures ` S ) /\ A e. RR+ ) -> ( x e. dom M |-> ( ( M ` x ) /𝑒 A ) ) = ( x e. S |-> ( ( M ` x ) /𝑒 A ) ) )
7	1, 6	eqtrd 2436	. 2 |- ( ( M e. (measures ` S ) /\ A e. RR+ ) -> ( M∘𝑓/𝑐 /𝑒 A ) = ( x e. S |-> ( ( M ` x ) /𝑒 A ) ) )
8		measvxrge0 24512	. . . . . 6 |- ( ( M e. (measures ` S ) /\ x e. S ) -> ( M ` x ) e. ( 0 [,] +oo ) )
9	8	adantlr 696	. . . . 5 |- ( ( ( M e. (measures ` S ) /\ A e. RR+ ) /\ x e. S ) -> ( M ` x ) e. ( 0 [,] +oo ) )
10		simplr 732	. . . . 5 |- ( ( ( M e. (measures ` S ) /\ A e. RR+ ) /\ x e. S ) -> A e. RR+ )
11	9, 10	xrpxdivcld 24134	. . . 4 |- ( ( ( M e. (measures ` S ) /\ A e. RR+ ) /\ x e. S ) -> ( ( M ` x ) /𝑒 A ) e. ( 0 [,] +oo ) )
12		eqid 2404	. . . 4 |- ( x e. S |-> ( ( M ` x ) /𝑒 A ) ) = ( x e. S |-> ( ( M ` x ) /𝑒 A ) )
13	11, 12	fmptd 5852	. . 3 |- ( ( M e. (measures ` S ) /\ A e. RR+ ) -> ( x e. S |-> ( ( M ` x ) /𝑒 A ) ) : S --> ( 0 [,] +oo ) )
14		measbase 24504	. . . . . . 7 |- ( M e. (measures ` S ) -> S e. U. ran sigAlgebra )
15		0elsiga 24450	. . . . . . 7 |- ( S e. U. ran sigAlgebra -> (/) e. S )
16	14, 15	syl 16	. . . . . 6 |- ( M e. (measures ` S ) -> (/) e. S )
17	16	adantr 452	. . . . 5 |- ( ( M e. (measures ` S ) /\ A e. RR+ ) -> (/) e. S )
18		ovex 6065	. . . . 5 |- ( ( M ` (/) ) /𝑒 A ) e. _V
19		fveq2 5687	. . . . . . 7 |- ( x = (/) -> ( M ` x ) = ( M ` (/) ) )
20	19	oveq1d 6055	. . . . . 6 |- ( x = (/) -> ( ( M ` x ) /𝑒 A ) = ( ( M ` (/) ) /𝑒 A ) )
21	20, 12	fvmptg 5763	. . . . 5 |- ( ( (/) e. S /\ ( ( M ` (/) ) /𝑒 A ) e. _V ) -> ( ( x e. S |-> ( ( M ` x ) /𝑒 A ) ) ` (/) ) = ( ( M ` (/) ) /𝑒 A ) )
22	17, 18, 21	sylancl 644	. . . 4 |- ( ( M e. (measures ` S ) /\ A e. RR+ ) -> ( ( x e. S |-> ( ( M ` x ) /𝑒 A ) ) ` (/) ) = ( ( M ` (/) ) /𝑒 A ) )
23		measvnul 24513	. . . . . 6 |- ( M e. (measures ` S ) -> ( M ` (/) ) = 0 )
24	23	oveq1d 6055	. . . . 5 |- ( M e. (measures ` S ) -> ( ( M ` (/) ) /𝑒 A ) = ( 0 /𝑒 A ) )
25		xdiv0rp 24129	. . . . 5 |- ( A e. RR+ -> ( 0 /𝑒 A ) = 0 )
26	24, 25	sylan9eq 2456	. . . 4 |- ( ( M e. (measures ` S ) /\ A e. RR+ ) -> ( ( M ` (/) ) /𝑒 A ) = 0 )
27	22, 26	eqtrd 2436	. . 3 |- ( ( M e. (measures ` S ) /\ A e. RR+ ) -> ( ( x e. S |-> ( ( M ` x ) /𝑒 A ) ) ` (/) ) = 0 )
28		simpll 731	. . . . . 6 |- ( ( ( ( M e. (measures ` S ) /\ A e. RR+ ) /\ y e. ~P S ) /\ ( y ~<_ om /\ Disj z e. y z ) ) -> ( M e. (measures ` S ) /\ A e. RR+ ) )
29		simplr 732	. . . . . . 7 |- ( ( ( ( M e. (measures ` S ) /\ A e. RR+ ) /\ y e. ~P S ) /\ ( y ~<_ om /\ Disj z e. y z ) ) -> y e. ~P S )
30		simprl 733	. . . . . . 7 |- ( ( ( ( M e. (measures ` S ) /\ A e. RR+ ) /\ y e. ~P S ) /\ ( y ~<_ om /\ Disj z e. y z ) ) -> y ~<_ om )
31		simprr 734	. . . . . . 7 |- ( ( ( ( M e. (measures ` S ) /\ A e. RR+ ) /\ y e. ~P S ) /\ ( y ~<_ om /\ Disj z e. y z ) ) -> Disj z e. y z )
32	29, 30, 31	3jca 1134	. . . . . 6 |- ( ( ( ( M e. (measures ` S ) /\ A e. RR+ ) /\ y e. ~P S ) /\ ( y ~<_ om /\ Disj z e. y z ) ) -> ( y e. ~P S /\ y ~<_ om /\ Disj z e. y z ) )
33		vex 2919	. . . . . . . . . 10 |- y e. _V
34	33	a1i 11	. . . . . . . . 9 |- ( ( ( M e. (measures ` S ) /\ A e. RR+ ) /\ y e. ~P S ) -> y e. _V )
35		simplll 735	. . . . . . . . . 10 |- ( ( ( ( M e. (measures ` S ) /\ A e. RR+ ) /\ y e. ~P S ) /\ z e. y ) -> M e. (measures ` S ) )
36	33	elpw 3765	. . . . . . . . . . . 12 |- ( y e. ~P S <-> y C_ S )
37		ssel2 3303	. . . . . . . . . . . 12 |- ( ( y C_ S /\ z e. y ) -> z e. S )
38	36, 37	sylanb 459	. . . . . . . . . . 11 |- ( ( y e. ~P S /\ z e. y ) -> z e. S )
39	38	adantll 695	. . . . . . . . . 10 |- ( ( ( ( M e. (measures ` S ) /\ A e. RR+ ) /\ y e. ~P S ) /\ z e. y ) -> z e. S )
40		measvxrge0 24512	. . . . . . . . . 10 |- ( ( M e. (measures ` S ) /\ z e. S ) -> ( M ` z ) e. ( 0 [,] +oo ) )
41	35, 39, 40	syl2anc 643	. . . . . . . . 9 |- ( ( ( ( M e. (measures ` S ) /\ A e. RR+ ) /\ y e. ~P S ) /\ z e. y ) -> ( M ` z ) e. ( 0 [,] +oo ) )
42		simplr 732	. . . . . . . . 9 |- ( ( ( M e. (measures ` S ) /\ A e. RR+ ) /\ y e. ~P S ) -> A e. RR+ )
43	34, 41, 42	esumdivc 24426	. . . . . . . 8 |- ( ( ( M e. (measures ` S ) /\ A e. RR+ ) /\ y e. ~P S ) -> (Σ* z e. y ( M ` z ) /𝑒 A ) = Σ* z e. y ( ( M ` z ) /𝑒 A ) )
44	43	3ad2antr1 1122	. . . . . . 7 |- ( ( ( M e. (measures ` S ) /\ A e. RR+ ) /\ ( y e. ~P S /\ y ~<_ om /\ Disj z e. y z ) ) -> (Σ* z e. y ( M ` z ) /𝑒 A ) = Σ* z e. y ( ( M ` z ) /𝑒 A ) )
45	14	ad2antrr 707	. . . . . . . . . 10 |- ( ( ( M e. (measures ` S ) /\ A e. RR+ ) /\ ( y e. ~P S /\ y ~<_ om /\ Disj z e. y z ) ) -> S e. U. ran sigAlgebra )
46		simpr1 963	. . . . . . . . . 10 |- ( ( ( M e. (measures ` S ) /\ A e. RR+ ) /\ ( y e. ~P S /\ y ~<_ om /\ Disj z e. y z ) ) -> y e. ~P S )
47		simpr2 964	. . . . . . . . . 10 |- ( ( ( M e. (measures ` S ) /\ A e. RR+ ) /\ ( y e. ~P S /\ y ~<_ om /\ Disj z e. y z ) ) -> y ~<_ om )
48		sigaclcu 24453	. . . . . . . . . 10 |- ( ( S e. U. ran sigAlgebra /\ y e. ~P S /\ y ~<_ om ) -> U. y e. S )
49	45, 46, 47, 48	syl3anc 1184	. . . . . . . . 9 |- ( ( ( M e. (measures ` S ) /\ A e. RR+ ) /\ ( y e. ~P S /\ y ~<_ om /\ Disj z e. y z ) ) -> U. y e. S )
50		fveq2 5687	. . . . . . . . . . 11 |- ( x = U. y -> ( M ` x ) = ( M ` U. y ) )
51	50	oveq1d 6055	. . . . . . . . . 10 |- ( x = U. y -> ( ( M ` x ) /𝑒 A ) = ( ( M ` U. y ) /𝑒 A ) )
52		ovex 6065	. . . . . . . . . 10 |- ( ( M ` x ) /𝑒 A ) e. _V
53	51, 12, 52	fvmpt3i 5768	. . . . . . . . 9 |- ( U. y e. S -> ( ( x e. S |-> ( ( M ` x ) /𝑒 A ) ) ` U. y ) = ( ( M ` U. y ) /𝑒 A ) )
54	49, 53	syl 16	. . . . . . . 8 |- ( ( ( M e. (measures ` S ) /\ A e. RR+ ) /\ ( y e. ~P S /\ y ~<_ om /\ Disj z e. y z ) ) -> ( ( x e. S |-> ( ( M ` x ) /𝑒 A ) ) ` U. y ) = ( ( M ` U. y ) /𝑒 A ) )
55		simpll 731	. . . . . . . . . 10 |- ( ( ( M e. (measures ` S ) /\ A e. RR+ ) /\ ( y e. ~P S /\ y ~<_ om /\ Disj z e. y z ) ) -> M e. (measures ` S ) )
56		simpr3 965	. . . . . . . . . 10 |- ( ( ( M e. (measures ` S ) /\ A e. RR+ ) /\ ( y e. ~P S /\ y ~<_ om /\ Disj z e. y z ) ) -> Disj z e. y z )
57		measvun 24516	. . . . . . . . . 10 |- ( ( M e. (measures ` S ) /\ y e. ~P S /\ ( y ~<_ om /\ Disj z e. y z ) ) -> ( M ` U. y ) = Σ* z e. y ( M ` z ) )
58	55, 46, 47, 56, 57	syl112anc 1188	. . . . . . . . 9 |- ( ( ( M e. (measures ` S ) /\ A e. RR+ ) /\ ( y e. ~P S /\ y ~<_ om /\ Disj z e. y z ) ) -> ( M ` U. y ) = Σ* z e. y ( M ` z ) )
59	58	oveq1d 6055	. . . . . . . 8 |- ( ( ( M e. (measures ` S ) /\ A e. RR+ ) /\ ( y e. ~P S /\ y ~<_ om /\ Disj z e. y z ) ) -> ( ( M ` U. y ) /𝑒 A ) = (Σ* z e. y ( M ` z ) /𝑒 A ) )
60	54, 59	eqtrd 2436	. . . . . . 7 |- ( ( ( M e. (measures ` S ) /\ A e. RR+ ) /\ ( y e. ~P S /\ y ~<_ om /\ Disj z e. y z ) ) -> ( ( x e. S |-> ( ( M ` x ) /𝑒 A ) ) ` U. y ) = (Σ* z e. y ( M ` z ) /𝑒 A ) )
61		fveq2 5687	. . . . . . . . . . . 12 |- ( x = z -> ( M ` x ) = ( M ` z ) )
62	61	oveq1d 6055	. . . . . . . . . . 11 |- ( x = z -> ( ( M ` x ) /𝑒 A ) = ( ( M ` z ) /𝑒 A ) )
63	62, 12, 52	fvmpt3i 5768	. . . . . . . . . 10 |- ( z e. S -> ( ( x e. S |-> ( ( M ` x ) /𝑒 A ) ) ` z ) = ( ( M ` z ) /𝑒 A ) )
64	38, 63	syl 16	. . . . . . . . 9 |- ( ( y e. ~P S /\ z e. y ) -> ( ( x e. S |-> ( ( M ` x ) /𝑒 A ) ) ` z ) = ( ( M ` z ) /𝑒 A ) )
65	64	esumeq2dv 24388	. . . . . . . 8 |- ( y e. ~P S -> Σ* z e. y ( ( x e. S |-> ( ( M ` x ) /𝑒 A ) ) ` z ) = Σ* z e. y ( ( M ` z ) /𝑒 A ) )
66	46, 65	syl 16	. . . . . . 7 |- ( ( ( M e. (measures ` S ) /\ A e. RR+ ) /\ ( y e. ~P S /\ y ~<_ om /\ Disj z e. y z ) ) -> Σ* z e. y ( ( x e. S |-> ( ( M ` x ) /𝑒 A ) ) ` z ) = Σ* z e. y ( ( M ` z ) /𝑒 A ) )
67	44, 60, 66	3eqtr4d 2446	. . . . . 6 |- ( ( ( M e. (measures ` S ) /\ A e. RR+ ) /\ ( y e. ~P S /\ y ~<_ om /\ Disj z e. y z ) ) -> ( ( x e. S |-> ( ( M ` x ) /𝑒 A ) ) ` U. y ) = Σ* z e. y ( ( x e. S |-> ( ( M ` x ) /𝑒 A ) ) ` z ) )
68	28, 32, 67	syl2anc 643	. . . . 5 |- ( ( ( ( M e. (measures ` S ) /\ A e. RR+ ) /\ y e. ~P S ) /\ ( y ~<_ om /\ Disj z e. y z ) ) -> ( ( x e. S |-> ( ( M ` x ) /𝑒 A ) ) ` U. y ) = Σ* z e. y ( ( x e. S |-> ( ( M ` x ) /𝑒 A ) ) ` z ) )
69	68	ex 424	. . . 4 |- ( ( ( M e. (measures ` S ) /\ A e. RR+ ) /\ y e. ~P S ) -> ( ( y ~<_ om /\ Disj z e. y z ) -> ( ( x e. S |-> ( ( M ` x ) /𝑒 A ) ) ` U. y ) = Σ* z e. y ( ( x e. S |-> ( ( M ` x ) /𝑒 A ) ) ` z ) ) )
70	69	ralrimiva 2749	. . 3 |- ( ( M e. (measures ` S ) /\ A e. RR+ ) -> A. y e. ~P S ( ( y ~<_ om /\ Disj z e. y z ) -> ( ( x e. S |-> ( ( M ` x ) /𝑒 A ) ) ` U. y ) = Σ* z e. y ( ( x e. S |-> ( ( M ` x ) /𝑒 A ) ) ` z ) ) )
71		ismeas 24506	. . . . . 6 |- ( S e. U. ran sigAlgebra -> ( ( x e. S |-> ( ( M ` x ) /𝑒 A ) ) e. (measures ` S ) <-> ( ( x e. S |-> ( ( M ` x ) /𝑒 A ) ) : S --> ( 0 [,] +oo ) /\ ( ( x e. S |-> ( ( M ` x ) /𝑒 A ) ) ` (/) ) = 0 /\ A. y e. ~P S ( ( y ~<_ om /\ Disj z e. y z ) -> ( ( x e. S |-> ( ( M ` x ) /𝑒 A ) ) ` U. y ) = Σ* z e. y ( ( x e. S |-> ( ( M ` x ) /𝑒 A ) ) ` z ) ) ) ) )
72	14, 71	syl 16	. . . . 5 |- ( M e. (measures ` S ) -> ( ( x e. S |-> ( ( M ` x ) /𝑒 A ) ) e. (measures ` S ) <-> ( ( x e. S |-> ( ( M ` x ) /𝑒 A ) ) : S --> ( 0 [,] +oo ) /\ ( ( x e. S |-> ( ( M ` x ) /𝑒 A ) ) ` (/) ) = 0 /\ A. y e. ~P S ( ( y ~<_ om /\ Disj z e. y z ) -> ( ( x e. S |-> ( ( M ` x ) /𝑒 A ) ) ` U. y ) = Σ* z e. y ( ( x e. S |-> ( ( M ` x ) /𝑒 A ) ) ` z ) ) ) ) )
73	72	biimprd 215	. . . 4 |- ( M e. (measures ` S ) -> ( ( ( x e. S |-> ( ( M ` x ) /𝑒 A ) ) : S --> ( 0 [,] +oo ) /\ ( ( x e. S |-> ( ( M ` x ) /𝑒 A ) ) ` (/) ) = 0 /\ A. y e. ~P S ( ( y ~<_ om /\ Disj z e. y z ) -> ( ( x e. S |-> ( ( M ` x ) /𝑒 A ) ) ` U. y ) = Σ* z e. y ( ( x e. S |-> ( ( M ` x ) /𝑒 A ) ) ` z ) ) ) -> ( x e. S |-> ( ( M ` x ) /𝑒 A ) ) e. (measures ` S ) ) )
74	73	adantr 452	. . 3 |- ( ( M e. (measures ` S ) /\ A e. RR+ ) -> ( ( ( x e. S |-> ( ( M ` x ) /𝑒 A ) ) : S --> ( 0 [,] +oo ) /\ ( ( x e. S |-> ( ( M ` x ) /𝑒 A ) ) ` (/) ) = 0 /\ A. y e. ~P S ( ( y ~<_ om /\ Disj z e. y z ) -> ( ( x e. S |-> ( ( M ` x ) /𝑒 A ) ) ` U. y ) = Σ* z e. y ( ( x e. S |-> ( ( M ` x ) /𝑒 A ) ) ` z ) ) ) -> ( x e. S |-> ( ( M ` x ) /𝑒 A ) ) e. (measures ` S ) ) )
75	13, 27, 70, 74	mp3and 1282	. 2 |- ( ( M e. (measures ` S ) /\ A e. RR+ ) -> ( x e. S |-> ( ( M ` x ) /𝑒 A ) ) e. (measures ` S ) )
76	7, 75	eqeltrd 2478	1 |- ( ( M e. (measures ` S ) /\ A e. RR+ ) -> ( M∘𝑓/𝑐 /𝑒 A ) e. (measures ` S ) )

Syntax hints:   -> wi 4   <-> wb 177   /\ wa 359   /\ w3a 936   = wceq 1649   e. wcel 1721   A.wral 2666   _Vcvv 2916   C_ wss 3280   (/)c0 3588   ~Pcpw 3759   U.cuni 3975  Disj wdisj 4142   class class class wbr 4172   e. cmpt 4226   omcom 4804   dom cdm 4837   ran crn 4838   -->wf 5409   ` cfv 5413  (class class class)co 6040   ~<_ cdom 7066   0cc0 8946   +oocpnf 9073   RR+crp 10568   [,]cicc 10875   /_𝑒 cxdiv 24116  Σ^*cesum 24377  ∘_𝑓/𝑐cofc 24431  sigAlgebracsiga 24443  measurescmeas 24502

This theorem is referenced by:  probfinmeasb  24640

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023  ax-pre-sup 9024

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-iin 4056  df-disj 4143  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-se 4502  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-isom 5422  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-of 6264  df-1st 6308  df-2nd 6309  df-riota 6508  df-recs 6592  df-rdg 6627  df-1o 6683  df-oadd 6687  df-er 6864  df-map 6979  df-en 7069  df-dom 7070  df-sdom 7071  df-fin 7072  df-fi 7374  df-sup 7404  df-oi 7435  df-card 7782  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-div 9634  df-nn 9957  df-2 10014  df-3 10015  df-4 10016  df-5 10017  df-6 10018  df-7 10019  df-8 10020  df-9 10021  df-10 10022  df-n0 10178  df-z 10239  df-dec 10339  df-uz 10445  df-q 10531  df-rp 10569  df-xneg 10666  df-xadd 10667  df-xmul 10668  df-ioo 10876  df-ioc 10877  df-ico 10878  df-icc 10879  df-fz 11000  df-fzo 11091  df-seq 11279  df-hash 11574  df-struct 13426  df-ndx 13427  df-slot 13428  df-base 13429  df-sets 13430  df-ress 13431  df-plusg 13497  df-mulr 13498  df-tset 13503  df-ple 13504  df-ds 13506  df-rest 13605  df-topn 13606  df-topgen 13622  df-ordt 13680  df-xrs 13681  df-0g 13682  df-gsum 13683  df-mre 13766  df-mrc 13767  df-acs 13769  df-ps 14584  df-tsr 14585  df-mnd 14645  df-mhm 14693  df-submnd 14694  df-cntz 15071  df-cmn 15369  df-fbas 16654  df-fg 16655  df-top 16918  df-bases 16920  df-topon 16921  df-topsp 16922  df-ntr 17039  df-nei 17117  df-cn 17245  df-cnp 17246  df-haus 17333  df-fil 17831  df-fm 17923  df-flim 17924  df-flf 17925  df-tsms 18109  df-xdiv 24117  df-esum 24378  df-ofc 24432  df-siga 24444  df-meas 24503