| 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.) Revise df-cnfld 21575. (Revised by GG, 27-Apr-2025.) |
| Ref | Expression |
|---|---|
| cnfldmul | ⊢ · = (.r‘ℂfld) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-mulf 11197 | . . . 4 ⊢ · :(ℂ × ℂ)⟶ℂ | |
| 2 | ffn 6709 | . . . 4 ⊢ ( · :(ℂ × ℂ)⟶ℂ → · Fn (ℂ × ℂ)) | |
| 3 | 1, 2 | ax-mp 5 | . . 3 ⊢ · Fn (ℂ × ℂ) |
| 4 | fnov 7550 | . . 3 ⊢ ( · Fn (ℂ × ℂ) ↔ · = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))) | |
| 5 | 3, 4 | mpbi 233 | . 2 ⊢ · = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) |
| 6 | mpocnfldmul 21581 | . 2 ⊢ (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) = (.r‘ℂfld) | |
| 7 | 5, 6 | eqtri 2788 | 1 ⊢ · = (.r‘ℂfld) |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: = wceq 1570 × cxp 5661 Fn wfn 6535 ⟶wf 6536 ‘cfv 6540 (class class class)co 7419 ∈ cmpo 7421 ℂcc 11115 · cmul 11122 .rcmulr 17335 ℂfldccnfld 21574 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7742 ax-cnex 11173 ax-resscn 11174 ax-1cn 11175 ax-icn 11176 ax-addcl 11177 ax-addrcl 11178 ax-mulcl 11179 ax-mulrcl 11180 ax-mulcom 11181 ax-addass 11182 ax-mulass 11183 ax-distr 11184 ax-i2m1 11185 ax-1ne0 11186 ax-1rid 11187 ax-rnegex 11188 ax-rrecex 11189 ax-cnre 11190 ax-pre-lttri 11191 ax-pre-lttrn 11192 ax-pre-ltadd 11193 ax-pre-mulgt0 11194 ax-mulf 11197 |
| This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3067 df-ral 3082 df-rex 3092 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-tp 4596 df-op 4598 df-uni 4875 df-iun 4960 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-riota 7376 df-ov 7422 df-oprab 7423 df-mpo 7424 df-om 7869 df-1st 7992 df-2nd 7993 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-1o 8459 df-er 8700 df-en 8950 df-dom 8951 df-sdom 8952 df-fin 8953 df-pnf 11262 df-mnf 11263 df-xr 11264 df-ltxr 11265 df-le 11266 df-sub 11460 df-neg 11461 df-nn 12251 df-2 12320 df-3 12321 df-4 12322 df-5 12323 df-6 12324 df-7 12325 df-8 12326 df-9 12327 df-n0 12522 df-z 12609 df-dec 12730 df-uz 12881 df-fz 13554 df-struct 17231 df-slot 17266 df-ndx 17278 df-base 17294 df-plusg 17347 df-mulr 17348 df-starv 17349 df-tset 17353 df-ple 17354 df-ds 17356 df-unif 17357 df-cnfld 21575 |
| This theorem is used by: cnfldexp 21607 cnsrng 21608 absabv 21626 cnsubrg 21629 cnmsubglem 21632 expmhm 21638 nn0srg 21639 rge0srg 21640 zringmulr 21659 expghm 21677 psgnghm 21782 psgnco 21785 evpmodpmf1o 21798 remulr 21813 mdetralt 22817 clmmul 25287 clmmcl 25297 isclmp 25309 cnlmod 25352 cnncvsmulassdemo 25376 cphsubrglem 25389 cphdivcl 25394 cphabscl 25397 cphsqrtcl2 25398 cphsqrtcl3 25399 ipcau2 25446 plypf1 26422 reefgim 26666 efabl 26768 efsubm 26769 amgmlem 27207 amgm 27208 wilthlem2 27286 wilthlem3 27287 dchrelbas3 27455 dchrzrhmul 27463 dchrmulcl 27466 dchrn0 27467 dchrinvcl 27470 dchrsum2 27485 sum2dchr 27491 qabvexp 27843 ostthlem2 27845 padicabv 27847 ostth2lem2 27851 ostth3 27855 xrge0slmod 33734 zringfrac 33910 ccfldsrarelvec 34127 ccfldextdgrr 34128 constrelextdg2 34203 constrsdrg 34231 2sqr3minply 34236 cos9thpiminplylem6 34243 iistmd 34358 xrge0iifmhm 34395 xrge0pluscn 34396 qqhrhm 34445 cnsrexpcl 43952 cnsrplycl 43954 rngunsnply 43956 amgm2d 44984 amgm3d 44985 amgm4d 44986 cnfldsrngmul 48987 aacllem 50680 amgmlemALT 50710 amgmw2d 50711 |
| Copyright terms: Public domain | W3C validator |