Metamath Proof Explorer

Theorem gg-cnfld1

Description: One is the unity element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014) Use mpocnfldmul . (Revised by GG, 31-Mar-2025)

Ref Expression
Assertion gg-cnfld1 ⊢1=1ℂfld

Proof

Step Hyp Ref Expression
1 ax-1cn ⊢1∈ℂ
2 mullid ⊢x∈ℂ→1⁢x=x
3 1cnd ⊢x∈ℂ→1∈ℂ
4 3 ancri ⊢x∈ℂ→1∈ℂ∧x∈ℂ
5 ovmpot ⊢1∈ℂ∧x∈ℂ→1u∈ℂ,v∈ℂ⟼u⁢vx=1⁢x
6 5 eqcomd ⊢1∈ℂ∧x∈ℂ→1⁢x=1u∈ℂ,v∈ℂ⟼u⁢vx
7 4 6 syl ⊢x∈ℂ→1⁢x=1u∈ℂ,v∈ℂ⟼u⁢vx
8 7 eqeq1d ⊢x∈ℂ→1⁢x=x↔1u∈ℂ,v∈ℂ⟼u⁢vx=x
9 8 biimpd ⊢x∈ℂ→1⁢x=x→1u∈ℂ,v∈ℂ⟼u⁢vx=x
10 2 9 mpd ⊢x∈ℂ→1u∈ℂ,v∈ℂ⟼u⁢vx=x
11 mulrid ⊢x∈ℂ→x⋅1=x
12 3 ancli ⊢x∈ℂ→x∈ℂ∧1∈ℂ
13 ovmpot ⊢x∈ℂ∧1∈ℂ→xu∈ℂ,v∈ℂ⟼u⁢v1=x⋅1
14 12 13 syl ⊢x∈ℂ→xu∈ℂ,v∈ℂ⟼u⁢v1=x⋅1
15 14 eqcomd ⊢x∈ℂ→x⋅1=xu∈ℂ,v∈ℂ⟼u⁢v1
16 15 eqeq1d ⊢x∈ℂ→x⋅1=x↔xu∈ℂ,v∈ℂ⟼u⁢v1=x
17 16 biimpd ⊢x∈ℂ→x⋅1=x→xu∈ℂ,v∈ℂ⟼u⁢v1=x
18 11 17 mpd ⊢x∈ℂ→xu∈ℂ,v∈ℂ⟼u⁢v1=x
19 10 18 jca ⊢x∈ℂ→1u∈ℂ,v∈ℂ⟼u⁢vx=x∧xu∈ℂ,v∈ℂ⟼u⁢v1=x
20 19 rgen ⊢∀x∈ℂ1u∈ℂ,v∈ℂ⟼u⁢vx=x∧xu∈ℂ,v∈ℂ⟼u⁢v1=x
21 1 20 pm3.2i ⊢1∈ℂ∧∀x∈ℂ1u∈ℂ,v∈ℂ⟼u⁢vx=x∧xu∈ℂ,v∈ℂ⟼u⁢v1=x
22 cnring ⊢ℂfld∈Ring
23 cnfldbas ⊢ℂ=Baseℂfld
24 mpocnfldmul ⊢u∈ℂ,v∈ℂ⟼u⁢v=⋅ℂfld
25 eqid ⊢1ℂfld=1ℂfld
26 23 24 25 isringid ⊢ℂfld∈Ring→1∈ℂ∧∀x∈ℂ1u∈ℂ,v∈ℂ⟼u⁢vx=x∧xu∈ℂ,v∈ℂ⟼u⁢v1=x↔1ℂfld=1
27 22 26 ax-mp ⊢1∈ℂ∧∀x∈ℂ1u∈ℂ,v∈ℂ⟼u⁢vx=x∧xu∈ℂ,v∈ℂ⟼u⁢v1=x↔1ℂfld=1
28 21 27 mpbi ⊢1ℂfld=1
29 28 eqcomi ⊢1=1ℂfld