| 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 21398. (Revised by GG, 27-Apr-2025.) |
| Ref | Expression |
|---|---|
| cnfldadd | ⊢ + = (+g‘ℂfld) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-addf 11142 | . . . 4 ⊢ + :(ℂ × ℂ)⟶ℂ | |
| 2 | ffn 6680 | . . . 4 ⊢ ( + :(ℂ × ℂ)⟶ℂ → + Fn (ℂ × ℂ)) | |
| 3 | 1, 2 | ax-mp 5 | . . 3 ⊢ + Fn (ℂ × ℂ) |
| 4 | fnov 7516 | . . 3 ⊢ ( + Fn (ℂ × ℂ) ↔ + = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦))) | |
| 5 | 3, 4 | mpbi 232 | . 2 ⊢ + = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦)) |
| 6 | mpocnfldadd 21402 | . 2 ⊢ (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 + 𝑦)) = (+g‘ℂfld) | |
| 7 | 5, 6 | eqtri 2779 | 1 ⊢ + = (+g‘ℂfld) |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1554 × cxp 5638 Fn wfn 6505 ⟶wf 6506 ‘cfv 6510 (class class class)co 7385 ∈ cmpo 7387 ℂcc 11061 + caddc 11066 +gcplusg 17262 ℂfldccnfld 21397 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1809 ax-4 1823 ax-5 1924 ax-6 1981 ax-7 2022 ax-8 2138 ax-9 2146 ax-10 2169 ax-11 2185 ax-12 2206 ax-ext 2728 ax-sep 5240 ax-nul 5250 ax-pow 5316 ax-pr 5384 ax-un 7707 ax-cnex 11119 ax-resscn 11120 ax-1cn 11121 ax-icn 11122 ax-addcl 11123 ax-addrcl 11124 ax-mulcl 11125 ax-mulrcl 11126 ax-mulcom 11127 ax-addass 11128 ax-mulass 11129 ax-distr 11130 ax-i2m1 11131 ax-1ne0 11132 ax-1rid 11133 ax-rnegex 11134 ax-rrecex 11135 ax-cnre 11136 ax-pre-lttri 11137 ax-pre-lttrn 11138 ax-pre-ltadd 11139 ax-pre-mulgt0 11140 ax-addf 11142 |
| This theorem depends on definitions: df-bi 209 df-an 399 df-or 857 df-3or 1096 df-3an 1097 df-tru 1557 df-fal 1567 df-ex 1794 df-nf 1798 df-sb 2085 df-mo 2560 df-eu 2590 df-clab 2735 df-cleq 2748 df-clel 2831 df-nfc 2905 df-ne 2952 df-nel 3056 df-ral 3071 df-rex 3081 df-reu 3362 df-rab 3409 df-v 3450 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4281 df-if 4475 df-pw 4551 df-sn 4577 df-pr 4579 df-tp 4581 df-op 4583 df-uni 4860 df-iun 4945 df-br 5095 df-opab 5157 df-mpt 5176 df-tr 5202 df-id 5535 df-eprel 5540 df-po 5548 df-so 5549 df-fr 5593 df-we 5595 df-xp 5646 df-rel 5647 df-cnv 5648 df-co 5649 df-dm 5650 df-rn 5651 df-res 5652 df-ima 5653 df-pred 6277 df-ord 6338 df-on 6339 df-lim 6340 df-suc 6341 df-iota 6466 df-fun 6512 df-fn 6513 df-f 6514 df-f1 6515 df-fo 6516 df-f1o 6517 df-fv 6518 df-riota 7342 df-ov 7388 df-oprab 7389 df-mpo 7390 df-om 7836 df-1st 7959 df-2nd 7960 df-frecs 8250 df-wrecs 8281 df-recs 8330 df-rdg 8369 df-1o 8425 df-er 8666 df-en 8917 df-dom 8918 df-sdom 8919 df-fin 8920 df-pnf 11208 df-mnf 11209 df-xr 11210 df-ltxr 11211 df-le 11212 df-sub 11406 df-neg 11407 df-nn 12201 df-2 12270 df-3 12271 df-4 12272 df-5 12273 df-6 12274 df-7 12275 df-8 12276 df-9 12277 df-n0 12472 df-z 12559 df-dec 12679 df-uz 12830 df-fz 13503 df-struct 17159 df-slot 17194 df-ndx 17206 df-base 17222 df-plusg 17275 df-mulr 17276 df-starv 17277 df-tset 17281 df-ple 17282 df-ds 17284 df-unif 17285 df-cnfld 21398 |
| This theorem is referenced by: cncrng 21418 cnfld0 21421 cnfldneg 21423 cnfldplusf 21424 cnfldsub 21425 cnfldmulg 21429 cnsrng 21431 cnsubmlem 21440 cnsubglem 21441 absabv 21449 cnsubrg 21452 gsumfsum 21459 regsumfsum 21460 expmhm 21461 nn0srg 21462 rge0srg 21463 zringplusg 21479 replusg 21635 regsumsupp 21647 mhpmulcl 22187 clmadd 25109 clmacl 25119 isclmp 25132 cnlmod 25175 cnncvsaddassdemo 25198 cphsqrtcl2 25221 ipcau2 25269 tdeglem3 26092 tdeglem4 26093 taylply2 26401 efgh 26576 efabl 26585 jensenlem1 27021 jensenlem2 27022 qabvle 27659 padicabv 27664 ostth2lem2 27668 ostth3 27672 gsumzrsum 33199 xrge0slmod 33488 zringfrac 33704 psrmonprod 33803 ccfldsrarelvec 33922 ccfldextdgrr 33923 constrelextdg2 33998 constrsdrg 34026 2sqr3minply 34031 cos9thpiminplylem6 34038 cos9thpiminply 34039 qqhghm 34239 qqhrhm 34240 esumpfinvallem 34325 mhphflem 43126 fsumcnsrcl 43691 rngunsnply 43694 deg1mhm 43725 amgm2d 44722 amgm3d 44723 amgm4d 44724 sge0tsms 46902 cnfldsrngadd 48732 aacllem 50370 amgmw2d 50373 |
| Copyright terms: Public domain | W3C validator |