Metamath Proof Explorer

Theorem cnfld1

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

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

Proof

Step Hyp Ref Expression
1 ax-1cn ⊢ 1 ∈ ℂ
2 ovmpot ⊢ ( ( 1 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 1 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑥 ) = ( 1 · 𝑥 ) )
3 2 eqcomd ⊢ ( ( 1 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 1 · 𝑥 ) = ( 1 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑥 ) )
4 1 3 mpan ⊢ ( 𝑥 ∈ ℂ → ( 1 · 𝑥 ) = ( 1 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑥 ) )
5 mullid ⊢ ( 𝑥 ∈ ℂ → ( 1 · 𝑥 ) = 𝑥 )
6 4 5 eqtr3d ⊢ ( 𝑥 ∈ ℂ → ( 1 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑥 ) = 𝑥 )
7 ovmpot ⊢ ( ( 𝑥 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 1 ) = ( 𝑥 · 1 ) )
8 1 7 mpan2 ⊢ ( 𝑥 ∈ ℂ → ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 1 ) = ( 𝑥 · 1 ) )
9 mulrid ⊢ ( 𝑥 ∈ ℂ → ( 𝑥 · 1 ) = 𝑥 )
10 8 9 eqtrd ⊢ ( 𝑥 ∈ ℂ → ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 1 ) = 𝑥 )
11 6 10 jca ⊢ ( 𝑥 ∈ ℂ → ( ( 1 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 1 ) = 𝑥 ) )
12 11 rgen ⊢ ∀ 𝑥 ∈ ℂ ( ( 1 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 1 ) = 𝑥 )
13 1 12 pm3.2i ⊢ ( 1 ∈ ℂ ∧ ∀ 𝑥 ∈ ℂ ( ( 1 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 1 ) = 𝑥 ) )
14 cnring ⊢ ℂfld ∈ Ring
15 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
16 mpocnfldmul ⊢ ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) = ( .r ‘ ℂfld )
17 eqid ⊢ ( 1r ‘ ℂfld ) = ( 1r ‘ ℂfld )
18 15 16 17 isringid ⊢ ( ℂfld ∈ Ring → ( ( 1 ∈ ℂ ∧ ∀ 𝑥 ∈ ℂ ( ( 1 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 1 ) = 𝑥 ) ) ↔ ( 1r ‘ ℂfld ) = 1 ) )
19 14 18 ax-mp ⊢ ( ( 1 ∈ ℂ ∧ ∀ 𝑥 ∈ ℂ ( ( 1 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 1 ) = 𝑥 ) ) ↔ ( 1r ‘ ℂfld ) = 1 )
20 13 19 mpbi ⊢ ( 1r ‘ ℂfld ) = 1
21 20 eqcomi ⊢ 1 = ( 1r ‘ ℂfld )