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

Theorem sitgclg 32609
Description: Closure of the Bochner integral on simple functions, generic version. See sitgclbn 32610 for the version for Banach spaces. (Contributed by Thierry Arnoux, 24-Feb-2018.) (Proof shortened by AV, 12-Dec-2019.)
Hypotheses
Ref Expression
sitgval.b 𝐵 = (Base‘𝑊)
sitgval.j 𝐽 = (TopOpen‘𝑊)
sitgval.s 𝑆 = (sigaGen‘𝐽)
sitgval.0 0 = (0g𝑊)
sitgval.x · = ( ·𝑠𝑊)
sitgval.h 𝐻 = (ℝHom‘(Scalar‘𝑊))
sitgval.1 (𝜑𝑊𝑉)
sitgval.2 (𝜑𝑀 ran measures)
sibfmbl.1 (𝜑𝐹 ∈ dom (𝑊sitg𝑀))
sitgclg.g 𝐺 = (Scalar‘𝑊)
sitgclg.d 𝐷 = ((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))
sitgclg.1 (𝜑𝑊 ∈ TopSp)
sitgclg.2 (𝜑𝑊 ∈ CMnd)
sitgclg.3 (𝜑 → (Scalar‘𝑊) ∈ ℝExt )
sitgclg.4 ((𝜑𝑚 ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥𝐵) → (𝑚 · 𝑥) ∈ 𝐵)
Assertion
Ref Expression
sitgclg (𝜑 → ((𝑊sitg𝑀)‘𝐹) ∈ 𝐵)
Distinct variable groups:   𝐵,𝑚   𝑥,𝐹   𝑚,𝐻   𝑥,𝑚,𝑀   𝑆,𝑚   𝑚,𝑊,𝑥   0 ,𝑚,𝑥   · ,𝑚   𝜑,𝑥   𝑥,𝐵   𝑚,𝐹   𝑚,𝐺   𝜑,𝑚
Allowed substitution hints:   𝐷(𝑥,𝑚)   𝑆(𝑥)   · (𝑥)   𝐺(𝑥)   𝐻(𝑥)   𝐽(𝑥,𝑚)   𝑉(𝑥,𝑚)

