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 25382

Description: Lemma for minvec 25388. 𝐹 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 7438	. . . . 5 ⊢ (𝐽 fLim (𝑋filGen𝐹)) ∈ V
3	2	uniex 7735	. . . 4 ⊢ ∪ (𝐽 fLim (𝑋filGen𝐹)) ∈ V
4	3	snid 4638	. . 3 ⊢ ∪ (𝐽 fLim (𝑋filGen𝐹)) ∈ {∪ (𝐽 fLim (𝑋filGen𝐹))}
5		minvec.u	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑈 ∈ ℂPreHil)
6		cphngp 25125	. . . . . . . . . . . 12 ⊢ (𝑈 ∈ ℂPreHil → 𝑈 ∈ NrmGrp)
7		ngpxms 24540	. . . . . . . . . . . 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 24390	. . . . . . . . . . 11 ⊢ (𝑈 ∈ ∞MetSp → 𝐽 = (MetOpen‘𝐷))
13	8, 12	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐽 = (MetOpen‘𝐷))
14	13	oveq1d 7420	. . . . . . . . 9 ⊢ (𝜑 → (𝐽 ↾_t 𝑌) = ((MetOpen‘𝐷) ↾_t 𝑌))
15	10, 11	xmsxmet 24395	. . . . . . . . . . 11 ⊢ (𝑈 ∈ ∞MetSp → 𝐷 ∈ (∞Met‘𝑋))
16	8, 15	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))
17		minvec.y	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈))
18		eqid 2735	. . . . . . . . . . . 12 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈)
19	10, 18	lssss 20893	. . . . . . . . . . 11 ⊢ (𝑌 ∈ (LSubSp‘𝑈) → 𝑌 ⊆ 𝑋)
20	17, 19	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑌 ⊆ 𝑋)
21		eqid 2735	. . . . . . . . . . 11 ⊢ (𝐷 ↾ (𝑌 × 𝑌)) = (𝐷 ↾ (𝑌 × 𝑌))
22		eqid 2735	. . . . . . . . . . 11 ⊢ (MetOpen‘𝐷) = (MetOpen‘𝐷)
23		eqid 2735	. . . . . . . . . . 11 ⊢ (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) = (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌)))
24	21, 22, 23	metrest 24463	. . . . . . . . . 10 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → ((MetOpen‘𝐷) ↾_t 𝑌) = (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))
25	16, 20, 24	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → ((MetOpen‘𝐷) ↾_t 𝑌) = (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))
26	14, 25	eqtr2d 2771	. . . . . . . 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 25380	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ (fBas‘𝑌))
35		fgcl 23816	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (fBas‘𝑌) → (𝑌filGen𝐹) ∈ (Fil‘𝑌))
36	34, 35	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝑌filGen𝐹) ∈ (Fil‘𝑌))
37	10	fvexi 6890	. . . . . . . . . . 11 ⊢ 𝑋 ∈ V
38	37	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ V)
39		trfg 23829	. . . . . . . . . 10 ⊢ (((𝑌filGen𝐹) ∈ (Fil‘𝑌) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑋 ∈ V) → ((𝑋filGen(𝑌filGen𝐹)) ↾_t 𝑌) = (𝑌filGen𝐹))
40	36, 20, 38, 39	syl3anc 1373	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋filGen(𝑌filGen𝐹)) ↾_t 𝑌) = (𝑌filGen𝐹))
41		fgabs 23817	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) → (𝑋filGen(𝑌filGen𝐹)) = (𝑋filGen𝐹))
42	34, 20, 41	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋filGen(𝑌filGen𝐹)) = (𝑋filGen𝐹))
43	42	oveq1d 7420	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋filGen(𝑌filGen𝐹)) ↾_t 𝑌) = ((𝑋filGen𝐹) ↾_t 𝑌))
44	40, 43	eqtr3d 2772	. . . . . . . 8 ⊢ (𝜑 → (𝑌filGen𝐹) = ((𝑋filGen𝐹) ↾_t 𝑌))
45	26, 44	oveq12d 7423	. . . . . . 7 ⊢ (𝜑 → ((MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) fLim (𝑌filGen𝐹)) = ((𝐽 ↾_t 𝑌) fLim ((𝑋filGen𝐹) ↾_t 𝑌)))
46		xmstps 24392	. . . . . . . . . 10 ⊢ (𝑈 ∈ ∞MetSp → 𝑈 ∈ TopSp)
47	8, 46	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑈 ∈ TopSp)
48	10, 9	istps 22872	. . . . . . . . 9 ⊢ (𝑈 ∈ TopSp ↔ 𝐽 ∈ (TopOn‘𝑋))
49	47, 48	sylib 218	. . . . . . . 8 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))
50		fbsspw 23770	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ (fBas‘𝑌) → 𝐹 ⊆ 𝒫 𝑌)
51	34, 50	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ⊆ 𝒫 𝑌)
52	20	sspwd 4588	. . . . . . . . . . 11 ⊢ (𝜑 → 𝒫 𝑌 ⊆ 𝒫 𝑋)
53	51, 52	sstrd 3969	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ⊆ 𝒫 𝑋)
54		fbasweak 23803	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (fBas‘𝑌) ∧ 𝐹 ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ V) → 𝐹 ∈ (fBas‘𝑋))
55	34, 53, 38, 54	syl3anc 1373	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ (fBas‘𝑋))
56		fgcl 23816	. . . . . . . . 9 ⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑋filGen𝐹) ∈ (Fil‘𝑋))
57	55, 56	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑋filGen𝐹) ∈ (Fil‘𝑋))
58		filfbas 23786	. . . . . . . . . . . . 13 ⊢ ((𝑌filGen𝐹) ∈ (Fil‘𝑌) → (𝑌filGen𝐹) ∈ (fBas‘𝑌))
59	34, 35, 58	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑌filGen𝐹) ∈ (fBas‘𝑌))
60		fbsspw 23770	. . . . . . . . . . . . . 14 ⊢ ((𝑌filGen𝐹) ∈ (fBas‘𝑌) → (𝑌filGen𝐹) ⊆ 𝒫 𝑌)
61	59, 60	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑌filGen𝐹) ⊆ 𝒫 𝑌)
62	61, 52	sstrd 3969	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑌filGen𝐹) ⊆ 𝒫 𝑋)
63		fbasweak 23803	. . . . . . . . . . . 12 ⊢ (((𝑌filGen𝐹) ∈ (fBas‘𝑌) ∧ (𝑌filGen𝐹) ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ V) → (𝑌filGen𝐹) ∈ (fBas‘𝑋))
64	59, 62, 38, 63	syl3anc 1373	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑌filGen𝐹) ∈ (fBas‘𝑋))
65		ssfg 23810	. . . . . . . . . . 11 ⊢ ((𝑌filGen𝐹) ∈ (fBas‘𝑋) → (𝑌filGen𝐹) ⊆ (𝑋filGen(𝑌filGen𝐹)))
66	64, 65	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝑌filGen𝐹) ⊆ (𝑋filGen(𝑌filGen𝐹)))
67	66, 42	sseqtrd 3995	. . . . . . . . 9 ⊢ (𝜑 → (𝑌filGen𝐹) ⊆ (𝑋filGen𝐹))
68		filtop 23793	. . . . . . . . . 10 ⊢ ((𝑌filGen𝐹) ∈ (Fil‘𝑌) → 𝑌 ∈ (𝑌filGen𝐹))
69	36, 68	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 ∈ (𝑌filGen𝐹))
70	67, 69	sseldd 3959	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ (𝑋filGen𝐹))
71		flimrest 23921	. . . . . . . 8 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑋filGen𝐹) ∈ (Fil‘𝑋) ∧ 𝑌 ∈ (𝑋filGen𝐹)) → ((𝐽 ↾_t 𝑌) fLim ((𝑋filGen𝐹) ↾_t 𝑌)) = ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌))
72	49, 57, 70, 71	syl3anc 1373	. . . . . . 7 ⊢ (𝜑 → ((𝐽 ↾_t 𝑌) fLim ((𝑋filGen𝐹) ↾_t 𝑌)) = ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌))
73	45, 72	eqtrd 2770	. . . . . 6 ⊢ (𝜑 → ((MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) fLim (𝑌filGen𝐹)) = ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌))
74	10, 27, 28, 5, 17, 29, 30, 9, 31, 32, 11	minveclem3a 25379	. . . . . . 7 ⊢ (𝜑 → (𝐷 ↾ (𝑌 × 𝑌)) ∈ (CMet‘𝑌))
75	10, 27, 28, 5, 17, 29, 30, 9, 31, 32, 11, 33	minveclem3 25381	. . . . . . 7 ⊢ (𝜑 → (𝑌filGen𝐹) ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌))))
76	23	cmetcvg 25237	. . . . . . 7 ⊢ (((𝐷 ↾ (𝑌 × 𝑌)) ∈ (CMet‘𝑌) ∧ (𝑌filGen𝐹) ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))) → ((MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) fLim (𝑌filGen𝐹)) ≠ ∅)
77	74, 75, 76	syl2anc 584	. . . . . 6 ⊢ (𝜑 → ((MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) fLim (𝑌filGen𝐹)) ≠ ∅)
78	73, 77	eqnetrrd 3000	. . . . 5 ⊢ (𝜑 → ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) ≠ ∅)
79	78	neneqd 2937	. . . 4 ⊢ (𝜑 → ¬ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) = ∅)
80		inss1 4212	. . . . . . 7 ⊢ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) ⊆ (𝐽 fLim (𝑋filGen𝐹))
81	22	methaus 24459	. . . . . . . . . . . . 13 ⊢ (𝐷 ∈ (∞Met‘𝑋) → (MetOpen‘𝐷) ∈ Haus)
82	15, 81	syl 17	. . . . . . . . . . . 12 ⊢ (𝑈 ∈ ∞MetSp → (MetOpen‘𝐷) ∈ Haus)
83	12, 82	eqeltrd 2834	. . . . . . . . . . 11 ⊢ (𝑈 ∈ ∞MetSp → 𝐽 ∈ Haus)
84		hausflimi 23918	. . . . . . . . . . 11 ⊢ (𝐽 ∈ Haus → ∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen𝐹)))
85	8, 83, 84	3syl 18	. . . . . . . . . 10 ⊢ (𝜑 → ∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen𝐹)))
86		ssn0 4379	. . . . . . . . . . . 12 ⊢ ((((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) ⊆ (𝐽 fLim (𝑋filGen𝐹)) ∧ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) ≠ ∅) → (𝐽 fLim (𝑋filGen𝐹)) ≠ ∅)
87	80, 78, 86	sylancr 587	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐽 fLim (𝑋filGen𝐹)) ≠ ∅)
88		n0moeu 4334	. . . . . . . . . . 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 9042	. . . . . . . . 9 ⊢ ((𝐽 fLim (𝑋filGen𝐹)) ≈ 1_o ↔ ∃!𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen𝐹)))
92	90, 91	sylibr 234	. . . . . . . 8 ⊢ (𝜑 → (𝐽 fLim (𝑋filGen𝐹)) ≈ 1_o)
93		en1b 9039	. . . . . . . 8 ⊢ ((𝐽 fLim (𝑋filGen𝐹)) ≈ 1_o ↔ (𝐽 fLim (𝑋filGen𝐹)) = {∪ (𝐽 fLim (𝑋filGen𝐹))})
94	92, 93	sylib 218	. . . . . . 7 ⊢ (𝜑 → (𝐽 fLim (𝑋filGen𝐹)) = {∪ (𝐽 fLim (𝑋filGen𝐹))})
95	80, 94	sseqtrid 4001	. . . . . 6 ⊢ (𝜑 → ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) ⊆ {∪ (𝐽 fLim (𝑋filGen𝐹))})
96		sssn 4802	. . . . . 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 864	. . . 4 ⊢ (𝜑 → (¬ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) = ∅ → ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) = {∪ (𝐽 fLim (𝑋filGen𝐹))}))
99	79, 98	mpd 15	. . 3 ⊢ (𝜑 → ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) = {∪ (𝐽 fLim (𝑋filGen𝐹))})
100	4, 99	eleqtrrid 2841	. 2 ⊢ (𝜑 → ∪ (𝐽 fLim (𝑋filGen𝐹)) ∈ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌))
101	1, 100	eqeltrid 2838	1 ⊢ (𝜑 → 𝑃 ∈ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∨ wo 847 = wceq 1540 ∈ wcel 2108 ∃*wmo 2537 ∃!weu 2567 ≠ wne 2932 {crab 3415 Vcvv 3459 ∩ cin 3925 ⊆ wss 3926 ∅c0 4308 𝒫 cpw 4575 {csn 4601 ∪ cuni 4883 class class class wbr 5119 ↦ cmpt 5201 × cxp 5652 ran crn 5655 ↾ cres 5656 ‘cfv 6531 (class class class)co 7405 1_oc1o 8473 ≈ cen 8956 infcinf 9453 ℝcr 11128 + caddc 11132 < clt 11269 ≤ cle 11270 2c2 12295 ℝ⁺crp 13008 ↑cexp 14079 Basecbs 17228 ↾_s cress 17251 distcds 17280 ↾_t crest 17434 TopOpenctopn 17435 -_gcsg 18918 LSubSpclss 20888 ∞Metcxmet 21300 fBascfbas 21303 filGencfg 21304 MetOpencmopn 21305 TopOnctopon 22848 TopSpctps 22870 Hauscha 23246 Filcfil 23783 fLim cflim 23872 ∞MetSpcxms 24256 normcnm 24515 NrmGrpcngp 24516 ℂPreHilccph 25118 CauFilccfil 25204 CMetccmet 25206 CMetSpccms 25284

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-rep 5249 ax-sep 5266 ax-nul 5276 ax-pow 5335 ax-pr 5402 ax-un 7729 ax-cnex 11185 ax-resscn 11186 ax-1cn 11187 ax-icn 11188 ax-addcl 11189 ax-addrcl 11190 ax-mulcl 11191 ax-mulrcl 11192 ax-mulcom 11193 ax-addass 11194 ax-mulass 11195 ax-distr 11196 ax-i2m1 11197 ax-1ne0 11198 ax-1rid 11199 ax-rnegex 11200 ax-rrecex 11201 ax-cnre 11202 ax-pre-lttri 11203 ax-pre-lttrn 11204 ax-pre-ltadd 11205 ax-pre-mulgt0 11206 ax-pre-sup 11207 ax-addf 11208 ax-mulf 11209

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2809 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3359 df-reu 3360 df-rab 3416 df-v 3461 df-sbc 3766 df-csb 3875 df-dif 3929 df-un 3931 df-in 3933 df-ss 3943 df-pss 3946 df-nul 4309 df-if 4501 df-pw 4577 df-sn 4602 df-pr 4604 df-tp 4606 df-op 4608 df-uni 4884 df-int 4923 df-iun 4969 df-br 5120 df-opab 5182 df-mpt 5202 df-tr 5230 df-id 5548 df-eprel 5553 df-po 5561 df-so 5562 df-fr 5606 df-we 5608 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-pred 6290 df-ord 6355 df-on 6356 df-lim 6357 df-suc 6358 df-iota 6484 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-riota 7362 df-ov 7408 df-oprab 7409 df-mpo 7410 df-om 7862 df-1st 7988 df-2nd 7989 df-tpos 8225 df-frecs 8280 df-wrecs 8311 df-recs 8385 df-rdg 8424 df-1o 8480 df-er 8719 df-map 8842 df-en 8960 df-dom 8961 df-sdom 8962 df-fin 8963 df-fi 9423 df-sup 9454 df-inf 9455 df-pnf 11271 df-mnf 11272 df-xr 11273 df-ltxr 11274 df-le 11275 df-sub 11468 df-neg 11469 df-div 11895 df-nn 12241 df-2 12303 df-3 12304 df-4 12305 df-5 12306 df-6 12307 df-7 12308 df-8 12309 df-9 12310 df-n0 12502 df-z 12589 df-dec 12709 df-uz 12853 df-q 12965 df-rp 13009 df-xneg 13128 df-xadd 13129 df-xmul 13130 df-ico 13368 df-icc 13369 df-fz 13525 df-seq 14020 df-exp 14080 df-cj 15118 df-re 15119 df-im 15120 df-sqrt 15254 df-abs 15255 df-struct 17166 df-sets 17183 df-slot 17201 df-ndx 17213 df-base 17229 df-ress 17252 df-plusg 17284 df-mulr 17285 df-starv 17286 df-sca 17287 df-vsca 17288 df-ip 17289 df-tset 17290 df-ple 17291 df-ds 17293 df-unif 17294 df-rest 17436 df-0g 17455 df-topgen 17457 df-mgm 18618 df-sgrp 18697 df-mnd 18713 df-mhm 18761 df-grp 18919 df-minusg 18920 df-sbg 18921 df-mulg 19051 df-subg 19106 df-ghm 19196 df-cmn 19763 df-abl 19764 df-mgp 20101 df-rng 20113 df-ur 20142 df-ring 20195 df-cring 20196 df-oppr 20297 df-dvdsr 20317 df-unit 20318 df-invr 20348 df-dvr 20361 df-rhm 20432 df-subrg 20530 df-drng 20691 df-staf 20799 df-srng 20800 df-lmod 20819 df-lss 20889 df-lmhm 20980 df-lvec 21061 df-sra 21131 df-rgmod 21132 df-psmet 21307 df-xmet 21308 df-met 21309 df-bl 21310 df-mopn 21311 df-fbas 21312 df-fg 21313 df-cnfld 21316 df-phl 21586 df-top 22832 df-topon 22849 df-topsp 22871 df-bases 22884 df-ntr 22958 df-nei 23036 df-haus 23253 df-fil 23784 df-flim 23877 df-xms 24259 df-ms 24260 df-nm 24521 df-ngp 24522 df-nlm 24525 df-clm 25014 df-cph 25120 df-cfil 25207 df-cmet 25209 df-cms 25287

This theorem is referenced by: minveclem4b 25383 minveclem4 25384

W3C validator