sitmcl - Mathbox for Thierry Arnoux

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

Theorem sitmcl 33350

Description: Closure of the integral distance between two simple functions, for an extended metric space. (Contributed by Thierry Arnoux, 13-Feb-2018.)

**Hypotheses**
Ref	Expression
sitmcl.0	⊢ (𝜑 → 𝑊 ∈ Mnd)
sitmcl.1	⊢ (𝜑 → 𝑊 ∈ ∞MetSp)
sitmcl.2	⊢ (𝜑 → 𝑀 ∈ ∪ ran measures)
sitmcl.3	⊢ (𝜑 → 𝐹 ∈ dom (𝑊sitg𝑀))
sitmcl.4	⊢ (𝜑 → 𝐺 ∈ dom (𝑊sitg𝑀))

**Assertion**
Ref	Expression
sitmcl	⊢ (𝜑 → (𝐹(𝑊sitm𝑀)𝐺) ∈ (0[,]+∞))

Proof of Theorem sitmcl Dummy variables 𝑥 𝑚 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2733	. . 3 ⊢ (dist‘𝑊) = (dist‘𝑊)
2		sitmcl.1	. . 3 ⊢ (𝜑 → 𝑊 ∈ ∞MetSp)
3		sitmcl.2	. . 3 ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures)
4		sitmcl.3	. . 3 ⊢ (𝜑 → 𝐹 ∈ dom (𝑊sitg𝑀))
5		sitmcl.4	. . 3 ⊢ (𝜑 → 𝐺 ∈ dom (𝑊sitg𝑀))
6	1, 2, 3, 4, 5	sitmfval 33349	. 2 ⊢ (𝜑 → (𝐹(𝑊sitm𝑀)𝐺) = (((ℝ^*_𝑠 ↾_s (0[,]+∞))sitg𝑀)‘(𝐹 ∘_f (dist‘𝑊)𝐺)))
7		xrge0base 32186	. . 3 ⊢ (0[,]+∞) = (Base‘(ℝ^*_𝑠 ↾_s (0[,]+∞)))
8		xrge0topn 32923	. . . 4 ⊢ (TopOpen‘(ℝ^*_𝑠 ↾_s (0[,]+∞))) = ((ordTop‘ ≤ ) ↾_t (0[,]+∞))
9	8	eqcomi 2742	. . 3 ⊢ ((ordTop‘ ≤ ) ↾_t (0[,]+∞)) = (TopOpen‘(ℝ^*_𝑠 ↾_s (0[,]+∞)))
10		eqid 2733	. . 3 ⊢ (sigaGen‘((ordTop‘ ≤ ) ↾_t (0[,]+∞))) = (sigaGen‘((ordTop‘ ≤ ) ↾_t (0[,]+∞)))
11		xrge00 32187	. . 3 ⊢ 0 = (0_g‘(ℝ^*_𝑠 ↾_s (0[,]+∞)))
12		ovex 7442	. . . 4 ⊢ (0[,]+∞) ∈ V
13		eqid 2733	. . . . 5 ⊢ (ℝ^_𝑠 ↾_s (0[,]+∞)) = (ℝ^_𝑠 ↾_s (0[,]+∞))
14		ax-xrsvsca 32175	. . . . 5 ⊢ ·_e = ( ·_𝑠 ‘ℝ^*_𝑠)
15	13, 14	ressvsca 17289	. . . 4 ⊢ ((0[,]+∞) ∈ V → ·_e = ( ·_𝑠 ‘(ℝ^*_𝑠 ↾_s (0[,]+∞))))
16	12, 15	ax-mp 5	. . 3 ⊢ ·_e = ( ·_𝑠 ‘(ℝ^*_𝑠 ↾_s (0[,]+∞)))
17		ax-xrssca 32174	. . . . . 6 ⊢ ℝ_fld = (Scalar‘ℝ^*_𝑠)
18	13, 17	resssca 17288	. . . . 5 ⊢ ((0[,]+∞) ∈ V → ℝ_fld = (Scalar‘(ℝ^*_𝑠 ↾_s (0[,]+∞))))
19	12, 18	ax-mp 5	. . . 4 ⊢ ℝ_fld = (Scalar‘(ℝ^*_𝑠 ↾_s (0[,]+∞)))
20	19	fveq2i 6895	. . 3 ⊢ (ℝHom‘ℝ_fld) = (ℝHom‘(Scalar‘(ℝ^*_𝑠 ↾_s (0[,]+∞))))
21		ovexd 7444	. . 3 ⊢ (𝜑 → (ℝ^*_𝑠 ↾_s (0[,]+∞)) ∈ V)
22		eqid 2733	. . . . . . 7 ⊢ (Base‘𝑊) = (Base‘𝑊)
23		eqid 2733	. . . . . . 7 ⊢ (TopOpen‘𝑊) = (TopOpen‘𝑊)
24		eqid 2733	. . . . . . 7 ⊢ (sigaGen‘(TopOpen‘𝑊)) = (sigaGen‘(TopOpen‘𝑊))
25		eqid 2733	. . . . . . 7 ⊢ (0_g‘𝑊) = (0_g‘𝑊)
26		eqid 2733	. . . . . . 7 ⊢ ( ·_𝑠 ‘𝑊) = ( ·_𝑠 ‘𝑊)
27		eqid 2733	. . . . . . 7 ⊢ (ℝHom‘(Scalar‘𝑊)) = (ℝHom‘(Scalar‘𝑊))
28	22, 23, 24, 25, 26, 27, 2, 3, 4	sibff 33335	. . . . . 6 ⊢ (𝜑 → 𝐹:∪ dom 𝑀⟶∪ (TopOpen‘𝑊))
29		xmstps 23959	. . . . . . . 8 ⊢ (𝑊 ∈ ∞MetSp → 𝑊 ∈ TopSp)
30	22, 23	tpsuni 22438	. . . . . . . 8 ⊢ (𝑊 ∈ TopSp → (Base‘𝑊) = ∪ (TopOpen‘𝑊))
31	2, 29, 30	3syl 18	. . . . . . 7 ⊢ (𝜑 → (Base‘𝑊) = ∪ (TopOpen‘𝑊))
32		feq3 6701	. . . . . . 7 ⊢ ((Base‘𝑊) = ∪ (TopOpen‘𝑊) → (𝐹:∪ dom 𝑀⟶(Base‘𝑊) ↔ 𝐹:∪ dom 𝑀⟶∪ (TopOpen‘𝑊)))
33	31, 32	syl 17	. . . . . 6 ⊢ (𝜑 → (𝐹:∪ dom 𝑀⟶(Base‘𝑊) ↔ 𝐹:∪ dom 𝑀⟶∪ (TopOpen‘𝑊)))
34	28, 33	mpbird 257	. . . . 5 ⊢ (𝜑 → 𝐹:∪ dom 𝑀⟶(Base‘𝑊))
35	22, 23, 24, 25, 26, 27, 2, 3, 5	sibff 33335	. . . . . 6 ⊢ (𝜑 → 𝐺:∪ dom 𝑀⟶∪ (TopOpen‘𝑊))
36		feq3 6701	. . . . . . 7 ⊢ ((Base‘𝑊) = ∪ (TopOpen‘𝑊) → (𝐺:∪ dom 𝑀⟶(Base‘𝑊) ↔ 𝐺:∪ dom 𝑀⟶∪ (TopOpen‘𝑊)))
37	31, 36	syl 17	. . . . . 6 ⊢ (𝜑 → (𝐺:∪ dom 𝑀⟶(Base‘𝑊) ↔ 𝐺:∪ dom 𝑀⟶∪ (TopOpen‘𝑊)))
38	35, 37	mpbird 257	. . . . 5 ⊢ (𝜑 → 𝐺:∪ dom 𝑀⟶(Base‘𝑊))
39		dmexg 7894	. . . . . 6 ⊢ (𝑀 ∈ ∪ ran measures → dom 𝑀 ∈ V)
40		uniexg 7730	. . . . . 6 ⊢ (dom 𝑀 ∈ V → ∪ dom 𝑀 ∈ V)
41	3, 39, 40	3syl 18	. . . . 5 ⊢ (𝜑 → ∪ dom 𝑀 ∈ V)
42	34, 38, 41	ofresid 31867	. . . 4 ⊢ (𝜑 → (𝐹 ∘_f (dist‘𝑊)𝐺) = (𝐹 ∘_f ((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))𝐺))
43	2, 29	syl 17	. . . . 5 ⊢ (𝜑 → 𝑊 ∈ TopSp)
44		eqid 2733	. . . . . . . 8 ⊢ ((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊))) = ((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))
45	22, 44	xmsxmet 23962	. . . . . . 7 ⊢ (𝑊 ∈ ∞MetSp → ((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊))) ∈ (∞Met‘(Base‘𝑊)))
46		xmetpsmet 23854	. . . . . . 7 ⊢ (((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊))) ∈ (∞Met‘(Base‘𝑊)) → ((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊))) ∈ (PsMet‘(Base‘𝑊)))
47	2, 45, 46	3syl 18	. . . . . 6 ⊢ (𝜑 → ((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊))) ∈ (PsMet‘(Base‘𝑊)))
48		psmetxrge0 23819	. . . . . 6 ⊢ (((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊))) ∈ (PsMet‘(Base‘𝑊)) → ((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊))):((Base‘𝑊) × (Base‘𝑊))⟶(0[,]+∞))
49	47, 48	syl 17	. . . . 5 ⊢ (𝜑 → ((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊))):((Base‘𝑊) × (Base‘𝑊))⟶(0[,]+∞))
50		xrge0tps 32922	. . . . . 6 ⊢ (ℝ^*_𝑠 ↾_s (0[,]+∞)) ∈ TopSp
51	50	a1i 11	. . . . 5 ⊢ (𝜑 → (ℝ^*_𝑠 ↾_s (0[,]+∞)) ∈ TopSp)
52	23, 22, 44	xmstopn 23957	. . . . . . . 8 ⊢ (𝑊 ∈ ∞MetSp → (TopOpen‘𝑊) = (MetOpen‘((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))))
53	2, 52	syl 17	. . . . . . 7 ⊢ (𝜑 → (TopOpen‘𝑊) = (MetOpen‘((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))))
54		eqid 2733	. . . . . . . . 9 ⊢ (MetOpen‘((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))) = (MetOpen‘((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊))))
55	54	methaus 24029	. . . . . . . 8 ⊢ (((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊))) ∈ (∞Met‘(Base‘𝑊)) → (MetOpen‘((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))) ∈ Haus)
56	2, 45, 55	3syl 18	. . . . . . 7 ⊢ (𝜑 → (MetOpen‘((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))) ∈ Haus)
57	53, 56	eqeltrd 2834	. . . . . 6 ⊢ (𝜑 → (TopOpen‘𝑊) ∈ Haus)
58		haust1 22856	. . . . . 6 ⊢ ((TopOpen‘𝑊) ∈ Haus → (TopOpen‘𝑊) ∈ Fre)
59	57, 58	syl 17	. . . . 5 ⊢ (𝜑 → (TopOpen‘𝑊) ∈ Fre)
60	2, 45	syl 17	. . . . . . 7 ⊢ (𝜑 → ((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊))) ∈ (∞Met‘(Base‘𝑊)))
61		sitmcl.0	. . . . . . . 8 ⊢ (𝜑 → 𝑊 ∈ Mnd)
62	22, 25	mndidcl 18640	. . . . . . . 8 ⊢ (𝑊 ∈ Mnd → (0_g‘𝑊) ∈ (Base‘𝑊))
63	61, 62	syl 17	. . . . . . 7 ⊢ (𝜑 → (0_g‘𝑊) ∈ (Base‘𝑊))
64		xmet0 23848	. . . . . . 7 ⊢ ((((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊))) ∈ (∞Met‘(Base‘𝑊)) ∧ (0_g‘𝑊) ∈ (Base‘𝑊)) → ((0_g‘𝑊)((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))(0_g‘𝑊)) = 0)
65	60, 63, 64	syl2anc 585	. . . . . 6 ⊢ (𝜑 → ((0_g‘𝑊)((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))(0_g‘𝑊)) = 0)
66	65, 11	eqtrdi 2789	. . . . 5 ⊢ (𝜑 → ((0_g‘𝑊)((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))(0_g‘𝑊)) = (0_g‘(ℝ^*_𝑠 ↾_s (0[,]+∞))))
67	22, 23, 24, 25, 26, 27, 2, 3, 4, 7, 43, 49, 5, 51, 59, 66	sibfof 33339	. . . 4 ⊢ (𝜑 → (𝐹 ∘_f ((dist‘𝑊) ↾ ((Base‘𝑊) × (Base‘𝑊)))𝐺) ∈ dom ((ℝ^*_𝑠 ↾_s (0[,]+∞))sitg𝑀))
68	42, 67	eqeltrd 2834	. . 3 ⊢ (𝜑 → (𝐹 ∘_f (dist‘𝑊)𝐺) ∈ dom ((ℝ^*_𝑠 ↾_s (0[,]+∞))sitg𝑀))
69		rebase 21159	. . . . 5 ⊢ ℝ = (Base‘ℝ_fld)
70	69, 69	xpeq12i 5705	. . . 4 ⊢ (ℝ × ℝ) = ((Base‘ℝ_fld) × (Base‘ℝ_fld))
71	70	reseq2i 5979	. . 3 ⊢ ((dist‘ℝ_fld) ↾ (ℝ × ℝ)) = ((dist‘ℝ_fld) ↾ ((Base‘ℝ_fld) × (Base‘ℝ_fld)))
72		xrge0cmn 20987	. . . 4 ⊢ (ℝ^*_𝑠 ↾_s (0[,]+∞)) ∈ CMnd
73	72	a1i 11	. . 3 ⊢ (𝜑 → (ℝ^*_𝑠 ↾_s (0[,]+∞)) ∈ CMnd)
74		rerrext 32989	. . . . 5 ⊢ ℝ_fld ∈ ℝExt
75	19, 74	eqeltrri 2831	. . . 4 ⊢ (Scalar‘(ℝ^*_𝑠 ↾_s (0[,]+∞))) ∈ ℝExt
76	75	a1i 11	. . 3 ⊢ (𝜑 → (Scalar‘(ℝ^*_𝑠 ↾_s (0[,]+∞))) ∈ ℝExt )
77		rrhre 33001	. . . . . . . . 9 ⊢ (ℝHom‘ℝ_fld) = ( I ↾ ℝ)
78	77	imaeq1i 6057	. . . . . . . 8 ⊢ ((ℝHom‘ℝ_fld) “ (0[,)+∞)) = (( I ↾ ℝ) “ (0[,)+∞))
79		0re 11216	. . . . . . . . . 10 ⊢ 0 ∈ ℝ
80		pnfxr 11268	. . . . . . . . . 10 ⊢ +∞ ∈ ℝ^*
81		icossre 13405	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ ∧ +∞ ∈ ℝ^*) → (0[,)+∞) ⊆ ℝ)
82	79, 80, 81	mp2an 691	. . . . . . . . 9 ⊢ (0[,)+∞) ⊆ ℝ
83		resiima 6076	. . . . . . . . 9 ⊢ ((0[,)+∞) ⊆ ℝ → (( I ↾ ℝ) “ (0[,)+∞)) = (0[,)+∞))
84	82, 83	ax-mp 5	. . . . . . . 8 ⊢ (( I ↾ ℝ) “ (0[,)+∞)) = (0[,)+∞)
85	78, 84	eqtri 2761	. . . . . . 7 ⊢ ((ℝHom‘ℝ_fld) “ (0[,)+∞)) = (0[,)+∞)
86		icossicc 13413	. . . . . . 7 ⊢ (0[,)+∞) ⊆ (0[,]+∞)
87	85, 86	eqsstri 4017	. . . . . 6 ⊢ ((ℝHom‘ℝ_fld) “ (0[,)+∞)) ⊆ (0[,]+∞)
88	87	sseli 3979	. . . . 5 ⊢ (𝑚 ∈ ((ℝHom‘ℝ_fld) “ (0[,)+∞)) → 𝑚 ∈ (0[,]+∞))
89	88	3ad2ant2 1135	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ((ℝHom‘ℝ_fld) “ (0[,)+∞)) ∧ 𝑥 ∈ (0[,]+∞)) → 𝑚 ∈ (0[,]+∞))
90		simp3 1139	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ ((ℝHom‘ℝ_fld) “ (0[,)+∞)) ∧ 𝑥 ∈ (0[,]+∞)) → 𝑥 ∈ (0[,]+∞))
91		ge0xmulcl 13440	. . . 4 ⊢ ((𝑚 ∈ (0[,]+∞) ∧ 𝑥 ∈ (0[,]+∞)) → (𝑚 ·_e 𝑥) ∈ (0[,]+∞))
92	89, 90, 91	syl2anc 585	. . 3 ⊢ ((𝜑 ∧ 𝑚 ∈ ((ℝHom‘ℝ_fld) “ (0[,)+∞)) ∧ 𝑥 ∈ (0[,]+∞)) → (𝑚 ·_e 𝑥) ∈ (0[,]+∞))
93	7, 9, 10, 11, 16, 20, 21, 3, 68, 19, 71, 51, 73, 76, 92	sitgclg 33341	. 2 ⊢ (𝜑 → (((ℝ^*_𝑠 ↾_s (0[,]+∞))sitg𝑀)‘(𝐹 ∘_f (dist‘𝑊)𝐺)) ∈ (0[,]+∞))
94	6, 93	eqeltrd 2834	1 ⊢ (𝜑 → (𝐹(𝑊sitm𝑀)𝐺) ∈ (0[,]+∞))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ w3a 1088 = wceq 1542 ∈ wcel 2107 Vcvv 3475 ⊆ wss 3949 ∪ cuni 4909 I cid 5574 × cxp 5675 dom cdm 5677 ran crn 5678 ↾ cres 5679 “ cima 5680 ⟶wf 6540 ‘cfv 6544 (class class class)co 7409 ∘_f cof 7668 ℝcr 11109 0cc0 11110 +∞cpnf 11245 ℝ^*cxr 11247 ≤ cle 11249 ·_e cxmu 13091 [,)cico 13326 [,]cicc 13327 Basecbs 17144 ↾_s cress 17173 Scalarcsca 17200 ·_𝑠 cvsca 17201 distcds 17206 ↾_t crest 17366 TopOpenctopn 17367 0_gc0g 17385 ordTopcordt 17445 ℝ^*_𝑠cxrs 17446 Mndcmnd 18625 CMndccmn 19648 PsMetcpsmet 20928 ∞Metcxmet 20929 MetOpencmopn 20934 ℝ_fldcrefld 21157 TopSpctps 22434 Frect1 22811 Hauscha 22812 ∞MetSpcxms 23823 ℝHomcrrh 32973 ℝExt crrext 32974 sigaGencsigagen 33136 measurescmeas 33193 sitmcsitm 33327 sitgcsitg 33328

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5286 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7725 ax-inf2 9636 ax-ac2 10458 ax-cnex 11166 ax-resscn 11167 ax-1cn 11168 ax-icn 11169 ax-addcl 11170 ax-addrcl 11171 ax-mulcl 11172 ax-mulrcl 11173 ax-mulcom 11174 ax-addass 11175 ax-mulass 11176 ax-distr 11177 ax-i2m1 11178 ax-1ne0 11179 ax-1rid 11180 ax-rnegex 11181 ax-rrecex 11182 ax-cnre 11183 ax-pre-lttri 11184 ax-pre-lttrn 11185 ax-pre-ltadd 11186 ax-pre-mulgt0 11187 ax-pre-sup 11188 ax-addf 11189 ax-mulf 11190 ax-xrssca 32174 ax-xrsvsca 32175

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-pss 3968 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-tp 4634 df-op 4636 df-uni 4910 df-int 4952 df-iun 5000 df-iin 5001 df-disj 5115 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 df-id 5575 df-eprel 5581 df-po 5589 df-so 5590 df-fr 5632 df-se 5633 df-we 5634 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-pred 6301 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-isom 6553 df-riota 7365 df-ov 7412 df-oprab 7413 df-mpo 7414 df-of 7670 df-om 7856 df-1st 7975 df-2nd 7976 df-supp 8147 df-tpos 8211 df-frecs 8266 df-wrecs 8297 df-recs 8371 df-rdg 8410 df-1o 8466 df-2o 8467 df-er 8703 df-map 8822 df-pm 8823 df-ixp 8892 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-fsupp 9362 df-fi 9406 df-sup 9437 df-inf 9438 df-oi 9505 df-dju 9896 df-card 9934 df-acn 9937 df-ac 10111 df-pnf 11250 df-mnf 11251 df-xr 11252 df-ltxr 11253 df-le 11254 df-sub 11446 df-neg 11447 df-div 11872 df-nn 12213 df-2 12275 df-3 12276 df-4 12277 df-5 12278 df-6 12279 df-7 12280 df-8 12281 df-9 12282 df-n0 12473 df-z 12559 df-dec 12678 df-uz 12823 df-q 12933 df-rp 12975 df-xneg 13092 df-xadd 13093 df-xmul 13094 df-ioo 13328 df-ioc 13329 df-ico 13330 df-icc 13331 df-fz 13485 df-fzo 13628 df-fl 13757 df-mod 13835 df-seq 13967 df-exp 14028 df-fac 14234 df-bc 14263 df-hash 14291 df-shft 15014 df-cj 15046 df-re 15047 df-im 15048 df-sqrt 15182 df-abs 15183 df-limsup 15415 df-clim 15432 df-rlim 15433 df-sum 15633 df-ef 16011 df-sin 16013 df-cos 16014 df-pi 16016 df-dvds 16198 df-gcd 16436 df-numer 16671 df-denom 16672 df-gz 16863 df-struct 17080 df-sets 17097 df-slot 17115 df-ndx 17127 df-base 17145 df-ress 17174 df-plusg 17210 df-mulr 17211 df-starv 17212 df-sca 17213 df-vsca 17214 df-ip 17215 df-tset 17216 df-ple 17217 df-ds 17219 df-unif 17220 df-hom 17221 df-cco 17222 df-rest 17368 df-topn 17369 df-0g 17387 df-gsum 17388 df-topgen 17389 df-pt 17390 df-prds 17393 df-ordt 17447 df-xrs 17448 df-qtop 17453 df-imas 17454 df-xps 17456 df-mre 17530 df-mrc 17531 df-acs 17533 df-proset 18248 df-poset 18266 df-plt 18283 df-toset 18370 df-ps 18519 df-tsr 18520 df-plusf 18560 df-mgm 18561 df-sgrp 18610 df-mnd 18626 df-mhm 18671 df-submnd 18672 df-grp 18822 df-minusg 18823 df-sbg 18824 df-mulg 18951 df-subg 19003 df-ghm 19090 df-cntz 19181 df-od 19396 df-cmn 19650 df-abl 19651 df-mgp 19988 df-ur 20005 df-ring 20058 df-cring 20059 df-oppr 20150 df-dvdsr 20171 df-unit 20172 df-invr 20202 df-dvr 20215 df-rnghom 20251 df-nzr 20292 df-subrg 20317 df-drng 20359 df-field 20360 df-abv 20425 df-lmod 20473 df-scaf 20474 df-sra 20785 df-rgmod 20786 df-psmet 20936 df-xmet 20937 df-met 20938 df-bl 20939 df-mopn 20940 df-fbas 20941 df-fg 20942 df-metu 20943 df-cnfld 20945 df-zring 21018 df-zrh 21053 df-zlm 21054 df-chr 21055 df-refld 21158 df-top 22396 df-topon 22413 df-topsp 22435 df-bases 22449 df-cld 22523 df-ntr 22524 df-cls 22525 df-nei 22602 df-lp 22640 df-perf 22641 df-cn 22731 df-cnp 22732 df-t1 22818 df-haus 22819 df-reg 22820 df-cmp 22891 df-tx 23066 df-hmeo 23259 df-fil 23350 df-fm 23442 df-flim 23443 df-flf 23444 df-fcls 23445 df-cnext 23564 df-tmd 23576 df-tgp 23577 df-tsms 23631 df-trg 23664 df-ust 23705 df-utop 23736 df-uss 23761 df-usp 23762 df-ucn 23781 df-cfilu 23792 df-cusp 23803 df-xms 23826 df-ms 23827 df-tms 23828 df-nm 24091 df-ngp 24092 df-nrg 24094 df-nlm 24095 df-ii 24393 df-cncf 24394 df-cfil 24772 df-cmet 24774 df-cms 24852 df-limc 25383 df-dv 25384 df-log 26065 df-omnd 32217 df-ogrp 32218 df-orng 32415 df-ofld 32416 df-qqh 32953 df-rrh 32975 df-rrext 32979 df-esum 33026 df-siga 33107 df-sigagen 33137 df-meas 33194 df-mbfm 33248 df-sitg 33329 df-sitm 33330

This theorem is referenced by: sitmf 33351

W3C validator