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

Theorem ftc2ditglem 24797
Description: Lemma for ftc2ditg 24798. (Contributed by Mario Carneiro, 3-Sep-2014.)
Hypotheses
Ref Expression
ftc2ditg.x (𝜑𝑋 ∈ ℝ)
ftc2ditg.y (𝜑𝑌 ∈ ℝ)
ftc2ditg.a (𝜑𝐴 ∈ (𝑋[,]𝑌))
ftc2ditg.b (𝜑𝐵 ∈ (𝑋[,]𝑌))
ftc2ditg.c (𝜑 → (ℝ D 𝐹) ∈ ((𝑋(,)𝑌)–cn→ℂ))
ftc2ditg.i (𝜑 → (ℝ D 𝐹) ∈ 𝐿1)
ftc2ditg.f (𝜑𝐹 ∈ ((𝑋[,]𝑌)–cn→ℂ))
Assertion
Ref Expression
ftc2ditglem ((𝜑𝐴𝐵) → ⨜[𝐴𝐵]((ℝ D 𝐹)‘𝑡) d𝑡 = ((𝐹𝐵) − (𝐹𝐴)))
Distinct variable groups:   𝑡,𝐴   𝑡,𝐵   𝑡,𝐹   𝜑,𝑡   𝑡,𝑋   𝑡,𝑌

