![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cncrng | Structured version Visualization version GIF version |
Description: The complex numbers form a commutative ring. (Contributed by Mario Carneiro, 8-Jan-2015.) |
Ref | Expression |
---|---|
cncrng | ⊢ ℂfld ∈ CRing |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnfldbas 19964 | . . . 4 ⊢ ℂ = (Base‘ℂfld) | |
2 | 1 | a1i 11 | . . 3 ⊢ (⊤ → ℂ = (Base‘ℂfld)) |
3 | cnfldadd 19965 | . . . 4 ⊢ + = (+g‘ℂfld) | |
4 | 3 | a1i 11 | . . 3 ⊢ (⊤ → + = (+g‘ℂfld)) |
5 | cnfldmul 19966 | . . . 4 ⊢ · = (.r‘ℂfld) | |
6 | 5 | a1i 11 | . . 3 ⊢ (⊤ → · = (.r‘ℂfld)) |
7 | addcl 10223 | . . . . 5 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 + 𝑦) ∈ ℂ) | |
8 | addass 10228 | . . . . 5 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) | |
9 | 0cn 10237 | . . . . 5 ⊢ 0 ∈ ℂ | |
10 | addid2 10424 | . . . . 5 ⊢ (𝑥 ∈ ℂ → (0 + 𝑥) = 𝑥) | |
11 | negcl 10486 | . . . . 5 ⊢ (𝑥 ∈ ℂ → -𝑥 ∈ ℂ) | |
12 | addcom 10427 | . . . . . . 7 ⊢ ((-𝑥 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (-𝑥 + 𝑥) = (𝑥 + -𝑥)) | |
13 | 11, 12 | mpancom 668 | . . . . . 6 ⊢ (𝑥 ∈ ℂ → (-𝑥 + 𝑥) = (𝑥 + -𝑥)) |
14 | negid 10533 | . . . . . 6 ⊢ (𝑥 ∈ ℂ → (𝑥 + -𝑥) = 0) | |
15 | 13, 14 | eqtrd 2805 | . . . . 5 ⊢ (𝑥 ∈ ℂ → (-𝑥 + 𝑥) = 0) |
16 | 1, 3, 7, 8, 9, 10, 11, 15 | isgrpi 17652 | . . . 4 ⊢ ℂfld ∈ Grp |
17 | 16 | a1i 11 | . . 3 ⊢ (⊤ → ℂfld ∈ Grp) |
18 | mulcl 10225 | . . . 4 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ) | |
19 | 18 | 3adant1 1124 | . . 3 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ) |
20 | mulass 10229 | . . . 4 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧))) | |
21 | 20 | adantl 467 | . . 3 ⊢ ((⊤ ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧))) |
22 | adddi 10230 | . . . 4 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧))) | |
23 | 22 | adantl 467 | . . 3 ⊢ ((⊤ ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧))) |
24 | adddir 10236 | . . . 4 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))) | |
25 | 24 | adantl 467 | . . 3 ⊢ ((⊤ ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))) |
26 | 1cnd 10261 | . . 3 ⊢ (⊤ → 1 ∈ ℂ) | |
27 | mulid2 10243 | . . . 4 ⊢ (𝑥 ∈ ℂ → (1 · 𝑥) = 𝑥) | |
28 | 27 | adantl 467 | . . 3 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (1 · 𝑥) = 𝑥) |
29 | mulid1 10242 | . . . 4 ⊢ (𝑥 ∈ ℂ → (𝑥 · 1) = 𝑥) | |
30 | 29 | adantl 467 | . . 3 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (𝑥 · 1) = 𝑥) |
31 | mulcom 10227 | . . . 4 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) = (𝑦 · 𝑥)) | |
32 | 31 | 3adant1 1124 | . . 3 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) = (𝑦 · 𝑥)) |
33 | 2, 4, 6, 17, 19, 21, 23, 25, 26, 28, 30, 32 | iscrngd 18793 | . 2 ⊢ (⊤ → ℂfld ∈ CRing) |
34 | 33 | trud 1641 | 1 ⊢ ℂfld ∈ CRing |
Colors of variables: wff setvar class |
Syntax hints: ∧ w3a 1071 = wceq 1631 ⊤wtru 1632 ∈ wcel 2145 ‘cfv 6030 (class class class)co 6795 ℂcc 10139 0cc0 10141 1c1 10142 + caddc 10144 · cmul 10146 -cneg 10472 Basecbs 16063 +gcplusg 16148 .rcmulr 16149 Grpcgrp 17629 CRingccrg 18755 ℂfldccnfld 19960 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-8 2147 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 ax-sep 4916 ax-nul 4924 ax-pow 4975 ax-pr 5035 ax-un 7099 ax-cnex 10197 ax-resscn 10198 ax-1cn 10199 ax-icn 10200 ax-addcl 10201 ax-addrcl 10202 ax-mulcl 10203 ax-mulrcl 10204 ax-mulcom 10205 ax-addass 10206 ax-mulass 10207 ax-distr 10208 ax-i2m1 10209 ax-1ne0 10210 ax-1rid 10211 ax-rnegex 10212 ax-rrecex 10213 ax-cnre 10214 ax-pre-lttri 10215 ax-pre-lttrn 10216 ax-pre-ltadd 10217 ax-pre-mulgt0 10218 ax-addf 10220 ax-mulf 10221 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-3or 1072 df-3an 1073 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-eu 2622 df-mo 2623 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ne 2944 df-nel 3047 df-ral 3066 df-rex 3067 df-reu 3068 df-rmo 3069 df-rab 3070 df-v 3353 df-sbc 3588 df-csb 3683 df-dif 3726 df-un 3728 df-in 3730 df-ss 3737 df-pss 3739 df-nul 4064 df-if 4227 df-pw 4300 df-sn 4318 df-pr 4320 df-tp 4322 df-op 4324 df-uni 4576 df-int 4613 df-iun 4657 df-br 4788 df-opab 4848 df-mpt 4865 df-tr 4888 df-id 5158 df-eprel 5163 df-po 5171 df-so 5172 df-fr 5209 df-we 5211 df-xp 5256 df-rel 5257 df-cnv 5258 df-co 5259 df-dm 5260 df-rn 5261 df-res 5262 df-ima 5263 df-pred 5822 df-ord 5868 df-on 5869 df-lim 5870 df-suc 5871 df-iota 5993 df-fun 6032 df-fn 6033 df-f 6034 df-f1 6035 df-fo 6036 df-f1o 6037 df-fv 6038 df-riota 6756 df-ov 6798 df-oprab 6799 df-mpt2 6800 df-om 7216 df-1st 7318 df-2nd 7319 df-wrecs 7562 df-recs 7624 df-rdg 7662 df-1o 7716 df-oadd 7720 df-er 7899 df-en 8113 df-dom 8114 df-sdom 8115 df-fin 8116 df-pnf 10281 df-mnf 10282 df-xr 10283 df-ltxr 10284 df-le 10285 df-sub 10473 df-neg 10474 df-nn 11226 df-2 11284 df-3 11285 df-4 11286 df-5 11287 df-6 11288 df-7 11289 df-8 11290 df-9 11291 df-n0 11499 df-z 11584 df-dec 11700 df-uz 11893 df-fz 12533 df-struct 16065 df-ndx 16066 df-slot 16067 df-base 16069 df-sets 16070 df-plusg 16161 df-mulr 16162 df-starv 16163 df-tset 16167 df-ple 16168 df-ds 16171 df-unif 16172 df-0g 16309 df-mgm 17449 df-sgrp 17491 df-mnd 17502 df-grp 17632 df-cmn 18401 df-mgp 18697 df-ring 18756 df-cring 18757 df-cnfld 19961 |
This theorem is referenced by: cnring 19982 cnmgpabl 20021 zringcrng 20034 zring0 20042 re0g 20174 refld 20181 smadiadetr 20699 plypf1 24187 amgmlem 24936 amgm 24937 wilthlem2 25015 wilthlem3 25016 gzcrng 30178 2zrng0 42463 amgmwlem 43076 amgmlemALT 43077 |
Copyright terms: Public domain | W3C validator |