| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > cnfldadd | Structured version Visualization version GIF version | ||
| Description: The addition operation of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) Revise df-cnfld 21426. (Revised by GG, 27-Apr-2025.) |
| Ref | Expression |
|---|---|
| cnfldadd | ⊢ + = (+g‘ℂfld) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-addf 11153 | . . . 4 ⊢ + :(ℂ × ℂ)⟶ℂ | |
| 2 | ffn 6692 | . . . 4 ⊢ ( + :(ℂ × ℂ)⟶ℂ → + Fn (ℂ × ℂ)) | |
| 3 | 1, 2 | ax-mp 5 | . . 3 ⊢ + Fn (ℂ × ℂ) |
| 4 | fnov 7528 | . . 3 ⊢ ( + Fn (ℂ × ℂ) ↔ + = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))) | |
| 5 | 3, 4 | mpbi 232 | . 2 ⊢ + = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦)) |
| 6 | mpocnfldadd 21430 | . 2 ⊢ (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦)) = (+g‘ℂfld) | |
| 7 | 5, 6 | eqtri 2786 | 1 ⊢ + = (+g‘ℂfld) |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1561 × cxp 5646 Fn wfn 6517 ⟶wf 6518 ‘cfv 6522 (class class class)co 7397 ∈ cmpo 7399 ℂcc 11072 + caddc 11077 +gcplusg 17287 ℂfldccnfld 21425 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1816 ax-4 1830 ax-5 1931 ax-6 1988 ax-7 2029 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-sep 5247 ax-nul 5257 ax-pow 5323 ax-pr 5391 ax-un 7719 ax-cnex 11130 ax-resscn 11131 ax-1cn 11132 ax-icn 11133 ax-addcl 11134 ax-addrcl 11135 ax-mulcl 11136 ax-mulrcl 11137 ax-mulcom 11138 ax-addass 11139 ax-mulass 11140 ax-distr 11141 ax-i2m1 11142 ax-1ne0 11143 ax-1rid 11144 ax-rnegex 11145 ax-rrecex 11146 ax-cnre 11147 ax-pre-lttri 11148 ax-pre-lttrn 11149 ax-pre-ltadd 11150 ax-pre-mulgt0 11151 ax-addf 11153 |
| This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1100 df-3an 1101 df-tru 1564 df-fal 1574 df-ex 1801 df-nf 1805 df-sb 2092 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3063 df-ral 3078 df-rex 3088 df-reu 3369 df-rab 3416 df-v 3457 df-sbc 3746 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4482 df-pw 4558 df-sn 4584 df-pr 4586 df-tp 4588 df-op 4590 df-uni 4867 df-iun 4952 df-br 5102 df-opab 5164 df-mpt 5183 df-tr 5209 df-id 5543 df-eprel 5548 df-po 5556 df-so 5557 df-fr 5601 df-we 5603 df-xp 5654 df-rel 5655 df-cnv 5656 df-co 5657 df-dm 5658 df-rn 5659 df-res 5660 df-ima 5661 df-pred 6289 df-ord 6350 df-on 6351 df-lim 6352 df-suc 6353 df-iota 6478 df-fun 6524 df-fn 6525 df-f 6526 df-f1 6527 df-fo 6528 df-f1o 6529 df-fv 6530 df-riota 7354 df-ov 7400 df-oprab 7401 df-mpo 7402 df-om 7848 df-1st 7971 df-2nd 7972 df-frecs 8263 df-wrecs 8294 df-recs 8343 df-rdg 8382 df-1o 8438 df-er 8679 df-en 8929 df-dom 8930 df-sdom 8931 df-fin 8932 df-pnf 11219 df-mnf 11220 df-xr 11221 df-ltxr 11222 df-le 11223 df-sub 11417 df-neg 11418 df-nn 12212 df-2 12281 df-3 12282 df-4 12283 df-5 12284 df-6 12285 df-7 12286 df-8 12287 df-9 12288 df-n0 12483 df-z 12570 df-dec 12690 df-uz 12841 df-fz 13514 df-struct 17184 df-slot 17219 df-ndx 17231 df-base 17247 df-plusg 17300 df-mulr 17301 df-starv 17302 df-tset 17306 df-ple 17307 df-ds 17309 df-unif 17310 df-cnfld 21426 |
| This theorem is referenced by: cncrng 21446 cnfld0 21449 cnfldneg 21451 cnfldplusf 21452 cnfldsub 21453 cnfldmulg 21457 cnsrng 21459 cnsubmlem 21468 cnsubglem 21469 absabv 21477 cnsubrg 21480 gsumfsum 21487 regsumfsum 21488 expmhm 21489 nn0srg 21490 rge0srg 21491 zringplusg 21507 replusg 21663 regsumsupp 21675 mhpmulcl 22215 clmadd 25137 clmacl 25147 isclmp 25160 cnlmod 25203 cnncvsaddassdemo 25226 cphsqrtcl2 25249 ipcau2 25297 tdeglem3 26120 tdeglem4 26121 taylply2 26432 efgh 26607 efabl 26616 jensenlem1 27052 jensenlem2 27053 qabvle 27690 padicabv 27695 ostth2lem2 27699 ostth3 27703 gsumzrsum 33246 xrge0slmod 33535 zringfrac 33751 psrmonprod 33850 ccfldsrarelvec 33969 ccfldextdgrr 33970 constrelextdg2 34045 constrsdrg 34073 2sqr3minply 34078 cos9thpiminplylem6 34085 cos9thpiminply 34086 qqhghm 34286 qqhrhm 34287 esumpfinvallem 34372 mhphflem 43179 fsumcnsrcl 43744 rngunsnply 43747 deg1mhm 43778 amgm2d 44775 amgm3d 44776 amgm4d 44777 sge0tsms 46955 cnfldsrngadd 48785 aacllem 50423 amgmw2d 50426 |
| Copyright terms: Public domain | W3C validator |