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 25479

Description: Lemma for minvec 25485. 𝐹 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 7423	. . . . 5 ⊢ (𝐽 fLim (𝑋filGen𝐹)) ∈ V
3	2	uniex 7718	. . . 4 ⊢ ∪ (𝐽 fLim (𝑋filGen𝐹)) ∈ V
4	3	snid 4618	. . 3 ⊢ ∪ (𝐽 fLim (𝑋filGen𝐹)) ∈ {∪ (𝐽 fLim (𝑋filGen𝐹))}
5		minvec.u	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑈 ∈ ℂPreHil)
6		cphngp 25222	. . . . . . . . . . . 12 ⊢ (𝑈 ∈ ℂPreHil → 𝑈 ∈ NrmGrp)
7		ngpxms 24648	. . . . . . . . . . . 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 24498	. . . . . . . . . . 11 ⊢ (𝑈 ∈ ∞MetSp → 𝐽 = (MetOpen‘𝐷))
13	8, 12	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐽 = (MetOpen‘𝐷))
14	13	oveq1d 7405	. . . . . . . . 9 ⊢ (𝜑 → (𝐽 ↾_t 𝑌) = ((MetOpen‘𝐷) ↾_t 𝑌))
15	10, 11	xmsxmet 24503	. . . . . . . . . . 11 ⊢ (𝑈 ∈ ∞MetSp → 𝐷 ∈ (∞Met‘𝑋))
16	8, 15	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))
17		minvec.y	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈))
18		eqid 2761	. . . . . . . . . . . 12 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈)
19	10, 18	lssss 20990	. . . . . . . . . . 11 ⊢ (𝑌 ∈ (LSubSp‘𝑈) → 𝑌 ⊆ 𝑋)
20	17, 19	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑌 ⊆ 𝑋)
21		eqid 2761	. . . . . . . . . . 11 ⊢ (𝐷 ↾ (𝑌 × 𝑌)) = (𝐷 ↾ (𝑌 × 𝑌))
22		eqid 2761	. . . . . . . . . . 11 ⊢ (MetOpen‘𝐷) = (MetOpen‘𝐷)
23		eqid 2761	. . . . . . . . . . 11 ⊢ (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) = (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌)))
24	21, 22, 23	metrest 24571	. . . . . . . . . 10 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → ((MetOpen‘𝐷) ↾_t 𝑌) = (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))
25	16, 20, 24	syl2anc 593	. . . . . . . . 9 ⊢ (𝜑 → ((MetOpen‘𝐷) ↾_t 𝑌) = (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))
26	14, 25	eqtr2d 2797	. . . . . . . 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 25477	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ (fBas‘𝑌))
35		fgcl 23925	. . . . . . . . . . 11 ⊢ (𝐹 ∈ (fBas‘𝑌) → (𝑌filGen𝐹) ∈ (Fil‘𝑌))
36	34, 35	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝑌filGen𝐹) ∈ (Fil‘𝑌))
37	10	fvexi 6875	. . . . . . . . . . 11 ⊢ 𝑋 ∈ V
38	37	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ V)
39		trfg 23938	. . . . . . . . . 10 ⊢ (((𝑌filGen𝐹) ∈ (Fil‘𝑌) ∧ 𝑌 ⊆ 𝑋 ∧ 𝑋 ∈ V) → ((𝑋filGen(𝑌filGen𝐹)) ↾_t 𝑌) = (𝑌filGen𝐹))
40	36, 20, 38, 39	syl3anc 1389	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋filGen(𝑌filGen𝐹)) ↾_t 𝑌) = (𝑌filGen𝐹))
41		fgabs 23926	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) → (𝑋filGen(𝑌filGen𝐹)) = (𝑋filGen𝐹))
42	34, 20, 41	syl2anc 593	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋filGen(𝑌filGen𝐹)) = (𝑋filGen𝐹))
43	42	oveq1d 7405	. . . . . . . . 9 ⊢ (𝜑 → ((𝑋filGen(𝑌filGen𝐹)) ↾_t 𝑌) = ((𝑋filGen𝐹) ↾_t 𝑌))
44	40, 43	eqtr3d 2798	. . . . . . . 8 ⊢ (𝜑 → (𝑌filGen𝐹) = ((𝑋filGen𝐹) ↾_t 𝑌))
45	26, 44	oveq12d 7408	. . . . . . 7 ⊢ (𝜑 → ((MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) fLim (𝑌filGen𝐹)) = ((𝐽 ↾_t 𝑌) fLim ((𝑋filGen𝐹) ↾_t 𝑌)))
46		xmstps 24500	. . . . . . . . . 10 ⊢ (𝑈 ∈ ∞MetSp → 𝑈 ∈ TopSp)
47	8, 46	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑈 ∈ TopSp)
48	10, 9	istps 22981	. . . . . . . . 9 ⊢ (𝑈 ∈ TopSp ↔ 𝐽 ∈ (TopOn‘𝑋))
49	47, 48	sylib 220	. . . . . . . 8 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))
50		fbsspw 23879	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ (fBas‘𝑌) → 𝐹 ⊆ 𝒫 𝑌)
51	34, 50	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ⊆ 𝒫 𝑌)
52	20	sspwd 4565	. . . . . . . . . . 11 ⊢ (𝜑 → 𝒫 𝑌 ⊆ 𝒫 𝑋)
53	51, 52	sstrd 3944	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ⊆ 𝒫 𝑋)
54		fbasweak 23912	. . . . . . . . . 10 ⊢ ((𝐹 ∈ (fBas‘𝑌) ∧ 𝐹 ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ V) → 𝐹 ∈ (fBas‘𝑋))
55	34, 53, 38, 54	syl3anc 1389	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ (fBas‘𝑋))
56		fgcl 23925	. . . . . . . . 9 ⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑋filGen𝐹) ∈ (Fil‘𝑋))
57	55, 56	syl 17	. . . . . . . 8 ⊢ (𝜑 → (𝑋filGen𝐹) ∈ (Fil‘𝑋))
58		filfbas 23895	. . . . . . . . . . . . 13 ⊢ ((𝑌filGen𝐹) ∈ (Fil‘𝑌) → (𝑌filGen𝐹) ∈ (fBas‘𝑌))
59	34, 35, 58	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑌filGen𝐹) ∈ (fBas‘𝑌))
60		fbsspw 23879	. . . . . . . . . . . . . 14 ⊢ ((𝑌filGen𝐹) ∈ (fBas‘𝑌) → (𝑌filGen𝐹) ⊆ 𝒫 𝑌)
61	59, 60	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑌filGen𝐹) ⊆ 𝒫 𝑌)
62	61, 52	sstrd 3944	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑌filGen𝐹) ⊆ 𝒫 𝑋)
63		fbasweak 23912	. . . . . . . . . . . 12 ⊢ (((𝑌filGen𝐹) ∈ (fBas‘𝑌) ∧ (𝑌filGen𝐹) ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ V) → (𝑌filGen𝐹) ∈ (fBas‘𝑋))
64	59, 62, 38, 63	syl3anc 1389	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑌filGen𝐹) ∈ (fBas‘𝑋))
65		ssfg 23919	. . . . . . . . . . 11 ⊢ ((𝑌filGen𝐹) ∈ (fBas‘𝑋) → (𝑌filGen𝐹) ⊆ (𝑋filGen(𝑌filGen𝐹)))
66	64, 65	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝑌filGen𝐹) ⊆ (𝑋filGen(𝑌filGen𝐹)))
67	66, 42	sseqtrd 3970	. . . . . . . . 9 ⊢ (𝜑 → (𝑌filGen𝐹) ⊆ (𝑋filGen𝐹))
68		filtop 23902	. . . . . . . . . 10 ⊢ ((𝑌filGen𝐹) ∈ (Fil‘𝑌) → 𝑌 ∈ (𝑌filGen𝐹))
69	36, 68	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 ∈ (𝑌filGen𝐹))
70	67, 69	sseldd 3935	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ (𝑋filGen𝐹))
71		flimrest 24030	. . . . . . . 8 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝑋filGen𝐹) ∈ (Fil‘𝑋) ∧ 𝑌 ∈ (𝑋filGen𝐹)) → ((𝐽 ↾_t 𝑌) fLim ((𝑋filGen𝐹) ↾_t 𝑌)) = ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌))
72	49, 57, 70, 71	syl3anc 1389	. . . . . . 7 ⊢ (𝜑 → ((𝐽 ↾_t 𝑌) fLim ((𝑋filGen𝐹) ↾_t 𝑌)) = ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌))
73	45, 72	eqtrd 2796	. . . . . 6 ⊢ (𝜑 → ((MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) fLim (𝑌filGen𝐹)) = ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌))
74	10, 27, 28, 5, 17, 29, 30, 9, 31, 32, 11	minveclem3a 25476	. . . . . . 7 ⊢ (𝜑 → (𝐷 ↾ (𝑌 × 𝑌)) ∈ (CMet‘𝑌))
75	10, 27, 28, 5, 17, 29, 30, 9, 31, 32, 11, 33	minveclem3 25478	. . . . . . 7 ⊢ (𝜑 → (𝑌filGen𝐹) ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌))))
76	23	cmetcvg 25334	. . . . . . 7 ⊢ (((𝐷 ↾ (𝑌 × 𝑌)) ∈ (CMet‘𝑌) ∧ (𝑌filGen𝐹) ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))) → ((MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) fLim (𝑌filGen𝐹)) ≠ ∅)
77	74, 75, 76	syl2anc 593	. . . . . 6 ⊢ (𝜑 → ((MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) fLim (𝑌filGen𝐹)) ≠ ∅)
78	73, 77	eqnetrrd 3024	. . . . 5 ⊢ (𝜑 → ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) ≠ ∅)
79	78	neneqd 2961	. . . 4 ⊢ (𝜑 → ¬ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) = ∅)
80		inss1 4186	. . . . . . 7 ⊢ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) ⊆ (𝐽 fLim (𝑋filGen𝐹))
81	22	methaus 24567	. . . . . . . . . . . . 13 ⊢ (𝐷 ∈ (∞Met‘𝑋) → (MetOpen‘𝐷) ∈ Haus)
82	15, 81	syl 17	. . . . . . . . . . . 12 ⊢ (𝑈 ∈ ∞MetSp → (MetOpen‘𝐷) ∈ Haus)
83	12, 82	eqeltrd 2861	. . . . . . . . . . 11 ⊢ (𝑈 ∈ ∞MetSp → 𝐽 ∈ Haus)
84		hausflimi 24027	. . . . . . . . . . 11 ⊢ (𝐽 ∈ Haus → ∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen𝐹)))
85	8, 83, 84	3syl 18	. . . . . . . . . 10 ⊢ (𝜑 → ∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen𝐹)))
86		ssn0 4355	. . . . . . . . . . . 12 ⊢ ((((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) ⊆ (𝐽 fLim (𝑋filGen𝐹)) ∧ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) ≠ ∅) → (𝐽 fLim (𝑋filGen𝐹)) ≠ ∅)
87	80, 78, 86	sylancr 596	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐽 fLim (𝑋filGen𝐹)) ≠ ∅)
88		n0moeu 4309	. . . . . . . . . . 11 ⊢ ((𝐽 fLim (𝑋filGen𝐹)) ≠ ∅ → (∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen𝐹)) ↔ ∃!𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen𝐹))))
89	87, 88	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (∃*𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen𝐹)) ↔ ∃!𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen𝐹))))
90	85, 89	mpbid 234	. . . . . . . . 9 ⊢ (𝜑 → ∃!𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen𝐹)))
91		euen1b 9002	. . . . . . . . 9 ⊢ ((𝐽 fLim (𝑋filGen𝐹)) ≈ 1_o ↔ ∃!𝑥 𝑥 ∈ (𝐽 fLim (𝑋filGen𝐹)))
92	90, 91	sylibr 236	. . . . . . . 8 ⊢ (𝜑 → (𝐽 fLim (𝑋filGen𝐹)) ≈ 1_o)
93		en1b 8999	. . . . . . . 8 ⊢ ((𝐽 fLim (𝑋filGen𝐹)) ≈ 1_o ↔ (𝐽 fLim (𝑋filGen𝐹)) = {∪ (𝐽 fLim (𝑋filGen𝐹))})
94	92, 93	sylib 220	. . . . . . 7 ⊢ (𝜑 → (𝐽 fLim (𝑋filGen𝐹)) = {∪ (𝐽 fLim (𝑋filGen𝐹))})
95	80, 94	sseqtrid 3976	. . . . . 6 ⊢ (𝜑 → ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) ⊆ {∪ (𝐽 fLim (𝑋filGen𝐹))})
96		sssn 4781	. . . . . 6 ⊢ (((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) ⊆ {∪ (𝐽 fLim (𝑋filGen𝐹))} ↔ (((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) = ∅ ∨ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) = {∪ (𝐽 fLim (𝑋filGen𝐹))}))
97	95, 96	sylib 220	. . . . 5 ⊢ (𝜑 → (((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) = ∅ ∨ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) = {∪ (𝐽 fLim (𝑋filGen𝐹))}))
98	97	ord 875	. . . 4 ⊢ (𝜑 → (¬ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) = ∅ → ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) = {∪ (𝐽 fLim (𝑋filGen𝐹))}))
99	79, 98	mpd 15	. . 3 ⊢ (𝜑 → ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌) = {∪ (𝐽 fLim (𝑋filGen𝐹))})
100	4, 99	eleqtrrid 2868	. 2 ⊢ (𝜑 → ∪ (𝐽 fLim (𝑋filGen𝐹)) ∈ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌))
101	1, 100	eqeltrid 2865	1 ⊢ (𝜑 → 𝑃 ∈ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∨ wo 858 = wceq 1559 ∈ wcel 2141 ∃*wmo 2563 ∃!weu 2594 ≠ wne 2956 {crab 3413 Vcvv 3453 ∩ cin 3901 ⊆ wss 3902 ∅c0 4283 𝒫 cpw 4552 {csn 4579 ∪ cuni 4862 class class class wbr 5097 ↦ cmpt 5178 × cxp 5641 ran crn 5644 ↾ cres 5645 ‘cfv 6515 (class class class)co 7390 1_oc1o 8423 ≈ cen 8917 infcinf 9380 ℝcr 11065 + caddc 11069 < clt 11209 ≤ cle 11210 2c2 12265 ℝ⁺crp 12986 ↑cexp 14067 Basecbs 17235 ↾_s cress 17256 distcds 17285 ↾_t crest 17439 TopOpenctopn 17440 -_gcsg 18967 LSubSpclss 20985 ∞Metcxmet 21396 fBascfbas 21399 filGencfg 21400 MetOpencmopn 21401 TopOnctopon 22957 TopSpctps 22979 Hauscha 23355 Filcfil 23892 fLim cflim 23981 ∞MetSpcxms 24364 normcnm 24623 NrmGrpcngp 24624 ℂPreHilccph 25215 CauFilccfil 25301 CMetccmet 25303 CMetSpccms 25381

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5224 ax-sep 5243 ax-nul 5253 ax-pow 5319 ax-pr 5387 ax-un 7712 ax-cnex 11122 ax-resscn 11123 ax-1cn 11124 ax-icn 11125 ax-addcl 11126 ax-addrcl 11127 ax-mulcl 11128 ax-mulrcl 11129 ax-mulcom 11130 ax-addass 11131 ax-mulass 11132 ax-distr 11133 ax-i2m1 11134 ax-1ne0 11135 ax-1rid 11136 ax-rnegex 11137 ax-rrecex 11138 ax-cnre 11139 ax-pre-lttri 11140 ax-pre-lttrn 11141 ax-pre-ltadd 11142 ax-pre-mulgt0 11143 ax-pre-sup 11144 ax-addf 11145 ax-mulf 11146

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3061 df-ral 3076 df-rex 3086 df-rmo 3366 df-reu 3367 df-rab 3414 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 4284 df-if 4478 df-pw 4554 df-sn 4580 df-pr 4582 df-tp 4584 df-op 4586 df-uni 4863 df-int 4903 df-iun 4948 df-br 5098 df-opab 5160 df-mpt 5179 df-tr 5205 df-id 5538 df-eprel 5543 df-po 5551 df-so 5552 df-fr 5596 df-we 5598 df-xp 5649 df-rel 5650 df-cnv 5651 df-co 5652 df-dm 5653 df-rn 5654 df-res 5655 df-ima 5656 df-pred 6282 df-ord 6343 df-on 6344 df-lim 6345 df-suc 6346 df-iota 6471 df-fun 6517 df-fn 6518 df-f 6519 df-f1 6520 df-fo 6521 df-f1o 6522 df-fv 6523 df-riota 7347 df-ov 7393 df-oprab 7394 df-mpo 7395 df-om 7841 df-1st 7964 df-2nd 7965 df-tpos 8199 df-frecs 8255 df-wrecs 8286 df-recs 8335 df-rdg 8374 df-1o 8430 df-er 8671 df-map 8803 df-en 8921 df-dom 8922 df-sdom 8923 df-fin 8924 df-fi 9350 df-sup 9381 df-inf 9382 df-pnf 11211 df-mnf 11212 df-xr 11213 df-ltxr 11214 df-le 11215 df-sub 11409 df-neg 11410 df-div 11838 df-nn 12204 df-2 12273 df-3 12274 df-4 12275 df-5 12276 df-6 12277 df-7 12278 df-8 12279 df-9 12280 df-n0 12475 df-z 12562 df-dec 12682 df-uz 12833 df-q 12943 df-rp 12987 df-xneg 13107 df-xadd 13108 df-xmul 13109 df-ico 13348 df-icc 13349 df-fz 13506 df-seq 14008 df-exp 14068 df-cj 15116 df-re 15117 df-im 15118 df-sqrt 15252 df-abs 15253 df-struct 17173 df-sets 17190 df-slot 17208 df-ndx 17220 df-base 17236 df-ress 17257 df-plusg 17289 df-mulr 17290 df-starv 17291 df-sca 17292 df-vsca 17293 df-ip 17294 df-tset 17295 df-ple 17296 df-ds 17298 df-unif 17299 df-rest 17441 df-0g 17460 df-topgen 17462 df-mgm 18664 df-sgrp 18743 df-mnd 18759 df-mhm 18807 df-grp 18968 df-minusg 18969 df-sbg 18970 df-mulg 19100 df-subg 19155 df-ghm 19244 df-cmn 19812 df-abl 19813 df-mgp 20177 df-rng 20189 df-ur 20218 df-ring 20271 df-cring 20272 df-oppr 20372 df-dvdsr 20392 df-unit 20393 df-invr 20423 df-dvr 20436 df-rhm 20507 df-subrg 20606 df-drng 20767 df-staf 20875 df-srng 20876 df-lmod 20916 df-lss 20986 df-lmhm 21076 df-lvec 21157 df-sra 21227 df-rgmod 21228 df-psmet 21403 df-xmet 21404 df-met 21405 df-bl 21406 df-mopn 21407 df-fbas 21408 df-fg 21409 df-cnfld 21412 df-phl 21665 df-top 22941 df-topon 22958 df-topsp 22980 df-bases 22993 df-ntr 23067 df-nei 23145 df-haus 23362 df-fil 23893 df-flim 23986 df-xms 24367 df-ms 24368 df-nm 24629 df-ngp 24630 df-nlm 24633 df-clm 25112 df-cph 25217 df-cfil 25304 df-cmet 25306 df-cms 25384

This theorem is referenced by: minveclem4b 25480 minveclem4 25481

W3C validator