Metamath Proof Explorer

Theorem cnfldstr

Description: The field of complex numbers is a structure. (Contributed by Mario Carneiro, 14-Aug-2015) (Revised by Thierry Arnoux, 17-Dec-2017) Revise df-cnfld . (Revised by GG, 31-Mar-2025)

Ref Expression
Assertion cnfldstr 
|- CCfld Struct <. 1 , ; 1 3 >.

Proof

Step Hyp Ref Expression
1 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. - ) ) >. } ) )
2 eqid 
 |-  ( { <. ( 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 >. , <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. , <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. } u. { <. ( *r ` ndx ) , * >. } )
3 2 srngstr 
 |-  ( { <. ( 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 ) , * >. } ) Struct <. 1 , 4 >.
4 9nn 
 |-  9 e. NN
5 tsetndx 
 |-  ( TopSet ` ndx ) = 9
6 9lt10 
 |-  9 < ; 1 0
7 10nn 
 |-  ; 1 0 e. NN
8 plendx 
 |-  ( le ` ndx ) = ; 1 0
9 1nn0 
 |-  1 e. NN0
10 0nn0 
 |-  0 e. NN0
11 2nn 
 |-  2 e. NN
12 2pos 
 |-  0 < 2
13 9 10 11 12 declt 
 |-  ; 1 0 < ; 1 2
14 9 11 decnncl 
 |-  ; 1 2 e. NN
15 dsndx 
 |-  ( dist ` ndx ) = ; 1 2
16 4 5 6 7 8 13 14 15 strle3 
 |-  { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } Struct <. 9 , ; 1 2 >.
17 3nn 
 |-  3 e. NN
18 9 17 decnncl 
 |-  ; 1 3 e. NN
19 unifndx 
 |-  ( UnifSet ` ndx ) = ; 1 3
20 18 19 strle1 
 |-  { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } Struct <. ; 1 3 , ; 1 3 >.
21 2nn0 
 |-  2 e. NN0
22 2lt3 
 |-  2 < 3
23 9 21 17 22 declt 
 |-  ; 1 2 < ; 1 3
24 16 20 23 strleun 
 |-  ( { <. ( TopSet ` ndx ) , ( MetOpen ` ( abs o. - ) ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( abs o. - ) >. } u. { <. ( UnifSet ` ndx ) , ( metUnif ` ( abs o. - ) ) >. } ) Struct <. 9 , ; 1 3 >.
25 4lt9 
 |-  4 < 9
26 3 24 25 strleun 
 |-  ( ( { <. ( 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. - ) ) >. } ) ) Struct <. 1 , ; 1 3 >.
27 1 26 eqbrtri 
 |-  CCfld Struct <. 1 , ; 1 3 >.