minveclem4a - Metamath Proof Explorer

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

Theorem minveclem4a 25397

Description: Lemma for minvec 25403. 𝐹 converges to a point 𝑃 in 𝑌. (Contributed by Mario Carneiro, 7-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.)

**Hypotheses**
Ref	Expression
minvec.x	⊢ 𝑋 = (Base‘𝑈)
minvec.m	⊢ − = (-_g‘𝑈)
minvec.n	⊢ 𝑁 = (norm‘𝑈)
minvec.u	⊢ (𝜑 → 𝑈 ∈ ℂPreHil)
minvec.y	⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈))
minvec.w	⊢ (𝜑 → (𝑈 ↾_s 𝑌) ∈ CMetSp)
minvec.a	⊢ (𝜑 → 𝐴 ∈ 𝑋)
minvec.j	⊢ 𝐽 = (TopOpen‘𝑈)
minvec.r	⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))
minvec.s	⊢ 𝑆 = inf(𝑅, ℝ, < )
minvec.d	⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋))
minvec.f	⊢ 𝐹 = ran (𝑟 ∈ ℝ⁺ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)})
minvec.p	⊢ 𝑃 = ∪ (𝐽 fLim (𝑋filGen𝐹))

**Assertion**
Ref	Expression
minveclem4a	⊢ (𝜑 → 𝑃 ∈ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌))

Distinct variable groups: 𝑦, − 𝑦,𝑟,𝐴 𝐽,𝑟,𝑦 𝑦,𝑃 𝑦,𝐹 𝑦,𝑁 𝜑,𝑟,𝑦 𝑦,𝑅 𝑦,𝑈 𝑋,𝑟,𝑦 𝑌,𝑟,𝑦 𝐷,𝑟,𝑦 𝑆,𝑟,𝑦 Allowed substitution hints: 𝑃(𝑟) 𝑅(𝑟) 𝑈(𝑟) 𝐹(𝑟) − (𝑟) 𝑁(𝑟)

