# Metamath Proof Explorer

## 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}↾}_{{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}↾}_{{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}},×⟩\right\}$
5 4 orci ${⊢}\left(⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩\in \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},×⟩\right\}\vee ⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩\in \left\{⟨{*}_{\mathrm{ndx}},*⟩\right\}\right)$
6 elun ${⊢}⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩\in \left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},×⟩\right\}\cup \left\{⟨{*}_{\mathrm{ndx}},*⟩\right\}\right)↔\left(⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩\in \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},×⟩\right\}\vee ⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩\in \left\{⟨{*}_{\mathrm{ndx}},*⟩\right\}\right)$
7 5 6 mpbir ${⊢}⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩\in \left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},×⟩\right\}\cup \left\{⟨{*}_{\mathrm{ndx}},*⟩\right\}\right)$
8 7 orci ${⊢}\left(⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩\in \left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},×⟩\right\}\cup \left\{⟨{*}_{\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}},×⟩\right\}\cup \left\{⟨{*}_{\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}}↔⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩\in \left(\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},×⟩\right\}\cup \left\{⟨{*}_{\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}},×⟩\right\}\cup \left\{⟨{*}_{\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)↔\left(⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩\in \left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},×⟩\right\}\cup \left\{⟨{*}_{\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}}↔\left(⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩\in \left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},×⟩\right\}\cup \left\{⟨{*}_{\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}$