Theorem cffldtocusgr

Description: The field of complex numbers can be made a complete simple graph with the set of pairs of complex numbers regarded as edges. This theorem demonstrates the capabilities of the current definitions for graphs applied to extensible structures. (Contributed by AV, 14-Nov-2021) (Proof shortened by AV, 17-Nov-2021)

	Ref	Expression
Hypotheses	cffldtocusgr.p	$$⊢P=\left\{x\in 𝒫ℂ|\left|x\right|=2\right\}$$
	cffldtocusgr.g	$$⊢G={ℂ}_{\mathrm{fld}}\mathrm{sSet}⟨\mathrm{ef}\left(\mathrm{ndx}\right),{\mathrm{I}\upharpoonright }_P⟩$$
Assertion	cffldtocusgr	$$⊢G\in \mathrm{ComplUSGraph}$$

Proof

Step	Hyp	Ref	Expression
1		cffldtocusgr.p	$$⊢P=\left\{x\in 𝒫ℂ|\left|x\right|=2\right\}$$
2		cffldtocusgr.g	$$⊢G={ℂ}_{\mathrm{fld}}\mathrm{sSet}⟨\mathrm{ef}\left(\mathrm{ndx}\right),{\mathrm{I}\upharpoonright }_P⟩$$
3		opex	$$⊢⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩\in \mathrm{V}$$
4	3	tpid1	$$⊢⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩\in \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}$$
5	4	orci	$$⊢\left(⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩\in \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\vee ⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩\in \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)$$
6		elun	$$⊢⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩\in \left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)\leftrightarrow \left(⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩\in \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\vee ⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩\in \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)$$
7	5 6	mpbir	$$⊢⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩\in \left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)$$
8	7	orci	$$⊢\left(⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩\in \left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)\vee ⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩\in \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)⟩\right\}\right)\right)$$
9		df-cnfld	$$⊢{ℂ}_{\mathrm{fld}}=\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\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)⟩\right\}\right)$$
10	9	eleq2i	$$⊢⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩\in {ℂ}_{\mathrm{fld}}\leftrightarrow ⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩\in \left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\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)⟩\right\}\right)\right)$$
11		elun	$$⊢⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩\in \left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\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)⟩\right\}\right)\right)\leftrightarrow \left(⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩\in \left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)\vee ⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩\in \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)⟩\right\}\right)\right)$$
12	10 11	bitri	$$⊢⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩\in {ℂ}_{\mathrm{fld}}\leftrightarrow \left(⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩\in \left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)\vee ⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩\in \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)⟩\right\}\right)\right)$$
13	8 12	mpbir	$$⊢⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩\in {ℂ}_{\mathrm{fld}}$$
14		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
15	14	pweqi	$$⊢𝒫ℂ=𝒫{\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
16	15	rabeqi	$$⊢\left\{x\in 𝒫ℂ|\left|x\right|=2\right\}=\left\{x\in 𝒫{\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}|\left|x\right|=2\right\}$$
17	1 16	eqtri	$$⊢P=\left\{x\in 𝒫{\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}|\left|x\right|=2\right\}$$
18		cnfldstr	$$⊢{ℂ}_{\mathrm{fld}}\mathrm{Struct}⟨1,13⟩$$
19	18	a1i	$$⊢⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩\in {ℂ}_{\mathrm{fld}}\to {ℂ}_{\mathrm{fld}}\mathrm{Struct}⟨1,13⟩$$
20		fvex	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\in \mathrm{V}$$
21		cnex	$$⊢ℂ\in \mathrm{V}$$
22	20 21	opeldm	$$⊢⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩\in {ℂ}_{\mathrm{fld}}\to {\mathrm{Base}}_{\mathrm{ndx}}\in \mathrm{dom}{ℂ}_{\mathrm{fld}}$$
23	17 19 2 22	structtocusgr	$$⊢⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩\in {ℂ}_{\mathrm{fld}}\to G\in \mathrm{ComplUSGraph}$$
24	13 23	ax-mp	$$⊢G\in \mathrm{ComplUSGraph}$$