Proof of Theorem minveclem4a Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		minvec.p	. 2 ⊢ 𝑃 = ∪ (𝐽 fLim (𝑋filGen𝐹))
2		ovex 7400	. . . . 5 ⊢ (𝐽 fLim (𝑋filGen𝐹)) ∈ V
3	2	uniex 7695	. . . 4 ⊢ ∪ (𝐽 fLim (𝑋filGen𝐹)) ∈ V
4	3	snid 4606	. . 3 ⊢ ∪ (𝐽 fLim (𝑋filGen𝐹)) ∈ {∪ (𝐽 fLim (𝑋filGen𝐹))}
5		minvec.u	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑈 ∈ ℂPreHil)
6		cphngp 25140	. . . . . . . . . . . 12 ⊢ (𝑈 ∈ ℂPreHil → 𝑈 ∈ NrmGrp)
7		ngpxms 24566	. . . . . . . . . . . 12 ⊢ (𝑈 ∈ NrmGrp → 𝑈 ∈ ∞MetSp)
8	5, 6, 7	3syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑈 ∈ ∞MetSp)
9		minvec.j	. . . . . . . . . . . 12 ⊢ 𝐽 = (TopOpen‘𝑈)
10		minvec.x	. . . . . . . . . . . 12 ⊢ 𝑋 = (Base‘𝑈)
11		minvec.d	. . . . . . . . . . . 12 ⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋))
12	9, 10, 11	xmstopn 24416	. . . . . . . . . . 11 ⊢ (𝑈 ∈ ∞MetSp → 𝐽 = (MetOpen‘𝐷))
13	8, 12	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐽 = (MetOpen‘𝐷))
14	13	oveq1d 7382	. . . . . . . . 9 ⊢ (𝜑 → (𝐽 ↾_t 𝑌) = ((MetOpen‘𝐷) ↾_t 𝑌))
15	10, 11	xmsxmet 24421	. . . . . . . . . . 11 ⊢ (𝑈 ∈ ∞MetSp → 𝐷 ∈ (∞Met‘𝑋))
16	8, 15	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))
17		minvec.y	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈))
18		eqid 2736	. . . . . . . . . . . 12 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈)
19	10, 18	lssss 20931	. . . . . . . . . . 11 ⊢ (𝑌 ∈ (LSubSp‘𝑈) → 𝑌 ⊆ 𝑋)
20	17, 19	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑌 ⊆ 𝑋)
21		eqid 2736	. . . . . . . . . . 11 ⊢ (𝐷 ↾ (𝑌 × 𝑌)) = (𝐷 ↾ (𝑌 × 𝑌))
22		eqid 2736	. . . . . . . . . . 11 ⊢ (MetOpen‘𝐷) = (MetOpen‘𝐷)
23		eqid 2736	. . . . . . . . . . 11 ⊢ (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) = (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌)))
24	21, 22, 23	metrest 24489	. . . . . . . . . 10 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → ((MetOpen‘𝐷) ↾_t 𝑌) = (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))
25	16, 20, 24	syl2anc 585	. . . . . . . . 9 ⊢ (𝜑 → ((MetOpen‘𝐷) ↾_t 𝑌) = (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))
26	14, 25	eqtr2d 2772	. . . . . . . 8 ⊢ (𝜑 → (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) = (𝐽 ↾_t 𝑌))
27		minvec.m	. . . . . . . . . . . 12 ⊢ − = (-_g‘𝑈)
28		minvec.n	. . . . . . . . . . . 12 ⊢ 𝑁 = (norm‘𝑈)
29		minvec.w	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑈 ↾_s 𝑌) ∈ CMetSp)
30		minvec.a	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ 𝑋)
31		minvec.r	. . . . . . . . . . . 12 ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))
32		minvec.s	. . . . . . . . . . . 12 ⊢ 𝑆 = inf(𝑅, ℝ, < )
33		minvec.f	. . . . . . . . . . . 12 ⊢ 𝐹 = ran (𝑟 ∈ ℝ⁺ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)})
34	10, 27, 28, 5, 17, 29, 30, 9, 31, 32, 11, 33	minveclem3b 25395	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ (fBas‘𝑌))
35		fgcl 23843	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (fBas‘𝑌) → (𝑌filGen𝐹) ∈ (Fil‘𝑌))
36	34, 35	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝑌filGen𝐹) ∈ (Fil‘𝑌))
37	10	fvexi 6854	. . . . . . . . . . 11 ⊢ 𝑋 ∈ V
38	37	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ V)
39		trfg 23856	. . . . . . . . . 10 ⊢ (((𝑌filGen𝐹) ∈ (Fil‘𝑌) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑋 ∈ V) → ((𝑋filGen(𝑌filGen𝐹)) ↾_t 𝑌) = (𝑌filGen𝐹))
40	36, 20, 38, 39	syl3anc 1374	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋filGen(𝑌filGen𝐹)) ↾_t 𝑌) = (𝑌filGen𝐹))
41		fgabs 23844	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) → (𝑋filGen(𝑌filGen𝐹)) = (𝑋filGen𝐹))
42	34, 20, 41	syl2anc 585	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋filGen(𝑌filGen𝐹)) = (𝑋filGen𝐹))
43	42	oveq1d 7382	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋filGen(𝑌filGen𝐹)) ↾_t 𝑌) = ((𝑋filGen𝐹) ↾_t 𝑌))
44	40, 43	eqtr3d 2773	. . . . . . . 8 ⊢ (𝜑 → (𝑌filGen𝐹) = ((𝑋filGen𝐹) ↾_t 𝑌))
45	26, 44	oveq12d 7385	. . . . . . 7 ⊢ (𝜑 → ((MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) fLim (𝑌filGen𝐹)) = ((𝐽 ↾_t 𝑌) fLim ((𝑋filGen𝐹) ↾_t 𝑌)))
46		xmstps 24418	. . . . . . . . . 10 ⊢ (𝑈 ∈ ∞MetSp → 𝑈 ∈ TopSp)
47	8, 46	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑈 ∈ TopSp)
48	10, 9	istps 22899	. . . . . . . . 9 ⊢ (𝑈 ∈ TopSp ↔ 𝐽 ∈ (TopOn‘𝑋))
49	47, 48	sylib 218	. . . . . . . 8 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))
50		fbsspw 23797	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ (fBas‘𝑌) → 𝐹 ⊆ 𝒫 𝑌)
51	34, 50	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ⊆ 𝒫 𝑌)
52	20	sspwd 4554	. . . . . . . . . . 11 ⊢ (𝜑 → 𝒫 𝑌 ⊆ 𝒫 𝑋)
53	51, 52	sstrd 3932	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ⊆ 𝒫 𝑋)
54		fbasweak 23830	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (fBas‘𝑌) ∧ 𝐹 ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ V) → 𝐹 ∈ (fBas‘𝑋))
55	34, 53, 38, 54	syl3anc 1374	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ (fBas‘𝑋))
56		fgcl 23843	. . . . . . . . 9 ⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑋filGen𝐹) ∈ (Fil‘𝑋))
57	55, 56	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑋filGen𝐹) ∈ (Fil‘𝑋))
58		filfbas 23813	. . . . . . . . . . . . 13 ⊢ ((𝑌filGen𝐹) ∈ (Fil‘𝑌) → (𝑌filGen𝐹) ∈ (fBas‘𝑌))
59	34, 35, 58	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑌filGen𝐹) ∈ (fBas‘𝑌))
60		fbsspw 23797	. . . . . . . . . . . . . 14 ⊢ ((𝑌filGen𝐹) ∈ (fBas‘𝑌) → (𝑌filGen𝐹) ⊆ 𝒫 𝑌)
61	59, 60	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑌filGen𝐹) ⊆ 𝒫 𝑌)
62	61, 52	sstrd 3932	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑌filGen𝐹) ⊆ 𝒫 𝑋)
63		fbasweak 23830	. . . . . . . . . . . 12 ⊢ (((𝑌filGen𝐹) ∈ (fBas‘𝑌) ∧ (𝑌filGen𝐹) ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ V) → (𝑌filGen𝐹) ∈ (fBas‘𝑋))
64	59, 62, 38, 63	syl3anc 1374	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑌filGen𝐹) ∈ (fBas‘𝑋))
65		ssfg 23837	. . . . . . . . . . 11 ⊢ ((𝑌filGen𝐹) ∈ (fBas‘𝑋) → (𝑌filGen𝐹) ⊆ (𝑋filGen(𝑌filGen𝐹)))
66	64, 65	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝑌filGen𝐹) ⊆ (𝑋filGen(𝑌filGen𝐹)))
67	66, 42	sseqtrd 3958	. . . . . . . . 9 ⊢ (𝜑 → (𝑌filGen𝐹) ⊆ (𝑋filGen𝐹))
68		filtop 23820	. . . . . . . . . 10 ⊢ ((𝑌filGen𝐹) ∈ (Fil‘𝑌) → 𝑌 ∈ (𝑌filGen𝐹))
69	36, 68	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 ∈ (𝑌filGen𝐹))
70	67, 69	sseldd 3922	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ (𝑋filGen𝐹))
71		flimrest 23948	. . . . . . . 8 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑋filGen𝐹) ∈ (Fil‘𝑋) ∧ 𝑌 ∈ (𝑋filGen𝐹)) → ((𝐽 ↾_t 𝑌) fLim ((𝑋filGen𝐹) ↾_t 𝑌)) = ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌))
72	49, 57, 70, 71	syl3anc 1374	. . . . . . 7 ⊢ (𝜑 → ((𝐽 ↾_t 𝑌) fLim ((𝑋filGen𝐹) ↾_t 𝑌)) = ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌))
73	45, 72	eqtrd 2771	. . . . . 6 ⊢ (𝜑 → ((MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) fLim (𝑌filGen𝐹)) = ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌))
74	10, 27, 28, 5, 17, 29, 30, 9, 31, 32, 11	minveclem3a 25394	. . . . . . 7 ⊢ (𝜑 → (𝐷 ↾ (𝑌 × 𝑌)) ∈ (CMet‘𝑌))
75	10, 27, 28, 5, 17, 29, 30, 9, 31, 32, 11, 33	minveclem3 25396	. . . . . . 7 ⊢ (𝜑 → (𝑌filGen𝐹) ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌))))
76	23	cmetcvg 25252	. . . . . . 7 ⊢ (((𝐷 ↾ (𝑌 × 𝑌)) ∈ (CMet‘𝑌) ∧ (𝑌filGen𝐹) ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))) → ((MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) fLim (𝑌filGen𝐹)) ≠ ∅)
77	74, 75, 76	syl2anc 585	. . . . . 6 ⊢ (𝜑 → ((MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) fLim (𝑌filGen𝐹)) ≠ ∅)
78	73, 77	eqnetrrd 3000	. . . . 5 ⊢ (𝜑 → ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) ≠ ∅)
79	78	neneqd 2937	. . . 4 ⊢ (𝜑 → ¬ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) = ∅)
80		inss1 4177	. . . . . . 7 ⊢ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) ⊆ (𝐽 fLim (𝑋filGen𝐹))
81	22	methaus 24485	. . . . . . . . . . . . 13 ⊢ (𝐷 ∈ (∞Met‘𝑋) → (MetOpen‘𝐷) ∈ Haus)
82	15, 81	syl 17	. . . . . . . . . . . 12 ⊢ (𝑈 ∈ ∞MetSp → (MetOpen‘𝐷) ∈ Haus)
83	12, 82	eqeltrd 2836	. . . . . . . . . . 11 ⊢ (𝑈 ∈ ∞MetSp → 𝐽 ∈ Haus)
84		hausflimi 23945	. . . . . . . . . . 11 ⊢ (𝐽 ∈ Haus → ∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen𝐹)))
85	8, 83, 84	3syl 18	. . . . . . . . . 10 ⊢ (𝜑 → ∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen𝐹)))
86		ssn0 4344	. . . . . . . . . . . 12 ⊢ ((((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) ⊆ (𝐽 fLim (𝑋filGen𝐹)) ∧ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) ≠ ∅) → (𝐽 fLim (𝑋filGen𝐹)) ≠ ∅)
87	80, 78, 86	sylancr 588	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐽 fLim (𝑋filGen𝐹)) ≠ ∅)
88		n0moeu 4299	. . . . . . . . . . 11 ⊢ ((𝐽 fLim (𝑋filGen𝐹)) ≠ ∅ → (∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen𝐹)) ↔ ∃!𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen𝐹))))
89	87, 88	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen𝐹)) ↔ ∃!𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen𝐹))))
90	85, 89	mpbid 232	. . . . . . . . 9 ⊢ (𝜑 → ∃!𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen𝐹)))
91		euen1b 8975	. . . . . . . . 9 ⊢ ((𝐽 fLim (𝑋filGen𝐹)) ≈ 1_o ↔ ∃!𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen𝐹)))
92	90, 91	sylibr 234	. . . . . . . 8 ⊢ (𝜑 → (𝐽 fLim (𝑋filGen𝐹)) ≈ 1_o)
93		en1b 8972	. . . . . . . 8 ⊢ ((𝐽 fLim (𝑋filGen𝐹)) ≈ 1_o ↔ (𝐽 fLim (𝑋filGen𝐹)) = {∪ (𝐽 fLim (𝑋filGen𝐹))})
94	92, 93	sylib 218	. . . . . . 7 ⊢ (𝜑 → (𝐽 fLim (𝑋filGen𝐹)) = {∪ (𝐽 fLim (𝑋filGen𝐹))})
95	80, 94	sseqtrid 3964	. . . . . 6 ⊢ (𝜑 → ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) ⊆ {∪ (𝐽 fLim (𝑋filGen𝐹))})
96		sssn 4769	. . . . . 6 ⊢ (((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) ⊆ {∪ (𝐽 fLim (𝑋filGen𝐹))} ↔ (((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) = ∅ ∨ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) = {∪ (𝐽 fLim (𝑋filGen𝐹))}))
97	95, 96	sylib 218	. . . . 5 ⊢ (𝜑 → (((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) = ∅ ∨ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) = {∪ (𝐽 fLim (𝑋filGen𝐹))}))
98	97	ord 865	. . . 4 ⊢ (𝜑 → (¬ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) = ∅ → ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) = {∪ (𝐽 fLim (𝑋filGen𝐹))}))
99	79, 98	mpd 15	. . 3 ⊢ (𝜑 → ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) = {∪ (𝐽 fLim (𝑋filGen𝐹))})
100	4, 99	eleqtrrid 2843	. 2 ⊢ (𝜑 → ∪ (𝐽 fLim (𝑋filGen𝐹)) ∈ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌))
101	1, 100	eqeltrid 2840	1 ⊢ (𝜑 → 𝑃 ∈ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∨ wo 848 = wceq 1542 ∈ wcel 2114 ∃*wmo 2537 ∃!weu 2568 ≠ wne 2932 {crab 3389 Vcvv 3429 ∩ cin 3888 ⊆ wss 3889 ∅c0 4273 𝒫 cpw 4541 {csn 4567 ∪ cuni 4850 class class class wbr 5085 ↦ cmpt 5166 × cxp 5629 ran crn 5632 ↾ cres 5633 ‘cfv 6498 (class class class)co 7367 1_oc1o 8398 ≈ cen 8890 infcinf 9354 ℝcr 11037 + caddc 11041 < clt 11179 ≤ cle 11180 2c2 12236 ℝ⁺crp 12942 ↑cexp 14023 Basecbs 17179 ↾_s cress 17200 distcds 17229 ↾_t crest 17383 TopOpenctopn 17384 -_gcsg 18911 LSubSpclss 20926 ∞Metcxmet 21337 fBascfbas 21340 filGencfg 21341 MetOpencmopn 21342 TopOnctopon 22875 TopSpctps 22897 Hauscha 23273 Filcfil 23810 fLim cflim 23899 ∞MetSpcxms 24282 normcnm 24541 NrmGrpcngp 24542 ℂPreHilccph 25133 CauFilccfil 25219 CMetccmet 25221 CMetSpccms 25299

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 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2708 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5307 ax-pr 5375 ax-un 7689 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115 ax-pre-sup 11116 ax-addf 11117 ax-mulf 11118

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3062 df-rmo 3342 df-reu 3343 df-rab 3390 df-v 3431 df-sbc 3729 df-csb 3838 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-pss 3909 df-nul 4274 df-if 4467 df-pw 4543 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4851 df-int 4890 df-iun 4935 df-br 5086 df-opab 5148 df-mpt 5167 df-tr 5193 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6265 df-ord 6326 df-on 6327 df-lim 6328 df-suc 6329 df-iota 6454 df-fun 6500 df-fn 6501 df-f 6502 df-f1 6503 df-fo 6504 df-f1o 6505 df-fv 6506 df-riota 7324 df-ov 7370 df-oprab 7371 df-mpo 7372 df-om 7818 df-1st 7942 df-2nd 7943 df-tpos 8176 df-frecs 8231 df-wrecs 8262 df-recs 8311 df-rdg 8349 df-1o 8405 df-er 8643 df-map 8775 df-en 8894 df-dom 8895 df-sdom 8896 df-fin 8897 df-fi 9324 df-sup 9355 df-inf 9356 df-pnf 11181 df-mnf 11182 df-xr 11183 df-ltxr 11184 df-le 11185 df-sub 11379 df-neg 11380 df-div 11808 df-nn 12175 df-2 12244 df-3 12245 df-4 12246 df-5 12247 df-6 12248 df-7 12249 df-8 12250 df-9 12251 df-n0 12438 df-z 12525 df-dec 12645 df-uz 12789 df-q 12899 df-rp 12943 df-xneg 13063 df-xadd 13064 df-xmul 13065 df-ico 13304 df-icc 13305 df-fz 13462 df-seq 13964 df-exp 14024 df-cj 15061 df-re 15062 df-im 15063 df-sqrt 15197 df-abs 15198 df-struct 17117 df-sets 17134 df-slot 17152 df-ndx 17164 df-base 17180 df-ress 17201 df-plusg 17233 df-mulr 17234 df-starv 17235 df-sca 17236 df-vsca 17237 df-ip 17238 df-tset 17239 df-ple 17240 df-ds 17242 df-unif 17243 df-rest 17385 df-0g 17404 df-topgen 17406 df-mgm 18608 df-sgrp 18687 df-mnd 18703 df-mhm 18751 df-grp 18912 df-minusg 18913 df-sbg 18914 df-mulg 19044 df-subg 19099 df-ghm 19188 df-cmn 19757 df-abl 19758 df-mgp 20122 df-rng 20134 df-ur 20163 df-ring 20216 df-cring 20217 df-oppr 20317 df-dvdsr 20337 df-unit 20338 df-invr 20368 df-dvr 20381 df-rhm 20452 df-subrg 20547 df-drng 20708 df-staf 20816 df-srng 20817 df-lmod 20857 df-lss 20927 df-lmhm 21017 df-lvec 21098 df-sra 21168 df-rgmod 21169 df-psmet 21344 df-xmet 21345 df-met 21346 df-bl 21347 df-mopn 21348 df-fbas 21349 df-fg 21350 df-cnfld 21353 df-phl 21606 df-top 22859 df-topon 22876 df-topsp 22898 df-bases 22911 df-ntr 22985 df-nei 23063 df-haus 23280 df-fil 23811 df-flim 23904 df-xms 24285 df-ms 24286 df-nm 24547 df-ngp 24548 df-nlm 24551 df-clm 25030 df-cph 25135 df-cfil 25222 df-cmet 25224 df-cms 25302

This theorem is referenced by: minveclem4b 25398 minveclem4 25399

W3C validator