Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > cnfldmul | Structured version Visualization version GIF version |
Description: The multiplication 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 |
---|---|
cnfldmul | ⊢ · = (.r‘ℂfld) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mulex 12738 | . 2 ⊢ · ∈ V | |
2 | cnfldstr 20608 | . . 3 ⊢ ℂfld Struct 〈1, ;13〉 | |
3 | mulrid 17013 | . . 3 ⊢ .r = Slot (.r‘ndx) | |
4 | snsstp3 4752 | . . . 4 ⊢ {〈(.r‘ndx), · 〉} ⊆ {〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), · 〉} | |
5 | ssun1 4107 | . . . . 5 ⊢ {〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), · 〉} ⊆ ({〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), · 〉} ∪ {〈(*𝑟‘ndx), ∗〉}) | |
6 | ssun1 4107 | . . . . . 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 20607 | . . . . . 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 | sseqtrri 3959 | . . . . 5 ⊢ ({〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), · 〉} ∪ {〈(*𝑟‘ndx), ∗〉}) ⊆ ℂfld |
9 | 5, 8 | sstri 3931 | . . . 4 ⊢ {〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), + 〉, 〈(.r‘ndx), · 〉} ⊆ ℂfld |
10 | 4, 9 | sstri 3931 | . . 3 ⊢ {〈(.r‘ndx), · 〉} ⊆ ℂfld |
11 | 2, 3, 10 | strfv 16914 | . 2 ⊢ ( · ∈ V → · = (.r‘ℂfld)) |
12 | 1, 11 | ax-mp 5 | 1 ⊢ · = (.r‘ℂfld) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1539 ∈ wcel 2107 Vcvv 3433 ∪ cun 3886 {csn 4562 {ctp 4566 〈cop 4568 ∘ ccom 5594 ‘cfv 6437 ℂcc 10878 1c1 10881 + caddc 10883 · cmul 10885 ≤ cle 11019 − cmin 11214 3c3 12038 ;cdc 12446 ∗ccj 14816 abscabs 14954 ndxcnx 16903 Basecbs 16921 +gcplusg 16971 .rcmulr 16972 *𝑟cstv 16973 TopSetcts 16977 lecple 16978 distcds 16980 UnifSetcunif 16981 MetOpencmopn 20596 metUnifcmetu 20597 ℂfldccnfld 20606 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2710 ax-sep 5224 ax-nul 5231 ax-pow 5289 ax-pr 5353 ax-un 7597 ax-cnex 10936 ax-resscn 10937 ax-1cn 10938 ax-icn 10939 ax-addcl 10940 ax-addrcl 10941 ax-mulcl 10942 ax-mulrcl 10943 ax-mulcom 10944 ax-addass 10945 ax-mulass 10946 ax-distr 10947 ax-i2m1 10948 ax-1ne0 10949 ax-1rid 10950 ax-rnegex 10951 ax-rrecex 10952 ax-cnre 10953 ax-pre-lttri 10954 ax-pre-lttrn 10955 ax-pre-ltadd 10956 ax-pre-mulgt0 10957 ax-mulf 10960 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2817 df-nfc 2890 df-ne 2945 df-nel 3051 df-ral 3070 df-rex 3071 df-reu 3073 df-rab 3074 df-v 3435 df-sbc 3718 df-csb 3834 df-dif 3891 df-un 3893 df-in 3895 df-ss 3905 df-pss 3907 df-nul 4258 df-if 4461 df-pw 4536 df-sn 4563 df-pr 4565 df-tp 4567 df-op 4569 df-uni 4841 df-iun 4927 df-br 5076 df-opab 5138 df-mpt 5159 df-tr 5193 df-id 5490 df-eprel 5496 df-po 5504 df-so 5505 df-fr 5545 df-we 5547 df-xp 5596 df-rel 5597 df-cnv 5598 df-co 5599 df-dm 5600 df-rn 5601 df-res 5602 df-ima 5603 df-pred 6206 df-ord 6273 df-on 6274 df-lim 6275 df-suc 6276 df-iota 6395 df-fun 6439 df-fn 6440 df-f 6441 df-f1 6442 df-fo 6443 df-f1o 6444 df-fv 6445 df-riota 7241 df-ov 7287 df-oprab 7288 df-mpo 7289 df-om 7722 df-1st 7840 df-2nd 7841 df-frecs 8106 df-wrecs 8137 df-recs 8211 df-rdg 8250 df-1o 8306 df-er 8507 df-en 8743 df-dom 8744 df-sdom 8745 df-fin 8746 df-pnf 11020 df-mnf 11021 df-xr 11022 df-ltxr 11023 df-le 11024 df-sub 11216 df-neg 11217 df-nn 11983 df-2 12045 df-3 12046 df-4 12047 df-5 12048 df-6 12049 df-7 12050 df-8 12051 df-9 12052 df-n0 12243 df-z 12329 df-dec 12447 df-uz 12592 df-fz 13249 df-struct 16857 df-slot 16892 df-ndx 16904 df-base 16922 df-plusg 16984 df-mulr 16985 df-starv 16986 df-tset 16990 df-ple 16991 df-ds 16993 df-unif 16994 df-cnfld 20607 |
This theorem is referenced by: cncrng 20628 cnfld1 20632 cndrng 20636 cnflddiv 20637 cnfldexp 20640 cnsrng 20641 cnsubrglem 20657 absabv 20664 cnsubrg 20667 cnmsubglem 20670 expmhm 20676 nn0srg 20677 rge0srg 20678 zringmulr 20688 expghm 20706 psgnghm 20794 psgnco 20797 evpmodpmf1o 20810 remulr 20825 mdetralt 21766 clmmul 24247 clmmcl 24257 isclmp 24269 cnlmod 24312 cnncvsmulassdemo 24337 cphsubrglem 24350 cphdivcl 24355 cphabscl 24358 cphsqrtcl2 24359 cphsqrtcl3 24360 ipcau2 24407 plypf1 25382 dvply2g 25454 taylply2 25536 reefgim 25618 efabl 25715 efsubm 25716 amgmlem 26148 amgm 26149 wilthlem2 26227 wilthlem3 26228 dchrelbas3 26395 dchrzrhmul 26403 dchrmulcl 26406 dchrn0 26407 dchrinvcl 26410 dchrsum2 26425 sum2dchr 26431 qabvexp 26783 ostthlem2 26785 padicabv 26787 ostth2lem2 26791 ostth3 26795 xrge0slmod 31557 ccfldsrarelvec 31750 ccfldextdgrr 31751 iistmd 31861 xrge0iifmhm 31898 xrge0pluscn 31899 qqhrhm 31948 cnsrexpcl 40997 cnsrplycl 40999 rngunsnply 41005 amgm2d 41816 amgm3d 41817 amgm4d 41818 cnfldsrngmul 45336 aacllem 46516 amgmlemALT 46518 amgmw2d 46519 |
Copyright terms: Public domain | W3C validator |