Metamath Proof Explorer

Theorem cnfldeuf

Description: The Euclidean function component of the complex numbers. (Contributed by Thierry Arnoux, 9-Nov-2026)

Ref Expression
Assertion cnfldeuf 
|- abs = ( EuclF ` CCfld )

Proof

Step Hyp Ref Expression
1 absex 
 |-  abs e. _V
2 cnfldstr 
 |-  CCfld Struct <. 1 , ; 2 1 >.
3 eufid 
 |-  EuclF = Slot ( EuclF ` ndx )
4 snsspr2 
 |-  { <. ( EuclF ` ndx ) , abs >. } C_ { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. , <. ( EuclF ` ndx ) , abs >. }
5 ssun2 
 |-  { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. , <. ( EuclF ` ndx ) , abs >. } C_ ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. , <. ( EuclF ` ndx ) , abs >. } )
6 ssun2 
 |-  ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. , <. ( EuclF ` ndx ) , abs >. } ) C_ ( ( { <. ( 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. - ) ) >. , <. ( EuclF ` ndx ) , abs >. } ) )
7 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. - ) ) >. , <. ( EuclF ` ndx ) , abs >. } ) )
8 6 7 sseqtrri 
 |-  ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. , <. ( EuclF ` ndx ) , abs >. } ) C_ CCfld
9 5 8 sstri 
 |-  { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. , <. ( EuclF ` ndx ) , abs >. } C_ CCfld
10 4 9 sstri 
 |-  { <. ( EuclF ` ndx ) , abs >. } C_ CCfld
11 2 3 10 strfv 
 |-  ( abs e. _V -> abs = ( EuclF ` CCfld ) )
12 1 11 ax-mp 
 |-  abs = ( EuclF ` CCfld )