![]() |
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.) |
Ref | Expression |
---|---|
cnfldadd | ⊢ + = (+g‘ℂfld) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | addex 12196 | . 2 ⊢ + ∈ V | |
2 | cnfldstr 20243 | . . 3 ⊢ ℂfld Struct 〈1, ;13〉 | |
3 | plusgid 16446 | . . 3 ⊢ +g = Slot (+g‘ndx) | |
4 | snsstp2 4618 | . . . 4 ⊢ {〈(+g‘ndx), + 〉} ⊆ {〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), · 〉} | |
5 | ssun1 4031 | . . . . 5 ⊢ {〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), · 〉} ⊆ ({〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), · 〉} ∪ {〈(*𝑟‘ndx), ∗〉}) | |
6 | ssun1 4031 | . . . . . 6 ⊢ ({〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), · 〉} ∪ {〈(*𝑟‘ndx), ∗〉}) ⊆ (({〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), · 〉} ∪ {〈(*𝑟‘ndx), ∗〉}) ∪ ({〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉, 〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ − )〉} ∪ {〈(UnifSet‘ndx), (metUnif‘(abs ∘ − ))〉})) | |
7 | df-cnfld 20242 | . . . . . 6 ⊢ ℂfld = (({〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), · 〉} ∪ {〈(*𝑟‘ndx), ∗〉}) ∪ ({〈(TopSet‘ndx), (MetOpen‘(abs ∘ − ))〉, 〈(le‘ndx), ≤ 〉, 〈(dist‘ndx), (abs ∘ − )〉} ∪ {〈(UnifSet‘ndx), (metUnif‘(abs ∘ − ))〉})) | |
8 | 6, 7 | sseqtr4i 3888 | . . . . 5 ⊢ ({〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), · 〉} ∪ {〈(*𝑟‘ndx), ∗〉}) ⊆ ℂfld |
9 | 5, 8 | sstri 3861 | . . . 4 ⊢ {〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), · 〉} ⊆ ℂfld |
10 | 4, 9 | sstri 3861 | . . 3 ⊢ {〈(+g‘ndx), + 〉} ⊆ ℂfld |
11 | 2, 3, 10 | strfv 16381 | . 2 ⊢ ( + ∈ V → + = (+g‘ℂfld)) |
12 | 1, 11 | ax-mp 5 | 1 ⊢ + = (+g‘ℂfld) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1507 ∈ wcel 2050 Vcvv 3409 ∪ cun 3821 {csn 4435 {ctp 4439 〈cop 4441 ∘ ccom 5405 ‘cfv 6182 ℂcc 10327 1c1 10330 + caddc 10332 · cmul 10334 ≤ cle 10469 − cmin 10664 3c3 11490 ;cdc 11905 ∗ccj 14310 abscabs 14448 ndxcnx 16330 Basecbs 16333 +gcplusg 16415 .rcmulr 16416 *𝑟cstv 16417 TopSetcts 16421 lecple 16422 distcds 16424 UnifSetcunif 16425 MetOpencmopn 20231 metUnifcmetu 20232 ℂfldccnfld 20241 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2744 ax-sep 5054 ax-nul 5061 ax-pow 5113 ax-pr 5180 ax-un 7273 ax-cnex 10385 ax-resscn 10386 ax-1cn 10387 ax-icn 10388 ax-addcl 10389 ax-addrcl 10390 ax-mulcl 10391 ax-mulrcl 10392 ax-mulcom 10393 ax-addass 10394 ax-mulass 10395 ax-distr 10396 ax-i2m1 10397 ax-1ne0 10398 ax-1rid 10399 ax-rnegex 10400 ax-rrecex 10401 ax-cnre 10402 ax-pre-lttri 10403 ax-pre-lttrn 10404 ax-pre-ltadd 10405 ax-pre-mulgt0 10406 ax-addf 10408 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2584 df-clab 2753 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ne 2962 df-nel 3068 df-ral 3087 df-rex 3088 df-reu 3089 df-rab 3091 df-v 3411 df-sbc 3676 df-csb 3781 df-dif 3826 df-un 3828 df-in 3830 df-ss 3837 df-pss 3839 df-nul 4173 df-if 4345 df-pw 4418 df-sn 4436 df-pr 4438 df-tp 4440 df-op 4442 df-uni 4707 df-int 4744 df-iun 4788 df-br 4924 df-opab 4986 df-mpt 5003 df-tr 5025 df-id 5306 df-eprel 5311 df-po 5320 df-so 5321 df-fr 5360 df-we 5362 df-xp 5407 df-rel 5408 df-cnv 5409 df-co 5410 df-dm 5411 df-rn 5412 df-res 5413 df-ima 5414 df-pred 5980 df-ord 6026 df-on 6027 df-lim 6028 df-suc 6029 df-iota 6146 df-fun 6184 df-fn 6185 df-f 6186 df-f1 6187 df-fo 6188 df-f1o 6189 df-fv 6190 df-riota 6931 df-ov 6973 df-oprab 6974 df-mpo 6975 df-om 7391 df-1st 7495 df-2nd 7496 df-wrecs 7744 df-recs 7806 df-rdg 7844 df-1o 7899 df-oadd 7903 df-er 8083 df-en 8301 df-dom 8302 df-sdom 8303 df-fin 8304 df-pnf 10470 df-mnf 10471 df-xr 10472 df-ltxr 10473 df-le 10474 df-sub 10666 df-neg 10667 df-nn 11434 df-2 11497 df-3 11498 df-4 11499 df-5 11500 df-6 11501 df-7 11502 df-8 11503 df-9 11504 df-n0 11702 df-z 11788 df-dec 11906 df-uz 12053 df-fz 12703 df-struct 16335 df-ndx 16336 df-slot 16337 df-base 16339 df-plusg 16428 df-mulr 16429 df-starv 16430 df-tset 16434 df-ple 16435 df-ds 16437 df-unif 16438 df-cnfld 20242 |
This theorem is referenced by: cncrng 20262 cnfld0 20265 cnfldneg 20267 cnfldplusf 20268 cnfldsub 20269 cnfldmulg 20273 cnsrng 20275 cnsubmlem 20289 cnsubglem 20290 absabv 20298 cnsubrg 20301 gsumfsum 20308 regsumfsum 20309 expmhm 20310 nn0srg 20311 rge0srg 20312 zringplusg 20320 replusg 20450 regsumsupp 20462 clmadd 23375 clmacl 23385 isclmp 23398 cnlmod 23441 cnncvsaddassdemo 23464 cphsqrtcl2 23487 ipcau2 23534 tdeglem3 24350 tdeglem4 24351 taylply2 24653 efgh 24820 efabl 24829 jensenlem1 25260 jensenlem2 25261 amgmlem 25263 qabvle 25897 padicabv 25902 ostth2lem2 25906 ostth3 25910 xrge0slmod 30596 ccfldsrarelvec 30685 ccfldextdgrr 30686 qqhghm 30873 qqhrhm 30874 esumpfinvallem 30977 fsumcnsrcl 39162 rngunsnply 39169 deg1mhm 39203 amgm2d 39916 amgm3d 39917 amgm4d 39918 sge0tsms 42093 cnfldsrngadd 43405 aacllem 44269 amgmw2d 44272 |
Copyright terms: Public domain | W3C validator |