Proof of Theorem ftc2ditglem
StepHypRef Expression
1 simpr 488 . . 3 ((𝜑𝐴𝐵) → 𝐴𝐵)
21ditgpos 24608 . 2 ((𝜑𝐴𝐵) → ⨜[𝐴𝐵]((ℝ D 𝐹)‘𝑡) d𝑡 = ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡)
3 ftc2ditg.x . . . . . . 7 (𝜑𝑋 ∈ ℝ)
4 ftc2ditg.y . . . . . . 7 (𝜑𝑌 ∈ ℝ)
5 iccssre 12904 . . . . . . 7 ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝑋[,]𝑌) ⊆ ℝ)
63, 4, 5syl2anc 587 . . . . . 6 (𝜑 → (𝑋[,]𝑌) ⊆ ℝ)
7 ftc2ditg.a . . . . . 6 (𝜑𝐴 ∈ (𝑋[,]𝑌))
86, 7sseldd 3879 . . . . 5 (𝜑𝐴 ∈ ℝ)
98adantr 484 . . . 4 ((𝜑𝐴𝐵) → 𝐴 ∈ ℝ)
10 ftc2ditg.b . . . . . 6 (𝜑𝐵 ∈ (𝑋[,]𝑌))
116, 10sseldd 3879 . . . . 5 (𝜑𝐵 ∈ ℝ)
1211adantr 484 . . . 4 ((𝜑𝐴𝐵) → 𝐵 ∈ ℝ)
13 ax-resscn 10673 . . . . . . . 8 ℝ ⊆ ℂ
1413a1i 11 . . . . . . 7 ((𝜑𝐴𝐵) → ℝ ⊆ ℂ)
15 ftc2ditg.f . . . . . . . . 9 (𝜑𝐹 ∈ ((𝑋[,]𝑌)–cn→ℂ))
16 cncff 23646 . . . . . . . . 9 (𝐹 ∈ ((𝑋[,]𝑌)–cn→ℂ) → 𝐹:(𝑋[,]𝑌)⟶ℂ)
1715, 16syl 17 . . . . . . . 8 (𝜑𝐹:(𝑋[,]𝑌)⟶ℂ)
1817adantr 484 . . . . . . 7 ((𝜑𝐴𝐵) → 𝐹:(𝑋[,]𝑌)⟶ℂ)
196adantr 484 . . . . . . 7 ((𝜑𝐴𝐵) → (𝑋[,]𝑌) ⊆ ℝ)
20 iccssre 12904 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
218, 11, 20syl2anc 587 . . . . . . . 8 (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
2221adantr 484 . . . . . . 7 ((𝜑𝐴𝐵) → (𝐴[,]𝐵) ⊆ ℝ)
23 eqid 2738 . . . . . . . 8 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
2423tgioo2 23556 . . . . . . . 8 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
2523, 24dvres 24663 . . . . . . 7 (((ℝ ⊆ ℂ ∧ 𝐹:(𝑋[,]𝑌)⟶ℂ) ∧ ((𝑋[,]𝑌) ⊆ ℝ ∧ (𝐴[,]𝐵) ⊆ ℝ)) → (ℝ D (𝐹 ↾ (𝐴[,]𝐵))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))))
2614, 18, 19, 22, 25syl22anc 838 . . . . . 6 ((𝜑𝐴𝐵) → (ℝ D (𝐹 ↾ (𝐴[,]𝐵))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))))
27 iccntr 23574 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))
288, 11, 27syl2anc 587 . . . . . . . 8 (𝜑 → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))
2928adantr 484 . . . . . . 7 ((𝜑𝐴𝐵) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵))
3029reseq2d 5826 . . . . . 6 ((𝜑𝐴𝐵) → ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵))) = ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)))
3126, 30eqtrd 2773 . . . . 5 ((𝜑𝐴𝐵) → (ℝ D (𝐹 ↾ (𝐴[,]𝐵))) = ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)))
323rexrd 10770 . . . . . . . . 9 (𝜑𝑋 ∈ ℝ*)
33 elicc2 12887 . . . . . . . . . . . 12 ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝐴 ∈ (𝑋[,]𝑌) ↔ (𝐴 ∈ ℝ ∧ 𝑋𝐴𝐴𝑌)))
343, 4, 33syl2anc 587 . . . . . . . . . . 11 (𝜑 → (𝐴 ∈ (𝑋[,]𝑌) ↔ (𝐴 ∈ ℝ ∧ 𝑋𝐴𝐴𝑌)))
357, 34mpbid 235 . . . . . . . . . 10 (𝜑 → (𝐴 ∈ ℝ ∧ 𝑋𝐴𝐴𝑌))
3635simp2d 1144 . . . . . . . . 9 (𝜑𝑋𝐴)
37 iooss1 12857 . . . . . . . . 9 ((𝑋 ∈ ℝ*𝑋𝐴) → (𝐴(,)𝐵) ⊆ (𝑋(,)𝐵))
3832, 36, 37syl2anc 587 . . . . . . . 8 (𝜑 → (𝐴(,)𝐵) ⊆ (𝑋(,)𝐵))
394rexrd 10770 . . . . . . . . 9 (𝜑𝑌 ∈ ℝ*)
40 elicc2 12887 . . . . . . . . . . . 12 ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝐵 ∈ (𝑋[,]𝑌) ↔ (𝐵 ∈ ℝ ∧ 𝑋𝐵𝐵𝑌)))
413, 4, 40syl2anc 587 . . . . . . . . . . 11 (𝜑 → (𝐵 ∈ (𝑋[,]𝑌) ↔ (𝐵 ∈ ℝ ∧ 𝑋𝐵𝐵𝑌)))
4210, 41mpbid 235 . . . . . . . . . 10 (𝜑 → (𝐵 ∈ ℝ ∧ 𝑋𝐵𝐵𝑌))
4342simp3d 1145 . . . . . . . . 9 (𝜑𝐵𝑌)
44 iooss2 12858 . . . . . . . . 9 ((𝑌 ∈ ℝ*𝐵𝑌) → (𝑋(,)𝐵) ⊆ (𝑋(,)𝑌))
4539, 43, 44syl2anc 587 . . . . . . . 8 (𝜑 → (𝑋(,)𝐵) ⊆ (𝑋(,)𝑌))
4638, 45sstrd 3888 . . . . . . 7 (𝜑 → (𝐴(,)𝐵) ⊆ (𝑋(,)𝑌))
4746adantr 484 . . . . . 6 ((𝜑𝐴𝐵) → (𝐴(,)𝐵) ⊆ (𝑋(,)𝑌))
48 ftc2ditg.c . . . . . . 7 (𝜑 → (ℝ D 𝐹) ∈ ((𝑋(,)𝑌)–cn→ℂ))
4948adantr 484 . . . . . 6 ((𝜑𝐴𝐵) → (ℝ D 𝐹) ∈ ((𝑋(,)𝑌)–cn→ℂ))
50 rescncf 23650 . . . . . 6 ((𝐴(,)𝐵) ⊆ (𝑋(,)𝑌) → ((ℝ D 𝐹) ∈ ((𝑋(,)𝑌)–cn→ℂ) → ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) ∈ ((𝐴(,)𝐵)–cn→ℂ)))
5147, 49, 50sylc 65 . . . . 5 ((𝜑𝐴𝐵) → ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) ∈ ((𝐴(,)𝐵)–cn→ℂ))
5231, 51eqeltrd 2833 . . . 4 ((𝜑𝐴𝐵) → (ℝ D (𝐹 ↾ (𝐴[,]𝐵))) ∈ ((𝐴(,)𝐵)–cn→ℂ))
53 cncff 23646 . . . . . . . . . . 11 ((ℝ D 𝐹) ∈ ((𝑋(,)𝑌)–cn→ℂ) → (ℝ D 𝐹):(𝑋(,)𝑌)⟶ℂ)
5448, 53syl 17 . . . . . . . . . 10 (𝜑 → (ℝ D 𝐹):(𝑋(,)𝑌)⟶ℂ)
5554feqmptd 6738 . . . . . . . . 9 (𝜑 → (ℝ D 𝐹) = (𝑡 ∈ (𝑋(,)𝑌) ↦ ((ℝ D 𝐹)‘𝑡)))
5655adantr 484 . . . . . . . 8 ((𝜑𝐴𝐵) → (ℝ D 𝐹) = (𝑡 ∈ (𝑋(,)𝑌) ↦ ((ℝ D 𝐹)‘𝑡)))
5756reseq1d 5825 . . . . . . 7 ((𝜑𝐴𝐵) → ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) = ((𝑡 ∈ (𝑋(,)𝑌) ↦ ((ℝ D 𝐹)‘𝑡)) ↾ (𝐴(,)𝐵)))
5847resmptd 5883 . . . . . . 7 ((𝜑𝐴𝐵) → ((𝑡 ∈ (𝑋(,)𝑌) ↦ ((ℝ D 𝐹)‘𝑡)) ↾ (𝐴(,)𝐵)) = (𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡)))
5957, 58eqtrd 2773 . . . . . 6 ((𝜑𝐴𝐵) → ((ℝ D 𝐹) ↾ (𝐴(,)𝐵)) = (𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡)))
6031, 59eqtrd 2773 . . . . 5 ((𝜑𝐴𝐵) → (ℝ D (𝐹 ↾ (𝐴[,]𝐵))) = (𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡)))
61 ioombl 24318 . . . . . . 7 (𝐴(,)𝐵) ∈ dom vol
6261a1i 11 . . . . . 6 ((𝜑𝐴𝐵) → (𝐴(,)𝐵) ∈ dom vol)
63 fvexd 6690 . . . . . 6 (((𝜑𝐴𝐵) ∧ 𝑡 ∈ (𝑋(,)𝑌)) → ((ℝ D 𝐹)‘𝑡) ∈ V)
64 ftc2ditg.i . . . . . . . 8 (𝜑 → (ℝ D 𝐹) ∈ 𝐿1)
6564adantr 484 . . . . . . 7 ((𝜑𝐴𝐵) → (ℝ D 𝐹) ∈ 𝐿1)
6656, 65eqeltrrd 2834 . . . . . 6 ((𝜑𝐴𝐵) → (𝑡 ∈ (𝑋(,)𝑌) ↦ ((ℝ D 𝐹)‘𝑡)) ∈ 𝐿1)
6747, 62, 63, 66iblss 24557 . . . . 5 ((𝜑𝐴𝐵) → (𝑡 ∈ (𝐴(,)𝐵) ↦ ((ℝ D 𝐹)‘𝑡)) ∈ 𝐿1)
6860, 67eqeltrd 2833 . . . 4 ((𝜑𝐴𝐵) → (ℝ D (𝐹 ↾ (𝐴[,]𝐵))) ∈ 𝐿1)
69 iccss2 12893 . . . . . . 7 ((𝐴 ∈ (𝑋[,]𝑌) ∧ 𝐵 ∈ (𝑋[,]𝑌)) → (𝐴[,]𝐵) ⊆ (𝑋[,]𝑌))
707, 10, 69syl2anc 587 . . . . . 6 (𝜑 → (𝐴[,]𝐵) ⊆ (𝑋[,]𝑌))
71 rescncf 23650 . . . . . 6 ((𝐴[,]𝐵) ⊆ (𝑋[,]𝑌) → (𝐹 ∈ ((𝑋[,]𝑌)–cn→ℂ) → (𝐹 ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)))
7270, 15, 71sylc 65 . . . . 5 (𝜑 → (𝐹 ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
7372adantr 484 . . . 4 ((𝜑𝐴𝐵) → (𝐹 ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
749, 12, 1, 52, 68, 73ftc2 24796 . . 3 ((𝜑𝐴𝐵) → ∫(𝐴(,)𝐵)((ℝ D (𝐹 ↾ (𝐴[,]𝐵)))‘𝑡) d𝑡 = (((𝐹 ↾ (𝐴[,]𝐵))‘𝐵) − ((𝐹 ↾ (𝐴[,]𝐵))‘𝐴)))
7531fveq1d 6677 . . . . 5 ((𝜑𝐴𝐵) → ((ℝ D (𝐹 ↾ (𝐴[,]𝐵)))‘𝑡) = (((ℝ D 𝐹) ↾ (𝐴(,)𝐵))‘𝑡))
76 fvres 6694 . . . . 5 (𝑡 ∈ (𝐴(,)𝐵) → (((ℝ D 𝐹) ↾ (𝐴(,)𝐵))‘𝑡) = ((ℝ D 𝐹)‘𝑡))
7775, 76sylan9eq 2793 . . . 4 (((𝜑𝐴𝐵) ∧ 𝑡 ∈ (𝐴(,)𝐵)) → ((ℝ D (𝐹 ↾ (𝐴[,]𝐵)))‘𝑡) = ((ℝ D 𝐹)‘𝑡))
7877itgeq2dv 24534 . . 3 ((𝜑𝐴𝐵) → ∫(𝐴(,)𝐵)((ℝ D (𝐹 ↾ (𝐴[,]𝐵)))‘𝑡) d𝑡 = ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡)
799rexrd 10770 . . . 4 ((𝜑𝐴𝐵) → 𝐴 ∈ ℝ*)
8012rexrd 10770 . . . 4 ((𝜑𝐴𝐵) → 𝐵 ∈ ℝ*)
81 ubicc2 12940 . . . . 5 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴𝐵) → 𝐵 ∈ (𝐴[,]𝐵))
82 lbicc2 12939 . . . . 5 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴𝐵) → 𝐴 ∈ (𝐴[,]𝐵))
83 fvres 6694 . . . . . 6 (𝐵 ∈ (𝐴[,]𝐵) → ((𝐹 ↾ (𝐴[,]𝐵))‘𝐵) = (𝐹𝐵))
84 fvres 6694 . . . . . 6 (𝐴 ∈ (𝐴[,]𝐵) → ((𝐹 ↾ (𝐴[,]𝐵))‘𝐴) = (𝐹𝐴))
8583, 84oveqan12d 7190 . . . . 5 ((𝐵 ∈ (𝐴[,]𝐵) ∧ 𝐴 ∈ (𝐴[,]𝐵)) → (((𝐹 ↾ (𝐴[,]𝐵))‘𝐵) − ((𝐹 ↾ (𝐴[,]𝐵))‘𝐴)) = ((𝐹𝐵) − (𝐹𝐴)))
8681, 82, 85syl2anc 587 . . . 4 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴𝐵) → (((𝐹 ↾ (𝐴[,]𝐵))‘𝐵) − ((𝐹 ↾ (𝐴[,]𝐵))‘𝐴)) = ((𝐹𝐵) − (𝐹𝐴)))
8779, 80, 1, 86syl3anc 1372 . . 3 ((𝜑𝐴𝐵) → (((𝐹 ↾ (𝐴[,]𝐵))‘𝐵) − ((𝐹 ↾ (𝐴[,]𝐵))‘𝐴)) = ((𝐹𝐵) − (𝐹𝐴)))
8874, 78, 873eqtr3d 2781 . 2 ((𝜑𝐴𝐵) → ∫(𝐴(,)𝐵)((ℝ D 𝐹)‘𝑡) d𝑡 = ((𝐹𝐵) − (𝐹𝐴)))
892, 88eqtrd 2773 1 ((𝜑𝐴𝐵) → ⨜[𝐴𝐵]((ℝ D 𝐹)‘𝑡) d𝑡 = ((𝐹𝐵) − (𝐹𝐴)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1088   = wceq 1542  wcel 2113  Vcvv 3398  wss 3844   class class class wbr 5031  cmpt 5111  dom cdm 5526  ran crn 5527  cres 5528  wf 6336  cfv 6340  (class class class)co 7171  cc 10614  cr 10615  *cxr 10753  cle 10755  cmin 10949  (,)cioo 12822  [,]cicc 12825  TopOpenctopn 16799  topGenctg 16815  fldccnfld 20218  intcnt 21769  cnccncf 23629  volcvol 24216  𝐿1cibl 24370  citg 24371  cdit 24598   D cdv 24615
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-rep 5155  ax-sep 5168  ax-nul 5175  ax-pow 5233  ax-pr 5297  ax-un 7480  ax-inf2 9178  ax-cc 9936  ax-cnex 10672  ax-resscn 10673  ax-1cn 10674  ax-icn 10675  ax-addcl 10676  ax-addrcl 10677  ax-mulcl 10678  ax-mulrcl 10679  ax-mulcom 10680  ax-addass 10681  ax-mulass 10682  ax-distr 10683  ax-i2m1 10684  ax-1ne0 10685  ax-1rid 10686  ax-rnegex 10687  ax-rrecex 10688  ax-cnre 10689  ax-pre-lttri 10690  ax-pre-lttrn 10691  ax-pre-ltadd 10692  ax-pre-mulgt0 10693  ax-pre-sup 10694  ax-addf 10695  ax-mulf 10696
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-nel 3039  df-ral 3058  df-rex 3059  df-reu 3060  df-rmo 3061  df-rab 3062  df-v 3400  df-sbc 3683  df-csb 3792  df-dif 3847  df-un 3849  df-in 3851  df-ss 3861  df-pss 3863  df-symdif 4134  df-nul 4213  df-if 4416  df-pw 4491  df-sn 4518  df-pr 4520  df-tp 4522  df-op 4524  df-uni 4798  df-int 4838  df-iun 4884  df-iin 4885  df-disj 4997  df-br 5032  df-opab 5094  df-mpt 5112  df-tr 5138  df-id 5430  df-eprel 5435  df-po 5443  df-so 5444  df-fr 5484  df-se 5485  df-we 5486  df-xp 5532  df-rel 5533  df-cnv 5534  df-co 5535  df-dm 5536  df-rn 5537  df-res 5538  df-ima 5539  df-pred 6130  df-ord 6176  df-on 6177  df-lim 6178  df-suc 6179  df-iota 6298  df-fun 6342  df-fn 6343  df-f 6344  df-f1 6345  df-fo 6346  df-f1o 6347  df-fv 6348  df-isom 6349  df-riota 7128  df-ov 7174  df-oprab 7175  df-mpo 7176  df-of 7426  df-ofr 7427  df-om 7601  df-1st 7715  df-2nd 7716  df-supp 7858  df-wrecs 7977  df-recs 8038  df-rdg 8076  df-1o 8132  df-2o 8133  df-oadd 8136  df-omul 8137  df-er 8321  df-map 8440  df-pm 8441  df-ixp 8509  df-en 8557  df-dom 8558  df-sdom 8559  df-fin 8560  df-fsupp 8908  df-fi 8949  df-sup 8980  df-inf 8981  df-oi 9048  df-dju 9404  df-card 9442  df-acn 9445  df-pnf 10756  df-mnf 10757  df-xr 10758  df-ltxr 10759  df-le 10760  df-sub 10951  df-neg 10952  df-div 11377  df-nn 11718  df-2 11780  df-3 11781  df-4 11782  df-5 11783  df-6 11784  df-7 11785  df-8 11786  df-9 11787  df-n0 11978  df-z 12064  df-dec 12181  df-uz 12326  df-q 12432  df-rp 12474  df-xneg 12591  df-xadd 12592  df-xmul 12593  df-ioo 12826  df-ioc 12827  df-ico 12828  df-icc 12829  df-fz 12983  df-fzo 13126  df-fl 13254  df-mod 13330  df-seq 13462  df-exp 13523  df-hash 13784  df-cj 14549  df-re 14550  df-im 14551  df-sqrt 14685  df-abs 14686  df-clim 14936  df-rlim 14937  df-sum 15137  df-struct 16589  df-ndx 16590  df-slot 16591  df-base 16593  df-sets 16594  df-ress 16595  df-plusg 16682  df-mulr 16683  df-starv 16684  df-sca 16685  df-vsca 16686  df-ip 16687  df-tset 16688  df-ple 16689  df-ds 16691  df-unif 16692  df-hom 16693  df-cco 16694  df-rest 16800  df-topn 16801  df-0g 16819  df-gsum 16820  df-topgen 16821  df-pt 16822  df-prds 16825  df-xrs 16879  df-qtop 16884  df-imas 16885  df-xps 16887  df-mre 16961  df-mrc 16962  df-acs 16964  df-mgm 17969  df-sgrp 18018  df-mnd 18029  df-submnd 18074  df-mulg 18344  df-cntz 18566  df-cmn 19027  df-psmet 20210  df-xmet 20211  df-met 20212  df-bl 20213  df-mopn 20214  df-fbas 20215  df-fg 20216  df-cnfld 20219  df-top 21646  df-topon 21663  df-topsp 21685  df-bases 21698  df-cld 21771  df-ntr 21772  df-cls 21773  df-nei 21850  df-lp 21888  df-perf 21889  df-cn 21979  df-cnp 21980  df-haus 22067  df-cmp 22139  df-tx 22314  df-hmeo 22507  df-fil 22598  df-fm 22690  df-flim 22691  df-flf 22692  df-xms 23074  df-ms 23075  df-tms 23076  df-cncf 23631  df-ovol 24217  df-vol 24218  df-mbf 24372  df-itg1 24373  df-itg2 24374  df-ibl 24375  df-itg 24376  df-0p 24423  df-ditg 24599  df-limc 24618  df-dv 24619
This theorem is referenced by:  ftc2ditg  24798
  Copyright terms: Public domain W3C validator