Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  axmulf Structured version   Unicode version

Theorem axmulf 9052
 Description: Multiplication 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 axmulcl 9059. This construction-dependent theorem should not be referenced directly; instead, use ax-mulf 9101. (Contributed by NM, 8-Feb-2005.) (New usage is discouraged.)
Assertion
Ref Expression
axmulf

Proof of Theorem axmulf
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 moeq 3116 . . . . . . . . 9
21mosubop 4484 . . . . . . . 8
32mosubop 4484 . . . . . . 7
4 anass 632 . . . . . . . . . . 11
542exbii 1594 . . . . . . . . . 10
6 19.42vv 1933 . . . . . . . . . 10
75, 6bitri 242 . . . . . . . . 9
872exbii 1594 . . . . . . . 8
98mobii 2323 . . . . . . 7
103, 9mpbir 202 . . . . . 6
1110moani 2339 . . . . 5
1211funoprab 6199 . . . 4
13 df-mul 9033 . . . . 5
1413funeqi 5503 . . . 4
1512, 14mpbir 202 . . 3
1613dmeqi 5100 . . . . 5
17 dmoprabss 6184 . . . . 5
1816, 17eqsstri 3364 . . . 4
19 0ncn 9039 . . . . 5
20 df-c 9027 . . . . . . 7
21 oveq1 6117 . . . . . . . 8
2221eleq1d 2508 . . . . . . 7
23 oveq2 6118 . . . . . . . 8
2423eleq1d 2508 . . . . . . 7
25 mulcnsr 9042 . . . . . . . 8
26 mulclsr 8990 . . . . . . . . . . 11
27 m1r 8988 . . . . . . . . . . . 12
28 mulclsr 8990 . . . . . . . . . . . 12
29 mulclsr 8990 . . . . . . . . . . . 12
3027, 28, 29sylancr 646 . . . . . . . . . . 11
31 addclsr 8989 . . . . . . . . . . 11
3226, 30, 31syl2an 465 . . . . . . . . . 10
3332an4s 801 . . . . . . . . 9
34 mulclsr 8990 . . . . . . . . . . 11
35 mulclsr 8990 . . . . . . . . . . 11
36 addclsr 8989 . . . . . . . . . . 11
3734, 35, 36syl2anr 466 . . . . . . . . . 10
3837an42s 802 . . . . . . . . 9
39 opelxpi 4939 . . . . . . . . 9
4033, 38, 39syl2anc 644 . . . . . . . 8
4125, 40eqeltrd 2516 . . . . . . 7
4220, 22, 24, 412optocl 4982 . . . . . 6
4342, 20syl6eleqr 2533 . . . . 5
4419, 43oprssdm 6257 . . . 4
4518, 44eqssi 3350 . . 3
46 df-fn 5486 . . 3
4715, 45, 46mpbir2an 888 . 2
4843rgen2a 2778 . 2
49 ffnov 6203 . 2
5047, 48, 49mpbir2an 888 1
 Colors of variables: wff set class Syntax hints:   wa 360  wex 1551   wceq 1653   wcel 1727  wmo 2288  wral 2711  cop 3841   cxp 4905   cdm 4907   wfun 5477   wfn 5478  wf 5479  (class class class)co 6110  coprab 6111  cnr 8773  cm1r 8776   cplr 8777   cmr 8778  cc 9019   cmul 9026 This theorem is referenced by:  axmulcl  9059 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-13 1729  ax-14 1731  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423  ax-sep 4355  ax-nul 4363  ax-pow 4406  ax-pr 4432  ax-un 4730  ax-inf2 7625 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2291  df-mo 2292  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ne 2607  df-ral 2716  df-rex 2717  df-reu 2718  df-rmo 2719  df-rab 2720  df-v 2964  df-sbc 3168  df-csb 3268  df-dif 3309  df-un 3311  df-in 3313  df-ss 3320  df-pss 3322  df-nul 3614  df-if 3764  df-pw 3825  df-sn 3844  df-pr 3845  df-tp 3846  df-op 3847  df-uni 4040  df-int 4075  df-iun 4119  df-br 4238  df-opab 4292  df-mpt 4293  df-tr 4328  df-eprel 4523  df-id 4527  df-po 4532  df-so 4533  df-fr 4570  df-we 4572  df-ord 4613  df-on 4614  df-lim 4615  df-suc 4616  df-om 4875  df-xp 4913  df-rel 4914  df-cnv 4915  df-co 4916  df-dm 4917  df-rn 4918  df-res 4919  df-ima 4920  df-iota 5447  df-fun 5485  df-fn 5486  df-f 5487  df-f1 5488  df-fo 5489  df-f1o 5490  df-fv 5491  df-ov 6113  df-oprab 6114  df-mpt2 6115  df-1st 6378  df-2nd 6379  df-recs 6662  df-rdg 6697  df-1o 6753  df-oadd 6757  df-omul 6758  df-er 6934  df-ec 6936  df-qs 6940  df-ni 8780  df-pli 8781  df-mi 8782  df-lti 8783  df-plpq 8816  df-mpq 8817  df-ltpq 8818  df-enq 8819  df-nq 8820  df-erq 8821  df-plq 8822  df-mq 8823  df-1nq 8824  df-rq 8825  df-ltnq 8826  df-np 8889  df-1p 8890  df-plp 8891  df-mp 8892  df-ltp 8893  df-plpr 8963  df-mpr 8964  df-enr 8965  df-nr 8966  df-plr 8967  df-mr 8968  df-m1r 8972  df-c 9027  df-mul 9033
 Copyright terms: Public domain W3C validator