Theorem cnfldfunALT

Description: The field of complex numbers is a function. Alternate proof of cnfldfun not requiring that the index set of the components is ordered, but using quadratically many inequalities for the indices. (Contributed by AV, 14-Nov-2021) (Proof shortened by AV, 11-Nov-2024) Revise df-cnfld . (Revised by GG, 31-Mar-2025) Revise df-cnfld . (Revised by Thierry Arnoux, 9-Nov-2026) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	cnfldfunALT	$$⊢\mathrm{Fun}{ℂ}_{\mathrm{fld}}$$

Proof

Step	Hyp	Ref	Expression
1		basendxnplusgndx	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne {+}_{\mathrm{ndx}}$$
2		basendxnmulrndx	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne {\cdot }_{\mathrm{ndx}}$$
3		plusgndxnmulrndx	$$⊢{+}_{\mathrm{ndx}}\ne {\cdot }_{\mathrm{ndx}}$$
4		fvex	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\in \mathrm{V}$$
5		fvex	$$⊢{+}_{\mathrm{ndx}}\in \mathrm{V}$$
6		fvex	$$⊢{\cdot }_{\mathrm{ndx}}\in \mathrm{V}$$
7		cnex	$$⊢ℂ\in \mathrm{V}$$
8		mpoaddex	$$⊢\left(u\in ℂ,v\in ℂ⟼u+v\right)\in \mathrm{V}$$
9		mpomulex	$$⊢\left(u\in ℂ,v\in ℂ⟼uv\right)\in \mathrm{V}$$
10	4 5 6 7 8 9	funtp	$$⊢\left({\mathrm{Base}}_{\mathrm{ndx}}\ne {+}_{\mathrm{ndx}}\wedge {\mathrm{Base}}_{\mathrm{ndx}}\ne {\cdot }_{\mathrm{ndx}}\wedge {+}_{\mathrm{ndx}}\ne {\cdot }_{\mathrm{ndx}}\right)\to \mathrm{Fun}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩\right\}$$
11	1 2 3 10	mp3an	$$⊢\mathrm{Fun}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩\right\}$$
12		fvex	$$⊢{\mathrm{*}}_{\mathrm{ndx}}\in \mathrm{V}$$
13		cjf	$$⊢*:ℂ⟶ℂ$$
14		fex	$$⊢\left(*:ℂ⟶ℂ\wedge ℂ\in \mathrm{V}\right)\to *\in \mathrm{V}$$
15	13 7 14	mp2an	$$⊢*\in \mathrm{V}$$
16	12 15	funsn	$$⊢\mathrm{Fun}\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}$$
17	11 16	pm3.2i	$$⊢\left(\mathrm{Fun}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩\right\}\wedge \mathrm{Fun}\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)$$
18	7 8 9	dmtpop	$$⊢\mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩\right\}=\left\{{\mathrm{Base}}_{\mathrm{ndx}},{+}_{\mathrm{ndx}},{\cdot }_{\mathrm{ndx}}\right\}$$
19	15	dmsnop	$$⊢\mathrm{dom}\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}=\left\{{\mathrm{*}}_{\mathrm{ndx}}\right\}$$
20	18 19	ineq12i	$$⊢\mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩\right\}\cap \mathrm{dom}\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}=\left\{{\mathrm{Base}}_{\mathrm{ndx}},{+}_{\mathrm{ndx}},{\cdot }_{\mathrm{ndx}}\right\}\cap \left\{{\mathrm{*}}_{\mathrm{ndx}}\right\}$$
21		starvndxnbasendx	$$⊢{\mathrm{*}}_{\mathrm{ndx}}\ne {\mathrm{Base}}_{\mathrm{ndx}}$$
22	21	necomi	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne {\mathrm{*}}_{\mathrm{ndx}}$$
23		starvndxnplusgndx	$$⊢{\mathrm{*}}_{\mathrm{ndx}}\ne {+}_{\mathrm{ndx}}$$
24	23	necomi	$$⊢{+}_{\mathrm{ndx}}\ne {\mathrm{*}}_{\mathrm{ndx}}$$
25		starvndxnmulrndx	$$⊢{\mathrm{*}}_{\mathrm{ndx}}\ne {\cdot }_{\mathrm{ndx}}$$
26	25	necomi	$$⊢{\cdot }_{\mathrm{ndx}}\ne {\mathrm{*}}_{\mathrm{ndx}}$$
27		disjtpsn	$$⊢\left({\mathrm{Base}}_{\mathrm{ndx}}\ne {\mathrm{*}}_{\mathrm{ndx}}\wedge {+}_{\mathrm{ndx}}\ne {\mathrm{*}}_{\mathrm{ndx}}\wedge {\cdot }_{\mathrm{ndx}}\ne {\mathrm{*}}_{\mathrm{ndx}}\right)\to \left\{{\mathrm{Base}}_{\mathrm{ndx}},{+}_{\mathrm{ndx}},{\cdot }_{\mathrm{ndx}}\right\}\cap \left\{{\mathrm{*}}_{\mathrm{ndx}}\right\}=\varnothing$$
28	22 24 26 27	mp3an	$$⊢\left\{{\mathrm{Base}}_{\mathrm{ndx}},{+}_{\mathrm{ndx}},{\cdot }_{\mathrm{ndx}}\right\}\cap \left\{{\mathrm{*}}_{\mathrm{ndx}}\right\}=\varnothing$$
29	20 28	eqtri	$$⊢\mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩\right\}\cap \mathrm{dom}\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}=\varnothing$$
30		funun	$$⊢\left(\left(\mathrm{Fun}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩\right\}\wedge \mathrm{Fun}\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)\wedge \mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩\right\}\cap \mathrm{dom}\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}=\varnothing \right)\to \mathrm{Fun}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)$$
31	17 29 30	mp2an	$$⊢\mathrm{Fun}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)$$
32		slotsdifplendx	$$⊢\left({\mathrm{*}}_{\mathrm{ndx}}\ne {\le }_{\mathrm{ndx}}\wedge \mathrm{TopSet}\left(\mathrm{ndx}\right)\ne {\le }_{\mathrm{ndx}}\right)$$
33	32	simpri	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne {\le }_{\mathrm{ndx}}$$
34		dsndxntsetndx	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)\ne \mathrm{TopSet}\left(\mathrm{ndx}\right)$$
35	34	necomi	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne \mathrm{dist}\left(\mathrm{ndx}\right)$$
36		slotsdifdsndx	$$⊢\left({\mathrm{*}}_{\mathrm{ndx}}\ne \mathrm{dist}\left(\mathrm{ndx}\right)\wedge {\le }_{\mathrm{ndx}}\ne \mathrm{dist}\left(\mathrm{ndx}\right)\right)$$
37	36	simpri	$$⊢{\le }_{\mathrm{ndx}}\ne \mathrm{dist}\left(\mathrm{ndx}\right)$$
38		fvex	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)\in \mathrm{V}$$
39		fvex	$$⊢{\le }_{\mathrm{ndx}}\in \mathrm{V}$$
40		fvex	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)\in \mathrm{V}$$
41		fvex	$$⊢\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)\in \mathrm{V}$$
42		letsr	$$⊢\le \in \mathrm{TosetRel}$$
43	42	elexi	$$⊢\le \in \mathrm{V}$$
44		absf	$$⊢\mathrm{abs}:ℂ⟶ℝ$$
45		fex	$$⊢\left(\mathrm{abs}:ℂ⟶ℝ\wedge ℂ\in \mathrm{V}\right)\to \mathrm{abs}\in \mathrm{V}$$
46	44 7 45	mp2an	$$⊢\mathrm{abs}\in \mathrm{V}$$
47		subf	$$⊢-:ℂ\times ℂ⟶ℂ$$
48	7 7	xpex	$$⊢ℂ\times ℂ\in \mathrm{V}$$
49		fex	$$⊢\left(-:ℂ\times ℂ⟶ℂ\wedge ℂ\times ℂ\in \mathrm{V}\right)\to -\in \mathrm{V}$$
50	47 48 49	mp2an	$$⊢-\in \mathrm{V}$$
51	46 50	coex	$$⊢\mathrm{abs}\circ -\in \mathrm{V}$$
52	38 39 40 41 43 51	funtp	$$⊢\left(\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne {\le }_{\mathrm{ndx}}\wedge \mathrm{TopSet}\left(\mathrm{ndx}\right)\ne \mathrm{dist}\left(\mathrm{ndx}\right)\wedge {\le }_{\mathrm{ndx}}\ne \mathrm{dist}\left(\mathrm{ndx}\right)\right)\to \mathrm{Fun}\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}$$
53	33 35 37 52	mp3an	$$⊢\mathrm{Fun}\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}$$
54		unifndx	$$⊢\mathrm{UnifSet}\left(\mathrm{ndx}\right)=13$$
55		1nn0	$$⊢1\in {\mathbb{N}}_0$$
56		3nn0	$$⊢3\in {\mathbb{N}}_0$$
57	55 56	deccl	$$⊢13\in {\mathbb{N}}_0$$
58	57	nn0rei	$$⊢13\in ℝ$$
59	54 58	eqeltri	$$⊢\mathrm{UnifSet}\left(\mathrm{ndx}\right)\in ℝ$$
60		2nn0	$$⊢2\in {\mathbb{N}}_0$$
61		3lt10	$$⊢3<10$$
62		1lt2	$$⊢1<2$$
63	55 60 56 55 61 62	decltc	$$⊢13<21$$
64		eufndx	$$⊢\mathrm{EuclF}\left(\mathrm{ndx}\right)=21$$
65	63 64	breqtrri	$$⊢13<\mathrm{EuclF}\left(\mathrm{ndx}\right)$$
66	54 65	eqbrtri	$$⊢\mathrm{UnifSet}\left(\mathrm{ndx}\right)<\mathrm{EuclF}\left(\mathrm{ndx}\right)$$
67	59 66	ltneii	$$⊢\mathrm{UnifSet}\left(\mathrm{ndx}\right)\ne \mathrm{EuclF}\left(\mathrm{ndx}\right)$$
68		fvex	$$⊢\mathrm{UnifSet}\left(\mathrm{ndx}\right)\in \mathrm{V}$$
69		fvex	$$⊢\mathrm{EuclF}\left(\mathrm{ndx}\right)\in \mathrm{V}$$
70		fvex	$$⊢\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)\in \mathrm{V}$$
71	68 69 70 46	funpr	$$⊢\mathrm{UnifSet}\left(\mathrm{ndx}\right)\ne \mathrm{EuclF}\left(\mathrm{ndx}\right)\to \mathrm{Fun}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩,⟨\mathrm{EuclF}\left(\mathrm{ndx}\right),\mathrm{abs}⟩\right\}$$
72	67 71	ax-mp	$$⊢\mathrm{Fun}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩,⟨\mathrm{EuclF}\left(\mathrm{ndx}\right),\mathrm{abs}⟩\right\}$$
73	53 72	pm3.2i	$$⊢\left(\mathrm{Fun}\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}\wedge \mathrm{Fun}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩,⟨\mathrm{EuclF}\left(\mathrm{ndx}\right),\mathrm{abs}⟩\right\}\right)$$
74	41 43 51	dmtpop	$$⊢\mathrm{dom}\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}=\left\{\mathrm{TopSet}\left(\mathrm{ndx}\right),{\le }_{\mathrm{ndx}},\mathrm{dist}\left(\mathrm{ndx}\right)\right\}$$
75	70 46	dmprop	$$⊢\mathrm{dom}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩,⟨\mathrm{EuclF}\left(\mathrm{ndx}\right),\mathrm{abs}⟩\right\}=\left\{\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{EuclF}\left(\mathrm{ndx}\right)\right\}$$
76	74 75	ineq12i	$$⊢\mathrm{dom}\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}\cap \mathrm{dom}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩,⟨\mathrm{EuclF}\left(\mathrm{ndx}\right),\mathrm{abs}⟩\right\}=\left\{\mathrm{TopSet}\left(\mathrm{ndx}\right),{\le }_{\mathrm{ndx}},\mathrm{dist}\left(\mathrm{ndx}\right)\right\}\cap \left\{\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{EuclF}\left(\mathrm{ndx}\right)\right\}$$
77		slotsdifunifndx	$$⊢\left(\left({+}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\cdot }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\mathrm{*}}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)\wedge \left({\le }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge \mathrm{dist}\left(\mathrm{ndx}\right)\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)\right)$$
78		unifndxntsetndx	$$⊢\mathrm{UnifSet}\left(\mathrm{ndx}\right)\ne \mathrm{TopSet}\left(\mathrm{ndx}\right)$$
79	78	necomi	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)$$
80	79	a1i	$$⊢\left({+}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\cdot }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\mathrm{*}}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)\to \mathrm{TopSet}\left(\mathrm{ndx}\right)\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)$$
81	80	anim1i	$$⊢\left(\left({+}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\cdot }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\mathrm{*}}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)\wedge \left({\le }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge \mathrm{dist}\left(\mathrm{ndx}\right)\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)\right)\to \left(\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge \left({\le }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge \mathrm{dist}\left(\mathrm{ndx}\right)\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)\right)$$
82		3anass	$$⊢\left(\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\le }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge \mathrm{dist}\left(\mathrm{ndx}\right)\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)\leftrightarrow \left(\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge \left({\le }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge \mathrm{dist}\left(\mathrm{ndx}\right)\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)\right)$$
83	81 82	sylibr	$$⊢\left(\left({+}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\cdot }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\mathrm{*}}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)\wedge \left({\le }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge \mathrm{dist}\left(\mathrm{ndx}\right)\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)\right)\to \left(\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\le }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge \mathrm{dist}\left(\mathrm{ndx}\right)\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)$$
84	77 83	ax-mp	$$⊢\left(\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\le }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge \mathrm{dist}\left(\mathrm{ndx}\right)\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)$$
85		tsetndx	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)=9$$
86		9nn0	$$⊢9\in {\mathbb{N}}_0$$
87	85 86	eqeltri	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)\in {\mathbb{N}}_0$$
88	87	nn0rei	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)\in ℝ$$
89		2nn	$$⊢2\in \mathbb{N}$$
90		9lt10	$$⊢9<10$$
91	89 55 86 90	declti	$$⊢9<21$$
92	91 64	breqtrri	$$⊢9<\mathrm{EuclF}\left(\mathrm{ndx}\right)$$
93	85 92	eqbrtri	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)<\mathrm{EuclF}\left(\mathrm{ndx}\right)$$
94	88 93	ltneii	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne \mathrm{EuclF}\left(\mathrm{ndx}\right)$$
95		plendx	$$⊢{\le }_{\mathrm{ndx}}=10$$
96		10nn0	$$⊢10\in {\mathbb{N}}_0$$
97	95 96	eqeltri	$$⊢{\le }_{\mathrm{ndx}}\in {\mathbb{N}}_0$$
98	97	nn0rei	$$⊢{\le }_{\mathrm{ndx}}\in ℝ$$
99		0nn0	$$⊢0\in {\mathbb{N}}_0$$
100		10pos	$$⊢0<10$$
101	55 60 99 55 100 62	decltc	$$⊢10<21$$
102	101 64	breqtrri	$$⊢10<\mathrm{EuclF}\left(\mathrm{ndx}\right)$$
103	95 102	eqbrtri	$$⊢{\le }_{\mathrm{ndx}}<\mathrm{EuclF}\left(\mathrm{ndx}\right)$$
104	98 103	ltneii	$$⊢{\le }_{\mathrm{ndx}}\ne \mathrm{EuclF}\left(\mathrm{ndx}\right)$$
105		dsndx	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)=12$$
106	55 60	deccl	$$⊢12\in {\mathbb{N}}_0$$
107	106	nn0rei	$$⊢12\in ℝ$$
108	105 107	eqeltri	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)\in ℝ$$
109		2lt10	$$⊢2<10$$
110	55 60 60 55 109 62	decltc	$$⊢12<21$$
111	110 64	breqtrri	$$⊢12<\mathrm{EuclF}\left(\mathrm{ndx}\right)$$
112	105 111	eqbrtri	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)<\mathrm{EuclF}\left(\mathrm{ndx}\right)$$
113	108 112	ltneii	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)\ne \mathrm{EuclF}\left(\mathrm{ndx}\right)$$
114	94 104 113	3pm3.2i	$$⊢\left(\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne \mathrm{EuclF}\left(\mathrm{ndx}\right)\wedge {\le }_{\mathrm{ndx}}\ne \mathrm{EuclF}\left(\mathrm{ndx}\right)\wedge \mathrm{dist}\left(\mathrm{ndx}\right)\ne \mathrm{EuclF}\left(\mathrm{ndx}\right)\right)$$
115		disjtppr	$$⊢\left(\left(\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\le }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge \mathrm{dist}\left(\mathrm{ndx}\right)\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)\wedge \left(\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne \mathrm{EuclF}\left(\mathrm{ndx}\right)\wedge {\le }_{\mathrm{ndx}}\ne \mathrm{EuclF}\left(\mathrm{ndx}\right)\wedge \mathrm{dist}\left(\mathrm{ndx}\right)\ne \mathrm{EuclF}\left(\mathrm{ndx}\right)\right)\right)\to \left\{\mathrm{TopSet}\left(\mathrm{ndx}\right),{\le }_{\mathrm{ndx}},\mathrm{dist}\left(\mathrm{ndx}\right)\right\}\cap \left\{\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{EuclF}\left(\mathrm{ndx}\right)\right\}=\varnothing$$
116	84 114 115	mp2an	$$⊢\left\{\mathrm{TopSet}\left(\mathrm{ndx}\right),{\le }_{\mathrm{ndx}},\mathrm{dist}\left(\mathrm{ndx}\right)\right\}\cap \left\{\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{EuclF}\left(\mathrm{ndx}\right)\right\}=\varnothing$$
117	76 116	eqtri	$$⊢\mathrm{dom}\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}\cap \mathrm{dom}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩,⟨\mathrm{EuclF}\left(\mathrm{ndx}\right),\mathrm{abs}⟩\right\}=\varnothing$$
118		funun	$$⊢\left(\left(\mathrm{Fun}\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}\wedge \mathrm{Fun}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩,⟨\mathrm{EuclF}\left(\mathrm{ndx}\right),\mathrm{abs}⟩\right\}\right)\wedge \mathrm{dom}\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}\cap \mathrm{dom}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩,⟨\mathrm{EuclF}\left(\mathrm{ndx}\right),\mathrm{abs}⟩\right\}=\varnothing \right)\to \mathrm{Fun}\left(\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}\cup \left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩,⟨\mathrm{EuclF}\left(\mathrm{ndx}\right),\mathrm{abs}⟩\right\}\right)$$
119	73 117 118	mp2an	$$⊢\mathrm{Fun}\left(\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}\cup \left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩,⟨\mathrm{EuclF}\left(\mathrm{ndx}\right),\mathrm{abs}⟩\right\}\right)$$
120	31 119	pm3.2i	$$⊢\left(\mathrm{Fun}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)\wedge \mathrm{Fun}\left(\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}\cup \left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩,⟨\mathrm{EuclF}\left(\mathrm{ndx}\right),\mathrm{abs}⟩\right\}\right)\right)$$
121		dmun	$$⊢\mathrm{dom}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)=\mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩\right\}\cup \mathrm{dom}\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}$$
122		dmun	$$⊢\mathrm{dom}\left(\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}\cup \left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩,⟨\mathrm{EuclF}\left(\mathrm{ndx}\right),\mathrm{abs}⟩\right\}\right)=\mathrm{dom}\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}\cup \mathrm{dom}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩,⟨\mathrm{EuclF}\left(\mathrm{ndx}\right),\mathrm{abs}⟩\right\}$$
123	121 122	ineq12i	$$⊢\mathrm{dom}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)\cap \mathrm{dom}\left(\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}\cup \left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩,⟨\mathrm{EuclF}\left(\mathrm{ndx}\right),\mathrm{abs}⟩\right\}\right)=\left(\mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩\right\}\cup \mathrm{dom}\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)\cap \left(\mathrm{dom}\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}\cup \mathrm{dom}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩,⟨\mathrm{EuclF}\left(\mathrm{ndx}\right),\mathrm{abs}⟩\right\}\right)$$
124	18 74	ineq12i	$$⊢\mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩\right\}\cap \mathrm{dom}\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}=\left\{{\mathrm{Base}}_{\mathrm{ndx}},{+}_{\mathrm{ndx}},{\cdot }_{\mathrm{ndx}}\right\}\cap \left\{\mathrm{TopSet}\left(\mathrm{ndx}\right),{\le }_{\mathrm{ndx}},\mathrm{dist}\left(\mathrm{ndx}\right)\right\}$$
125		tsetndxnbasendx	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne {\mathrm{Base}}_{\mathrm{ndx}}$$
126	125	necomi	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{TopSet}\left(\mathrm{ndx}\right)$$
127		tsetndxnplusgndx	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne {+}_{\mathrm{ndx}}$$
128	127	necomi	$$⊢{+}_{\mathrm{ndx}}\ne \mathrm{TopSet}\left(\mathrm{ndx}\right)$$
129		tsetndxnmulrndx	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}$$
130	129	necomi	$$⊢{\cdot }_{\mathrm{ndx}}\ne \mathrm{TopSet}\left(\mathrm{ndx}\right)$$
131	126 128 130	3pm3.2i	$$⊢\left({\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{TopSet}\left(\mathrm{ndx}\right)\wedge {+}_{\mathrm{ndx}}\ne \mathrm{TopSet}\left(\mathrm{ndx}\right)\wedge {\cdot }_{\mathrm{ndx}}\ne \mathrm{TopSet}\left(\mathrm{ndx}\right)\right)$$
132		plendxnbasendx	$$⊢{\le }_{\mathrm{ndx}}\ne {\mathrm{Base}}_{\mathrm{ndx}}$$
133	132	necomi	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne {\le }_{\mathrm{ndx}}$$
134		plendxnplusgndx	$$⊢{\le }_{\mathrm{ndx}}\ne {+}_{\mathrm{ndx}}$$
135	134	necomi	$$⊢{+}_{\mathrm{ndx}}\ne {\le }_{\mathrm{ndx}}$$
136		plendxnmulrndx	$$⊢{\le }_{\mathrm{ndx}}\ne {\cdot }_{\mathrm{ndx}}$$
137	136	necomi	$$⊢{\cdot }_{\mathrm{ndx}}\ne {\le }_{\mathrm{ndx}}$$
138	133 135 137	3pm3.2i	$$⊢\left({\mathrm{Base}}_{\mathrm{ndx}}\ne {\le }_{\mathrm{ndx}}\wedge {+}_{\mathrm{ndx}}\ne {\le }_{\mathrm{ndx}}\wedge {\cdot }_{\mathrm{ndx}}\ne {\le }_{\mathrm{ndx}}\right)$$
139		dsndxnbasendx	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)\ne {\mathrm{Base}}_{\mathrm{ndx}}$$
140	139	necomi	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{dist}\left(\mathrm{ndx}\right)$$
141		dsndxnplusgndx	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)\ne {+}_{\mathrm{ndx}}$$
142	141	necomi	$$⊢{+}_{\mathrm{ndx}}\ne \mathrm{dist}\left(\mathrm{ndx}\right)$$
143		dsndxnmulrndx	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}$$
144	143	necomi	$$⊢{\cdot }_{\mathrm{ndx}}\ne \mathrm{dist}\left(\mathrm{ndx}\right)$$
145	140 142 144	3pm3.2i	$$⊢\left({\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{dist}\left(\mathrm{ndx}\right)\wedge {+}_{\mathrm{ndx}}\ne \mathrm{dist}\left(\mathrm{ndx}\right)\wedge {\cdot }_{\mathrm{ndx}}\ne \mathrm{dist}\left(\mathrm{ndx}\right)\right)$$
146		disjtp2	$$⊢\left(\left({\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{TopSet}\left(\mathrm{ndx}\right)\wedge {+}_{\mathrm{ndx}}\ne \mathrm{TopSet}\left(\mathrm{ndx}\right)\wedge {\cdot }_{\mathrm{ndx}}\ne \mathrm{TopSet}\left(\mathrm{ndx}\right)\right)\wedge \left({\mathrm{Base}}_{\mathrm{ndx}}\ne {\le }_{\mathrm{ndx}}\wedge {+}_{\mathrm{ndx}}\ne {\le }_{\mathrm{ndx}}\wedge {\cdot }_{\mathrm{ndx}}\ne {\le }_{\mathrm{ndx}}\right)\wedge \left({\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{dist}\left(\mathrm{ndx}\right)\wedge {+}_{\mathrm{ndx}}\ne \mathrm{dist}\left(\mathrm{ndx}\right)\wedge {\cdot }_{\mathrm{ndx}}\ne \mathrm{dist}\left(\mathrm{ndx}\right)\right)\right)\to \left\{{\mathrm{Base}}_{\mathrm{ndx}},{+}_{\mathrm{ndx}},{\cdot }_{\mathrm{ndx}}\right\}\cap \left\{\mathrm{TopSet}\left(\mathrm{ndx}\right),{\le }_{\mathrm{ndx}},\mathrm{dist}\left(\mathrm{ndx}\right)\right\}=\varnothing$$
147	131 138 145 146	mp3an	$$⊢\left\{{\mathrm{Base}}_{\mathrm{ndx}},{+}_{\mathrm{ndx}},{\cdot }_{\mathrm{ndx}}\right\}\cap \left\{\mathrm{TopSet}\left(\mathrm{ndx}\right),{\le }_{\mathrm{ndx}},\mathrm{dist}\left(\mathrm{ndx}\right)\right\}=\varnothing$$
148	124 147	eqtri	$$⊢\mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩\right\}\cap \mathrm{dom}\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}=\varnothing$$
149	18 75	ineq12i	$$⊢\mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩\right\}\cap \mathrm{dom}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩,⟨\mathrm{EuclF}\left(\mathrm{ndx}\right),\mathrm{abs}⟩\right\}=\left\{{\mathrm{Base}}_{\mathrm{ndx}},{+}_{\mathrm{ndx}},{\cdot }_{\mathrm{ndx}}\right\}\cap \left\{\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{EuclF}\left(\mathrm{ndx}\right)\right\}$$
150		unifndxnbasendx	$$⊢\mathrm{UnifSet}\left(\mathrm{ndx}\right)\ne {\mathrm{Base}}_{\mathrm{ndx}}$$
151	150	necomi	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)$$
152	151	a1i	$$⊢\left({+}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\cdot }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\mathrm{*}}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)\to {\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)$$
153		3simpa	$$⊢\left({+}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\cdot }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\mathrm{*}}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)\to \left({+}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\cdot }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)$$
154		3anass	$$⊢\left({\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {+}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\cdot }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)\leftrightarrow \left({\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge \left({+}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\cdot }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)\right)$$
155	152 153 154	sylanbrc	$$⊢\left({+}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\cdot }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\mathrm{*}}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)\to \left({\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {+}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\cdot }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)$$
156	155	adantr	$$⊢\left(\left({+}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\cdot }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\mathrm{*}}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)\wedge \left({\le }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge \mathrm{dist}\left(\mathrm{ndx}\right)\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)\right)\to \left({\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {+}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\cdot }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)$$
157	77 156	ax-mp	$$⊢\left({\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {+}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\cdot }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)$$
158		basendx	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}=1$$
159	158 55	eqeltri	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\in {\mathbb{N}}_0$$
160	159	nn0rei	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\in ℝ$$
161		1lt10	$$⊢1<10$$
162	89 55 55 161	declti	$$⊢1<21$$
163	162 64	breqtrri	$$⊢1<\mathrm{EuclF}\left(\mathrm{ndx}\right)$$
164	158 163	eqbrtri	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}<\mathrm{EuclF}\left(\mathrm{ndx}\right)$$
165	160 164	ltneii	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{EuclF}\left(\mathrm{ndx}\right)$$
166		plusgndx	$$⊢{+}_{\mathrm{ndx}}=2$$
167	166 60	eqeltri	$$⊢{+}_{\mathrm{ndx}}\in {\mathbb{N}}_0$$
168	167	nn0rei	$$⊢{+}_{\mathrm{ndx}}\in ℝ$$
169	89 55 60 109	declti	$$⊢2<21$$
170	169 64	breqtrri	$$⊢2<\mathrm{EuclF}\left(\mathrm{ndx}\right)$$
171	166 170	eqbrtri	$$⊢{+}_{\mathrm{ndx}}<\mathrm{EuclF}\left(\mathrm{ndx}\right)$$
172	168 171	ltneii	$$⊢{+}_{\mathrm{ndx}}\ne \mathrm{EuclF}\left(\mathrm{ndx}\right)$$
173		mulrndx	$$⊢{\cdot }_{\mathrm{ndx}}=3$$
174	173 56	eqeltri	$$⊢{\cdot }_{\mathrm{ndx}}\in {\mathbb{N}}_0$$
175	174	nn0rei	$$⊢{\cdot }_{\mathrm{ndx}}\in ℝ$$
176	89 55 56 61	declti	$$⊢3<21$$
177	176 64	breqtrri	$$⊢3<\mathrm{EuclF}\left(\mathrm{ndx}\right)$$
178	173 177	eqbrtri	$$⊢{\cdot }_{\mathrm{ndx}}<\mathrm{EuclF}\left(\mathrm{ndx}\right)$$
179	175 178	ltneii	$$⊢{\cdot }_{\mathrm{ndx}}\ne \mathrm{EuclF}\left(\mathrm{ndx}\right)$$
180	165 172 179	3pm3.2i	$$⊢\left({\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{EuclF}\left(\mathrm{ndx}\right)\wedge {+}_{\mathrm{ndx}}\ne \mathrm{EuclF}\left(\mathrm{ndx}\right)\wedge {\cdot }_{\mathrm{ndx}}\ne \mathrm{EuclF}\left(\mathrm{ndx}\right)\right)$$
181		disjtppr	$$⊢\left(\left({\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {+}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\cdot }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)\wedge \left({\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{EuclF}\left(\mathrm{ndx}\right)\wedge {+}_{\mathrm{ndx}}\ne \mathrm{EuclF}\left(\mathrm{ndx}\right)\wedge {\cdot }_{\mathrm{ndx}}\ne \mathrm{EuclF}\left(\mathrm{ndx}\right)\right)\right)\to \left\{{\mathrm{Base}}_{\mathrm{ndx}},{+}_{\mathrm{ndx}},{\cdot }_{\mathrm{ndx}}\right\}\cap \left\{\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{EuclF}\left(\mathrm{ndx}\right)\right\}=\varnothing$$
182	157 180 181	mp2an	$$⊢\left\{{\mathrm{Base}}_{\mathrm{ndx}},{+}_{\mathrm{ndx}},{\cdot }_{\mathrm{ndx}}\right\}\cap \left\{\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{EuclF}\left(\mathrm{ndx}\right)\right\}=\varnothing$$
183	149 182	eqtri	$$⊢\mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩\right\}\cap \mathrm{dom}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩,⟨\mathrm{EuclF}\left(\mathrm{ndx}\right),\mathrm{abs}⟩\right\}=\varnothing$$
184	148 183	pm3.2i	$$⊢\left(\mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩\right\}\cap \mathrm{dom}\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}=\varnothing \wedge \mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩\right\}\cap \mathrm{dom}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩,⟨\mathrm{EuclF}\left(\mathrm{ndx}\right),\mathrm{abs}⟩\right\}=\varnothing \right)$$
185		undisj2	$$⊢\left(\mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩\right\}\cap \mathrm{dom}\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}=\varnothing \wedge \mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩\right\}\cap \mathrm{dom}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩,⟨\mathrm{EuclF}\left(\mathrm{ndx}\right),\mathrm{abs}⟩\right\}=\varnothing \right)\leftrightarrow \mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩\right\}\cap \left(\mathrm{dom}\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}\cup \mathrm{dom}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩,⟨\mathrm{EuclF}\left(\mathrm{ndx}\right),\mathrm{abs}⟩\right\}\right)=\varnothing$$
186	184 185	mpbi	$$⊢\mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩\right\}\cap \left(\mathrm{dom}\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}\cup \mathrm{dom}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩,⟨\mathrm{EuclF}\left(\mathrm{ndx}\right),\mathrm{abs}⟩\right\}\right)=\varnothing$$
187	19 74	ineq12i	$$⊢\mathrm{dom}\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\cap \mathrm{dom}\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}=\left\{{\mathrm{*}}_{\mathrm{ndx}}\right\}\cap \left\{\mathrm{TopSet}\left(\mathrm{ndx}\right),{\le }_{\mathrm{ndx}},\mathrm{dist}\left(\mathrm{ndx}\right)\right\}$$
188		tsetndxnstarvndx	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne {\mathrm{*}}_{\mathrm{ndx}}$$
189		necom	$$⊢{\mathrm{*}}_{\mathrm{ndx}}\ne {\le }_{\mathrm{ndx}}\leftrightarrow {\le }_{\mathrm{ndx}}\ne {\mathrm{*}}_{\mathrm{ndx}}$$
190	189	birani	$$⊢\left({\mathrm{*}}_{\mathrm{ndx}}\ne {\le }_{\mathrm{ndx}}\wedge \mathrm{TopSet}\left(\mathrm{ndx}\right)\ne {\le }_{\mathrm{ndx}}\right)\to {\le }_{\mathrm{ndx}}\ne {\mathrm{*}}_{\mathrm{ndx}}$$
191	32 190	ax-mp	$$⊢{\le }_{\mathrm{ndx}}\ne {\mathrm{*}}_{\mathrm{ndx}}$$
192		necom	$$⊢{\mathrm{*}}_{\mathrm{ndx}}\ne \mathrm{dist}\left(\mathrm{ndx}\right)\leftrightarrow \mathrm{dist}\left(\mathrm{ndx}\right)\ne {\mathrm{*}}_{\mathrm{ndx}}$$
193	192	birani	$$⊢\left({\mathrm{*}}_{\mathrm{ndx}}\ne \mathrm{dist}\left(\mathrm{ndx}\right)\wedge {\le }_{\mathrm{ndx}}\ne \mathrm{dist}\left(\mathrm{ndx}\right)\right)\to \mathrm{dist}\left(\mathrm{ndx}\right)\ne {\mathrm{*}}_{\mathrm{ndx}}$$
194	36 193	ax-mp	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)\ne {\mathrm{*}}_{\mathrm{ndx}}$$
195		disjtpsn	$$⊢\left(\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne {\mathrm{*}}_{\mathrm{ndx}}\wedge {\le }_{\mathrm{ndx}}\ne {\mathrm{*}}_{\mathrm{ndx}}\wedge \mathrm{dist}\left(\mathrm{ndx}\right)\ne {\mathrm{*}}_{\mathrm{ndx}}\right)\to \left\{\mathrm{TopSet}\left(\mathrm{ndx}\right),{\le }_{\mathrm{ndx}},\mathrm{dist}\left(\mathrm{ndx}\right)\right\}\cap \left\{{\mathrm{*}}_{\mathrm{ndx}}\right\}=\varnothing$$
196	188 191 194 195	mp3an	$$⊢\left\{\mathrm{TopSet}\left(\mathrm{ndx}\right),{\le }_{\mathrm{ndx}},\mathrm{dist}\left(\mathrm{ndx}\right)\right\}\cap \left\{{\mathrm{*}}_{\mathrm{ndx}}\right\}=\varnothing$$
197	196	ineqcomi	$$⊢\left\{{\mathrm{*}}_{\mathrm{ndx}}\right\}\cap \left\{\mathrm{TopSet}\left(\mathrm{ndx}\right),{\le }_{\mathrm{ndx}},\mathrm{dist}\left(\mathrm{ndx}\right)\right\}=\varnothing$$
198	187 197	eqtri	$$⊢\mathrm{dom}\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\cap \mathrm{dom}\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}=\varnothing$$
199	19 75	ineq12i	$$⊢\mathrm{dom}\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\cap \mathrm{dom}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩,⟨\mathrm{EuclF}\left(\mathrm{ndx}\right),\mathrm{abs}⟩\right\}=\left\{{\mathrm{*}}_{\mathrm{ndx}}\right\}\cap \left\{\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{EuclF}\left(\mathrm{ndx}\right)\right\}$$
200		incom	$$⊢\left\{{\mathrm{*}}_{\mathrm{ndx}}\right\}\cap \left\{\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{EuclF}\left(\mathrm{ndx}\right)\right\}=\left\{\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{EuclF}\left(\mathrm{ndx}\right)\right\}\cap \left\{{\mathrm{*}}_{\mathrm{ndx}}\right\}$$
201		simpl3	$$⊢\left(\left({+}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\cdot }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\mathrm{*}}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)\wedge \left({\le }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge \mathrm{dist}\left(\mathrm{ndx}\right)\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)\right)\to {\mathrm{*}}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)$$
202	77 201	ax-mp	$$⊢{\mathrm{*}}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)$$
203	202	necomi	$$⊢\mathrm{UnifSet}\left(\mathrm{ndx}\right)\ne {\mathrm{*}}_{\mathrm{ndx}}$$
204		starvndx	$$⊢{\mathrm{*}}_{\mathrm{ndx}}=4$$
205		4nn0	$$⊢4\in {\mathbb{N}}_0$$
206	204 205	eqeltri	$$⊢{\mathrm{*}}_{\mathrm{ndx}}\in {\mathbb{N}}_0$$
207	206	nn0rei	$$⊢{\mathrm{*}}_{\mathrm{ndx}}\in ℝ$$
208		4lt10	$$⊢4<10$$
209	89 55 205 208	declti	$$⊢4<21$$
210	209 64	breqtrri	$$⊢4<\mathrm{EuclF}\left(\mathrm{ndx}\right)$$
211	204 210	eqbrtri	$$⊢{\mathrm{*}}_{\mathrm{ndx}}<\mathrm{EuclF}\left(\mathrm{ndx}\right)$$
212	207 211	gtneii	$$⊢\mathrm{EuclF}\left(\mathrm{ndx}\right)\ne {\mathrm{*}}_{\mathrm{ndx}}$$
213		disjprsn	$$⊢\left(\mathrm{UnifSet}\left(\mathrm{ndx}\right)\ne {\mathrm{*}}_{\mathrm{ndx}}\wedge \mathrm{EuclF}\left(\mathrm{ndx}\right)\ne {\mathrm{*}}_{\mathrm{ndx}}\right)\to \left\{\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{EuclF}\left(\mathrm{ndx}\right)\right\}\cap \left\{{\mathrm{*}}_{\mathrm{ndx}}\right\}=\varnothing$$
214	203 212 213	mp2an	$$⊢\left\{\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{EuclF}\left(\mathrm{ndx}\right)\right\}\cap \left\{{\mathrm{*}}_{\mathrm{ndx}}\right\}=\varnothing$$
215	200 214	eqtri	$$⊢\left\{{\mathrm{*}}_{\mathrm{ndx}}\right\}\cap \left\{\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{EuclF}\left(\mathrm{ndx}\right)\right\}=\varnothing$$
216	199 215	eqtri	$$⊢\mathrm{dom}\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\cap \mathrm{dom}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩,⟨\mathrm{EuclF}\left(\mathrm{ndx}\right),\mathrm{abs}⟩\right\}=\varnothing$$
217	198 216	pm3.2i	$$⊢\left(\mathrm{dom}\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\cap \mathrm{dom}\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}=\varnothing \wedge \mathrm{dom}\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\cap \mathrm{dom}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩,⟨\mathrm{EuclF}\left(\mathrm{ndx}\right),\mathrm{abs}⟩\right\}=\varnothing \right)$$
218		undisj2	$$⊢\left(\mathrm{dom}\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\cap \mathrm{dom}\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}=\varnothing \wedge \mathrm{dom}\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\cap \mathrm{dom}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩,⟨\mathrm{EuclF}\left(\mathrm{ndx}\right),\mathrm{abs}⟩\right\}=\varnothing \right)\leftrightarrow \mathrm{dom}\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\cap \left(\mathrm{dom}\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}\cup \mathrm{dom}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩,⟨\mathrm{EuclF}\left(\mathrm{ndx}\right),\mathrm{abs}⟩\right\}\right)=\varnothing$$
219	217 218	mpbi	$$⊢\mathrm{dom}\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\cap \left(\mathrm{dom}\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}\cup \mathrm{dom}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩,⟨\mathrm{EuclF}\left(\mathrm{ndx}\right),\mathrm{abs}⟩\right\}\right)=\varnothing$$
220	186 219	pm3.2i	$$⊢\left(\mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩\right\}\cap \left(\mathrm{dom}\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}\cup \mathrm{dom}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩,⟨\mathrm{EuclF}\left(\mathrm{ndx}\right),\mathrm{abs}⟩\right\}\right)=\varnothing \wedge \mathrm{dom}\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\cap \left(\mathrm{dom}\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}\cup \mathrm{dom}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩,⟨\mathrm{EuclF}\left(\mathrm{ndx}\right),\mathrm{abs}⟩\right\}\right)=\varnothing \right)$$
221		undisj1	$$⊢\left(\mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩\right\}\cap \left(\mathrm{dom}\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}\cup \mathrm{dom}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩,⟨\mathrm{EuclF}\left(\mathrm{ndx}\right),\mathrm{abs}⟩\right\}\right)=\varnothing \wedge \mathrm{dom}\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\cap \left(\mathrm{dom}\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}\cup \mathrm{dom}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩,⟨\mathrm{EuclF}\left(\mathrm{ndx}\right),\mathrm{abs}⟩\right\}\right)=\varnothing \right)\leftrightarrow \left(\mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩\right\}\cup \mathrm{dom}\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)\cap \left(\mathrm{dom}\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}\cup \mathrm{dom}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩,⟨\mathrm{EuclF}\left(\mathrm{ndx}\right),\mathrm{abs}⟩\right\}\right)=\varnothing$$
222	220 221	mpbi	$$⊢\left(\mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩\right\}\cup \mathrm{dom}\left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)\cap \left(\mathrm{dom}\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}\cup \mathrm{dom}\left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩,⟨\mathrm{EuclF}\left(\mathrm{ndx}\right),\mathrm{abs}⟩\right\}\right)=\varnothing$$
223	123 222	eqtri	$$⊢\mathrm{dom}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)\cap \mathrm{dom}\left(\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}\cup \left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩,⟨\mathrm{EuclF}\left(\mathrm{ndx}\right),\mathrm{abs}⟩\right\}\right)=\varnothing$$
224		funun	$$⊢\left(\left(\mathrm{Fun}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)\wedge \mathrm{Fun}\left(\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}\cup \left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩,⟨\mathrm{EuclF}\left(\mathrm{ndx}\right),\mathrm{abs}⟩\right\}\right)\right)\wedge \mathrm{dom}\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)\cap \mathrm{dom}\left(\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}\cup \left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩,⟨\mathrm{EuclF}\left(\mathrm{ndx}\right),\mathrm{abs}⟩\right\}\right)=\varnothing \right)\to \mathrm{Fun}\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)\cup \left(\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}\cup \left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩,⟨\mathrm{EuclF}\left(\mathrm{ndx}\right),\mathrm{abs}⟩\right\}\right)\right)$$
225	120 223 224	mp2an	$$⊢\mathrm{Fun}\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)\cup \left(\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}\cup \left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩,⟨\mathrm{EuclF}\left(\mathrm{ndx}\right),\mathrm{abs}⟩\right\}\right)\right)$$
226		df-cnfld	$$⊢{ℂ}_{\mathrm{fld}}=\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)\cup \left(\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}\cup \left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩,⟨\mathrm{EuclF}\left(\mathrm{ndx}\right),\mathrm{abs}⟩\right\}\right)$$
227	226	funeqi	$$⊢\mathrm{Fun}{ℂ}_{\mathrm{fld}}\leftrightarrow \mathrm{Fun}\left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)\cup \left(\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}\cup \left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩,⟨\mathrm{EuclF}\left(\mathrm{ndx}\right),\mathrm{abs}⟩\right\}\right)\right)$$
228	225 227	mpbir	$$⊢\mathrm{Fun}{ℂ}_{\mathrm{fld}}$$