Metamath Proof Explorer

Theorem axaddf

Description: Addition is an operation on the complex numbers. This theorem can be used as an alternate axiom for complex numbers in place of the less specific axaddcl . This construction-dependent theorem should not be referenced directly; instead, use ax-addf . (Contributed by NM, 8-Feb-2005) (New usage is discouraged.)

Ref Expression
Assertion axaddf 
|- + : ( CC X. CC ) --> CC

Proof

Step Hyp Ref Expression
1 moeq 
 |-  E* z z = <. ( w +R u ) , ( v +R f ) >.
2 1 mosubop 
 |-  E* z E. u E. f ( y = <. u , f >. /\ z = <. ( w +R u ) , ( v +R f ) >. )
3 2 mosubop 
 |-  E* z E. w E. v ( x = <. w , v >. /\ E. u E. f ( y = <. u , f >. /\ z = <. ( w +R u ) , ( v +R f ) >. ) )
4 anass 
 |-  ( ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( w +R u ) , ( v +R f ) >. ) <-> ( x = <. w , v >. /\ ( y = <. u , f >. /\ z = <. ( w +R u ) , ( v +R f ) >. ) ) )
5 4 2exbii 
 |-  ( E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( w +R u ) , ( v +R f ) >. ) <-> E. u E. f ( x = <. w , v >. /\ ( y = <. u , f >. /\ z = <. ( w +R u ) , ( v +R f ) >. ) ) )
6 19.42vv 
 |-  ( E. u E. f ( x = <. w , v >. /\ ( y = <. u , f >. /\ z = <. ( w +R u ) , ( v +R f ) >. ) ) <-> ( x = <. w , v >. /\ E. u E. f ( y = <. u , f >. /\ z = <. ( w +R u ) , ( v +R f ) >. ) ) )
7 5 6 bitri 
 |-  ( E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( w +R u ) , ( v +R f ) >. ) <-> ( x = <. w , v >. /\ E. u E. f ( y = <. u , f >. /\ z = <. ( w +R u ) , ( v +R f ) >. ) ) )
8 7 2exbii 
 |-  ( E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( w +R u ) , ( v +R f ) >. ) <-> E. w E. v ( x = <. w , v >. /\ E. u E. f ( y = <. u , f >. /\ z = <. ( w +R u ) , ( v +R f ) >. ) ) )
9 8 mobii 
 |-  ( E* z E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( w +R u ) , ( v +R f ) >. ) <-> E* z E. w E. v ( x = <. w , v >. /\ E. u E. f ( y = <. u , f >. /\ z = <. ( w +R u ) , ( v +R f ) >. ) ) )
10 3 9 mpbir 
 |-  E* z E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( w +R u ) , ( v +R f ) >. )
11 10 moani 
 |-  E* z ( ( x e. CC /\ y e. CC ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( w +R u ) , ( v +R f ) >. ) )
12 11 funoprab 
 |-  Fun { <. <. x , y >. , z >. | ( ( x e. CC /\ y e. CC ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( w +R u ) , ( v +R f ) >. ) ) }
13 df-add 
 |-  + = { <. <. x , y >. , z >. | ( ( x e. CC /\ y e. CC ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( w +R u ) , ( v +R f ) >. ) ) }
14 13 funeqi 
 |-  ( Fun + <-> Fun { <. <. x , y >. , z >. | ( ( x e. CC /\ y e. CC ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( w +R u ) , ( v +R f ) >. ) ) } )
15 12 14 mpbir 
 |-  Fun +
16 13 dmeqi 
 |-  dom + = dom { <. <. x , y >. , z >. | ( ( x e. CC /\ y e. CC ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( w +R u ) , ( v +R f ) >. ) ) }
17 dmoprabss 
 |-  dom { <. <. x , y >. , z >. | ( ( x e. CC /\ y e. CC ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( w +R u ) , ( v +R f ) >. ) ) } C_ ( CC X. CC )
18 16 17 eqsstri 
 |-  dom + C_ ( CC X. CC )
19 0ncn 
 |-  -. (/) e. CC
20 df-c 
 |-  CC = ( R. X. R. )
21 oveq1 
 |-  ( <. z , w >. = x -> ( <. z , w >. + <. v , u >. ) = ( x + <. v , u >. ) )
22 21 eleq1d 
 |-  ( <. z , w >. = x -> ( ( <. z , w >. + <. v , u >. ) e. ( R. X. R. ) <-> ( x + <. v , u >. ) e. ( R. X. R. ) ) )
23 oveq2 
 |-  ( <. v , u >. = y -> ( x + <. v , u >. ) = ( x + y ) )
24 23 eleq1d 
 |-  ( <. v , u >. = y -> ( ( x + <. v , u >. ) e. ( R. X. R. ) <-> ( x + y ) e. ( R. X. R. ) ) )
25 addcnsr 
 |-  ( ( ( z e. R. /\ w e. R. ) /\ ( v e. R. /\ u e. R. ) ) -> ( <. z , w >. + <. v , u >. ) = <. ( z +R v ) , ( w +R u ) >. )
26 addclsr 
 |-  ( ( z e. R. /\ v e. R. ) -> ( z +R v ) e. R. )
27 addclsr 
 |-  ( ( w e. R. /\ u e. R. ) -> ( w +R u ) e. R. )
28 26 27 anim12i 
 |-  ( ( ( z e. R. /\ v e. R. ) /\ ( w e. R. /\ u e. R. ) ) -> ( ( z +R v ) e. R. /\ ( w +R u ) e. R. ) )
29 28 an4s 
 |-  ( ( ( z e. R. /\ w e. R. ) /\ ( v e. R. /\ u e. R. ) ) -> ( ( z +R v ) e. R. /\ ( w +R u ) e. R. ) )
30 opelxpi 
 |-  ( ( ( z +R v ) e. R. /\ ( w +R u ) e. R. ) -> <. ( z +R v ) , ( w +R u ) >. e. ( R. X. R. ) )
31 29 30 syl 
 |-  ( ( ( z e. R. /\ w e. R. ) /\ ( v e. R. /\ u e. R. ) ) -> <. ( z +R v ) , ( w +R u ) >. e. ( R. X. R. ) )
32 25 31 eqeltrd 
 |-  ( ( ( z e. R. /\ w e. R. ) /\ ( v e. R. /\ u e. R. ) ) -> ( <. z , w >. + <. v , u >. ) e. ( R. X. R. ) )
33 20 22 24 32 2optocl 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x + y ) e. ( R. X. R. ) )
34 33 20 eleqtrrdi 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x + y ) e. CC )
35 19 34 oprssdm 
 |-  ( CC X. CC ) C_ dom +
36 18 35 eqssi 
 |-  dom + = ( CC X. CC )
37 df-fn 
 |-  ( + Fn ( CC X. CC ) <-> ( Fun + /\ dom + = ( CC X. CC ) ) )
38 15 36 37 mpbir2an 
 |-  + Fn ( CC X. CC )
39 34 rgen2 
 |-  A. x e. CC A. y e. CC ( x + y ) e. CC
40 ffnov 
 |-  ( + : ( CC X. CC ) --> CC <-> ( + Fn ( CC X. CC ) /\ A. x e. CC A. y e. CC ( x + y ) e. CC ) )
41 38 39 40 mpbir2an 
 |-  + : ( CC X. CC ) --> CC