![]() |
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 20263 | . . . 4 ⊢ ℂ = (Base‘ℂfld) | |
2 | 1 | a1i 11 | . . 3 ⊢ (⊤ → ℂ = (Base‘ℂfld)) |
3 | cnfldadd 20264 | . . . 4 ⊢ + = (+g‘ℂfld) | |
4 | 3 | a1i 11 | . . 3 ⊢ (⊤ → + = (+g‘ℂfld)) |
5 | cnfldmul 20265 | . . . 4 ⊢ · = (.r‘ℂfld) | |
6 | 5 | a1i 11 | . . 3 ⊢ (⊤ → · = (.r‘ℂfld)) |
7 | addcl 10415 | . . . . 5 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 + 𝑦) ∈ ℂ) | |
8 | addass 10420 | . . . . 5 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) | |
9 | 0cn 10429 | . . . . 5 ⊢ 0 ∈ ℂ | |
10 | addid2 10621 | . . . . 5 ⊢ (𝑥 ∈ ℂ → (0 + 𝑥) = 𝑥) | |
11 | negcl 10684 | . . . . 5 ⊢ (𝑥 ∈ ℂ → -𝑥 ∈ ℂ) | |
12 | addcom 10624 | . . . . . . 7 ⊢ ((-𝑥 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (-𝑥 + 𝑥) = (𝑥 + -𝑥)) | |
13 | 11, 12 | mpancom 675 | . . . . . 6 ⊢ (𝑥 ∈ ℂ → (-𝑥 + 𝑥) = (𝑥 + -𝑥)) |
14 | negid 10732 | . . . . . 6 ⊢ (𝑥 ∈ ℂ → (𝑥 + -𝑥) = 0) | |
15 | 13, 14 | eqtrd 2808 | . . . . 5 ⊢ (𝑥 ∈ ℂ → (-𝑥 + 𝑥) = 0) |
16 | 1, 3, 7, 8, 9, 10, 11, 15 | isgrpi 17926 | . . . 4 ⊢ ℂfld ∈ Grp |
17 | 16 | a1i 11 | . . 3 ⊢ (⊤ → ℂfld ∈ Grp) |
18 | mulcl 10417 | . . . 4 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ) | |
19 | 18 | 3adant1 1110 | . . 3 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ) |
20 | mulass 10421 | . . . 4 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧))) | |
21 | 20 | adantl 474 | . . 3 ⊢ ((⊤ ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧))) |
22 | adddi 10422 | . . . 4 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧))) | |
23 | 22 | adantl 474 | . . 3 ⊢ ((⊤ ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧))) |
24 | adddir 10428 | . . . 4 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))) | |
25 | 24 | adantl 474 | . . 3 ⊢ ((⊤ ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))) |
26 | 1cnd 10432 | . . 3 ⊢ (⊤ → 1 ∈ ℂ) | |
27 | mulid2 10436 | . . . 4 ⊢ (𝑥 ∈ ℂ → (1 · 𝑥) = 𝑥) | |
28 | 27 | adantl 474 | . . 3 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (1 · 𝑥) = 𝑥) |
29 | mulid1 10435 | . . . 4 ⊢ (𝑥 ∈ ℂ → (𝑥 · 1) = 𝑥) | |
30 | 29 | adantl 474 | . . 3 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ) → (𝑥 · 1) = 𝑥) |
31 | mulcom 10419 | . . . 4 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) = (𝑦 · 𝑥)) | |
32 | 31 | 3adant1 1110 | . . 3 ⊢ ((⊤ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) = (𝑦 · 𝑥)) |
33 | 2, 4, 6, 17, 19, 21, 23, 25, 26, 28, 30, 32 | iscrngd 19071 | . 2 ⊢ (⊤ → ℂfld ∈ CRing) |
34 | 33 | mptru 1514 | 1 ⊢ ℂfld ∈ CRing |
Colors of variables: wff setvar class |
Syntax hints: ∧ w3a 1068 = wceq 1507 ⊤wtru 1508 ∈ wcel 2050 ‘cfv 6185 (class class class)co 6974 ℂcc 10331 0cc0 10333 1c1 10334 + caddc 10336 · cmul 10338 -cneg 10669 Basecbs 16337 +gcplusg 16419 .rcmulr 16420 Grpcgrp 17903 CRingccrg 19033 ℂfldccnfld 20259 |
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 5056 ax-nul 5063 ax-pow 5115 ax-pr 5182 ax-un 7277 ax-cnex 10389 ax-resscn 10390 ax-1cn 10391 ax-icn 10392 ax-addcl 10393 ax-addrcl 10394 ax-mulcl 10395 ax-mulrcl 10396 ax-mulcom 10397 ax-addass 10398 ax-mulass 10399 ax-distr 10400 ax-i2m1 10401 ax-1ne0 10402 ax-1rid 10403 ax-rnegex 10404 ax-rrecex 10405 ax-cnre 10406 ax-pre-lttri 10407 ax-pre-lttrn 10408 ax-pre-ltadd 10409 ax-pre-mulgt0 10410 ax-addf 10412 ax-mulf 10413 |
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-rmo 3090 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 4709 df-int 4746 df-iun 4790 df-br 4926 df-opab 4988 df-mpt 5005 df-tr 5027 df-id 5308 df-eprel 5313 df-po 5322 df-so 5323 df-fr 5362 df-we 5364 df-xp 5409 df-rel 5410 df-cnv 5411 df-co 5412 df-dm 5413 df-rn 5414 df-res 5415 df-ima 5416 df-pred 5983 df-ord 6029 df-on 6030 df-lim 6031 df-suc 6032 df-iota 6149 df-fun 6187 df-fn 6188 df-f 6189 df-f1 6190 df-fo 6191 df-f1o 6192 df-fv 6193 df-riota 6935 df-ov 6977 df-oprab 6978 df-mpo 6979 df-om 7395 df-1st 7499 df-2nd 7500 df-wrecs 7748 df-recs 7810 df-rdg 7848 df-1o 7903 df-oadd 7907 df-er 8087 df-en 8305 df-dom 8306 df-sdom 8307 df-fin 8308 df-pnf 10474 df-mnf 10475 df-xr 10476 df-ltxr 10477 df-le 10478 df-sub 10670 df-neg 10671 df-nn 11438 df-2 11501 df-3 11502 df-4 11503 df-5 11504 df-6 11505 df-7 11506 df-8 11507 df-9 11508 df-n0 11706 df-z 11792 df-dec 11910 df-uz 12057 df-fz 12707 df-struct 16339 df-ndx 16340 df-slot 16341 df-base 16343 df-sets 16344 df-plusg 16432 df-mulr 16433 df-starv 16434 df-tset 16438 df-ple 16439 df-ds 16441 df-unif 16442 df-0g 16569 df-mgm 17722 df-sgrp 17764 df-mnd 17775 df-grp 17906 df-cmn 18680 df-mgp 18975 df-ring 19034 df-cring 19035 df-cnfld 20260 |
This theorem is referenced by: cnring 20281 cnmgpabl 20320 zringcrng 20333 zring0 20341 re0g 20470 refld 20477 smadiadetr 21000 plypf1 24517 amgmlem 25281 amgm 25282 wilthlem2 25360 wilthlem3 25361 gzcrng 30620 ccfldextrr 30696 2zrng0 43598 amgmwlem 44295 amgmlemALT 44296 |
Copyright terms: Public domain | W3C validator |