Theorem cnfld1 20192

Description: One is the unit element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.)

Assertion

Ref	Expression
cnfld1	⊢ 1 = (1r‘ℂfld)

Proof of Theorem cnfld1

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ax-1cn 10634	. . . 4 ⊢ 1 ∈ ℂ
2		mulid2 10679	. . . . . 6 ⊢ (𝑥 ∈ ℂ → (1 · 𝑥) = 𝑥)
3		mulid1 10678	. . . . . 6 ⊢ (𝑥 ∈ ℂ → (𝑥 · 1) = 𝑥)
4	2, 3	jca 516	. . . . 5 ⊢ (𝑥 ∈ ℂ → ((1 · 𝑥) = 𝑥 ∧ (𝑥 · 1) = 𝑥))
5	4	rgen 3081	. . . 4 ⊢ ∀𝑥 ∈ ℂ ((1 · 𝑥) = 𝑥 ∧ (𝑥 · 1) = 𝑥)
6	1, 5	pm3.2i 475	. . 3 ⊢ (1 ∈ ℂ ∧ ∀𝑥 ∈ ℂ ((1 · 𝑥) = 𝑥 ∧ (𝑥 · 1) = 𝑥))
7		cnring 20189	. . . 4 ⊢ ℂfld ∈ Ring
8		cnfldbas 20171	. . . . 5 ⊢ ℂ = (Base‘ℂfld)
9		cnfldmul 20173	. . . . 5 ⊢ · = (.r‘ℂfld)
10		eqid 2759	. . . . 5 ⊢ (1r‘ℂfld) = (1r‘ℂfld)
11	8, 9, 10	isringid 19395	. . . 4 ⊢ (ℂfld ∈ Ring → ((1 ∈ ℂ ∧ ∀𝑥 ∈ ℂ ((1 · 𝑥) = 𝑥 ∧ (𝑥 · 1) = 𝑥)) ↔ (1r‘ℂfld) = 1))
12	7, 11	ax-mp 5	. . 3 ⊢ ((1 ∈ ℂ ∧ ∀𝑥 ∈ ℂ ((1 · 𝑥) = 𝑥 ∧ (𝑥 · 1) = 𝑥)) ↔ (1r‘ℂfld) = 1)
13	6, 12	mpbi 233	. 2 ⊢ (1r‘ℂfld) = 1
14	13	eqcomi 2768	1 ⊢ 1 = (1r‘ℂfld)

Syntax hints:   ↔ wb 209   ∧ wa 400   = wceq 1539   ∈ wcel 2112  ∀wral 3071  ‘cfv 6336  (class class class)co 7151  ℂcc 10574  1c1 10577   · cmul 10581  1_rcur 19320  Ringcrg 19366  ℂ_fldccnfld 20167

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 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5170  ax-nul 5177  ax-pow 5235  ax-pr 5299  ax-un 7460  ax-cnex 10632  ax-resscn 10633  ax-1cn 10634  ax-icn 10635  ax-addcl 10636  ax-addrcl 10637  ax-mulcl 10638  ax-mulrcl 10639  ax-mulcom 10640  ax-addass 10641  ax-mulass 10642  ax-distr 10643  ax-i2m1 10644  ax-1ne0 10645  ax-1rid 10646  ax-rnegex 10647  ax-rrecex 10648  ax-cnre 10649  ax-pre-lttri 10650  ax-pre-lttrn 10651  ax-pre-ltadd 10652  ax-pre-mulgt0 10653  ax-addf 10655  ax-mulf 10656

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-reu 3078  df-rmo 3079  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-pss 3878  df-nul 4227  df-if 4422  df-pw 4497  df-sn 4524  df-pr 4526  df-tp 4528  df-op 4530  df-uni 4800  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5431  df-eprel 5436  df-po 5444  df-so 5445  df-fr 5484  df-we 5486  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-pred 6127  df-ord 6173  df-on 6174  df-lim 6175  df-suc 6176  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-om 7581  df-1st 7694  df-2nd 7695  df-wrecs 7958  df-recs 8019  df-rdg 8057  df-1o 8113  df-er 8300  df-en 8529  df-dom 8530  df-sdom 8531  df-fin 8532  df-pnf 10716  df-mnf 10717  df-xr 10718  df-ltxr 10719  df-le 10720  df-sub 10911  df-neg 10912  df-nn 11676  df-2 11738  df-3 11739  df-4 11740  df-5 11741  df-6 11742  df-7 11743  df-8 11744  df-9 11745  df-n0 11936  df-z 12022  df-dec 12139  df-uz 12284  df-fz 12941  df-struct 16544  df-ndx 16545  df-slot 16546  df-base 16548  df-sets 16549  df-plusg 16637  df-mulr 16638  df-starv 16639  df-tset 16643  df-ple 16644  df-ds 16646  df-unif 16647  df-0g 16774  df-mgm 17919  df-sgrp 17968  df-mnd 17979  df-grp 18173  df-cmn 18976  df-mgp 19309  df-ur 19321  df-ring 19368  df-cring 19369  df-cnfld 20168

This theorem is referenced by:  cndrng  20196  cnfldinv  20198  cnfldexp  20200  cnsubrglem  20217  cnsubdrglem  20218  zsssubrg  20225  cnmgpid  20229  gzrngunitlem  20232  expmhm  20236  nn0srg  20237  rge0srg  20238  zring1  20250  re1r  20379  clm1  23775  isclmp  23799  cnlmod  23842  cphsubrglem  23879  taylply2  25063  efsubm  25243  amgmlem  25675  amgm  25676  wilthlem2  25754  wilthlem3  25755  dchrelbas3  25922  dchrzrh1  25928  dchrmulcl  25933  dchrn0  25934  dchrinvcl  25937  dchrfi  25939  dchrabs  25944  sumdchr2  25954  rpvmasum2  26196  qrng1  26306  psgnid  30891  cnmsgn0g  30940  altgnsg  30943  xrge0slmod  31070  znfermltl  31084  iistmd  31374  xrge0iifmhm  31411  cnsrexpcl  40483  rngunsnply  40491  proot1ex  40519  amgmwlem  45722  amgmlemALT  45723