Proof of Theorem sitgclg
StepHypRef Expression
1 sitgval.b . . 3 𝐵 = (Base‘𝑊)
2 sitgval.j . . 3 𝐽 = (TopOpen‘𝑊)
3 sitgval.s . . 3 𝑆 = (sigaGen‘𝐽)
4 sitgval.0 . . 3 0 = (0g𝑊)
5 sitgval.x . . 3 · = ( ·𝑠𝑊)
6 sitgval.h . . 3 𝐻 = (ℝHom‘(Scalar‘𝑊))
7 sitgval.1 . . 3 (𝜑𝑊𝑉)
8 sitgval.2 . . 3 (𝜑𝑀 ran measures)
9 sibfmbl.1 . . 3 (𝜑𝐹 ∈ dom (𝑊sitg𝑀))
101, 2, 3, 4, 5, 6, 7, 8, 9sitgfval 32608 . 2 (𝜑 → ((𝑊sitg𝑀)‘𝐹) = (𝑊 Σg (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(𝐹 “ {𝑥}))) · 𝑥))))
11 sitgclg.2 . . 3 (𝜑𝑊 ∈ CMnd)
12 rnexg 7819 . . . 4 (𝐹 ∈ dom (𝑊sitg𝑀) → ran 𝐹 ∈ V)
13 difexg 5271 . . . 4 (ran 𝐹 ∈ V → (ran 𝐹 ∖ { 0 }) ∈ V)
149, 12, 133syl 18 . . 3 (𝜑 → (ran 𝐹 ∖ { 0 }) ∈ V)
15 simpl 483 . . . . 5 ((𝜑𝑥 ∈ (ran 𝐹 ∖ { 0 })) → 𝜑)
161, 2, 3, 4, 5, 6, 7, 8, 9sibfima 32605 . . . . . 6 ((𝜑𝑥 ∈ (ran 𝐹 ∖ { 0 })) → (𝑀‘(𝐹 “ {𝑥})) ∈ (0[,)+∞))
17 sitgclg.d . . . . . . . . . . 11 𝐷 = ((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺)))
18 sitgclg.g . . . . . . . . . . . . 13 𝐺 = (Scalar‘𝑊)
1918fveq2i 6828 . . . . . . . . . . . 12 (dist‘𝐺) = (dist‘(Scalar‘𝑊))
2018fveq2i 6828 . . . . . . . . . . . . 13 (Base‘𝐺) = (Base‘(Scalar‘𝑊))
2120, 20xpeq12i 5648 . . . . . . . . . . . 12 ((Base‘𝐺) × (Base‘𝐺)) = ((Base‘(Scalar‘𝑊)) × (Base‘(Scalar‘𝑊)))
2219, 21reseq12i 5921 . . . . . . . . . . 11 ((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺))) = ((dist‘(Scalar‘𝑊)) ↾ ((Base‘(Scalar‘𝑊)) × (Base‘(Scalar‘𝑊))))
2317, 22eqtri 2764 . . . . . . . . . 10 𝐷 = ((dist‘(Scalar‘𝑊)) ↾ ((Base‘(Scalar‘𝑊)) × (Base‘(Scalar‘𝑊))))
24 eqid 2736 . . . . . . . . . 10 (topGen‘ran (,)) = (topGen‘ran (,))
25 eqid 2736 . . . . . . . . . 10 (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
2618fveq2i 6828 . . . . . . . . . 10 (TopOpen‘𝐺) = (TopOpen‘(Scalar‘𝑊))
2718fveq2i 6828 . . . . . . . . . 10 (ℤMod‘𝐺) = (ℤMod‘(Scalar‘𝑊))
28 sitgclg.3 . . . . . . . . . . . . 13 (𝜑 → (Scalar‘𝑊) ∈ ℝExt )
2918, 28eqeltrid 2841 . . . . . . . . . . . 12 (𝜑𝐺 ∈ ℝExt )
30 rrextdrg 32250 . . . . . . . . . . . 12 (𝐺 ∈ ℝExt → 𝐺 ∈ DivRing)
3129, 30syl 17 . . . . . . . . . . 11 (𝜑𝐺 ∈ DivRing)
3218, 31eqeltrrid 2842 . . . . . . . . . 10 (𝜑 → (Scalar‘𝑊) ∈ DivRing)
33 rrextnrg 32249 . . . . . . . . . . . 12 (𝐺 ∈ ℝExt → 𝐺 ∈ NrmRing)
3429, 33syl 17 . . . . . . . . . . 11 (𝜑𝐺 ∈ NrmRing)
3518, 34eqeltrrid 2842 . . . . . . . . . 10 (𝜑 → (Scalar‘𝑊) ∈ NrmRing)
36 eqid 2736 . . . . . . . . . . . 12 (ℤMod‘𝐺) = (ℤMod‘𝐺)
3736rrextnlm 32251 . . . . . . . . . . 11 (𝐺 ∈ ℝExt → (ℤMod‘𝐺) ∈ NrmMod)
3829, 37syl 17 . . . . . . . . . 10 (𝜑 → (ℤMod‘𝐺) ∈ NrmMod)
3918fveq2i 6828 . . . . . . . . . . 11 (chr‘𝐺) = (chr‘(Scalar‘𝑊))
40 rrextchr 32252 . . . . . . . . . . . 12 (𝐺 ∈ ℝExt → (chr‘𝐺) = 0)
4129, 40syl 17 . . . . . . . . . . 11 (𝜑 → (chr‘𝐺) = 0)
4239, 41eqtr3id 2790 . . . . . . . . . 10 (𝜑 → (chr‘(Scalar‘𝑊)) = 0)
43 rrextcusp 32253 . . . . . . . . . . . 12 (𝐺 ∈ ℝExt → 𝐺 ∈ CUnifSp)
4429, 43syl 17 . . . . . . . . . . 11 (𝜑𝐺 ∈ CUnifSp)
4518, 44eqeltrrid 2842 . . . . . . . . . 10 (𝜑 → (Scalar‘𝑊) ∈ CUnifSp)
4618fveq2i 6828 . . . . . . . . . . 11 (UnifSt‘𝐺) = (UnifSt‘(Scalar‘𝑊))
47 eqid 2736 . . . . . . . . . . . . 13 (Base‘𝐺) = (Base‘𝐺)
4847, 17rrextust 32256 . . . . . . . . . . . 12 (𝐺 ∈ ℝExt → (UnifSt‘𝐺) = (metUnif‘𝐷))
4929, 48syl 17 . . . . . . . . . . 11 (𝜑 → (UnifSt‘𝐺) = (metUnif‘𝐷))
5046, 49eqtr3id 2790 . . . . . . . . . 10 (𝜑 → (UnifSt‘(Scalar‘𝑊)) = (metUnif‘𝐷))
5123, 24, 25, 26, 27, 32, 35, 38, 42, 45, 50rrhf 32246 . . . . . . . . 9 (𝜑 → (ℝHom‘(Scalar‘𝑊)):ℝ⟶(Base‘(Scalar‘𝑊)))
526feq1i 6642 . . . . . . . . 9 (𝐻:ℝ⟶(Base‘(Scalar‘𝑊)) ↔ (ℝHom‘(Scalar‘𝑊)):ℝ⟶(Base‘(Scalar‘𝑊)))
5351, 52sylibr 233 . . . . . . . 8 (𝜑𝐻:ℝ⟶(Base‘(Scalar‘𝑊)))
5453ffund 6655 . . . . . . 7 (𝜑 → Fun 𝐻)
55 rge0ssre 13289 . . . . . . . 8 (0[,)+∞) ⊆ ℝ
5653fdmd 6662 . . . . . . . 8 (𝜑 → dom 𝐻 = ℝ)
5755, 56sseqtrrid 3985 . . . . . . 7 (𝜑 → (0[,)+∞) ⊆ dom 𝐻)
58 funfvima2 7163 . . . . . . 7 ((Fun 𝐻 ∧ (0[,)+∞) ⊆ dom 𝐻) → ((𝑀‘(𝐹 “ {𝑥})) ∈ (0[,)+∞) → (𝐻‘(𝑀‘(𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞))))
5954, 57, 58syl2anc 584 . . . . . 6 (𝜑 → ((𝑀‘(𝐹 “ {𝑥})) ∈ (0[,)+∞) → (𝐻‘(𝑀‘(𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞))))
6015, 16, 59sylc 65 . . . . 5 ((𝜑𝑥 ∈ (ran 𝐹 ∖ { 0 })) → (𝐻‘(𝑀‘(𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞)))
61 dmmeas 32467 . . . . . . . . . . . 12 (𝑀 ran measures → dom 𝑀 ran sigAlgebra)
628, 61syl 17 . . . . . . . . . . 11 (𝜑 → dom 𝑀 ran sigAlgebra)
632fvexi 6839 . . . . . . . . . . . . . 14 𝐽 ∈ V
6463a1i 11 . . . . . . . . . . . . 13 (𝜑𝐽 ∈ V)
6564sgsiga 32408 . . . . . . . . . . . 12 (𝜑 → (sigaGen‘𝐽) ∈ ran sigAlgebra)
663, 65eqeltrid 2841 . . . . . . . . . . 11 (𝜑𝑆 ran sigAlgebra)
671, 2, 3, 4, 5, 6, 7, 8, 9sibfmbl 32602 . . . . . . . . . . 11 (𝜑𝐹 ∈ (dom 𝑀MblFnM𝑆))
6862, 66, 67mbfmf 32520 . . . . . . . . . 10 (𝜑𝐹: dom 𝑀 𝑆)
6968frnd 6659 . . . . . . . . 9 (𝜑 → ran 𝐹 𝑆)
703unieqi 4865 . . . . . . . . . . 11 𝑆 = (sigaGen‘𝐽)
71 unisg 32409 . . . . . . . . . . . 12 (𝐽 ∈ V → (sigaGen‘𝐽) = 𝐽)
7263, 71mp1i 13 . . . . . . . . . . 11 (𝜑 (sigaGen‘𝐽) = 𝐽)
7370, 72eqtrid 2788 . . . . . . . . . 10 (𝜑 𝑆 = 𝐽)
74 sitgclg.1 . . . . . . . . . . 11 (𝜑𝑊 ∈ TopSp)
751, 2tpsuni 22191 . . . . . . . . . . 11 (𝑊 ∈ TopSp → 𝐵 = 𝐽)
7674, 75syl 17 . . . . . . . . . 10 (𝜑𝐵 = 𝐽)
7773, 76eqtr4d 2779 . . . . . . . . 9 (𝜑 𝑆 = 𝐵)
7869, 77sseqtrd 3972 . . . . . . . 8 (𝜑 → ran 𝐹𝐵)
7978ssdifd 4087 . . . . . . 7 (𝜑 → (ran 𝐹 ∖ { 0 }) ⊆ (𝐵 ∖ { 0 }))
8079sselda 3932 . . . . . 6 ((𝜑𝑥 ∈ (ran 𝐹 ∖ { 0 })) → 𝑥 ∈ (𝐵 ∖ { 0 }))
8180eldifad 3910 . . . . 5 ((𝜑𝑥 ∈ (ran 𝐹 ∖ { 0 })) → 𝑥𝐵)
82 simp2 1136 . . . . . 6 ((𝜑 ∧ (𝐻‘(𝑀‘(𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥𝐵) → (𝐻‘(𝑀‘(𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞)))
83 eleq1 2824 . . . . . . . . 9 (𝑚 = (𝐻‘(𝑀‘(𝐹 “ {𝑥}))) → (𝑚 ∈ (𝐻 “ (0[,)+∞)) ↔ (𝐻‘(𝑀‘(𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞))))
84833anbi2d 1440 . . . . . . . 8 (𝑚 = (𝐻‘(𝑀‘(𝐹 “ {𝑥}))) → ((𝜑𝑚 ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥𝐵) ↔ (𝜑 ∧ (𝐻‘(𝑀‘(𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥𝐵)))
85 oveq1 7344 . . . . . . . . 9 (𝑚 = (𝐻‘(𝑀‘(𝐹 “ {𝑥}))) → (𝑚 · 𝑥) = ((𝐻‘(𝑀‘(𝐹 “ {𝑥}))) · 𝑥))
8685eleq1d 2821 . . . . . . . 8 (𝑚 = (𝐻‘(𝑀‘(𝐹 “ {𝑥}))) → ((𝑚 · 𝑥) ∈ 𝐵 ↔ ((𝐻‘(𝑀‘(𝐹 “ {𝑥}))) · 𝑥) ∈ 𝐵))
8784, 86imbi12d 344 . . . . . . 7 (𝑚 = (𝐻‘(𝑀‘(𝐹 “ {𝑥}))) → (((𝜑𝑚 ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥𝐵) → (𝑚 · 𝑥) ∈ 𝐵) ↔ ((𝜑 ∧ (𝐻‘(𝑀‘(𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥𝐵) → ((𝐻‘(𝑀‘(𝐹 “ {𝑥}))) · 𝑥) ∈ 𝐵)))
88 sitgclg.4 . . . . . . 7 ((𝜑𝑚 ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥𝐵) → (𝑚 · 𝑥) ∈ 𝐵)
8987, 88vtoclg 3514 . . . . . 6 ((𝐻‘(𝑀‘(𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞)) → ((𝜑 ∧ (𝐻‘(𝑀‘(𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥𝐵) → ((𝐻‘(𝑀‘(𝐹 “ {𝑥}))) · 𝑥) ∈ 𝐵))
9082, 89mpcom 38 . . . . 5 ((𝜑 ∧ (𝐻‘(𝑀‘(𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥𝐵) → ((𝐻‘(𝑀‘(𝐹 “ {𝑥}))) · 𝑥) ∈ 𝐵)
9115, 60, 81, 90syl3anc 1370 . . . 4 ((𝜑𝑥 ∈ (ran 𝐹 ∖ { 0 })) → ((𝐻‘(𝑀‘(𝐹 “ {𝑥}))) · 𝑥) ∈ 𝐵)
9291fmpttd 7045 . . 3 (𝜑 → (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(𝐹 “ {𝑥}))) · 𝑥)):(ran 𝐹 ∖ { 0 })⟶𝐵)
93 mptexg 7153 . . . . . 6 ((ran 𝐹 ∖ { 0 }) ∈ V → (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(𝐹 “ {𝑥}))) · 𝑥)) ∈ V)
9414, 93syl 17 . . . . 5 (𝜑 → (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(𝐹 “ {𝑥}))) · 𝑥)) ∈ V)
954fvexi 6839 . . . . 5 0 ∈ V
96 suppimacnv 8060 . . . . 5 (((𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(𝐹 “ {𝑥}))) · 𝑥)) ∈ V ∧ 0 ∈ V) → ((𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(𝐹 “ {𝑥}))) · 𝑥)) supp 0 ) = ((𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(𝐹 “ {𝑥}))) · 𝑥)) “ (V ∖ { 0 })))
9794, 95, 96sylancl 586 . . . 4 (𝜑 → ((𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(𝐹 “ {𝑥}))) · 𝑥)) supp 0 ) = ((𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(𝐹 “ {𝑥}))) · 𝑥)) “ (V ∖ { 0 })))
981, 2, 3, 4, 5, 6, 7, 8, 9sibfrn 32604 . . . . 5 (𝜑 → ran 𝐹 ∈ Fin)
99 cnvimass 6019 . . . . . . 7 ((𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(𝐹 “ {𝑥}))) · 𝑥)) “ (V ∖ { 0 })) ⊆ dom (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(𝐹 “ {𝑥}))) · 𝑥))
100 eqid 2736 . . . . . . . 8 (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(𝐹 “ {𝑥}))) · 𝑥)) = (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(𝐹 “ {𝑥}))) · 𝑥))
101100dmmptss 6179 . . . . . . 7 dom (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(𝐹 “ {𝑥}))) · 𝑥)) ⊆ (ran 𝐹 ∖ { 0 })
10299, 101sstri 3941 . . . . . 6 ((𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(𝐹 “ {𝑥}))) · 𝑥)) “ (V ∖ { 0 })) ⊆ (ran 𝐹 ∖ { 0 })
103 difss 4078 . . . . . 6 (ran 𝐹 ∖ { 0 }) ⊆ ran 𝐹
104102, 103sstri 3941 . . . . 5 ((𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(𝐹 “ {𝑥}))) · 𝑥)) “ (V ∖ { 0 })) ⊆ ran 𝐹
105 ssfi 9038 . . . . 5 ((ran 𝐹 ∈ Fin ∧ ((𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(𝐹 “ {𝑥}))) · 𝑥)) “ (V ∖ { 0 })) ⊆ ran 𝐹) → ((𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(𝐹 “ {𝑥}))) · 𝑥)) “ (V ∖ { 0 })) ∈ Fin)
10698, 104, 105sylancl 586 . . . 4 (𝜑 → ((𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(𝐹 “ {𝑥}))) · 𝑥)) “ (V ∖ { 0 })) ∈ Fin)
10797, 106eqeltrd 2837 . . 3 (𝜑 → ((𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(𝐹 “ {𝑥}))) · 𝑥)) supp 0 ) ∈ Fin)
1081, 4, 11, 14, 92, 107gsumcl2 19610 . 2 (𝜑 → (𝑊 Σg (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(𝐹 “ {𝑥}))) · 𝑥))) ∈ 𝐵)
10910, 108eqeltrd 2837 1 (𝜑 → ((𝑊sitg𝑀)‘𝐹) ∈ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1086   = wceq 1540  wcel 2105  Vcvv 3441  cdif 3895  wss 3898  {csn 4573   cuni 4852  cmpt 5175   × cxp 5618  ccnv 5619  dom cdm 5620  ran crn 5621  cres 5622  cima 5623  Fun wfun 6473  wf 6475  cfv 6479  (class class class)co 7337   supp csupp 8047  Fincfn 8804  cr 10971  0cc0 10972  +∞cpnf 11107  (,)cioo 13180  [,)cico 13182  Basecbs 17009  Scalarcsca 17062   ·𝑠 cvsca 17063  distcds 17068  TopOpenctopn 17229  topGenctg 17245  0gc0g 17247   Σg cgsu 17248  CMndccmn 19481  DivRingcdr 20093  metUnifcmetu 20694  ℤModczlm 20808  chrcchr 20809  TopSpctps 22187  UnifStcuss 23511  CUnifSpccusp 23555  NrmRingcnrg 23841  NrmModcnlm 23842  ℝHomcrrh 32241   ℝExt crrext 32242  sigAlgebracsiga 32374  sigaGencsigagen 32404  measurescmeas 32461  sitgcsitg 32596
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5229  ax-sep 5243  ax-nul 5250  ax-pow 5308  ax-pr 5372  ax-un 7650  ax-cnex 11028  ax-resscn 11029  ax-1cn 11030  ax-icn 11031  ax-addcl 11032  ax-addrcl 11033  ax-mulcl 11034  ax-mulrcl 11035  ax-mulcom 11036  ax-addass 11037  ax-mulass 11038  ax-distr 11039  ax-i2m1 11040  ax-1ne0 11041  ax-1rid 11042  ax-rnegex 11043  ax-rrecex 11044  ax-cnre 11045  ax-pre-lttri 11046  ax-pre-lttrn 11047  ax-pre-ltadd 11048  ax-pre-mulgt0 11049  ax-pre-sup 11050  ax-addf 11051  ax-mulf 11052
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3917  df-nul 4270  df-if 4474  df-pw 4549  df-sn 4574  df-pr 4576  df-tp 4578  df-op 4580  df-uni 4853  df-int 4895  df-iun 4943  df-iin 4944  df-br 5093  df-opab 5155  df-mpt 5176  df-tr 5210  df-id 5518  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5575  df-se 5576  df-we 5577  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-pred 6238  df-ord 6305  df-on 6306  df-lim 6307  df-suc 6308  df-iota 6431  df-fun 6481  df-fn 6482  df-f 6483  df-f1 6484  df-fo 6485  df-f1o 6486  df-fv 6487  df-isom 6488  df-riota 7293  df-ov 7340  df-oprab 7341  df-mpo 7342  df-of 7595  df-om 7781  df-1st 7899  df-2nd 7900  df-supp 8048  df-tpos 8112  df-frecs 8167  df-wrecs 8198  df-recs 8272  df-rdg 8311  df-1o 8367  df-2o 8368  df-er 8569  df-map 8688  df-pm 8689  df-ixp 8757  df-en 8805  df-dom 8806  df-sdom 8807  df-fin 8808  df-fsupp 9227  df-fi 9268  df-sup 9299  df-inf 9300  df-oi 9367  df-card 9796  df-pnf 11112  df-mnf 11113  df-xr 11114  df-ltxr 11115  df-le 11116  df-sub 11308  df-neg 11309  df-div 11734  df-nn 12075  df-2 12137  df-3 12138  df-4 12139  df-5 12140  df-6 12141  df-7 12142  df-8 12143  df-9 12144  df-n0 12335  df-z 12421  df-dec 12539  df-uz 12684  df-q 12790  df-rp 12832  df-xneg 12949  df-xadd 12950  df-xmul 12951  df-ioo 13184  df-ico 13186  df-icc 13187  df-fz 13341  df-fzo 13484  df-fl 13613  df-mod 13691  df-seq 13823  df-exp 13884  df-hash 14146  df-cj 14909  df-re 14910  df-im 14911  df-sqrt 15045  df-abs 15046  df-dvds 16063  df-gcd 16301  df-numer 16536  df-denom 16537  df-gz 16728  df-struct 16945  df-sets 16962  df-slot 16980  df-ndx 16992  df-base 17010  df-ress 17039  df-plusg 17072  df-mulr 17073  df-starv 17074  df-sca 17075  df-vsca 17076  df-ip 17077  df-tset 17078  df-ple 17079  df-ds 17081  df-unif 17082  df-hom 17083  df-cco 17084  df-rest 17230  df-topn 17231  df-0g 17249  df-gsum 17250  df-topgen 17251  df-pt 17252  df-prds 17255  df-xrs 17310  df-qtop 17315  df-imas 17316  df-xps 17318  df-mre 17392  df-mrc 17393  df-acs 17395  df-mgm 18423  df-sgrp 18472  df-mnd 18483  df-mhm 18527  df-submnd 18528  df-grp 18676  df-minusg 18677  df-sbg 18678  df-mulg 18797  df-subg 18848  df-ghm 18928  df-cntz 19019  df-od 19232  df-cmn 19483  df-abl 19484  df-mgp 19816  df-ur 19833  df-ring 19880  df-cring 19881  df-oppr 19957  df-dvdsr 19978  df-unit 19979  df-invr 20009  df-dvr 20020  df-rnghom 20054  df-drng 20095  df-subrg 20127  df-abv 20183  df-lmod 20231  df-nzr 20635  df-psmet 20695  df-xmet 20696  df-met 20697  df-bl 20698  df-mopn 20699  df-fbas 20700  df-fg 20701  df-metu 20702  df-cnfld 20704  df-zring 20777  df-zrh 20811  df-zlm 20812  df-chr 20813  df-refld 20916  df-top 22149  df-topon 22166  df-topsp 22188  df-bases 22202  df-cld 22276  df-ntr 22277  df-cls 22278  df-nei 22355  df-cn 22484  df-cnp 22485  df-haus 22572  df-reg 22573  df-cmp 22644  df-tx 22819  df-hmeo 23012  df-fil 23103  df-fm 23195  df-flim 23196  df-flf 23197  df-fcls 23198  df-cnext 23317  df-ust 23458  df-utop 23489  df-uss 23514  df-usp 23515  df-ucn 23534  df-cfilu 23545  df-cusp 23556  df-xms 23579  df-ms 23580  df-tms 23581  df-nm 23844  df-ngp 23845  df-nrg 23847  df-nlm 23848  df-cncf 24147  df-cfil 24525  df-cmet 24527  df-cms 24605  df-qqh 32221  df-rrh 32243  df-rrext 32247  df-esum 32294  df-siga 32375  df-sigagen 32405  df-meas 32462  df-mbfm 32516  df-sitg 32597
This theorem is referenced by:  sitgclbn  32610  sitmcl  32618
  Copyright terms: Public domain W3C validator