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

Metamath Proof Explorer

Theorem dfcnfldOLD

Description: Obsolete version of df-cnfld as of 27-Apr-2025. (Contributed by Stefan O'Rear, 27-Nov-2014) (Revised by Thierry Arnoux, 15-Dec-2017) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion dfcnfldOLD 
|- 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. - ) ) >. } ) )

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 eqidd 
 |-  ( T. -> <. ( Base ` ndx ) , CC >. = <. ( Base ` ndx ) , CC >. )
3 ax-addf 
 |-  + : ( CC X. CC ) --> CC
4 ffn 
 |-  ( + : ( CC X. CC ) --> CC -> + Fn ( CC X. CC ) )
5 3 4 ax-mp 
 |-  + Fn ( CC X. CC )
6 fnov 
 |-  ( + Fn ( CC X. CC ) <-> + = ( u e. CC , v e. CC |-> ( u + v ) ) )
7 5 6 mpbi 
 |-  + = ( u e. CC , v e. CC |-> ( u + v ) )
8 eqcom 
 |-  ( + = ( u e. CC , v e. CC |-> ( u + v ) ) <-> ( u e. CC , v e. CC |-> ( u + v ) ) = + )
9 7 8 mpbi 
 |-  ( u e. CC , v e. CC |-> ( u + v ) ) = +
10 9 opeq2i 
 |-  <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. = <. ( +g ` ndx ) , + >.
11 10 a1i 
 |-  ( T. -> <. ( +g ` ndx ) , ( u e. CC , v e. CC |-> ( u + v ) ) >. = <. ( +g ` ndx ) , + >. )
12 ax-mulf 
 |-  x. : ( CC X. CC ) --> CC
13 ffn 
 |-  ( x. : ( CC X. CC ) --> CC -> x. Fn ( CC X. CC ) )
14 12 13 ax-mp 
 |-  x. Fn ( CC X. CC )
15 fnov 
 |-  ( x. Fn ( CC X. CC ) <-> x. = ( u e. CC , v e. CC |-> ( u x. v ) ) )
16 14 15 mpbi 
 |-  x. = ( u e. CC , v e. CC |-> ( u x. v ) )
17 eqcom 
 |-  ( x. = ( u e. CC , v e. CC |-> ( u x. v ) ) <-> ( u e. CC , v e. CC |-> ( u x. v ) ) = x. )
18 16 17 mpbi 
 |-  ( u e. CC , v e. CC |-> ( u x. v ) ) = x.
19 18 opeq2i 
 |-  <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. = <. ( .r ` ndx ) , x. >.
20 19 a1i 
 |-  ( T. -> <. ( .r ` ndx ) , ( u e. CC , v e. CC |-> ( u x. v ) ) >. = <. ( .r ` ndx ) , x. >. )
21 2 11 20 tpeq123d 
 |-  ( T. -> { <. ( 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 >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. } )
22 21 mptru 
 |-  { <. ( 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 >. , <. ( +g ` ndx ) , + >. , <. ( .r ` ndx ) , x. >. }
23 22 uneq1i 
 |-  ( { <. ( 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 ) , + >. , <. ( .r ` ndx ) , x. >. } u. { <. ( *r ` ndx ) , * >. } )
24 23 uneq1i 
 |-  ( ( { <. ( 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 >. , <. ( +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. - ) ) >. } ) )
25 1 24 eqtri 
 |-  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. - ) ) >. } ) )