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 +:×

Proof

Step Hyp Ref Expression
1 moeq *zz=w+𝑹uv+𝑹f
2 1 mosubop *zufy=ufz=w+𝑹uv+𝑹f
3 2 mosubop *zwvx=wvufy=ufz=w+𝑹uv+𝑹f
4 anass x=wvy=ufz=w+𝑹uv+𝑹fx=wvy=ufz=w+𝑹uv+𝑹f
5 4 2exbii ufx=wvy=ufz=w+𝑹uv+𝑹fufx=wvy=ufz=w+𝑹uv+𝑹f
6 19.42vv ufx=wvy=ufz=w+𝑹uv+𝑹fx=wvufy=ufz=w+𝑹uv+𝑹f
7 5 6 bitri ufx=wvy=ufz=w+𝑹uv+𝑹fx=wvufy=ufz=w+𝑹uv+𝑹f
8 7 2exbii wvufx=wvy=ufz=w+𝑹uv+𝑹fwvx=wvufy=ufz=w+𝑹uv+𝑹f
9 8 mobii *zwvufx=wvy=ufz=w+𝑹uv+𝑹f*zwvx=wvufy=ufz=w+𝑹uv+𝑹f
10 3 9 mpbir *zwvufx=wvy=ufz=w+𝑹uv+𝑹f
11 10 moani *zxywvufx=wvy=ufz=w+𝑹uv+𝑹f
12 11 funoprab Funxyz|xywvufx=wvy=ufz=w+𝑹uv+𝑹f
13 df-add +=xyz|xywvufx=wvy=ufz=w+𝑹uv+𝑹f
14 13 funeqi Fun+Funxyz|xywvufx=wvy=ufz=w+𝑹uv+𝑹f
15 12 14 mpbir Fun+
16 13 dmeqi dom+=domxyz|xywvufx=wvy=ufz=w+𝑹uv+𝑹f
17 dmoprabss domxyz|xywvufx=wvy=ufz=w+𝑹uv+𝑹f×
18 16 17 eqsstri dom+×
19 0ncn ¬
20 df-c =𝑹×𝑹
21 oveq1 zw=xzw+vu=x+vu
22 21 eleq1d zw=xzw+vu𝑹×𝑹x+vu𝑹×𝑹
23 oveq2 vu=yx+vu=x+y
24 23 eleq1d vu=yx+vu𝑹×𝑹x+y𝑹×𝑹
25 addcnsr z𝑹w𝑹v𝑹u𝑹zw+vu=z+𝑹vw+𝑹u
26 addclsr z𝑹v𝑹z+𝑹v𝑹
27 addclsr w𝑹u𝑹w+𝑹u𝑹
28 26 27 anim12i z𝑹v𝑹w𝑹u𝑹z+𝑹v𝑹w+𝑹u𝑹
29 28 an4s z𝑹w𝑹v𝑹u𝑹z+𝑹v𝑹w+𝑹u𝑹
30 opelxpi z+𝑹v𝑹w+𝑹u𝑹z+𝑹vw+𝑹u𝑹×𝑹
31 29 30 syl z𝑹w𝑹v𝑹u𝑹z+𝑹vw+𝑹u𝑹×𝑹
32 25 31 eqeltrd z𝑹w𝑹v𝑹u𝑹zw+vu𝑹×𝑹
33 20 22 24 32 2optocl xyx+y𝑹×𝑹
34 33 20 eleqtrrdi xyx+y
35 19 34 oprssdm ×dom+
36 18 35 eqssi dom+=×
37 df-fn +Fn×Fun+dom+=×
38 15 36 37 mpbir2an +Fn×
39 34 rgen2 xyx+y
40 ffnov +:×+Fn×xyx+y
41 38 39 40 mpbir2an +:×