# 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 = { x e. ~P CC | ( # ` x ) = 2 }`
cffldtocusgr.g
`|- G = ( CCfld sSet <. ( .ef ` ndx ) , ( _I |` P ) >. )`
Assertion cffldtocusgr
`|- G e. ComplUSGraph`

### Proof

Step Hyp Ref Expression
1 cffldtocusgr.p
` |-  P = { x e. ~P CC | ( # ` x ) = 2 }`
2 cffldtocusgr.g
` |-  G = ( CCfld sSet <. ( .ef ` ndx ) , ( _I |` P ) >. )`
3 opex
` |-  <. ( Base ` ndx ) , CC >. e. _V`
4 3 tpid1
` |-  <. ( Base ` ndx ) , CC >. e. { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. }`
5 4 orci
` |-  ( <. ( Base ` ndx ) , CC >. e. { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } \/ <. ( Base ` ndx ) , CC >. e. { <. ( *r ` ndx ) , * >. } )`
6 elun
` |-  ( <. ( Base ` ndx ) , CC >. e. ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } ) <-> ( <. ( Base ` ndx ) , CC >. e. { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } \/ <. ( Base ` ndx ) , CC >. e. { <. ( *r ` ndx ) , * >. } ) )`
7 5 6 mpbir
` |-  <. ( Base ` ndx ) , CC >. e. ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } )`
8 7 orci
` |-  ( <. ( Base ` ndx ) , CC >. e. ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } ) \/ <. ( Base ` ndx ) , CC >. e. ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) )`
9 df-cnfld
` |-  CCfld = ( ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } ) u. ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) )`
10 9 eleq2i
` |-  ( <. ( Base ` ndx ) , CC >. e. CCfld <-> <. ( Base ` ndx ) , CC >. e. ( ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } ) u. ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) )`
11 elun
` |-  ( <. ( Base ` ndx ) , CC >. e. ( ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } ) u. ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) <-> ( <. ( Base ` ndx ) , CC >. e. ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } ) \/ <. ( Base ` ndx ) , CC >. e. ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) )`
12 10 11 bitri
` |-  ( <. ( Base ` ndx ) , CC >. e. CCfld <-> ( <. ( Base ` ndx ) , CC >. e. ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } ) \/ <. ( Base ` ndx ) , CC >. e. ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) ) )`
13 8 12 mpbir
` |-  <. ( Base ` ndx ) , CC >. e. CCfld`
14 cnfldbas
` |-  CC = ( Base ` CCfld )`
15 14 pweqi
` |-  ~P CC = ~P ( Base ` CCfld )`
16 15 rabeqi
` |-  { x e. ~P CC | ( # ` x ) = 2 } = { x e. ~P ( Base ` CCfld ) | ( # ` x ) = 2 }`
17 1 16 eqtri
` |-  P = { x e. ~P ( Base ` CCfld ) | ( # ` x ) = 2 }`
18 cnfldstr
` |-  CCfld Struct <. 1 , ; 1 3 >.`
19 18 a1i
` |-  ( <. ( Base ` ndx ) , CC >. e. CCfld -> CCfld Struct <. 1 , ; 1 3 >. )`
20 fvex
` |-  ( Base ` ndx ) e. _V`
21 cnex
` |-  CC e. _V`
22 20 21 opeldm
` |-  ( <. ( Base ` ndx ) , CC >. e. CCfld -> ( Base ` ndx ) e. dom CCfld )`
23 17 19 2 22 structtocusgr
` |-  ( <. ( Base ` ndx ) , CC >. e. CCfld -> G e. ComplUSGraph )`
24 13 23 ax-mp
` |-  G e. ComplUSGraph`