Theorem cnfld1

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

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

Proof

Step	Hyp	Ref	Expression
1		ax-1cn	⊢ 1 ∈ ℂ
2		mulid2	⊢ ( 𝑥 ∈ ℂ → ( 1 · 𝑥 ) = 𝑥 )
3		mulid1	⊢ ( 𝑥 ∈ ℂ → ( 𝑥 · 1 ) = 𝑥 )
4	2 3	jca	⊢ ( 𝑥 ∈ ℂ → ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 1 ) = 𝑥 ) )
5	4	rgen	⊢ ∀ 𝑥 ∈ ℂ ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 1 ) = 𝑥 )
6	1 5	pm3.2i	⊢ ( 1 ∈ ℂ ∧ ∀ 𝑥 ∈ ℂ ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 1 ) = 𝑥 ) )
7		cnring	⊢ ℂfld ∈ Ring
8		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
9		cnfldmul	⊢ · = ( .r ‘ ℂfld )
10		eqid	⊢ ( 1r ‘ ℂfld ) = ( 1r ‘ ℂfld )
11	8 9 10	isringid	⊢ ( ℂfld ∈ Ring → ( ( 1 ∈ ℂ ∧ ∀ 𝑥 ∈ ℂ ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 1 ) = 𝑥 ) ) ↔ ( 1r ‘ ℂfld ) = 1 ) )
12	7 11	ax-mp	⊢ ( ( 1 ∈ ℂ ∧ ∀ 𝑥 ∈ ℂ ( ( 1 · 𝑥 ) = 𝑥 ∧ ( 𝑥 · 1 ) = 𝑥 ) ) ↔ ( 1r ‘ ℂfld ) = 1 )
13	6 12	mpbi	⊢ ( 1r ‘ ℂfld ) = 1
14	13	eqcomi	⊢ 1 = ( 1r ‘ ℂfld )