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 25664

Description: Lemma for minvec 25670. 𝐹 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 7450	. . . . 5 ⊢ (𝐽 fLim (𝑋filGen𝐹)) ∈ V
3	2	uniex 7747	. . . 4 ⊢ ∪ (𝐽 fLim (𝑋filGen𝐹)) ∈ V
4	3	snid 4626	. . 3 ⊢ ∪ (𝐽 fLim (𝑋filGen𝐹)) ∈ {∪ (𝐽 fLim (𝑋filGen𝐹))}
5		minvec.u	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑈 ∈ ℂPreHil)
6		cphngp 25407	. . . . . . . . . . . 12 ⊢ (𝑈 ∈ ℂPreHil → 𝑈 ∈ NrmGrp)
7		ngpxms 24833	. . . . . . . . . . . 12 ⊢ (𝑈 ∈ NrmGrp → 𝑈 ∈ ∞MetSp)
8	5, 6, 7	3syl 19	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑈 ∈ ∞MetSp)
9		minvec.j	. . . . . . . . . . . 12 ⊢ 𝐽 = (TopOpen‘𝑈)
10		minvec.x	. . . . . . . . . . . 12 ⊢ 𝑋 = (Base‘𝑈)
11		minvec.d	. . . . . . . . . . . 12 ⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋))
12	9, 10, 11	xmstopn 24683	. . . . . . . . . . 11 ⊢ (𝑈 ∈ ∞MetSp → 𝐽 = (MetOpen‘𝐷))
13	8, 12	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝐽 = (MetOpen‘𝐷))
14	13	oveq1d 7432	. . . . . . . . 9 ⊢ (𝜑 → (𝐽 ↾_t 𝑌) = ((MetOpen‘𝐷) ↾_t 𝑌))
15	10, 11	xmsxmet 24688	. . . . . . . . . . 11 ⊢ (𝑈 ∈ ∞MetSp → 𝐷 ∈ (∞Met‘𝑋))
16	8, 15	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))
17		minvec.y	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈))
18		eqid 2762	. . . . . . . . . . . 12 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈)
19	10, 18	lssss 21126	. . . . . . . . . . 11 ⊢ (𝑌 ∈ (LSubSp‘𝑈) → 𝑌 ⊆ 𝑋)
20	17, 19	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝑌 ⊆ 𝑋)
21		eqid 2762	. . . . . . . . . . 11 ⊢ (𝐷 ↾ (𝑌 × 𝑌)) = (𝐷 ↾ (𝑌 × 𝑌))
22		eqid 2762	. . . . . . . . . . 11 ⊢ (MetOpen‘𝐷) = (MetOpen‘𝐷)
23		eqid 2762	. . . . . . . . . . 11 ⊢ (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) = (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌)))
24	21, 22, 23	metrest 24756	. . . . . . . . . 10 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → ((MetOpen‘𝐷) ↾_t 𝑌) = (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))
25	16, 20, 24	syl2anc 596	. . . . . . . . 9 ⊢ (𝜑 → ((MetOpen‘𝐷) ↾_t 𝑌) = (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))
26	14, 25	eqtr2d 2798	. . . . . . . 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 25662	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ (fBas‘𝑌))
35		fgcl 24110	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (fBas‘𝑌) → (𝑌filGen𝐹) ∈ (Fil‘𝑌))
36	34, 35	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (𝑌filGen𝐹) ∈ (Fil‘𝑌))
37	10	fvexi 6896	. . . . . . . . . . 11 ⊢ 𝑋 ∈ V
38	37	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ V)
39		trfg 24123	. . . . . . . . . 10 ⊢ (((𝑌filGen𝐹) ∈ (Fil‘𝑌) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑋 ∈ V) → ((𝑋filGen(𝑌filGen𝐹)) ↾_t 𝑌) = (𝑌filGen𝐹))
40	36, 20, 38, 39	syl3anc 1398	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋filGen(𝑌filGen𝐹)) ↾_t 𝑌) = (𝑌filGen𝐹))
41		fgabs 24111	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) → (𝑋filGen(𝑌filGen𝐹)) = (𝑋filGen𝐹))
42	34, 20, 41	syl2anc 596	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋filGen(𝑌filGen𝐹)) = (𝑋filGen𝐹))
43	42	oveq1d 7432	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋filGen(𝑌filGen𝐹)) ↾_t 𝑌) = ((𝑋filGen𝐹) ↾_t 𝑌))
44	40, 43	eqtr3d 2799	. . . . . . . 8 ⊢ (𝜑 → (𝑌filGen𝐹) = ((𝑋filGen𝐹) ↾_t 𝑌))
45	26, 44	oveq12d 7435	. . . . . . 7 ⊢ (𝜑 → ((MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) fLim (𝑌filGen𝐹)) = ((𝐽 ↾_t 𝑌) fLim ((𝑋filGen𝐹) ↾_t 𝑌)))
46		xmstps 24685	. . . . . . . . . 10 ⊢ (𝑈 ∈ ∞MetSp → 𝑈 ∈ TopSp)
47	8, 46	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝑈 ∈ TopSp)
48	10, 9	istps 23165	. . . . . . . . 9 ⊢ (𝑈 ∈ TopSp ↔ 𝐽 ∈ (TopOn‘𝑋))
49	47, 48	sylib 221	. . . . . . . 8 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))
50		fbsspw 24064	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ (fBas‘𝑌) → 𝐹 ⊆ 𝒫 𝑌)
51	34, 50	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ⊆ 𝒫 𝑌)
52	20	sspwd 4573	. . . . . . . . . . 11 ⊢ (𝜑 → 𝒫 𝑌 ⊆ 𝒫 𝑋)
53	51, 52	sstrd 3944	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ⊆ 𝒫 𝑋)
54		fbasweak 24097	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (fBas‘𝑌) ∧ 𝐹 ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ V) → 𝐹 ∈ (fBas‘𝑋))
55	34, 53, 38, 54	syl3anc 1398	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ (fBas‘𝑋))
56		fgcl 24110	. . . . . . . . 9 ⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑋filGen𝐹) ∈ (Fil‘𝑋))
57	55, 56	syl 18	. . . . . . . 8 ⊢ (𝜑 → (𝑋filGen𝐹) ∈ (Fil‘𝑋))
58		filfbas 24080	. . . . . . . . . . . . 13 ⊢ ((𝑌filGen𝐹) ∈ (Fil‘𝑌) → (𝑌filGen𝐹) ∈ (fBas‘𝑌))
59	34, 35, 58	3syl 19	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑌filGen𝐹) ∈ (fBas‘𝑌))
60		fbsspw 24064	. . . . . . . . . . . . . 14 ⊢ ((𝑌filGen𝐹) ∈ (fBas‘𝑌) → (𝑌filGen𝐹) ⊆ 𝒫 𝑌)
61	59, 60	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑌filGen𝐹) ⊆ 𝒫 𝑌)
62	61, 52	sstrd 3944	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑌filGen𝐹) ⊆ 𝒫 𝑋)
63		fbasweak 24097	. . . . . . . . . . . 12 ⊢ (((𝑌filGen𝐹) ∈ (fBas‘𝑌) ∧ (𝑌filGen𝐹) ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ V) → (𝑌filGen𝐹) ∈ (fBas‘𝑋))
64	59, 62, 38, 63	syl3anc 1398	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑌filGen𝐹) ∈ (fBas‘𝑋))
65		ssfg 24104	. . . . . . . . . . 11 ⊢ ((𝑌filGen𝐹) ∈ (fBas‘𝑋) → (𝑌filGen𝐹) ⊆ (𝑋filGen(𝑌filGen𝐹)))
66	64, 65	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (𝑌filGen𝐹) ⊆ (𝑋filGen(𝑌filGen𝐹)))
67	66, 42	sseqtrd 3970	. . . . . . . . 9 ⊢ (𝜑 → (𝑌filGen𝐹) ⊆ (𝑋filGen𝐹))
68		filtop 24087	. . . . . . . . . 10 ⊢ ((𝑌filGen𝐹) ∈ (Fil‘𝑌) → 𝑌 ∈ (𝑌filGen𝐹))
69	36, 68	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 ∈ (𝑌filGen𝐹))
70	67, 69	sseldd 3935	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ (𝑋filGen𝐹))
71		flimrest 24215	. . . . . . . 8 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑋filGen𝐹) ∈ (Fil‘𝑋) ∧ 𝑌 ∈ (𝑋filGen𝐹)) → ((𝐽 ↾_t 𝑌) fLim ((𝑋filGen𝐹) ↾_t 𝑌)) = ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌))
72	49, 57, 70, 71	syl3anc 1398	. . . . . . 7 ⊢ (𝜑 → ((𝐽 ↾_t 𝑌) fLim ((𝑋filGen𝐹) ↾_t 𝑌)) = ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌))
73	45, 72	eqtrd 2797	. . . . . 6 ⊢ (𝜑 → ((MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) fLim (𝑌filGen𝐹)) = ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌))
74	10, 27, 28, 5, 17, 29, 30, 9, 31, 32, 11	minveclem3a 25661	. . . . . . 7 ⊢ (𝜑 → (𝐷 ↾ (𝑌 × 𝑌)) ∈ (CMet‘𝑌))
75	10, 27, 28, 5, 17, 29, 30, 9, 31, 32, 11, 33	minveclem3 25663	. . . . . . 7 ⊢ (𝜑 → (𝑌filGen𝐹) ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌))))
76	23	cmetcvg 25519	. . . . . . 7 ⊢ (((𝐷 ↾ (𝑌 × 𝑌)) ∈ (CMet‘𝑌) ∧ (𝑌filGen𝐹) ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))) → ((MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) fLim (𝑌filGen𝐹)) ≠ ∅)
77	74, 75, 76	syl2anc 596	. . . . . 6 ⊢ (𝜑 → ((MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) fLim (𝑌filGen𝐹)) ≠ ∅)
78	73, 77	eqnetrrd 3025	. . . . 5 ⊢ (𝜑 → ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) ≠ ∅)
79	78	neneqd 2962	. . . 4 ⊢ (𝜑 → ¬ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) = ∅)
80		inss1 4185	. . . . . . 7 ⊢ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) ⊆ (𝐽 fLim (𝑋filGen𝐹))
81	22	methaus 24752	. . . . . . . . . . . . 13 ⊢ (𝐷 ∈ (∞Met‘𝑋) → (MetOpen‘𝐷) ∈ Haus)
82	15, 81	syl 18	. . . . . . . . . . . 12 ⊢ (𝑈 ∈ ∞MetSp → (MetOpen‘𝐷) ∈ Haus)
83	12, 82	eqeltrd 2862	. . . . . . . . . . 11 ⊢ (𝑈 ∈ ∞MetSp → 𝐽 ∈ Haus)
84		hausflimi 24212	. . . . . . . . . . 11 ⊢ (𝐽 ∈ Haus → ∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen𝐹)))
85	8, 83, 84	3syl 19	. . . . . . . . . 10 ⊢ (𝜑 → ∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen𝐹)))
86		ssn0 4358	. . . . . . . . . . . 12 ⊢ ((((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) ⊆ (𝐽 fLim (𝑋filGen𝐹)) ∧ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) ≠ ∅) → (𝐽 fLim (𝑋filGen𝐹)) ≠ ∅)
87	80, 78, 86	sylancr 599	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐽 fLim (𝑋filGen𝐹)) ≠ ∅)
88		n0moeu 4310	. . . . . . . . . . 11 ⊢ ((𝐽 fLim (𝑋filGen𝐹)) ≠ ∅ → (∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen𝐹)) ↔ ∃!𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen𝐹))))
89	87, 88	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen𝐹)) ↔ ∃!𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen𝐹))))
90	85, 89	mpbid 235	. . . . . . . . 9 ⊢ (𝜑 → ∃!𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen𝐹)))
91		euen1b 9038	. . . . . . . . 9 ⊢ ((𝐽 fLim (𝑋filGen𝐹)) ≈ 1_o ↔ ∃!𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen𝐹)))
92	90, 91	sylibr 237	. . . . . . . 8 ⊢ (𝜑 → (𝐽 fLim (𝑋filGen𝐹)) ≈ 1_o)
93		en1b 9035	. . . . . . . 8 ⊢ ((𝐽 fLim (𝑋filGen𝐹)) ≈ 1_o ↔ (𝐽 fLim (𝑋filGen𝐹)) = {∪ (𝐽 fLim (𝑋filGen𝐹))})
94	92, 93	sylib 221	. . . . . . 7 ⊢ (𝜑 → (𝐽 fLim (𝑋filGen𝐹)) = {∪ (𝐽 fLim (𝑋filGen𝐹))})
95	80, 94	sseqtrid 3976	. . . . . 6 ⊢ (𝜑 → ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) ⊆ {∪ (𝐽 fLim (𝑋filGen𝐹))})
96		sssn 4790	. . . . . 6 ⊢ (((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) ⊆ {∪ (𝐽 fLim (𝑋filGen𝐹))} ↔ (((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) = ∅ ∨ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) = {∪ (𝐽 fLim (𝑋filGen𝐹))}))
97	95, 96	sylib 221	. . . . 5 ⊢ (𝜑 → (((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) = ∅ ∨ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) = {∪ (𝐽 fLim (𝑋filGen𝐹))}))
98	97	ord 878	. . . 4 ⊢ (𝜑 → (¬ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) = ∅ → ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) = {∪ (𝐽 fLim (𝑋filGen𝐹))}))
99	79, 98	mpd 16	. . 3 ⊢ (𝜑 → ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) = {∪ (𝐽 fLim (𝑋filGen𝐹))})
100	4, 99	eleqtrrid 2869	. 2 ⊢ (𝜑 → ∪ (𝐽 fLim (𝑋filGen𝐹)) ∈ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌))
101	1, 100	eqeltrid 2866	1 ⊢ (𝜑 → 𝑃 ∈ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∨ wo 861 = wceq 1570 ∈ wcel 2145 ∃*wmo 2564 ∃!weu 2595 ≠ wne 2957 {crab 3414 Vcvv 3453 ∩ cin 3901 ⊆ wss 3902 ∅c0 4282 𝒫 cpw 4560 {csn 4587 ∪ cuni 4870 class class class wbr 5107 ↦ cmpt 5190 × cxp 5657 ran crn 5660 ↾ cres 5661 ‘cfv 6537 (class class class)co 7417 1_oc1o 8452 ≈ cen 8953 infcinf 9415 ℝcr 11127 + caddc 11131 < clt 11271 ≤ cle 11272 2c2 12323 ℝ⁺crp 13046 ↑cexp 14129 Basecbs 17307 ↾_s cress 17328 distcds 17357 ↾_t crest 17511 TopOpenctopn 17512 -_gcsg 19065 LSubSpclss 21121 ∞Metcxmet 21576 fBascfbas 21579 filGencfg 21580 MetOpencmopn 21581 TopOnctopon 23141 TopSpctps 23163 Hauscha 23539 Filcfil 24077 fLim cflim 24166 ∞MetSpcxms 24549 normcnm 24808 NrmGrpcngp 24809 ℂPreHilccph 25400 CauFilccfil 25486 CMetccmet 25488 CMetSpccms 25566

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2734 ax-rep 5236 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7740 ax-cnex 11184 ax-resscn 11185 ax-1cn 11186 ax-icn 11187 ax-addcl 11188 ax-addrcl 11189 ax-mulcl 11190 ax-mulrcl 11191 ax-mulcom 11192 ax-addass 11193 ax-mulass 11194 ax-distr 11195 ax-i2m1 11196 ax-1ne0 11197 ax-1rid 11198 ax-rnegex 11199 ax-rrecex 11200 ax-cnre 11201 ax-pre-lttri 11202 ax-pre-lttrn 11203 ax-pre-ltadd 11204 ax-pre-mulgt0 11205 ax-pre-sup 11206 ax-addf 11207 ax-mulf 11208

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-tp 4592 df-op 4594 df-uni 4871 df-int 4911 df-iun 4956 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7374 df-ov 7420 df-oprab 7421 df-mpo 7422 df-om 7867 df-1st 7990 df-2nd 7991 df-tpos 8228 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-1o 8459 df-er 8700 df-map 8832 df-en 8957 df-dom 8958 df-sdom 8959 df-fin 8960 df-fi 9385 df-sup 9416 df-inf 9417 df-pnf 11273 df-mnf 11274 df-xr 11275 df-ltxr 11276 df-le 11277 df-sub 11471 df-neg 11472 df-div 11900 df-nn 12262 df-2 12331 df-3 12332 df-4 12333 df-5 12334 df-6 12335 df-7 12336 df-8 12337 df-9 12338 df-n0 12533 df-z 12620 df-dec 12741 df-uz 12892 df-q 13002 df-rp 13047 df-xneg 13167 df-xadd 13168 df-xmul 13169 df-ico 13408 df-icc 13409 df-fz 13566 df-seq 14070 df-exp 14130 df-cj 15190 df-re 15191 df-im 15192 df-sqrt 15326 df-abs 15327 df-struct 17245 df-sets 17262 df-slot 17280 df-ndx 17292 df-base 17308 df-ress 17329 df-plusg 17361 df-mulr 17362 df-starv 17363 df-sca 17364 df-vsca 17365 df-ip 17366 df-tset 17367 df-ple 17368 df-ds 17370 df-unif 17371 df-rest 17513 df-0g 17532 df-topgen 17534 df-mgm 18736 df-sgrp 18827 df-mnd 18843 df-mhm 18897 df-grp 19066 df-minusg 19067 df-sbg 19068 df-mulg 19197 df-subg 19252 df-ghm 19347 df-cmn 19915 df-abl 19916 df-mgp 20280 df-rng 20294 df-ur 20327 df-ring 20380 df-cring 20381 df-oppr 20484 df-dvdsr 20504 df-unit 20505 df-invr 20535 df-dvr 20548 df-rhm 20619 df-subrg 20738 df-drng 20898 df-staf 21011 df-srng 21012 df-lmod 21052 df-lss 21122 df-lmhm 21212 df-lvec 21293 df-sra 21363 df-rgmod 21364 df-psmet 21583 df-xmet 21584 df-met 21585 df-bl 21586 df-mopn 21587 df-fbas 21588 df-fg 21589 df-cnfld 21592 df-phl 21845 df-top 23125 df-topon 23142 df-topsp 23164 df-bases 23177 df-ntr 23251 df-nei 23329 df-haus 23546 df-fil 24078 df-flim 24171 df-xms 24552 df-ms 24553 df-nm 24814 df-ngp 24815 df-nlm 24818 df-clm 25297 df-cph 25402 df-cfil 25489 df-cmet 25491 df-cms 25569

This theorem is used by: minveclem4b 25665 minveclem4 25666

W3C validator