Theorem sitgaddlemb 34330

Description: Lemma for * sitgadd . (Contributed by Thierry Arnoux, 10-Mar-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)
sitgadd.1	⊢ (𝜑 → 𝑊 ∈ TopSp)
sitgadd.2	⊢ (𝜑 → (𝑊 ↾v (𝐻 “ (0[,)+∞))) ∈ SLMod)
sitgadd.3	⊢ (𝜑 → 𝐽 ∈ Fre)
sitgadd.4	⊢ (𝜑 → 𝐹 ∈ dom (𝑊sitg𝑀))
sitgadd.5	⊢ (𝜑 → 𝐺 ∈ dom (𝑊sitg𝑀))
sitgadd.6	⊢ (𝜑 → (Scalar‘𝑊) ∈ ℝExt )
sitgadd.7	⊢ + = (+g‘𝑊)

Assertion

Ref	Expression
sitgaddlemb	⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {⟨ 0 , 0 ⟩})) → ((𝐻‘(𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))) · (2nd ‘𝑝)) ∈ 𝐵)

Proof of Theorem sitgaddlemb

Step	Hyp	Ref	Expression
1		sitgadd.2	. . 3 ⊢ (𝜑 → (𝑊 ↾v (𝐻 “ (0[,)+∞))) ∈ SLMod)
2	1	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {⟨ 0 , 0 ⟩})) → (𝑊 ↾v (𝐻 “ (0[,)+∞))) ∈ SLMod)
3		simpl 482	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {⟨ 0 , 0 ⟩})) → 𝜑)
4		sitgadd.6	. . . . . . . 8 ⊢ (𝜑 → (Scalar‘𝑊) ∈ ℝExt )
5		eqid 2735	. . . . . . . . 9 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
6	5	rrhfe 33975	. . . . . . . 8 ⊢ ((Scalar‘𝑊) ∈ ℝExt → (ℝHom‘(Scalar‘𝑊)):ℝ⟶(Base‘(Scalar‘𝑊)))
7	4, 6	syl 17	. . . . . . 7 ⊢ (𝜑 → (ℝHom‘(Scalar‘𝑊)):ℝ⟶(Base‘(Scalar‘𝑊)))
8		sitgval.h	. . . . . . . 8 ⊢ 𝐻 = (ℝHom‘(Scalar‘𝑊))
9	8	feq1i 6728	. . . . . . 7 ⊢ (𝐻:ℝ⟶(Base‘(Scalar‘𝑊)) ↔ (ℝHom‘(Scalar‘𝑊)):ℝ⟶(Base‘(Scalar‘𝑊)))
10	7, 9	sylibr 234	. . . . . 6 ⊢ (𝜑 → 𝐻:ℝ⟶(Base‘(Scalar‘𝑊)))
11	10	ffnd 6738	. . . . 5 ⊢ (𝜑 → 𝐻 Fn ℝ)
12	3, 11	syl 17	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {⟨ 0 , 0 ⟩})) → 𝐻 Fn ℝ)
13		rge0ssre 13493	. . . . 5 ⊢ (0[,)+∞) ⊆ ℝ
14	13	a1i 11	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {⟨ 0 , 0 ⟩})) → (0[,)+∞) ⊆ ℝ)
15		simpr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {⟨ 0 , 0 ⟩})) → 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {⟨ 0 , 0 ⟩}))
16	15	eldifad 3975	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {⟨ 0 , 0 ⟩})) → 𝑝 ∈ (ran 𝐹 × ran 𝐺))
17		xp1st 8045	. . . . . 6 ⊢ (𝑝 ∈ (ran 𝐹 × ran 𝐺) → (1st ‘𝑝) ∈ ran 𝐹)
18	16, 17	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {⟨ 0 , 0 ⟩})) → (1st ‘𝑝) ∈ ran 𝐹)
19		xp2nd 8046	. . . . . 6 ⊢ (𝑝 ∈ (ran 𝐹 × ran 𝐺) → (2nd ‘𝑝) ∈ ran 𝐺)
20	16, 19	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {⟨ 0 , 0 ⟩})) → (2nd ‘𝑝) ∈ ran 𝐺)
21	15	eldifbd 3976	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {⟨ 0 , 0 ⟩})) → ¬ 𝑝 ∈ {⟨ 0 , 0 ⟩})
22		velsn 4647	. . . . . . . . 9 ⊢ (𝑝 ∈ {⟨ 0 , 0 ⟩} ↔ 𝑝 = ⟨ 0 , 0 ⟩)
23	22	notbii 320	. . . . . . . 8 ⊢ (¬ 𝑝 ∈ {⟨ 0 , 0 ⟩} ↔ ¬ 𝑝 = ⟨ 0 , 0 ⟩)
24	21, 23	sylib 218	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {⟨ 0 , 0 ⟩})) → ¬ 𝑝 = ⟨ 0 , 0 ⟩)
25		eqopi 8049	. . . . . . . . . 10 ⊢ ((𝑝 ∈ (ran 𝐹 × ran 𝐺) ∧ ((1st ‘𝑝) = 0 ∧ (2nd ‘𝑝) = 0 )) → 𝑝 = ⟨ 0 , 0 ⟩)
26	25	ex 412	. . . . . . . . 9 ⊢ (𝑝 ∈ (ran 𝐹 × ran 𝐺) → (((1st ‘𝑝) = 0 ∧ (2nd ‘𝑝) = 0 ) → 𝑝 = ⟨ 0 , 0 ⟩))
27	26	con3d 152	. . . . . . . 8 ⊢ (𝑝 ∈ (ran 𝐹 × ran 𝐺) → (¬ 𝑝 = ⟨ 0 , 0 ⟩ → ¬ ((1st ‘𝑝) = 0 ∧ (2nd ‘𝑝) = 0 )))
28	27	imp 406	. . . . . . 7 ⊢ ((𝑝 ∈ (ran 𝐹 × ran 𝐺) ∧ ¬ 𝑝 = ⟨ 0 , 0 ⟩) → ¬ ((1st ‘𝑝) = 0 ∧ (2nd ‘𝑝) = 0 ))
29	16, 24, 28	syl2anc 584	. . . . . 6 ⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {⟨ 0 , 0 ⟩})) → ¬ ((1st ‘𝑝) = 0 ∧ (2nd ‘𝑝) = 0 ))
30		ianor 983	. . . . . . 7 ⊢ (¬ ((1st ‘𝑝) = 0 ∧ (2nd ‘𝑝) = 0 ) ↔ (¬ (1st ‘𝑝) = 0 ∨ ¬ (2nd ‘𝑝) = 0 ))
31		df-ne 2939	. . . . . . . 8 ⊢ ((1st ‘𝑝) ≠ 0 ↔ ¬ (1st ‘𝑝) = 0 )
32		df-ne 2939	. . . . . . . 8 ⊢ ((2nd ‘𝑝) ≠ 0 ↔ ¬ (2nd ‘𝑝) = 0 )
33	31, 32	orbi12i 914	. . . . . . 7 ⊢ (((1st ‘𝑝) ≠ 0 ∨ (2nd ‘𝑝) ≠ 0 ) ↔ (¬ (1st ‘𝑝) = 0 ∨ ¬ (2nd ‘𝑝) = 0 ))
34	30, 33	bitr4i 278	. . . . . 6 ⊢ (¬ ((1st ‘𝑝) = 0 ∧ (2nd ‘𝑝) = 0 ) ↔ ((1st ‘𝑝) ≠ 0 ∨ (2nd ‘𝑝) ≠ 0 ))
35	29, 34	sylib 218	. . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {⟨ 0 , 0 ⟩})) → ((1st ‘𝑝) ≠ 0 ∨ (2nd ‘𝑝) ≠ 0 ))
36		sitgval.b	. . . . . 6 ⊢ 𝐵 = (Base‘𝑊)
37		sitgval.j	. . . . . 6 ⊢ 𝐽 = (TopOpen‘𝑊)
38		sitgval.s	. . . . . 6 ⊢ 𝑆 = (sigaGen‘𝐽)
39		sitgval.0	. . . . . 6 ⊢ 0 = (0g‘𝑊)
40		sitgval.x	. . . . . 6 ⊢ · = ( ·𝑠 ‘𝑊)
41		sitgval.1	. . . . . 6 ⊢ (𝜑 → 𝑊 ∈ 𝑉)
42		sitgval.2	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ∪ ran measures)
43		sitgadd.4	. . . . . 6 ⊢ (𝜑 → 𝐹 ∈ dom (𝑊sitg𝑀))
44		sitgadd.5	. . . . . 6 ⊢ (𝜑 → 𝐺 ∈ dom (𝑊sitg𝑀))
45		sitgadd.1	. . . . . 6 ⊢ (𝜑 → 𝑊 ∈ TopSp)
46		sitgadd.3	. . . . . 6 ⊢ (𝜑 → 𝐽 ∈ Fre)
47	36, 37, 38, 39, 40, 8, 41, 42, 43, 44, 45, 46	sibfinima 34321	. . . . 5 ⊢ (((𝜑 ∧ (1st ‘𝑝) ∈ ran 𝐹 ∧ (2nd ‘𝑝) ∈ ran 𝐺) ∧ ((1st ‘𝑝) ≠ 0 ∨ (2nd ‘𝑝) ≠ 0 )) → (𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) ∈ (0[,)+∞))
48	3, 18, 20, 35, 47	syl31anc 1372	. . . 4 ⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {⟨ 0 , 0 ⟩})) → (𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) ∈ (0[,)+∞))
49		fnfvima 7253	. . . 4 ⊢ ((𝐻 Fn ℝ ∧ (0[,)+∞) ⊆ ℝ ∧ (𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) ∈ (0[,)+∞)) → (𝐻‘(𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))) ∈ (𝐻 “ (0[,)+∞)))
50	12, 14, 48, 49	syl3anc 1370	. . 3 ⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {⟨ 0 , 0 ⟩})) → (𝐻‘(𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))) ∈ (𝐻 “ (0[,)+∞)))
51		imassrn 6091	. . . . . 6 ⊢ (𝐻 “ (0[,)+∞)) ⊆ ran 𝐻
52	10	frnd 6745	. . . . . 6 ⊢ (𝜑 → ran 𝐻 ⊆ (Base‘(Scalar‘𝑊)))
53	51, 52	sstrid 4007	. . . . 5 ⊢ (𝜑 → (𝐻 “ (0[,)+∞)) ⊆ (Base‘(Scalar‘𝑊)))
54		eqid 2735	. . . . . 6 ⊢ ((Scalar‘𝑊) ↾s (𝐻 “ (0[,)+∞))) = ((Scalar‘𝑊) ↾s (𝐻 “ (0[,)+∞)))
55	54, 5	ressbas2 17283	. . . . 5 ⊢ ((𝐻 “ (0[,)+∞)) ⊆ (Base‘(Scalar‘𝑊)) → (𝐻 “ (0[,)+∞)) = (Base‘((Scalar‘𝑊) ↾s (𝐻 “ (0[,)+∞)))))
56	53, 55	syl 17	. . . 4 ⊢ (𝜑 → (𝐻 “ (0[,)+∞)) = (Base‘((Scalar‘𝑊) ↾s (𝐻 “ (0[,)+∞)))))
57	3, 56	syl 17	. . 3 ⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {⟨ 0 , 0 ⟩})) → (𝐻 “ (0[,)+∞)) = (Base‘((Scalar‘𝑊) ↾s (𝐻 “ (0[,)+∞)))))
58	50, 57	eleqtrd 2841	. 2 ⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {⟨ 0 , 0 ⟩})) → (𝐻‘(𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))) ∈ (Base‘((Scalar‘𝑊) ↾s (𝐻 “ (0[,)+∞)))))
59	36, 37, 38, 39, 40, 8, 41, 42, 44	sibff 34318	. . . . . 6 ⊢ (𝜑 → 𝐺:∪ dom 𝑀⟶∪ 𝐽)
60	36, 37	tpsuni 22958	. . . . . . 7 ⊢ (𝑊 ∈ TopSp → 𝐵 = ∪ 𝐽)
61		feq3 6719	. . . . . . 7 ⊢ (𝐵 = ∪ 𝐽 → (𝐺:∪ dom 𝑀⟶𝐵 ↔ 𝐺:∪ dom 𝑀⟶∪ 𝐽))
62	45, 60, 61	3syl 18	. . . . . 6 ⊢ (𝜑 → (𝐺:∪ dom 𝑀⟶𝐵 ↔ 𝐺:∪ dom 𝑀⟶∪ 𝐽))
63	59, 62	mpbird 257	. . . . 5 ⊢ (𝜑 → 𝐺:∪ dom 𝑀⟶𝐵)
64	63	frnd 6745	. . . 4 ⊢ (𝜑 → ran 𝐺 ⊆ 𝐵)
65	64	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {⟨ 0 , 0 ⟩})) → ran 𝐺 ⊆ 𝐵)
66	65, 20	sseldd 3996	. 2 ⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {⟨ 0 , 0 ⟩})) → (2nd ‘𝑝) ∈ 𝐵)
67	8	fvexi 6921	. . . 4 ⊢ 𝐻 ∈ V
68		imaexg 7936	. . . 4 ⊢ (𝐻 ∈ V → (𝐻 “ (0[,)+∞)) ∈ V)
69		eqid 2735	. . . . 5 ⊢ (𝑊 ↾v (𝐻 “ (0[,)+∞))) = (𝑊 ↾v (𝐻 “ (0[,)+∞)))
70	69, 36	resvbas 33339	. . . 4 ⊢ ((𝐻 “ (0[,)+∞)) ∈ V → 𝐵 = (Base‘(𝑊 ↾v (𝐻 “ (0[,)+∞)))))
71	67, 68, 70	mp2b 10	. . 3 ⊢ 𝐵 = (Base‘(𝑊 ↾v (𝐻 “ (0[,)+∞))))
72		eqid 2735	. . . . 5 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
73	69, 72, 5	resvsca 33336	. . . 4 ⊢ ((𝐻 “ (0[,)+∞)) ∈ V → ((Scalar‘𝑊) ↾s (𝐻 “ (0[,)+∞))) = (Scalar‘(𝑊 ↾v (𝐻 “ (0[,)+∞)))))
74	67, 68, 73	mp2b 10	. . 3 ⊢ ((Scalar‘𝑊) ↾s (𝐻 “ (0[,)+∞))) = (Scalar‘(𝑊 ↾v (𝐻 “ (0[,)+∞))))
75	69, 40	resvvsca 33343	. . . 4 ⊢ ((𝐻 “ (0[,)+∞)) ∈ V → · = ( ·𝑠 ‘(𝑊 ↾v (𝐻 “ (0[,)+∞)))))
76	67, 68, 75	mp2b 10	. . 3 ⊢ · = ( ·𝑠 ‘(𝑊 ↾v (𝐻 “ (0[,)+∞))))
77		eqid 2735	. . 3 ⊢ (Base‘((Scalar‘𝑊) ↾s (𝐻 “ (0[,)+∞)))) = (Base‘((Scalar‘𝑊) ↾s (𝐻 “ (0[,)+∞))))
78	71, 74, 76, 77	slmdvscl 33203	. 2 ⊢ (((𝑊 ↾v (𝐻 “ (0[,)+∞))) ∈ SLMod ∧ (𝐻‘(𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))) ∈ (Base‘((Scalar‘𝑊) ↾s (𝐻 “ (0[,)+∞)))) ∧ (2nd ‘𝑝) ∈ 𝐵) → ((𝐻‘(𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))) · (2nd ‘𝑝)) ∈ 𝐵)
79	2, 58, 66, 78	syl3anc 1370	1 ⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {⟨ 0 , 0 ⟩})) → ((𝐻‘(𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))) · (2nd ‘𝑝)) ∈ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1537   ∈ wcel 2106   ≠ wne 2938  Vcvv 3478   ∖ cdif 3960   ∩ cin 3962   ⊆ wss 3963  {csn 4631  ⟨cop 4637  ∪ cuni 4912   × cxp 5687  ^◡ccnv 5688  dom cdm 5689  ran crn 5690   “ cima 5692   Fn wfn 6558  ⟶wf 6559  ‘cfv 6563  (class class class)co 7431  1^st c1st 8011  2^nd c2nd 8012  ℝcr 11152  0cc0 11153  +∞cpnf 11290  [,)cico 13386  Basecbs 17245   ↾_s cress 17274  +_gcplusg 17298  Scalarcsca 17301   ·_𝑠 cvsca 17302  TopOpenctopn 17468  0_gc0g 17486  TopSpctps 22954  Frect1 23331  SLModcslmd 33189   ↾_v cresv 33330  ℝHomcrrh 33956   ℝExt crrext 33957  sigaGencsigagen 34119  measurescmeas 34176  sitgcsitg 34311

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-inf2 9679  ax-ac2 10501  ax-cnex 11209  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-mulcom 11217  ax-addass 11218  ax-mulass 11219  ax-distr 11220  ax-i2m1 11221  ax-1ne0 11222  ax-1rid 11223  ax-rnegex 11224  ax-rrecex 11225  ax-cnre 11226  ax-pre-lttri 11227  ax-pre-lttrn 11228  ax-pre-ltadd 11229  ax-pre-mulgt0 11230  ax-pre-sup 11231  ax-addf 11232  ax-mulf 11233

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-tp 4636  df-op 4638  df-uni 4913  df-int 4952  df-iun 4998  df-iin 4999  df-disj 5116  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-se 5642  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-isom 6572  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-of 7697  df-om 7888  df-1st 8013  df-2nd 8014  df-supp 8185  df-tpos 8250  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-1o 8505  df-2o 8506  df-er 8744  df-map 8867  df-pm 8868  df-ixp 8937  df-en 8985  df-dom 8986  df-sdom 8987  df-fin 8988  df-fsupp 9400  df-fi 9449  df-sup 9480  df-inf 9481  df-oi 9548  df-dju 9939  df-card 9977  df-acn 9980  df-ac 10154  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299  df-sub 11492  df-neg 11493  df-div 11919  df-nn 12265  df-2 12327  df-3 12328  df-4 12329  df-5 12330  df-6 12331  df-7 12332  df-8 12333  df-9 12334  df-n0 12525  df-z 12612  df-dec 12732  df-uz 12877  df-q 12989  df-rp 13033  df-xneg 13152  df-xadd 13153  df-xmul 13154  df-ioo 13388  df-ioc 13389  df-ico 13390  df-icc 13391  df-fz 13545  df-fzo 13692  df-fl 13829  df-mod 13907  df-seq 14040  df-exp 14100  df-fac 14310  df-bc 14339  df-hash 14367  df-shft 15103  df-cj 15135  df-re 15136  df-im 15137  df-sqrt 15271  df-abs 15272  df-limsup 15504  df-clim 15521  df-rlim 15522  df-sum 15720  df-ef 16100  df-sin 16102  df-cos 16103  df-pi 16105  df-dvds 16288  df-gcd 16529  df-numer 16769  df-denom 16770  df-gz 16964  df-struct 17181  df-sets 17198  df-slot 17216  df-ndx 17228  df-base 17246  df-ress 17275  df-plusg 17311  df-mulr 17312  df-starv 17313  df-sca 17314  df-vsca 17315  df-ip 17316  df-tset 17317  df-ple 17318  df-ds 17320  df-unif 17321  df-hom 17322  df-cco 17323  df-rest 17469  df-topn 17470  df-0g 17488  df-gsum 17489  df-topgen 17490  df-pt 17491  df-prds 17494  df-ordt 17548  df-xrs 17549  df-qtop 17554  df-imas 17555  df-xps 17557  df-mre 17631  df-mrc 17632  df-acs 17634  df-ps 18624  df-tsr 18625  df-plusf 18665  df-mgm 18666  df-sgrp 18745  df-mnd 18761  df-mhm 18809  df-submnd 18810  df-grp 18967  df-minusg 18968  df-sbg 18969  df-mulg 19099  df-subg 19154  df-ghm 19244  df-cntz 19348  df-od 19561  df-cmn 19815  df-abl 19816  df-mgp 20153  df-rng 20171  df-ur 20200  df-ring 20253  df-cring 20254  df-oppr 20351  df-dvdsr 20374  df-unit 20375  df-invr 20405  df-dvr 20418  df-rhm 20489  df-nzr 20530  df-subrng 20563  df-subrg 20587  df-drng 20748  df-abv 20827  df-lmod 20877  df-scaf 20878  df-sra 21190  df-rgmod 21191  df-psmet 21374  df-xmet 21375  df-met 21376  df-bl 21377  df-mopn 21378  df-fbas 21379  df-fg 21380  df-metu 21381  df-cnfld 21383  df-zring 21476  df-zrh 21532  df-zlm 21533  df-chr 21534  df-refld 21641  df-top 22916  df-topon 22933  df-topsp 22955  df-bases 22969  df-cld 23043  df-ntr 23044  df-cls 23045  df-nei 23122  df-lp 23160  df-perf 23161  df-cn 23251  df-cnp 23252  df-t1 23338  df-haus 23339  df-reg 23340  df-cmp 23411  df-tx 23586  df-hmeo 23779  df-fil 23870  df-fm 23962  df-flim 23963  df-flf 23964  df-fcls 23965  df-cnext 24084  df-tmd 24096  df-tgp 24097  df-tsms 24151  df-trg 24184  df-ust 24225  df-utop 24256  df-uss 24281  df-usp 24282  df-ucn 24301  df-cfilu 24312  df-cusp 24323  df-xms 24346  df-ms 24347  df-tms 24348  df-nm 24611  df-ngp 24612  df-nrg 24614  df-nlm 24615  df-ii 24917  df-cncf 24918  df-cfil 25303  df-cmet 25305  df-cms 25383  df-limc 25916  df-dv 25917  df-log 26613  df-slmd 33190  df-resv 33331  df-qqh 33934  df-rrh 33958  df-rrext 33962  df-esum 34009  df-siga 34090  df-sigagen 34120  df-meas 34177  df-mbfm 34231  df-sitg 34312

This theorem is referenced by: (None)