This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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) Revise df-cnfld . (Revised by GG, 31-Mar-2025)

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 ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. }
5 4 orci 
 |-  ( <. ( Base ` ndx ) , CC >. e. { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } \/ <. ( Base ` ndx ) , CC >. e. { <. ( *r ` ndx ) , * >. } )
6 elun 
 |-  ( <. ( Base ` ndx ) , CC >. e. ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } u. { <. ( *r ` ndx ) , * >. } ) <-> ( <. ( Base ` ndx ) , CC >. e. { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } \/ <. ( Base ` ndx ) , CC >. e. { <. ( *r ` ndx ) , * >. } ) )
7 5 6 mpbir 
 |-  <. ( Base ` ndx ) , CC >. e. ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } u. { <. ( *r ` ndx ) , * >. } )
8 7 orci 
 |-  ( <. ( Base ` ndx ) , CC >. e. ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } 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 ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } 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 ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } 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 ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } 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 ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } 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 ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } 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