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

Theorem volmeas 31550
Description: The Lebesgue measure is a measure. (Contributed by Thierry Arnoux, 16-Oct-2017.)
Assertion
Ref Expression
volmeas vol ∈ (measures‘dom vol)

Proof of Theorem volmeas
Dummy variables 𝑓 𝑛 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 volf 24139 . 2 vol:dom vol⟶(0[,]+∞)
2 fvssunirn 6690 . . . . . 6 (sigAlgebra‘ℝ) ⊆ ran sigAlgebra
3 dmvlsiga 31448 . . . . . 6 dom vol ∈ (sigAlgebra‘ℝ)
42, 3sselii 3950 . . . . 5 dom vol ∈ ran sigAlgebra
5 0elsiga 31433 . . . . 5 (dom vol ∈ ran sigAlgebra → ∅ ∈ dom vol)
64, 5ax-mp 5 . . . 4 ∅ ∈ dom vol
7 mblvol 24140 . . . 4 (∅ ∈ dom vol → (vol‘∅) = (vol*‘∅))
86, 7ax-mp 5 . . 3 (vol‘∅) = (vol*‘∅)
9 ovol0 24103 . . 3 (vol*‘∅) = 0
108, 9eqtri 2847 . 2 (vol‘∅) = 0
11 simpr 488 . . . . . 6 (((𝑥 ∈ 𝒫 dom vol ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑥 ∈ Fin) → 𝑥 ∈ Fin)
12 nfv 1916 . . . . . . . . 9 𝑦 𝑥 ∈ 𝒫 dom vol
13 nfv 1916 . . . . . . . . . 10 𝑦 𝑥 ≼ ω
14 nfdisj1 5031 . . . . . . . . . 10 𝑦Disj 𝑦𝑥 𝑦
1513, 14nfan 1901 . . . . . . . . 9 𝑦(𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)
1612, 15nfan 1901 . . . . . . . 8 𝑦(𝑥 ∈ 𝒫 dom vol ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦))
17 nfv 1916 . . . . . . . 8 𝑦 𝑥 ∈ Fin
1816, 17nfan 1901 . . . . . . 7 𝑦((𝑥 ∈ 𝒫 dom vol ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑥 ∈ Fin)
19 elpwi 4531 . . . . . . . . . 10 (𝑥 ∈ 𝒫 dom vol → 𝑥 ⊆ dom vol)
2019ad3antrrr 729 . . . . . . . . 9 ((((𝑥 ∈ 𝒫 dom vol ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑥 ∈ Fin) ∧ 𝑦𝑥) → 𝑥 ⊆ dom vol)
21 simpr 488 . . . . . . . . 9 ((((𝑥 ∈ 𝒫 dom vol ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑥 ∈ Fin) ∧ 𝑦𝑥) → 𝑦𝑥)
2220, 21sseldd 3954 . . . . . . . 8 ((((𝑥 ∈ 𝒫 dom vol ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑥 ∈ Fin) ∧ 𝑦𝑥) → 𝑦 ∈ dom vol)
2322ex 416 . . . . . . 7 (((𝑥 ∈ 𝒫 dom vol ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑥 ∈ Fin) → (𝑦𝑥𝑦 ∈ dom vol))
2418, 23ralrimi 3210 . . . . . 6 (((𝑥 ∈ 𝒫 dom vol ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑥 ∈ Fin) → ∀𝑦𝑥 𝑦 ∈ dom vol)
25 simplrr 777 . . . . . 6 (((𝑥 ∈ 𝒫 dom vol ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑥 ∈ Fin) → Disj 𝑦𝑥 𝑦)
26 uniiun 4968 . . . . . . . 8 𝑥 = 𝑦𝑥 𝑦
2726fveq2i 6664 . . . . . . 7 (vol‘ 𝑥) = (vol‘ 𝑦𝑥 𝑦)
28 volfiniune 31549 . . . . . . 7 ((𝑥 ∈ Fin ∧ ∀𝑦𝑥 𝑦 ∈ dom vol ∧ Disj 𝑦𝑥 𝑦) → (vol‘ 𝑦𝑥 𝑦) = Σ*𝑦𝑥(vol‘𝑦))
2927, 28syl5eq 2871 . . . . . 6 ((𝑥 ∈ Fin ∧ ∀𝑦𝑥 𝑦 ∈ dom vol ∧ Disj 𝑦𝑥 𝑦) → (vol‘ 𝑥) = Σ*𝑦𝑥(vol‘𝑦))
3011, 24, 25, 29syl3anc 1368 . . . . 5 (((𝑥 ∈ 𝒫 dom vol ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑥 ∈ Fin) → (vol‘ 𝑥) = Σ*𝑦𝑥(vol‘𝑦))
31 bren 8514 . . . . . 6 (ℕ ≈ 𝑥 ↔ ∃𝑓 𝑓:ℕ–1-1-onto𝑥)
32 nfv 1916 . . . . . . . . . . . 12 𝑛(𝑥 ∈ 𝒫 dom vol ∧ 𝑓:ℕ–1-1-onto𝑥)
33 nfcv 2982 . . . . . . . . . . . 12 𝑛(vol‘𝑦)
34 nfcv 2982 . . . . . . . . . . . 12 𝑦(vol‘(𝑓𝑛))
35 nfcv 2982 . . . . . . . . . . . 12 𝑛𝑥
36 nfcv 2982 . . . . . . . . . . . 12 𝑛
37 nfcv 2982 . . . . . . . . . . . 12 𝑛𝑓
38 fveq2 6661 . . . . . . . . . . . 12 (𝑦 = (𝑓𝑛) → (vol‘𝑦) = (vol‘(𝑓𝑛)))
39 simpl 486 . . . . . . . . . . . 12 ((𝑥 ∈ 𝒫 dom vol ∧ 𝑓:ℕ–1-1-onto𝑥) → 𝑥 ∈ 𝒫 dom vol)
40 simpr 488 . . . . . . . . . . . 12 ((𝑥 ∈ 𝒫 dom vol ∧ 𝑓:ℕ–1-1-onto𝑥) → 𝑓:ℕ–1-1-onto𝑥)
41 eqidd 2825 . . . . . . . . . . . 12 (((𝑥 ∈ 𝒫 dom vol ∧ 𝑓:ℕ–1-1-onto𝑥) ∧ 𝑛 ∈ ℕ) → (𝑓𝑛) = (𝑓𝑛))
421a1i 11 . . . . . . . . . . . . 13 (((𝑥 ∈ 𝒫 dom vol ∧ 𝑓:ℕ–1-1-onto𝑥) ∧ 𝑦𝑥) → vol:dom vol⟶(0[,]+∞))
4339, 19syl 17 . . . . . . . . . . . . . 14 ((𝑥 ∈ 𝒫 dom vol ∧ 𝑓:ℕ–1-1-onto𝑥) → 𝑥 ⊆ dom vol)
4443sselda 3953 . . . . . . . . . . . . 13 (((𝑥 ∈ 𝒫 dom vol ∧ 𝑓:ℕ–1-1-onto𝑥) ∧ 𝑦𝑥) → 𝑦 ∈ dom vol)
4542, 44ffvelrnd 6843 . . . . . . . . . . . 12 (((𝑥 ∈ 𝒫 dom vol ∧ 𝑓:ℕ–1-1-onto𝑥) ∧ 𝑦𝑥) → (vol‘𝑦) ∈ (0[,]+∞))
4632, 33, 34, 35, 36, 37, 38, 39, 40, 41, 45esumf1o 31369 . . . . . . . . . . 11 ((𝑥 ∈ 𝒫 dom vol ∧ 𝑓:ℕ–1-1-onto𝑥) → Σ*𝑦𝑥(vol‘𝑦) = Σ*𝑛 ∈ ℕ(vol‘(𝑓𝑛)))
4746adantlr 714 . . . . . . . . . 10 (((𝑥 ∈ 𝒫 dom vol ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑓:ℕ–1-1-onto𝑥) → Σ*𝑦𝑥(vol‘𝑦) = Σ*𝑛 ∈ ℕ(vol‘(𝑓𝑛)))
4819ad3antrrr 729 . . . . . . . . . . . . 13 ((((𝑥 ∈ 𝒫 dom vol ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑓:ℕ–1-1-onto𝑥) ∧ 𝑛 ∈ ℕ) → 𝑥 ⊆ dom vol)
49 f1of 6606 . . . . . . . . . . . . . . 15 (𝑓:ℕ–1-1-onto𝑥𝑓:ℕ⟶𝑥)
5049adantl 485 . . . . . . . . . . . . . 14 (((𝑥 ∈ 𝒫 dom vol ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑓:ℕ–1-1-onto𝑥) → 𝑓:ℕ⟶𝑥)
5150ffvelrnda 6842 . . . . . . . . . . . . 13 ((((𝑥 ∈ 𝒫 dom vol ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑓:ℕ–1-1-onto𝑥) ∧ 𝑛 ∈ ℕ) → (𝑓𝑛) ∈ 𝑥)
5248, 51sseldd 3954 . . . . . . . . . . . 12 ((((𝑥 ∈ 𝒫 dom vol ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑓:ℕ–1-1-onto𝑥) ∧ 𝑛 ∈ ℕ) → (𝑓𝑛) ∈ dom vol)
5352ralrimiva 3177 . . . . . . . . . . 11 (((𝑥 ∈ 𝒫 dom vol ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑓:ℕ–1-1-onto𝑥) → ∀𝑛 ∈ ℕ (𝑓𝑛) ∈ dom vol)
54 simpr 488 . . . . . . . . . . . 12 (((𝑥 ∈ 𝒫 dom vol ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑓:ℕ–1-1-onto𝑥) → 𝑓:ℕ–1-1-onto𝑥)
55 simplrr 777 . . . . . . . . . . . 12 (((𝑥 ∈ 𝒫 dom vol ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑓:ℕ–1-1-onto𝑥) → Disj 𝑦𝑥 𝑦)
56 id 22 . . . . . . . . . . . . . 14 (𝑓:ℕ–1-1-onto𝑥𝑓:ℕ–1-1-onto𝑥)
57 simpr 488 . . . . . . . . . . . . . 14 ((𝑓:ℕ–1-1-onto𝑥𝑦 = (𝑓𝑛)) → 𝑦 = (𝑓𝑛))
5856, 57disjrdx 30355 . . . . . . . . . . . . 13 (𝑓:ℕ–1-1-onto𝑥 → (Disj 𝑛 ∈ ℕ (𝑓𝑛) ↔ Disj 𝑦𝑥 𝑦))
5958biimpar 481 . . . . . . . . . . . 12 ((𝑓:ℕ–1-1-onto𝑥Disj 𝑦𝑥 𝑦) → Disj 𝑛 ∈ ℕ (𝑓𝑛))
6054, 55, 59syl2anc 587 . . . . . . . . . . 11 (((𝑥 ∈ 𝒫 dom vol ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑓:ℕ–1-1-onto𝑥) → Disj 𝑛 ∈ ℕ (𝑓𝑛))
61 voliune 31548 . . . . . . . . . . 11 ((∀𝑛 ∈ ℕ (𝑓𝑛) ∈ dom vol ∧ Disj 𝑛 ∈ ℕ (𝑓𝑛)) → (vol‘ 𝑛 ∈ ℕ (𝑓𝑛)) = Σ*𝑛 ∈ ℕ(vol‘(𝑓𝑛)))
6253, 60, 61syl2anc 587 . . . . . . . . . 10 (((𝑥 ∈ 𝒫 dom vol ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑓:ℕ–1-1-onto𝑥) → (vol‘ 𝑛 ∈ ℕ (𝑓𝑛)) = Σ*𝑛 ∈ ℕ(vol‘(𝑓𝑛)))
63 f1ofo 6613 . . . . . . . . . . . . . 14 (𝑓:ℕ–1-1-onto𝑥𝑓:ℕ–onto𝑥)
6463, 57iunrdx 30329 . . . . . . . . . . . . 13 (𝑓:ℕ–1-1-onto𝑥 𝑛 ∈ ℕ (𝑓𝑛) = 𝑦𝑥 𝑦)
6564, 26syl6eqr 2877 . . . . . . . . . . . 12 (𝑓:ℕ–1-1-onto𝑥 𝑛 ∈ ℕ (𝑓𝑛) = 𝑥)
6665fveq2d 6665 . . . . . . . . . . 11 (𝑓:ℕ–1-1-onto𝑥 → (vol‘ 𝑛 ∈ ℕ (𝑓𝑛)) = (vol‘ 𝑥))
6766adantl 485 . . . . . . . . . 10 (((𝑥 ∈ 𝒫 dom vol ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑓:ℕ–1-1-onto𝑥) → (vol‘ 𝑛 ∈ ℕ (𝑓𝑛)) = (vol‘ 𝑥))
6847, 62, 673eqtr2rd 2866 . . . . . . . . 9 (((𝑥 ∈ 𝒫 dom vol ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ 𝑓:ℕ–1-1-onto𝑥) → (vol‘ 𝑥) = Σ*𝑦𝑥(vol‘𝑦))
6968ex 416 . . . . . . . 8 ((𝑥 ∈ 𝒫 dom vol ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) → (𝑓:ℕ–1-1-onto𝑥 → (vol‘ 𝑥) = Σ*𝑦𝑥(vol‘𝑦)))
7069exlimdv 1935 . . . . . . 7 ((𝑥 ∈ 𝒫 dom vol ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) → (∃𝑓 𝑓:ℕ–1-1-onto𝑥 → (vol‘ 𝑥) = Σ*𝑦𝑥(vol‘𝑦)))
7170imp 410 . . . . . 6 (((𝑥 ∈ 𝒫 dom vol ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ ∃𝑓 𝑓:ℕ–1-1-onto𝑥) → (vol‘ 𝑥) = Σ*𝑦𝑥(vol‘𝑦))
7231, 71sylan2b 596 . . . . 5 (((𝑥 ∈ 𝒫 dom vol ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) ∧ ℕ ≈ 𝑥) → (vol‘ 𝑥) = Σ*𝑦𝑥(vol‘𝑦))
73 brdom2 8535 . . . . . . . 8 (𝑥 ≼ ω ↔ (𝑥 ≺ ω ∨ 𝑥 ≈ ω))
7473biimpi 219 . . . . . . 7 (𝑥 ≼ ω → (𝑥 ≺ ω ∨ 𝑥 ≈ ω))
75 isfinite2 8773 . . . . . . . 8 (𝑥 ≺ ω → 𝑥 ∈ Fin)
76 ensymb 8553 . . . . . . . . 9 (𝑥 ≈ ω ↔ ω ≈ 𝑥)
77 nnenom 13352 . . . . . . . . . 10 ℕ ≈ ω
78 entr 8557 . . . . . . . . . 10 ((ℕ ≈ ω ∧ ω ≈ 𝑥) → ℕ ≈ 𝑥)
7977, 78mpan 689 . . . . . . . . 9 (ω ≈ 𝑥 → ℕ ≈ 𝑥)
8076, 79sylbi 220 . . . . . . . 8 (𝑥 ≈ ω → ℕ ≈ 𝑥)
8175, 80orim12i 906 . . . . . . 7 ((𝑥 ≺ ω ∨ 𝑥 ≈ ω) → (𝑥 ∈ Fin ∨ ℕ ≈ 𝑥))
8274, 81syl 17 . . . . . 6 (𝑥 ≼ ω → (𝑥 ∈ Fin ∨ ℕ ≈ 𝑥))
8382ad2antrl 727 . . . . 5 ((𝑥 ∈ 𝒫 dom vol ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) → (𝑥 ∈ Fin ∨ ℕ ≈ 𝑥))
8430, 72, 83mpjaodan 956 . . . 4 ((𝑥 ∈ 𝒫 dom vol ∧ (𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦)) → (vol‘ 𝑥) = Σ*𝑦𝑥(vol‘𝑦))
8584ex 416 . . 3 (𝑥 ∈ 𝒫 dom vol → ((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → (vol‘ 𝑥) = Σ*𝑦𝑥(vol‘𝑦)))
8685rgen 3143 . 2 𝑥 ∈ 𝒫 dom vol((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → (vol‘ 𝑥) = Σ*𝑦𝑥(vol‘𝑦))
87 ismeas 31518 . . 3 (dom vol ∈ ran sigAlgebra → (vol ∈ (measures‘dom vol) ↔ (vol:dom vol⟶(0[,]+∞) ∧ (vol‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 dom vol((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → (vol‘ 𝑥) = Σ*𝑦𝑥(vol‘𝑦)))))
884, 87ax-mp 5 . 2 (vol ∈ (measures‘dom vol) ↔ (vol:dom vol⟶(0[,]+∞) ∧ (vol‘∅) = 0 ∧ ∀𝑥 ∈ 𝒫 dom vol((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → (vol‘ 𝑥) = Σ*𝑦𝑥(vol‘𝑦))))
891, 10, 86, 88mpbir3an 1338 1 vol ∈ (measures‘dom vol)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  wo 844  w3a 1084   = wceq 1538  wex 1781  wcel 2115  wral 3133  wss 3919  c0 4276  𝒫 cpw 4522   cuni 4824   ciun 4905  Disj wdisj 5017   class class class wbr 5052  dom cdm 5542  ran crn 5543  wf 6339  1-1-ontowf1o 6342  cfv 6343  (class class class)co 7149  ωcom 7574  cen 8502  cdom 8503  csdm 8504  Fincfn 8505  cr 10534  0cc0 10535  +∞cpnf 10670  cn 11634  [,]cicc 12738  vol*covol 24072  volcvol 24073  Σ*cesum 31346  sigAlgebracsiga 31427  measurescmeas 31514
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7455  ax-inf2 9101  ax-cc 9855  ax-cnex 10591  ax-resscn 10592  ax-1cn 10593  ax-icn 10594  ax-addcl 10595  ax-addrcl 10596  ax-mulcl 10597  ax-mulrcl 10598  ax-mulcom 10599  ax-addass 10600  ax-mulass 10601  ax-distr 10602  ax-i2m1 10603  ax-1ne0 10604  ax-1rid 10605  ax-rnegex 10606  ax-rrecex 10607  ax-cnre 10608  ax-pre-lttri 10609  ax-pre-lttrn 10610  ax-pre-ltadd 10611  ax-pre-mulgt0 10612  ax-pre-sup 10613  ax-addf 10614  ax-mulf 10615
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-nel 3119  df-ral 3138  df-rex 3139  df-reu 3140  df-rmo 3141  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4825  df-int 4863  df-iun 4907  df-iin 4908  df-disj 5018  df-br 5053  df-opab 5115  df-mpt 5133  df-tr 5159  df-id 5447  df-eprel 5452  df-po 5461  df-so 5462  df-fr 5501  df-se 5502  df-we 5503  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-pred 6135  df-ord 6181  df-on 6182  df-lim 6183  df-suc 6184  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-isom 6352  df-riota 7107  df-ov 7152  df-oprab 7153  df-mpo 7154  df-of 7403  df-om 7575  df-1st 7684  df-2nd 7685  df-supp 7827  df-wrecs 7943  df-recs 8004  df-rdg 8042  df-1o 8098  df-2o 8099  df-oadd 8102  df-er 8285  df-map 8404  df-pm 8405  df-ixp 8458  df-en 8506  df-dom 8507  df-sdom 8508  df-fin 8509  df-fsupp 8831  df-fi 8872  df-sup 8903  df-inf 8904  df-oi 8971  df-dju 9327  df-card 9365  df-pnf 10675  df-mnf 10676  df-xr 10677  df-ltxr 10678  df-le 10679  df-sub 10870  df-neg 10871  df-div 11296  df-nn 11635  df-2 11697  df-3 11698  df-4 11699  df-5 11700  df-6 11701  df-7 11702  df-8 11703  df-9 11704  df-n0 11895  df-xnn0 11965  df-z 11979  df-dec 12096  df-uz 12241  df-q 12346  df-rp 12387  df-xneg 12504  df-xadd 12505  df-xmul 12506  df-ioo 12739  df-ioc 12740  df-ico 12741  df-icc 12742  df-fz 12895  df-fzo 13038  df-fl 13166  df-mod 13242  df-seq 13374  df-exp 13435  df-fac 13639  df-bc 13668  df-hash 13696  df-shft 14426  df-cj 14458  df-re 14459  df-im 14460  df-sqrt 14594  df-abs 14595  df-limsup 14828  df-clim 14845  df-rlim 14846  df-sum 15043  df-ef 15421  df-sin 15423  df-cos 15424  df-pi 15426  df-struct 16485  df-ndx 16486  df-slot 16487  df-base 16489  df-sets 16490  df-ress 16491  df-plusg 16578  df-mulr 16579  df-starv 16580  df-sca 16581  df-vsca 16582  df-ip 16583  df-tset 16584  df-ple 16585  df-ds 16587  df-unif 16588  df-hom 16589  df-cco 16590  df-rest 16696  df-topn 16697  df-0g 16715  df-gsum 16716  df-topgen 16717  df-pt 16718  df-prds 16721  df-ordt 16774  df-xrs 16775  df-qtop 16780  df-imas 16781  df-xps 16783  df-mre 16857  df-mrc 16858  df-acs 16860  df-ps 17810  df-tsr 17811  df-plusf 17851  df-mgm 17852  df-sgrp 17901  df-mnd 17912  df-mhm 17956  df-submnd 17957  df-grp 18106  df-minusg 18107  df-sbg 18108  df-mulg 18225  df-subg 18276  df-cntz 18447  df-cmn 18908  df-abl 18909  df-mgp 19240  df-ur 19252  df-ring 19299  df-cring 19300  df-subrg 19533  df-abv 19588  df-lmod 19636  df-scaf 19637  df-sra 19944  df-rgmod 19945  df-psmet 20090  df-xmet 20091  df-met 20092  df-bl 20093  df-mopn 20094  df-fbas 20095  df-fg 20096  df-cnfld 20099  df-top 21505  df-topon 21522  df-topsp 21544  df-bases 21557  df-cld 21630  df-ntr 21631  df-cls 21632  df-nei 21709  df-lp 21747  df-perf 21748  df-cn 21838  df-cnp 21839  df-haus 21926  df-tx 22173  df-hmeo 22366  df-fil 22457  df-fm 22549  df-flim 22550  df-flf 22551  df-tmd 22683  df-tgp 22684  df-tsms 22738  df-trg 22771  df-xms 22933  df-ms 22934  df-tms 22935  df-nm 23195  df-ngp 23196  df-nrg 23198  df-nlm 23199  df-ii 23488  df-cncf 23489  df-ovol 24074  df-vol 24075  df-limc 24475  df-dv 24476  df-log 25154  df-esum 31347  df-siga 31428  df-meas 31515
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator